Invariants for One-Counter Automata with Disequality Tests

TL;DR

This work studies reachability in one-counter automata with disequality tests and proves a tight placement in the second level of the polynomial hierarchy, specifically coNP^{NP}, via a novel leaky-invariant framework that overapproximates a core portion of the reachability set. It introduces forward and backward invariants within strongly connected components and composes them across the SCC structure using a separator mechanism to certify non-reachability. When equality tests are added, the complexity rises to P^{NP^{NP}}, reflecting the higher expressive power needed to lift candidate runs. The approach relies on concise descriptions of invariant cores (arithmetic progressions within bounded chains) and a lifting technique that connects local analyses to global reachability. Overall, the results advance the theoretical understanding of OCA with tests and offer a compositional method that could inform practical invariant construction for VASS-like systems.

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érez, 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.

Figures (2)

• Figure 1: Left. This OCA without tests is constructed from an instance of the subset sum problem $(a_1, \ldots, a_n, v)$; this is in fact how the reachability problem in OCA without tests is proved to be NP-hard in HaaseKOW09. Configuration $(t,0)$ can be reached from configuration $(s,0)$ whenever there exists a subset of $\{a_1, \ldots, a_n\}$ whose elements sum up to $v$. Note that all unlabelled transitions have update zero. The set of configurations reachable from $(s,0)$ can have size exponential in $n$, and its structure is unwieldy. Right. (For Section \ref{['sec:bg-oca']}.) The named state $q$ belongs to $Q_+$ since there is a simple $q$-cycle with positive effect. There are six bounded chains of configurations at $q$. The disequality test $\neq 5$ bounds the counter values with residue $0$ modulo $5$, so $\{(q, 0)\}$ and $\{(q, 5)\}$ are bounded chains. The disequality test $\neq 30$ bounds the counter values with residue $3$ modulo $5$, so $\{(q, 3), (q, 8), (q, 13), (q, 18), (q, 23),(q, 28)\}$ is a bounded chain. The disequality test $\neq 15$ bounds the counter values with residue $2$ modulo $5$, so $\{(q, 2), (q, 7), (q,12)\}$ is a bounded chain.
• Figure 2: Core inductive sets and the separator they induce. The core of the forward leaky invariant is $I = I_1 \cup I_2 \cup I_3 \cup I_4$ (the blue circular sets) and the core of the backward leaky invariant is $J = J_1 \cup J_2 \cup J_3 \cup J_4$ (the red circular sets). The induced separator $(\mathcal{I}, \mathcal{J})$ is shown as blue and red rounded quadrilaterals containing the core sets. Notice that $\mathsf{src} \in I$ and $\mathsf{trg} \in J$. The upwards coiled arrow from $c'$ represents that $c'$ is locally unbounded in the SCC $S_2$ and the downwards coiled arrow from $d'$ represents that $d'$ is locally unbounded in the SCC $S_3^{\textit{R}}$. Note also the separator conditions: Condition \ref{['con:separator']}\ref{['sep1']} means that configurations $c \in \mathcal{I}$ and $d \in \mathcal{J}$ cannot reach one another by one transition, so $c \not\to{} d$; Condition \ref{['con:separator']}\ref{['sep2']} means that unbounded configurations $c' \in \mathcal{I}$ and $d' \in \mathcal{J}$ cannot reach one another via a candidate run, so $c\: \hbox{;\tiny $/$}{\xrightarrow[\mathbb Z]{*}} \:d$.

Theorems & Definitions (41)

• Lemma 1: see AlmagorCPS020
• Lemma 1
• Lemma 1
• Remark 2
• Lemma 2: see AlmagorCPS020
• Lemma 3
• Theorem 4
• Lemma 5
• Theorem 6
• Lemma 6: Lifting