3-VASS Reachability is in EXPSPACE
Formal Languages and Automata TheoryLogic in Computer Science
Summary
The authors study a computational model called a 3-dimensional VASS, which is like a machine with three counters that hold non-negative numbers. They focus on the reachability problem, which asks if you can get from one machine state and counter values to another. While the problem's complexity was known to be very high for general cases, the exact difficulty for three counters was unclear for a long time. The authors show that this problem can be solved within EXPSPACE, an improvement over earlier known upper bounds. Their approach uses a method called hierarchical pumpability to find an upper limit on how long the shortest solution runs can be.
Authors
Weijun Chen, Bo Fu, Yuxi Fu, Huan Long, Chengfeng Xue, Qizhe Yang, Yangluo Zheng
Abstract
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.