Document Open Access Logo

One-Counter Automata with Counter Observability

Author Benedikt Bollig

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.20.pdf
  • Filesize: 0.54 MB
  • 14 pages

Document Identifiers

Author Details

Benedikt Bollig

Cite AsGet BibTex

Benedikt Bollig. One-Counter Automata with Counter Observability. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 20:1-20:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSTTCS.2016.20

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. 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.
Keywords
  • One-counter automata
  • inclusion checking
  • observability
  • visibly one- counter automata
  • strong automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  2. 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. Google Scholar
  3. R. Alur and P. Madhusudan. Adding nesting structure to words. Journal of the ACM, 56(3):1-43, 2009. Google Scholar
  4. D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87-106, 1987. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. L. D'Antoni and M. Veanes. Minimization of symbolic automata. In Proceedings of POPL'14, pages 541-554. ACM, 2014. Google Scholar
  11. 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. Google Scholar
  12. S. A. Greibach. An infinite hierarchy of context-free languages. Journal of the ACM, 16(1):91-106, 1969. Google Scholar
  13. C. Haase, J. Ouaknine, and J. Worrell. Relating reachability problems in timed and counter automata. Fundamenta Informaticae, 143(3-4):317-338, 2016. Google Scholar
  14. O. H. Ibarra. Restricted one-counter machines with undecidable universe problems. Mathematical Systems Theory, 13:181-186, 1979. Google Scholar
  15. P. Jančar. Decidability of bisimilarity for one-counter processes. Information and Computation, 158(1):1-17, 2000. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. D. Neider and C. Löding. Learning visibly one-counter automata in polynomial time. Technical Report AIB-2010-02, RWTH Aachen, January 2010. Google Scholar
  19. 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. Google Scholar
  20. R. J. Parikh. On context-free languages. Journal of the ACM, 13(4):570-581, 1966. Google Scholar
  21. J.-P. Pécuchet. Automates boustrophédon et mots infinis. Theoretical Computer Science, 35:115-122, 1985. Google Scholar
  22. 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. Google Scholar
  23. W. Thomas. Languages, automata and logic. In A. Salomaa and G. Rozenberg, editors, Handbook of Formal Languages, volume 3, pages 389-455. Springer, 1997. Google Scholar
  24. L. G. Valiant and M. S. Paterson. Deterministic one-counter automata. Journal of Computer and System Sciences, 10(3):340-350, 1975. Google Scholar
  25. J. van Leeuwen. Effective constructions in well-partially-ordered free monoids. Discrete Mathematics, 21(3):237-252, 1978. Google Scholar
  26. A. Widjaja To. Unary finite automata vs. arithmetic progressions. Inf. Process. Lett., 109(17):1010-1014, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact