Titre :  Acceleration for Vector Addition Systems

Exposant : Jerome Leroux

Résumé :  The reachability problem for vector addition systems, a.k.a. Petri nets 
is a central problem of net
theory. The problem is known to be decidable by inductive invariants
definable in the Presburger arithmetic. When the reachability set is
definable in the Presburger arithmetic, the existence of such an
inductive invariant is immediate. However, in this case, the
computation of a Presburger formula denoting the reachability set is
an open problem. Recently this problem got closed by proving that if
the reachability set of a vector addition system is definable in the Presburger
arithmetic, then the vector addition system is flatable, i.e. its reachability set
can be obtained by runs labeled by words in a bounded language. As a
direct consequence, classical algorithms based on acceleration
techniques effectively compute a formula in the Presburger arithmetic
denoting the reachability set. In this presentation, the framework of
verification of infinite-state systems based on acceleration
techniques is recalled. We also explain the completeness of this
method on the computation of Presburger formulas denoting the
reachability sets of vector addition systems.