Invariants for One-Counter Automata with Disequality Tests
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911999072403456 |
|---|---|
| author | Chistikov, Dmitry Leroux, Jérôme Sinclair-Banks, Henry Waldburger, Nicolas |
| author_facet | Chistikov, Dmitry Leroux, Jérôme Sinclair-Banks, Henry Waldburger, Nicolas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_11908 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Invariants for One-Counter Automata with Disequality Tests Chistikov, Dmitry Leroux, Jérôme Sinclair-Banks, Henry Waldburger, Nicolas Formal Languages and Automata Theory Logic in Computer Science 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. |
| title | Invariants for One-Counter Automata with Disequality Tests |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2408.11908 |