Pushdown Automata and Vector Addition Systems: A New Look At Two Classical Problems

January 20, 2011 — Cachan

This special event focuses on two recent major claims/results:

Our aim here is to provide an exceptional opportunity for Jančar and Leroux to provide an in-depth presentation of their proofs in front of a large audience of expert specialists as well as younger researchers interested in the field. This will be a unique occasion for the kind of interaction and attention to details that is only possible in a 3-hour tutorial format.

List of participants


Jérôme Leroux 's slides

Petr Jančar's slides (This the Jan. 28th version of the slides by P. Jančar, referring to the serious problem in the nondeterministic case found by G. Sénizergues.)


Detailed programme

Thursday, 20 January, 2011
09:30 10:00 Welcome & Coffee
10:00 13:00 Petr Jančar Decidability and complexity of DPDA Language Equivalence via 1st Order Grammars
13:00 14:30 Lunch
14:30 17:30 Jérôme Leroux Vector Addition System Reachability Problem (A Short Self-Contained Proof)
17:30 Closing
20:00 Banquet (in Paris)


The banquet will take place at the "Au moulin vert" restaurant. All the information are present in the programme.pdf.


The tutorials will take place in the Amphithéâtre Marie Curie, in the Bâtiment d'Alembert of the École normale supérieure de Cachan.

How to reach ENS Cachan by metro is explained here. See there for a map of the campus, where Bâtiment d'Alembert is building number 1.


Please write to pavas.at.lsv.ens-cachan.fr for any question regarding this event. The organizers are Ph. Schnoebelen, L. Doyen, V. Guenard, B. Gourdin and H. Djafri.

Abstracts of the Tutorials

Petr Jančar (Techn. Univ. Ostrava, CZ)

Decidability and complexity of DPDA Language Equivalence via 1st Order Grammars

The aim of the talk is to present a complete proof of the decidability of language equivalence for deterministic pushdown automata, which is the famous problem solved by G. Senizergues, for which C. Stirling derived a primitive recursive complexity upper bound. The planned presentation is novel, based on a reduction to trace equivalence of deterministic first order grammars; this can be viewed as a problem in term rewriting systems. The presentation is intended to illuminate all crucial ideas, avoiding technicalities when possible; an ideal form of the talk supposes an interactive cooperation with the audience.

After all ideas are understood and the decidability is established, the above mentioned complexity result can be easily explained. We can also discuss a smooth generalization of the decidability result to bisimulation equivalence for general (nondeterministic) first order grammars; this is more-or-less equivalent to the decidability result for nondeterministic pushdown automata with restricted use of epsilon-steps, for which the first proof was also given by G. Senizergues.

The slides of the talk are available here

The talk is based on a written version which has been made public at http://arxiv.org/abs/1010.4760.

Jérôme Leroux (LaBRI, CNRS & Univ. Bordeaux, FR)

Vector Addition System Reachability Problem (A Short Self-Contained Proof)

The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In this presentation we provide the first proof of the VAS reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations inspired from Hauschildt that directly provides the existence of Presburger inductive invariants.

The slides of the talk are available here

The talk is based on a written version which has been made public at http://hal.archives-ouvertes.fr/hal-00502865/fr/.

About LSV