# Demystifying Reachability in Vector Addition Systems

arXiv: https://arxiv.org/abs/1503.00745 · HTML: https://mlsanity.com/paper/1503.00745/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Mar 2015.

## Built on by (most cited first, 4 of 4)

- [Improved Ackermannian lower bound for the Petri nets reachability problem](https://mlsanity.com/paper/2105.08551/) (2021)
- [Bi-reachability in Petri nets with data](https://mlsanity.com/paper/2405.16176/) (2024)
- [Solvability of orbit-finite systems of linear equations](https://mlsanity.com/paper/2201.09060/) (2022)
- [Directed Regular and Context-Free Languages](https://mlsanity.com/paper/2401.07106/) (2024)

## Abstract (arXiv)

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.