Extending VASS with Additional Integer Counters

This presentation is about automata equipped with both natural- and integer-valued counters that can be incremented and decremented but cannot be tested for zero (denoted VASS+Z). The focus will be on the reachability problem for 1-VASS+Z and 2-VASS+Z; these automata have one and two natural-valued counters, respectively, as well as any number of integer counters. The first goal of this presentation is to share the key ideas in the relatively simple, robust proof that reachability in binary-encoded 1-VASS+Z is in NP. The second goal of this presentation is to show intriguing techniques that we developed to prove that reachability in unary-encoded 2-VASS+Z is PSPACE-hard.

This presentation concerns a part of joint work with Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, and Antoni Puch accepted into LICS'26.

Highlights 2026
TU Wien, Vienna, Austria
Henry Sinclair-Banks, 09/09/26