The General Vector Addition System Reachability Problem by Presburger Inductive Invariants" and "TaPAS : The Talence Presburger Arithmetic Suite

Jerome Leroux
Labri, Bordeaux
Friday, 13 February, 2009 (All day)
NO

The reachability problem for Vector Addition Systems (VAS) 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. This decomposition can be used to prove that Parikh images of languages accepted by VAS are semi-pseudo-linear; a class of sets that can be precisely over-approximated by sets definable in the Presburger arithmetic. We provide an application of this result; we prove that if a final configuration is not reachable from an initial one, there exists a Presburger inductive invariant proving this property. Since we can decide with any decision procedure for the Presburger arithmetic if formulas denote inductive invariants, we deduce that there exist checkable certificates of non-reachability. 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 non-deterministically selecting finite sequences of actions and a second one that tries to prove the non-reachability by non-deterministically selecting Presburger formulas. In this presentation we show the existence of these Presburger checkable certificates proving the non-reachability. Note that the Presburger arithmetic has positive aspects: it is decidable and actually many solvers implement decision procedures. In this presentation we also provide an overview of the tool suite TaPAS (The Talence Presburger Arithmetic Suite) developed in Bordeaux. Actually TaPAS encapsulates several classical solvers : LASH, LIRA, MONA, OMEGA, PPL. TaPAS is also distributed with SaTAF, the BDD-like library used for encoding Presburger formulae to automata and the very first implementation of an algorithm decoding automata to Presburger formulae. This is joint work with Gérald Point.
Some external links:
"TaPAS : The Talence Presburger Arithmetic Suite" (TACAS'09)
http://altarica.labri.fr/wiki/tools:tapas:start
http://www.labri.fr/perso/leroux/publi/Author/LEROUX-J.html
"The General Vector Addition System Reachability Problem by Presburger Inductive Invariants" (Submitted)
http://hal.archives-ouvertes.fr/hal-00272667/fr/
"Least Significant Digit First Presburger Automata" (Extended version of LICS'05)
http://hal.archives-ouvertes.fr/hal-00118748/en/