Demystifying Reachability in Vector Addition Systems
arXiv:1503.00745 · doi:10.1109/LICS.2015.16
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.
To appear in the Proceedings of LICS 2015
References in corpus (5)
Cited by in corpus (18)
- Complexity Hierarchies Beyond Elementary
- Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension
- Open Petri Nets
- Approaching the Coverability Problem Continuously
- Reasoning about Data Repetitions with Counter Systems
- A Characterization for Decidable Separability by Piecewise Testable Languages
- Verifying Unboundedness via Amalgamation
- Shortest paths in one-counter systems
- On Freeze LTL with Ordered Attributes
- Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
- The Tractability Border of Reachability in Simple Vector Addition Systems with States
- The Complexity of Reachability in Affine Vector Addition Systems with States
- Continuous Reachability for Unordered Data Petri nets is in PTime
- History-Constrained Systems
- An Approach to Regular Separability in Vector Addition Systems
- Critical Observability for Automata and Petri Nets
- Efficient Algorithms for Checking Fast Termination in VASS
- PTL-separability and closures for WQOs on words