Reachability in Five-Dimensional Vector Addition Systems Is PSPACE-Complete
Abstract
Abstract. Vector addition systems (VAS) are a fundamental model of concurrent computation in which transitions update nonnegative integer counters by adding integer vectors, provided all counters remain nonnegative. Closely related to Petri nets, VAS are the single-state counterpart of vector addition systems with states (VASS), which use finitely many states to restrict the available transitions.
A classical simulation of d-VASS by (d+3)-VAS connects their reachability problems, but the complexity-theoretic picture of fixed-dimensional VAS remains largely unclear. While reachability in 2-VASS is PSPACE-complete under binary encoding, the best known upper bound for 5-VAS was only elementary. We prove that every reachable 5-VAS instance has a reachability witness of length polynomial in its unary size.
Consequently, 5-VAS reachability is NL-complete under unary encoding and PSPACE-complete under binary encoding. We also establish a polynomial factorization of the reachability relation of every d-VAS with d ≥ 3. For 5-VAS, this strengthens Hopcroft and Pansiot's effective semilinearity of reachability sets to the full reachability relation. For every fixed d ≥ 3, it also yields an Fd upper bound for reachability in (d+3)-VAS.
