Demystifying Reachability in Vector Addition Systems

TL;DR

This paper clarifies the decomposition technique used in proving reachability in vector addition systems and establishes the first known complexity upper bounds, specifically a cubic Ackermann bound, for the problem.

Contribution

It justifies the run decomposition method via ideal decomposition and applies recent complexity results to derive an Ackermann upper bound for VAS reachability.

Findings

Decomposition computes the ideal decomposition of run sets.

Established a cubic Ackermann upper bound for VAS reachability.

Provided the first known complexity upper bounds for general VAS reachability.

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.