Improved Algorithm for Reachability in $d$-VASS

TL;DR

This paper addresses reachability in fixed-dimension $d$-VASS and improves the known upper bound to $ extsf{F}_d$ for $d \,\ge\, 3$, tightening previous results that placed the bound at $ extsf{F}_{d+4}$. The authors introduce two novel lemmas: (i) a generalization of the linear path scheme characterization to cases where the geometric dimension is at most $2$, enabling short linear path schemes, and (ii) a refined fast-growing-function analysis that reduces the bound from $ extsf{F}_{d+1}$ to $ extsf{F}_d$, together with a streamlined KLMST decomposition. These components together yield a simplified algorithmic framework for reachability in $d$-VASS and advance the theoretical understanding of fixed-dimension complexity, aligning upper bounds more closely with known lower bounds. The results have implications for the design of decision procedures in Petri nets and related models where dimension is fixed.

Abstract

An $\mathsf{F}_{d}$ upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where $\mathsf{F}_d$ is the $d$-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the $2$-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the $\mathsf{F}_{d + 4}$ upper bound due to Leroux and Schmitz (LICS 2019).