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 netsreachability analysisprogram verification

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

(46)

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

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)