Precise Complexity Analysis of Coverability in Vector Addition Systems

Coverability in Vector Addition Systems with States (VASS) is a well-known, well-studied, fundamental problem for infinite-state systems. In short, VASS can be seen as finite automata equipped with non-negative integer counters that can be incremented and decremented but cannot be zero-tested. Over the last few years, our understanding of the exact complexity of coverability in VASS has significantly improved. In this presentation, I will explain: (i) a conditionally optimal ETH-based lower bound on the time required to decide coverability in VASS with a non-fixed number of counters, (ii) a conditional lower bound on the time required to decide coverability in unary-encoded VASS with two counters, and (iii) the state-of-the-art complexity of coverability in binary-encoded VASS with one counter.

The 24th International Workshop on Verification of Infinite-State Systems (INFINITY 2026)
Windsor Building, Royal Holloway, University of London, Egham, UK
Henry Sinclair-Banks, 06/07/26