2 papers
cs.LO2026
A Forward-Only Construction of Semilinear Inductive Invariants for VAS
Clotilde Bizière, Jérôme Leroux, Grégoire Sutre
The reachability problem for Vector Addition Systems (VAS) is a central decision problem in the theory of infinite-state systems, first solved by Kosaraju and Mayr in the 1980s. An…
cs.FL2026
Reachability in VASS Extended with Integer Counters
Clotilde Bizière, Clotilde Bizière, Wojciech CzerwiÅski +9
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 a…