English

Reachability in VASS Extended with Integer Counters

Formal Languages and Automata Theory 2026-03-06 v1

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 d2d \geq 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class Fd+2\mathcal{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.

Cite

@article{arxiv.2603.05221,
  title  = {Reachability in VASS Extended with Integer Counters},
  author = {Clotilde Bizière and Wojciech Czerwiński and Roland Guttenberg and Jérôme Leroux and Vincent Michielini and Łukasz Orlikowski and Antoni Puch and Henry Sinclair-Banks},
  journal= {arXiv preprint arXiv:2603.05221},
  year   = {2026}
}
R2 v1 2026-07-01T11:04:58.804Z