Document Open Access Logo

On Büchi One-Counter Automata

Authors Stanislav Böhm, Stefan Göller, Simon Halfon, Piotr Hofman

PDF
Thumbnail PDF

File

LIPIcs.STACS.2017.14.pdf
  • Filesize: 0.55 MB
  • 13 pages

Document Identifiers

Author Details

Stanislav Böhm
Stefan Göller
Simon Halfon
Piotr Hofman

Cite As Get BibTex

Stanislav Böhm, Stefan Göller, Simon Halfon, and Piotr Hofman. On Büchi One-Counter Automata. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.STACS.2017.14

Abstract

Equivalence of deterministic pushdown automata is a famous problem in theoretical computer science whose decidability has been shown by Sénizergues. Our first result shows that decidability no longer holds when moving from finite words to infinite words. This solves an open problem that has recently been raised by Löding. In fact, we show that already the equivalence problem for deterministic Büchi one-counter automata is undecidable. Hence, the decidability border is rather tight when taking into account a recent result by Löding and Repke that equivalence of deterministic weak parity pushdown automata (a subclass of deterministic Büchi pushdown automata) is decidable.

Another known result on finite words is that the universality problem for vector addition systems is decidable. We show undecidability when moving to infinite words. In fact, we prove that already the universality problem for nondeterministic Büchi one-counter nets (or equivalently vector addition systems with one unbounded dimension) is undecidable.

Subject Classification

Keywords
  • infinite words
  • deterministic pushdown automata

Metrics

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

References

  1. Rajeev Alur and P. Madhusudan. Visibly pushdown languages. In Proc. of STOC, pages 202-211. ACM, 2004. Google Scholar
  2. Stanislav Böhm, Stefan Göller, and Petr Jančar. Equivalence of deterministic one-counter automata is NL-complete. In Proc. of STOC, pages 131-140, Palo Alto, California, USA, June 2013. ACM Press. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGJ-stoc13.pdf, URL: http://dx.doi.org/10.1145/2488608.2488626.
  3. Didier Caucal, Dung T. Huynh, and Lu Tian. Deciding Branching Bimiliarity of Normed Context-Free Processes Is in Σ₂^p. Inf. Comput., 118(2):306-315, 1995. Google Scholar
  4. Yuxi Fu. Checking Equality and Regularity for Normed BPA with Silent Moves. In Proc. of ICALP, Lecture Notes in Computer Science. Springer, 2013. to appear. Google Scholar
  5. Yoram Hirshfeld and Mark Jerrum. Bisimulation equivanlence is decidable for normed process algebra. In Proc. of ICALP, volume 1644 of Lecture Notes in Computer Science, pages 412-421. Springer, 1999. Google Scholar
  6. Yoram Hirshfeld, Mark Jerrum, and Faron Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science, 158(1&2):143-159, 1996. Google Scholar
  7. Piotr Hofman and Patrick Totzke. Trace inclusion for one-counter nets revisited. In Proc. of Reachability Problems, pages 151-162, 2014. Google Scholar
  8. Petr Jancar. Equivalences of pushdown systems are hard. In Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, pages 1-28, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_1.
  9. Christof Löding. Simplification Problems for Deterministic Pushdown Automata on Infinite Words. Int. J. Found. Comput. Sci., 26(8):1041-1068, 2015. Google Scholar
  10. Christof Löding and Stefan Repke. Regularity Problems for Weak Pushdown ω-Automata and Games. In In Proc. of MFCS, pages 764-776. Springer, 2012. Google Scholar
  11. M. L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall International, Englewood Cliffs, 1967. Google Scholar
  12. Dirk Nowotka and Jirí Srba. Height-Deterministic Pushdown Automata. In Proc. of MFCS, volume 4708 of Lecture Notes in Computer Science, pages 125-134. Springer, 2007. Google Scholar
  13. Joël Ouaknine and James Worrell. On Metric Temporal Logic and Faulty Turing Machines. In In Proc. of FoSSaCSs, volume 3921 of Lecture Notes in Computer Science, pages 217-230. Springer, 2006. Google Scholar
  14. Joël Ouaknine and James Worrell. On the decidability and complexity of Metric Temporal Logic over finite words. Logical Methods in Computer Science, 3(1), 2007. Google Scholar
  15. S. Repke. Simplification problems for automata and games. PhD thesis, RWTH Aachen, 2014. Google Scholar
  16. Philippe Schnoebelen. Lossy Counter Machines Decidability Cheat Sheet. In Antonín Kučera and Igor Potapov, editors, Proc. of Reachability Problems, pages 51-75. Springer, 2010. Google Scholar
  17. Géraud Sénizergues. L(A)=L(B)? decidability results from complete formal systems. Theor. Comput. Sci., 251(1-2):1-166, 2001. Google Scholar
  18. Colin Stirling. Deciding DPDA Equivalence Is Primitive Recursive. In Proc. of ICALP, volume 2380 of Lecture Notes in Computer Science, pages 821-832. Springer, 2002. Google Scholar
  19. Leslie G. Valiant. Regularity and related problems for deterministic pushdown automata. J. ACM, 22(1):1-10, January 1975. 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 About DROPS Imprint Privacy Contact