The General Vector Addition System Reachability Problem by Presburger Inductive Invariants

摘要

The reachability problem for Vector Addition Systems (VASs) is a centralproblem of net theory. The general problem is known to be decidable byalgorithms exclusively based on the classicalKosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition isused in this paper to prove that the Parikh images of languages recognized byVASs are semi-pseudo-linear; a class that extends the semi-linear sets, a.k.a.the sets definable in Presburger arithmetic. We provide an application of thisresu we prove that a final configuration is not reachable from an initialone if and only if there exists a semi-linear inductive invariant that containsthe initial configuration but not the final one. Since we can decide if aPresburger formula denotes an inductive invariant, we deduce that there existcheckable certificates of non-reachability. In particular, there exists asimple algorithm for deciding the general VAS reachability problem based on twosemi-algorithms. A first one that tries to prove the reachability byenumerating finite sequences of actions and a second one that tries to provethe non-reachability by enumerating Presburger formulas.