Demystifying Reachability in Vector Addition Systems
From MaRDI portal
Publication:4635791
DOI10.1109/LICS.2015.16zbMATH Open1392.68308arXiv1503.00745MaRDI QIDQ4635791FDOQ4635791
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)
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.
Full work available at URL: https://arxiv.org/abs/1503.00745
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
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)
Cited In (46)
- Reachability problems on reliable and lossy queue automata
- Petri nets and semilinear sets (extended abstract)
- Title not available (Why is that?)
- 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)
- Unboundedness problems for machines with reversal-bounded counters
- Extensional Petri net
- Directed reachability for infinite-state systems
- A counter abstraction technique for verifying properties of probabilistic swarm systems
- Coverability trees for Petri nets with unordered data
- Forward analysis for WSTS, part I: completions
- Reasoning about reversal-bounded counter machines
- Context-free commutative grammars with integer counters and resets
- 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
- Title not available (Why is that?)
- The ideal view on Rackoff's coverability technique
- Title not available (Why is that?)
- Ackermannian completion of separators
- Reachability in fixed VASS: expressiveness and lower bounds
- Vector addition system reachability problem, a short self-contained proof
- Rewriting systems for reachability in vector addition systems with pairs
- Solvability of orbit-finite systems of linear equations
- The complexity of soundness in workflow nets
- Vector Addition System Reversible Reachability Problem
- 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)
- Title not available (Why is that?)
- 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)
