Document Open Access Logo

Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors Christof Löding, Anton Pirogov

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2019.120.pdf
  • Filesize: 0.55 MB
  • 13 pages

Document Identifiers

Author Details

Christof Löding
  • RWTH Aachen University, Ahornstr. 55, 52074 Aachen, Germany
Anton Pirogov
  • RWTH Aachen University, Ahornstr. 55, 52074 Aachen, Germany

Funding

  • Pirogov, Anton: This author is supported by the German research council (DFG) Research Training Group 2236 UnRAVeL

Cite As Get BibTex

Christof Löding and Anton Pirogov. Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 120:1-120:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ICALP.2019.120

Abstract

Determinization of Büchi automata is a long-known difficult problem, and after the seminal result of Safra, who developed the first asymptotically optimal construction from Büchi into Rabin automata, much work went into improving, simplifying, or avoiding Safra’s construction. A different, less known determinization construction was proposed by Muller and Schupp. The two types of constructions share some similarities but their precise relationship was still unclear. In this paper, we shed some light on this relationship by proposing a construction from nondeterministic Büchi to deterministic parity automata that subsumes both constructions: Our construction leaves some freedom in the choice of the successor states of the deterministic automaton, and by instantiating these choices in different ways, one obtains as particular cases the construction of Safra and the construction of Muller and Schupp. The basis is a correspondence between structures that are encoded in the macrostates of the determinization procedures - Safra trees on one hand, and levels of the split-tree, which underlies the Muller and Schupp construction, on the other hand. Our construction also allows for mixing the mentioned constructions, and opens up new directions for the development of heuristics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Büchi automata
  • determinization
  • parity automata

Metrics

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

Related Versions

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  2. J Richard Büchi. On a decision method in restricted second order arithmetic. In Studies in Logic and the Foundations of Mathematics, volume 44, pages 1-11. Elsevier, 1966. Google Scholar
  3. Thomas Colcombet and Konrad Zdanowski. A Tight Lower Bound for Determinization of Transition Labeled Büchi Automata. In ICALP 2009, volume 5556 of Lecture Notes in Computer Science, pages 151-162. Springer, 2009. Google Scholar
  4. Seth Fogarty, Orna Kupferman, Moshe Y Vardi, and Thomas Wilke. Profile trees for Büchi word automata, with application to determinization. Information and Computation, 245:136-151, 2015. Google Scholar
  5. Paul Gastin and Denis Oddoux. Fast LTL to Büchi Automata Translation. In Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings, pages 53-65, 2001. URL: http://dx.doi.org/10.1007/3-540-44585-4_6.
  6. Dimitra Giannakopoulou and Klaus Havelund. Automata-Based Verification of Temporal Properties on Running Programs. In 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 26-29 November 2001, Coronado Island, San Diego, CA, USA, pages 412-416, 2001. URL: http://dx.doi.org/10.1109/ASE.2001.989841.
  7. Detlef Kähler and Thomas Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In ICALP 2008, pages 724-735. Springer, 2008. Google Scholar
  8. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and control, 9(5):521-530, 1966. Google Scholar
  9. Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. Strix: Explicit Reactive Synthesis Strikes Back! In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, pages 578-586, 2018. URL: http://dx.doi.org/10.1007/978-3-319-96145-3_31.
  10. David E Muller and Paul E Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141(1-2):69-107, 1995. Google Scholar
  11. Nir Piterman. From nondeterministic Buchi and Streett automata to deterministic parity automata. In Logic in Computer Science, 2006 21st Annual IEEE Symposium on, pages 255-264. IEEE, 2006. Google Scholar
  12. Roman R Redziejowski. An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae, 119(3-4):393-406, 2012. Google Scholar
  13. Shmuel Safra. On the complexity of omega-automata. In 29th Annual Symposium on Foundations of Computer Science, 1988., pages 319-327. IEEE, 1988. Google Scholar
  14. Sven Schewe. Tighter bounds for the determinisation of Büchi automata. In FOSSACS, pages 167-181. Springer, 2009. Google Scholar
  15. Fabio Somenzi and Roderick Bloem. Efficient Büchi Automata from LTL Formulae. In Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, pages 248-263, 2000. URL: http://dx.doi.org/10.1007/10722167_21.
  16. Wolfgang Thomas. Languages, Automata, and Logic. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Vol. 3, pages 389-455. Springer-Verlag New York, Inc., New York, NY, USA, 1997. Google Scholar
  17. Wolfgang Thomas. Church’s Problem and a Tour through Automata Theory. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, pages 635-655. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78127-1.
  18. Moshe Y. Vardi and Thomas Wilke. Automata: from logics to algorithms. In Logic and automata - history and perspectives, volume 2 of Texts in Logic and Games, pages 629-724. Amsterdam University Press, 2007. 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