eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-12-10
20:1
20:14
10.4230/LIPIcs.FSTTCS.2016.20
article
One-Counter Automata with Counter Observability
Bollig, Benedikt
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. Moreover, it turns out that they are expressively equivalent to strong automata, in which transitions are guarded by MSO formulas over the natural numbers with successor.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol065-fsttcs2016/LIPIcs.FSTTCS.2016.20/LIPIcs.FSTTCS.2016.20.pdf
One-counter automata
inclusion checking
observability
visibly one- counter automata
strong automata