Reachability in VASS Extended with Integer Counters
Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, Antoni Puch, and Henry Sinclair-Banks
To appear in LICS'26
DOI: 
Full version: https://arxiv.org/abs/2603.05221

Abstract: 
We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N- and Z-counters; the N-counters are required to remain nonnegative and the Z-counters do not have this restriction. We study the complexity of the reachability problem for VASS+Z when the number of N-counters is fixed. We show that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class F_{d+2}. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the Z-counters with N-counters.
To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of N-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+Z is PSPACE-hard; without Z-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+Z is Tower-hard. Without Z-counters, reachability in 3-VASS has elementary complexity and Tower-hardness is only known in dimension 8.