Invariants for One-Counter Automata with Disequality Tests

TL;DR

This paper refines the computational complexity classification of the reachability problem in one-counter automata with disequality tests, placing it into the second level of the polynomial hierarchy and introducing invariant-based methods for analysis.

Contribution

It establishes tighter complexity bounds for the reachability problem and introduces invariant-based techniques that approximate the reachability set with almost inductive invariants.

Findings

The reachability problem is in the class coNP^NP for disequality tests.

In presence of both equality and disequality tests, the problem is in P^NP^NP.

Invariant-based methods can witness non-reachability through almost inductive invariants.

Abstract

We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value. This reachability problem has been known to be NP-hard and in PSPACE, and characterising its computational complexity has been left as a challenging open question by Almagor, Cohen, P\'erez, Shirmohammadi, and Worrell (2020). We reduce the complexity gap, placing the problem into the second level of the polynomial hierarchy, namely into the class $\mathsf{coNP}^{\mathsf{NP}}$. In the presence of both equality and disequality tests, our upper bound is at the third level, $\mathsf{P}^{\mathsf{NP}^{\mathsf{NP}}}$. To prove this result, we show that non-reachability can be witnessed by a pair of invariants (forward and backward). These invariants are almost inductive. They aim to over-approximate only a "core" of the reachability set instead of the entire set. The invariants are also leaky: it is possible to escape the set. We complement this with separate checks as the leaks can only occur in a controlled way.