Reachability in Geometrically $d$-Dimensional VASS

TL;DR

This work proves that reachability for geometrically $d$-dimensional VASS, with $d>2$, lies in the complexity class $\mathbf{F}_d$, extending previous bounds and matching the complexity of high-dimensional cases. The authors develop a refined KLMST-style decomposition based on constraint graphs, introducing Eulerian and orthogonal simplifications and algebraic/combinatorial decompositions to obtain normal CGSes with short witnesses. A geometric termination argument shows that refinement sequences have length at most $d$, and size bounds on decompositions are governed by polynomial and $2^{\text{poly}()}$ factors, culminating in a final $\mathbf{F}_d$ upper bound. A dedicated treatment of geometrically $2$-dimensional VASS yields short witness representations via linear constraint graph sequences, and the overall framework yields a simple algorithmic recipe: nondeterministically guess a witness path whose length is bounded by $F_d(|\mathbf{a}G\mathbf{b}|)$. The paper also sketches future research directions, including tighter lower bounds, understanding the relation between geometrically constrained and unconstrained VASS, and extending results to related models like BVASS and PVASS.

Abstract

Reachability of vector addition systems with states (VASS) is Ackermann complete~\cite{leroux2021reachability,czerwinski2021reachability}. For $d$-dimensional VASS reachability it is known that the problem is NP-complete~\cite{HaaseKreutzerOuaknineWorrell2009} when $d=1$, PSPACE-complete~\cite{BlondinFinkelGoellerHaaseMcKenzie2015} when $d=2$, and in $\mathbf{F}_d$~\cite{FuYangZheng2024} when $d>2$. A geometrically $d$-dimensional VASS is a $D$-dimensional VASS for some $D\ge d$ such that the space spanned by the displacements of the circular paths admitted in the $D$-dimensional VASS is $d$-dimensional. It is proved that the $\mathbf{F}_d$ upper bounds remain valid for the reachability problem in the geometrically $d$-dimensional VASSes with $d>2$.

Figures (5)

• Figure 1: Constraint Graph Sequence
• Figure 2: Decomposition
• Figure 3: Constructing Witness for Normal CGS.
• Figure 4: A Walk Divided by the Border between $\mathbb{L}_G$ and $\mathbb{U}_G$.
• Figure 5: Swapping the order of the growth of $a$ and $b$.

Theorems & Definitions (37)

• Theorem 1
• Lemma 2: Pottier
• Corollary 3
• Definition 4
• Lemma 5
• proof
• Lemma 6
• Definition 7
• Definition 8
• Lemma 9