LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
The Computational Complexity of Verifying One-Counter Processes
- Date
- Tuesday, November 22 2011 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Stefan Göller (University of Bremen)
A one-counter automaton is a pushdown automaton over a singleton stack alphabet plus a bottom-of-stack symbol. I will talk about equivalence checking and model checking of processes generated by one-counter automata, so-called one-counter processes (OCPs).
The goal of the talk is to present some ideas and techniques that are used for obtaining complexity bounds for these problems.
In the first part of the talk I plan to show that it is PSPACE-complete to decide strong bisimulation equivalence for OCPs. The previously best known upper bound for this problem was 3-EXPSPACE. The same problem turns out to be NL-complete when the processes are described by deterministic one-counter automata.
In the second part of the talk, I plan to discuss a technique for proving lower bounds by employing two known results from complexity theory: (i) Converting a natural number in Chinese remainder presentation into binary presentation is in logspace-uniform NC^1 and (ii) PSPACE is AC^0-serializable. With the latter one can prove that there exists a fixed CTL formula for which model checking of OCPs is PSPACE-hard.
With the same technique one can show some further lower bounds, as for example the following one: The emptiness problem for timed automata with two clocks but with modulo tests is PSPACE-complete even if all numbers are encoded in unary.
The results were obtained in joint works with Stanislav Böhm, Petr Jancar and Markus Lohrey.