Document Open Access Logo

A Modular Approach for Büchi Determinization

Authors Dana Fisman, Yoad Lustig

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.368.pdf
  • Filesize: 0.63 MB
  • 15 pages

Document Identifiers

Author Details

Dana Fisman
Yoad Lustig

Cite As Get BibTex

Dana Fisman and Yoad Lustig. A Modular Approach for Büchi Determinization. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 368-382, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.368

Abstract

The problem of Büchi determinization is a fundamental problem with important applications in reactive synthesis, multi-agent systems and probabilistic verification. The first asymptotically optimal Büchi determinization (a.k.a the Safra construction), was published in 1988. While asymptotically optimal, the Safra construction is notorious for its technical complexity and opaqueness in terms of intuition.  While some improvements were published since the Safra construction, notably Kähler and Wilke’s construction, understanding the constructions remains a non-trivial task.

In this paper we present a modular approach to Büchi determinization, where the difficulties are addressed one at a time, rather than simultaneously, making the solutions natural and easy to understand. We build on the notion of the skeleton trees of Kähler and Wilke. We first show how to construct a deterministic automaton in the case the skeleton's width is one. Then we show how to construct a deterministic automaton in the case the skeleton's width is k (for any given k). The overall construction is obtained by running in parallel the automata for all widths.

Subject Classification

Keywords
  • Büchi automata
  • Determinization
  • Verification
  • Games
  • Synthesis

Metrics

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

References

  1. R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In In Proc. 38th Symp. on Foundations of Computer Science, pages 100-109, 1997. Google Scholar
  2. J.R. Büchi. Weak second-order arithmetic and finite automata. Zeit. Math. Logik und Grundl. Math., 6:66-92, 1960. Google Scholar
  3. A. Church. Applications of recursive arithmetic to the problem of circuit synthesis. In Summaries of the Summer Institute of Symbolic Logic, volume I, pages 3-50, 1957. Google Scholar
  4. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857-907, 1995. Google Scholar
  5. J. Esparza and J. Kretínský. From LTL to deterministic automata: A Safraless compositional approach. In In Proc 26th Int. Conf. on Comp. Aided Verif., pages 192-208, 2014. Google Scholar
  6. S. Fogarty, O. Kupferman, M.Y. Vardi, and T. Wilke. Profile trees for büchi word automata, with application to determinization. In GandALF, pages 107-121, 2013. Google Scholar
  7. S. Fogarty, O. Kupferman, T. Wilke, and M.Y. Vardi. Unifying büchi complementation constructions. ogical Methods in Computer Science, 9, 2013. Google Scholar
  8. E. Friedgut, O. Kupferman, and M.Y. Vardi. Büchi complementation made tighter. Int. J. Found. Comput. Sci., 17:851-868, 2004. Google Scholar
  9. S. Gurumurthy, O. Kupferman, F. Somenzi, and M.Y. Vardi. On complementing nondeterministic Büchi automata. In In Proc. 12th Conf. on CHARME, volume 2860 of LNCS, pages 96-110. Springer, 2003. Google Scholar
  10. T.A. Henzinger and N. Piterman. Solving games without determinization. In Annual Conf. of the Eur. Asso. for Comp. Sci. Log., volume 4207 of LNCS, pages 394-410, 2006. Google Scholar
  11. D. Kähler and T. Wilke. Complementation, disambiguation, and determinization of Büchi automata unified. In ICALP08, volume 5125 of LNCS, pages 724-735. Springer, 2008. Google Scholar
  12. N. Klarlund. Progress measures for complementation of ω-automata with applications to temporal logic. In In Proc. 32nd Symp. on Found. of Comp. Sci., pages 358-367, 1991. Google Scholar
  13. D. Kozen. Theory of Computation. Texts in Computer Science. Springer, 2006. Google Scholar
  14. O. Kupferman, N. Piterman, and M.Y. Vardi. Safraless compositional synthesis. In Proc 18th of CAV, volume 4144 of LNCS, pages 31-44. Springer, 2006. Google Scholar
  15. O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak. In Proc. 5th Israeli Symp. on Theory of Computing and Systems, pages 147-158, 1997. Google Scholar
  16. O. Kupferman and M.Y. Vardi. Synthesizing distributed systems. In In Proc. 16th IEEE Symp. on Logic in Computer Science, pages 389-398, 2001. Google Scholar
  17. O. Kupferman and M.Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. Google Scholar
  18. L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969. Google Scholar
  19. W. Liu and J. Wang. A tighter analysis of piterman’s büchi determinization. Inf. Process. Lett., 109(16):941-945, 2009. Google Scholar
  20. R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521-530, 1966. Google Scholar
  21. M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 1988. Google Scholar
  22. S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984. Google Scholar
  23. D.E. Muller and P.E. Schupp. Simulating alternating tree automata by nondeterministic automata. TCS, 141:69-107, 1995. Google Scholar
  24. Jean-Pierre Pécuchet. On the complementation of büchi automata. Theoretical Computer Science, 47:95-98, 1986. Google Scholar
  25. N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In Proc. 21st IEEE Symp. on Logic in Computer Science, 2006. Google Scholar
  26. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 179-190, 1989. Google Scholar
  27. M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1-35, 1969. Google Scholar
  28. S. Safra. On the complexity of ω-automata. In In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988. Google Scholar
  29. S. Safra. Exponential determinization for ω-automata with strong-fairness acceptance condition. In Proc. 24th ACM Symp. on Theory of Computing, Victoria, 1992. Google Scholar
  30. S. Schewe. Tighter bounds for the determinisation of büchi automata. In Found. of Soft. Sci. and Comp. Struc. 12th Inter. Conf. FOSSACS, pages 167-181, 2009. Google Scholar
  31. A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217-237, 1987. Google Scholar
  32. W. Thomas. Complementation of büchi automata revised. Jewels are Forever, pages 109-120, 1999. Google Scholar
  33. M.-H. Tsai, S. Fogarty, M.Y. Vardi, and Y.-K. Tsay. State of büchi complementation. In 15th Int. Conf. on Impl. and Appl. of Aut., volume 6482, pages 261-271, 2010. Google Scholar
  34. M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In n Proc. 26th IEEE Symp. on Foundations of Computer Science, pages 327-338, 1985. Google Scholar
  35. M.Y. Vardi. The büchi complementation saga. In In Proc. 24th Symp. on Theoretical Aspects of Computer Science, pages 12-22, 2007. Google Scholar
  36. Q. Yan. Lower bounds for complementation of ω-automata via the full automata technique. In Proc. 33rd ICALP, volume 4052 of LNCS, pages 589-600. Springer, 2006. 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