leroux jerome - The General Vector Addition System Reachability Problem by Presburger Inductive Invariants

lmcs:1024 - Logical Methods in Computer Science, September 9, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:22)2010
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants

Authors: leroux jerome

    The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition is used in this paper to prove that the Parikh images of languages recognized by VASs 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 this result; we prove that a final configuration is not reachable from an initial one if and only if there exists a semi-linear inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, 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 enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas.

    Volume: Volume 6, Issue 3
    Published on: September 9, 2010
    Imported on: January 4, 2010
    Keywords: Computer Science - Logic in Computer Science,F.1

    Linked publications - datasets - softwares

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.icalp.2021.128
    • 10.4230/lipics.icalp.2021.128
    Improved Lower Bounds for Reachability in Vector Addition Systems
    Czerwiński, Wojciech ; Lasota, Sławomir ; Orlikowski, Łukasz ;

    11 Documents citing this article

    Consultation statistics

    This page has been seen 804 times.
    This article's PDF has been downloaded 383 times.