Vector addition system reachability problem
- 26 January 2011
- journal article
- conference paper
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 46 (1), 307-316
- https://doi.org/10.1145/1925844.1926421
Abstract
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 paper 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.Keywords
Other Versions
This publication has 7 references indexed in Scilit:
- The General Vector Addition System Reachability Problem by Presburger Inductive InvariantsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2009
- A structure to decide reachability in Petri netsTheoretical Computer Science, 1992
- Decidability of reachability in vector addition systems (Preliminary Version)Published by Association for Computing Machinery (ACM) ,1982
- The Complexity of the Finite Containment Problem for Petri NetsJournal of the ACM, 1981
- An algorithm for the general Petri net reachability problemPublished by Association for Computing Machinery (ACM) ,1981
- The decidability of the reachability problem for vector addition systems (Preliminary Version)Published by Association for Computing Machinery (ACM) ,1977
- Semigroups, Presburger formulas, and languagesPacific Journal of Mathematics, 1966