The general vector addition system reachability problem by Presburger inductive invariants

DOI10.2168/LMCS-6(3:22)2010MaRDI QIDQ2786139zbMATH OpenOpenAlexFDO

Authors Jérôme Leroux

Publication date 21 September 2010

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1009.1076

zbMATH Keywords

Petri netPresburger formulareachabilityvector addition system

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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.

Recommendations

• Vector addition system reachability problem: a short self-contained proof
• Vector addition system reachability problem, a short self-contained proof
• Presburger vector addition systems
• scientific article; zbMATH DE number 3928356
• Demystifying Reachability in Vector Addition Systems

Cited in

(20)

• Flat Petri nets (invited talk)
• A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness
• A Note on Decidable Separability by Piecewise Testable Languages
• Vector addition system reachability problem: a short self-contained proof
• Rewriting systems for reachability in vector addition systems with pairs
• scientific article; zbMATH DE number 3928356 (Why is no real title available?)
• scientific article; zbMATH DE number 4024808 (Why is no real title available?)
• Unboundedness problems for languages of vector addition systems
• scientific article; zbMATH DE number 7559493 (Why is no real title available?)
• scientific article; zbMATH DE number 7407775 (Why is no real title available?)
• Regular graphs and the spectra of two-variable logic with counting
• Presburger vector addition systems
• Vector addition system reachability problem, a short self-contained proof
• Property directed reachability for generalized Petri nets
• Porous invariants for linear systems
• Invariants for one-counter automata with disequality tests
• On the home-space problem for Petri nets and its Ackermannian complexity
• Improved lower bounds for reachability in vector addition systems
• The controllability of vector addition systems
• Porous invariants

This page was built for publication: The general vector addition system reachability problem by Presburger inductive invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2786139)