A Modular Approach for Büchi Determinization
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.
Büchi automata
Determinization
Verification
Games
Synthesis
368-382
Regular Paper
Dana
Fisman
Dana Fisman
Yoad
Lustig
Yoad Lustig
10.4230/LIPIcs.CONCUR.2015.368
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.
J.R. Büchi. Weak second-order arithmetic and finite automata. Zeit. Math. Logik und Grundl. Math., 6:66-92, 1960.
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.
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857-907, 1995.
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.
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.
S. Fogarty, O. Kupferman, T. Wilke, and M.Y. Vardi. Unifying büchi complementation constructions. ogical Methods in Computer Science, 9, 2013.
E. Friedgut, O. Kupferman, and M.Y. Vardi. Büchi complementation made tighter. Int. J. Found. Comput. Sci., 17:851-868, 2004.
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.
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.
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.
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.
D. Kozen. Theory of Computation. Texts in Computer Science. Springer, 2006.
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.
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.
O. Kupferman and M.Y. Vardi. Synthesizing distributed systems. In In Proc. 16th IEEE Symp. on Logic in Computer Science, pages 389-398, 2001.
O. Kupferman and M.Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273-294, 2005.
L.H. Landweber. Decision problems for ω-automata. Mathematical Systems Theory, 3:376-384, 1969.
W. Liu and J. Wang. A tighter analysis of piterman’s büchi determinization. Inf. Process. Lett., 109(16):941-945, 2009.
R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521-530, 1966.
M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 1988.
S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321-330, 1984.
D.E. Muller and P.E. Schupp. Simulating alternating tree automata by nondeterministic automata. TCS, 141:69-107, 1995.
Jean-Pierre Pécuchet. On the complementation of büchi automata. Theoretical Computer Science, 47:95-98, 1986.
N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. In Proc. 21st IEEE Symp. on Logic in Computer Science, 2006.
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.
M.O. Rabin. Decidability of second order theories and automata on infinite trees. Transaction of the AMS, 141:1-35, 1969.
S. Safra. On the complexity of ω-automata. In In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319-327, 1988.
S. Safra. Exponential determinization for ω-automata with strong-fairness acceptance condition. In Proc. 24th ACM Symp. on Theory of Computing, Victoria, 1992.
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.
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.
W. Thomas. Complementation of büchi automata revised. Jewels are Forever, pages 109-120, 1999.
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.
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.
M.Y. Vardi. The büchi complementation saga. In In Proc. 24th Symp. on Theoretical Aspects of Computer Science, pages 12-22, 2007.
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.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode