3-VASS Reachability is in EXPSPACE
For theoretical computer scientists studying VASS reachability, this paper tightens the complexity upper bound for 3-VASS from 2-EXPSPACE to EXPSPACE, narrowing the gap with the PSPACE lower bound.
The paper proves that the reachability problem for 3-dimensional VASS is in EXPSPACE, improving the previous 2-EXPSPACE upper bound. The proof uses a hierarchical pumpability analysis to establish a doubly-exponential bound on the length of shortest runs.
A VASS can be viewed as a finite-state automaton manipulating a fixed number (called its dimension) of counters holding non-negative values. The reachability problem, asking whether there is a run from one configuration, defined by a state and values of the counters, to another configuration, has been a long-standing algorithmic challenge in theoretical computer science. When the dimension is part of the input, the problem has been shown to be ACKERMANN-complete in 2021. For fixed dimension greater than 2, and in particular for dimension 3, the exact complexity of the reachability problem remains unclear. For a long time the known algorithms for the 3-dimensional VASS reachability problem had been non-elementary, while the best known lower bound is merely PSPACE hardness inherited from dimension 2. A recent breakthrough in (Czerwiński, Jecker, Lasota, Orlikowski, ICALP 2025) gave the first elementary upper bound for the problem, namely 2-EXPSPACE. In this paper it is shown that the reachability problem in 3-VASS belongs to EXPSPACE. The proof is based on a hierarchical pumpability analysis, yielding a doubly-exponential length bound on the shortest runs between two configurations.