Technical Summary: 3-VASS Reachability is in EXPSPACE

Problem Statement

The paper addresses the reachability problem for 3-dimensional Vector Addition Systems with States (3-VASS). A VASS is a finite-state automaton equipped with a fixed number of counters (dimensions) holding non-negative integers. The reachability problem asks whether a target configuration (state and counter values) is reachable from a source configuration via a sequence of valid transitions.

While the general VASS reachability problem (where dimension is part of the input) was proven to be ACKERMANN-complete in 2021, the exact complexity for fixed dimensions $d > 2$ remains a central open question. Specifically for 3-VASS:

• Lower Bound: The problem is known to be PSPACE-hard, inherited from the 2-dimensional case.
• Previous Upper Bound: Until this work, the best known upper bound was 2-EXPSPACE (double-exponential space), established by Czerwiński et al. (ICALP 2025). Prior to that, algorithms were non-elementary.

The paper aims to close the gap between the PSPACE lower bound and the 2-EXPSPACE upper bound by proving that 3-VASS reachability belongs to EXPSPACE (single-exponential space).

Methodology and Proof Strategy

The core of the proof is establishing a doubly-exponential length bound on the shortest runs between two configurations in a 3-VASS. If the shortest run length is bounded by $N^{2^{poly(k)}}$ (where $N$ is the input size and $k$ is the number of strongly connected components), then reachability can be decided in EXPSPACE by nondeterministically guessing a path of that length.

The authors employ a hierarchical reduction strategy and a separation-of-concerns proof technique, refining the class of 3-VASS instances into a sequence of subclasses. This approach avoids the "nested" induction that led to triple-exponential bounds in previous work.

1. Hierarchical Classification of VASS

The paper defines a hierarchy of subclasses for 3-VASS, ordered by increasing generality:
$$\text{DiagVASS}_3 \subsetneq \text{Semi-diagVASS}_3 \subsetneq \text{PumpVASS}_3 \subsetneq \text{Semi-pumpVASS}_3 \subsetneq \text{SeqVASS}_3$$

• DiagVASS: Instances where both forward and backward "diagonal" cycles exist (cycles that can pump all counters positively).
• PumpVASS: Instances where both forward and backward "pumpable" cycles exist (cycles that can pump at least one counter positively).
• SeqVASS: General sequential VASS, where the run traverses a sequence of Strongly Connected Components (SCCs) connected by bridges.

The proof proceeds by establishing the length bound for the most restrictive class (DiagVASS) and then using length-controlled self-reductions to transfer these bounds to the more general classes.

2. Key Technical Components

A. Efficient Representation of Reachability Sets (Geometrically 2D VASS)

A crucial tool is the analysis of geometrically 2-dimensional VASS, where all runs stay between two parallel 2D planes. The authors extend results from Czerwiński et al. to show that the reachability set of such systems, even when starting from a "hybrid set" (a base vector plus a restricted periodic set), can be represented as a finite union of hybrid sets with polynomial-sized descriptions. This allows for efficient manipulation of reachability sets without incurring exponential blowup in the representation size.

B. Handling Non-Wide Diagonal Instances

For DiagVASS, the authors distinguish between "wide" and "non-wide" instances.

• Wide: The sequential cone of the system contains all positive vectors. These are handled by reducing to known results.
• Non-Wide: The authors prove that in non-wide diagonal instances, the sequential cones of the prefix and suffix of the run are separated by a hyperplane. This geometric separation implies that counter values in intermediate components are constrained within a pair of parallel 2D planes. Consequently, the problem can be transformed into a sequence of geometrically 2-dimensional VASS instances, allowing the application of the efficient representation techniques mentioned above to derive a doubly-exponential bound.

C. Length-Controlled Self-Reduction

To move from PumpVASS and SeqVASS to DiagVASS, the paper introduces a length-controlled self-reduction.

• Extraction of Joint Diagonality: For a pumpable instance, the authors show that one can extract a "jointly diagonal" prefix (a sequence of cycles that collectively pump all counters).
• Reduction: This prefix is used to construct a new VASS instance with fewer components (or a simpler structure) that is diagonal. The size of this new instance is controlled by the length function of the target class.
• Avoiding Nesting: Unlike previous approaches that nested the length bound function (e.g., $h_k(h_{k-1}(\dots))$), this method ensures the length bound appears only once on the right-hand side of the recurrence. This structural change is what reduces the complexity from 2-EXPSPACE to EXPSPACE.

Key Contributions and Results

1. Main Theorem: The 3-VASS reachability problem is in EXPSPACE.

   • This holds for both unary and binary encodings of the input.
   • The proof relies on showing that for any $k$-component 3-VASS, the length of the shortest run is bounded by $size(V, s, t)^{2^{poly(k)}}$.

2. Refined Complexity Landscape: The paper provides a detailed analysis of the complexity of subclasses of 3-VASS:

   • DiagVASS3: Proven to be in EXPSPACE (improving the previous 2-EXPSPACE bound).
   • PumpVASS3: Proven to admit doubly-exponentially short runs.
   • SeqVASS3: Proven to admit doubly-exponentially short runs via self-reduction to PumpVASS.

3. Methodological Advancement: The paper introduces a hierarchical pumpability analysis and a separation-of-concerns strategy. By decomposing the problem into geometrically 2D subproblems and using self-reductions that respect the component hierarchy, the authors eliminate the triple-exponential growth inherent in previous inductive proofs.

Significance and Claims

The paper claims to significantly advance the understanding of the 3-VASS reachability problem, which has been a long-standing challenge in theoretical computer science.

• Tightening the Bound: The result narrows the complexity gap for 3-VASS from a double-exponential upper bound to a single-exponential one. While the lower bound remains PSPACE, the authors note that the reduction from general 3-VASS to pumpable 3-VASS likely cannot be done in polynomial space, suggesting that 3-VASS might indeed be EXPSPACE-hard.
• Foundation for Future Work: The paper explicitly states that determining the exact complexity (PSPACE vs. EXPSPACE) remains open. It highlights that a definitive EXPSPACE-hardness proof would require an example of a 3-VASS admitting doubly-exponential shortest runs, which is currently unknown.
• Implications for Higher Dimensions: The authors suggest that their perspective on bounding shortest runs could be fruitful for analyzing VASS in dimensions $d \ge 4$, where current upper bounds are far from elementary.

In summary, the paper provides a rigorous proof that 3-VASS reachability is solvable in exponential space, utilizing a novel combination of geometric separation arguments, efficient reachability set representations, and a refined self-reduction framework that avoids the complexity blowup of previous methods.