One-Counter Automata with Counter Observability

TL;DR

This paper studies one-counter automata with counter observability, showing that key decision problems become PSPACE-complete and that the model is effectively determinizable, bridging the gap with finite automata.

Contribution

It introduces counter observability in OCAs, proving that universality and inclusion are PSPACE-complete and establishing effective determinization and closure properties.

Findings

Universality and inclusion are PSPACE-complete.

OCAs with counter observability are effectively determinizable.

The model is closed under all boolean operations.

Abstract

In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations.