Demystifying Reachability in Vector Addition Systems

DOI10.1109/LICS.2015.16MaRDI QIDQ4635791zbMATH OpenFDO

Authors Jérôme Leroux, Sylvain Schmitz

Publication date 23 April 2018

Published in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

computational complexitydecidabilityPetri netsprogram verificationreachability analysis

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known. We first offer a justification for this decomposition technique, by showing that it computes the ideal decomposition of the set of runs, using the natural embedding relation between runs as well quasi ordering. In a second part, we apply recent results on the complexity of termination thanks to well quasi orders and well orders to obtain a cubic Ackermann upper bound for the decomposition algorithms, thus providing the first known upper bounds for general VAS reachability.

Recommendations

• scientific article; zbMATH DE number 3878366
• scientific article; zbMATH DE number 4092784
• Vector addition system reachability problem: a short self-contained proof
• Vector addition system reachability problem, a short self-contained proof
• scientific article; zbMATH DE number 7559504
• Vector addition system reversible reachability problem
• Vector Addition System Reversible Reachability Problem
• Separability of reachability sets of vector addition systems
• The complexity of reachability in affine vector addition systems with states
• scientific article; zbMATH DE number 7407775

Cited in

(57)

• Handling infinitely branching well-structured transition systems
• On the decision problem for MELL
• Flat Petri nets (invited talk)
• A lazy query scheme for reachability analysis in Petri nets
• A counter abstraction technique for verifying properties of probabilistic swarm systems
• Directed reachability for infinite-state systems
• Context-free commutative grammars with integer counters and resets
• The general vector addition system reachability problem by Presburger inductive invariants
• On freeze LTL with ordered attributes
• Coverability trees for Petri nets with unordered data
• Complexity hierarchies beyond elementary
• A Relational Trace Logic for Vector Addition Systems with Application to Context-Freeness
• Expand, Enlarge, and Check for Branching Vector Addition Systems
• Deciding Structural Liveness of Petri Nets
• Vector addition system reachability problem: a short self-contained proof
• Model Checking Coverability Graphs of Vector Addition Systems
• The Reachability Problem for Vector Addition System with One Zero-Test
• Vector Addition System Reversible Reachability Problem
• Petri nets and semilinear sets (extended abstract)
• The ideal approach to computing closed subsets in well-quasi-orderings
• Forward analysis for WSTS, part I: completions
• 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?)
• Ideal decompositions for vector addition systems (invited talk)
• Polynomial vector addition systems with states
• Linear equations with ordered data
• Regular separability of well-structured transition systems
• Infinitary Noetherian constructions I. Infinite words
• Open Petri nets
• scientific article; zbMATH DE number 7407775 (Why is no real title available?)
• Verification of population protocols
• Zeno, Hercules, and the Hydra: safety metric temporal logic is Ackermann-complete
• Vector addition system reachability problem, a short self-contained proof
• Reachability for bounded branching VASS
• On the complexity of resource-bounded logics
• The ideal view on Rackoff's coverability technique
• A Note on C² Interpreted over Finite Data-Words
• Unboundedness problems for machines with reversal-bounded counters
• Reasoning about reversal-bounded counter machines
• Ackermannian completion of separators
• Reachability in fixed VASS: expressiveness and lower bounds
• Solvability of orbit-finite systems of linear equations
• The complexity of soundness in workflow nets
• Extensional Petri net
• Bi-reachability in Petri nets with data
• Improved algorithm for reachability in d-VASS
• Separability in Büchi VASS and singly nonlinear systems of inequalities
• Directed regular and context-free languages
• Counter machines with infrequent reversals
• Separability and non-determinizability of WSTS
• Geometry of reachability sets of vector addition systems
• On the separability problem of VASS reachability languages
• Verifying unboundedness via amalgamation
• Improved lower bounds for reachability in vector addition systems
• The controllability of vector addition systems
• Reachability problems on reliable and lossy queue automata

This page was built for publication: Demystifying Reachability in Vector Addition Systems

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