Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

The Computational Complexity of Verifying One-Counter Processes

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Stefan Göller
Le mardi 22 novembre 2011 à 11:00
Salle de Conférence (Pavillon des Jardins)
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.

À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents