Reachability in VASS Extended with Integer Counters
Clotilde Bizi\`ere, Wojciech Czerwi\'nski, Roland Guttenberg, J\'er\^ome Leroux, Vincent Michielini, {\L}ukasz Orlikowski, Antoni Puch, Henry Sinclair-Banks

TL;DR
This paper investigates the reachability problem in VASS extended with integer counters, establishing complexity bounds and demonstrating how integer counters affect the number of counters needed for hardness.
Contribution
It provides new complexity results for VASS+Z, including NP-completeness for 1-VASS+Z and upper bounds in higher dimensions, showing how integer counters influence computational complexity.
Findings
NP-complete reachability in 1-VASS+Z
Upper bounds in $ ext{F}_{d+2}$ for d-VASS+Z
Lower bounds showing reduced N-counter requirements due to Z-counters
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 , using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class . 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
Topicssemigroups and automata theory · Complexity and Algorithms in Graphs · Formal Methods in Verification
