One-Counter Automata with Counter Observability
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.
One-counter automata
inclusion checking
observability
visibly one- counter automata
strong automata
20:1-20:14
Regular Paper
Benedikt
Bollig
Benedikt Bollig
10.4230/LIPIcs.FSTTCS.2016.20
R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
R. Alur, V. Kumar, P. Madhusudan, and M. Viswanathan. Congruences for visibly pushdown languages. In Proceedings of ICALP'05, volume 3580 of Lecture Notes in Computer Science, pages 1102-1114, 2005.
R. Alur and P. Madhusudan. Adding nesting structure to words. Journal of the ACM, 56(3):1-43, 2009.
D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87-106, 1987.
V. Bárány, C. Löding, and O. Serre. Regularity problems for visibly pushdown languages. In Proceedings of STACS'06, volume 3884 of Lecture Notes in Computer Science, pages 420-431. Springer, 2006.
A. Bès. An application of the Feferman-Vaught theorem to automata and logics for words over an infinite alphabet. Logical Methods in Computer Science, 4(1), 2008.
P. Chervet and I. Walukiewicz. Minimizing variants of visibly pushdown automata. In Proceedings of MFCS'07, volume 4708 of Lecture Notes in Computer Science, pages 135-146, 2007.
D. Chistikov, W. Czerwiński, P. Hofman, M. Pilipczuk, and M. Wehar. Shortest paths in one-counter systems. In Proceedings of FoSSaCS'16, volume 9634 of Lecture Notes in Computer Science, pages 462-478. Springer, 2016.
C. Czyba, C. Spinrath, and W. Thomas. Finite automata over infinite alphabets: Two models with transitions for local change. In Proceedings of DLT'15, volume 9168 of Lecture Notes in Computer Science, pages 203-214. Springer, 2015.
L. D'Antoni and M. Veanes. Minimization of symbolic automata. In Proceedings of POPL'14, pages 541-554. ACM, 2014.
S. Göller, R. Mayr, and A. Widjaja To. On the computational complexity of verifying one-counter processes. In Proceedings of LICS'09, pages 235-244. IEEE Computer Society Press, 2009.
S. A. Greibach. An infinite hierarchy of context-free languages. Journal of the ACM, 16(1):91-106, 1969.
C. Haase, J. Ouaknine, and J. Worrell. Relating reachability problems in timed and counter automata. Fundamenta Informaticae, 143(3-4):317-338, 2016.
O. H. Ibarra. Restricted one-counter machines with undecidable universe problems. Mathematical Systems Theory, 13:181-186, 1979.
P. Jančar. Decidability of bisimilarity for one-counter processes. Information and Computation, 158(1):1-17, 2000.
K. Mehlhorn. Pebbling mountain ranges and its application of DCFL-recognition. In Proceedings of ICALP'80, volume 85 of Lecture Notes in Computer Science, pages 422-435. Springer, 1980.
A. R. Meyer and L. J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In 13th Annual Symposium on Switching and Automata Theory, pages 125-129, 1972.
D. Neider and C. Löding. Learning visibly one-counter automata in polynomial time. Technical Report AIB-2010-02, RWTH Aachen, January 2010.
D. Nowotka and J. Srba. Height-deterministic pushdown automata. In Proceedings of MFCS'07, volume 4708 of Lecture Notes in Computer Science, pages 125-134. Springer, 2007.
R. J. Parikh. On context-free languages. Journal of the ACM, 13(4):570-581, 1966.
J.-P. Pécuchet. Automates boustrophédon et mots infinis. Theoretical Computer Science, 35:115-122, 1985.
J. Srba. Visibly pushdown automata: From language equivalence to simulation and bisimulation. In Proceedings of CSL'06, volume 4207 of Lecture Notes in Computer Science, pages 89-103. Springer, 2006.
W. Thomas. Languages, automata and logic. In A. Salomaa and G. Rozenberg, editors, Handbook of Formal Languages, volume 3, pages 389-455. Springer, 1997.
L. G. Valiant and M. S. Paterson. Deterministic one-counter automata. Journal of Computer and System Sciences, 10(3):340-350, 1975.
J. van Leeuwen. Effective constructions in well-partially-ordered free monoids. Discrete Mathematics, 21(3):237-252, 1978.
A. Widjaja To. Unary finite automata vs. arithmetic progressions. Inf. Process. Lett., 109(17):1010-1014, 2009.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode