Abstract
We present a uniform framework for (1) complementing Büchi automata, (2) turning Büchi automata into equivalent unambiguous Büchi automata, and (3) turning Büchi automata into equivalent deterministic automata. We present the first solution to (2) which does not make use of McNaughton’s theorem (determinization) and an intuitive and conceptually simple solution to (3).
Our results are based on Muller and Schupp’s procedure for turning alternating tree automata into non-deterministic ones.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Schulte-Althoff, C., Thomas, W., Wallmeier, N.: Observations on determinization of Büchi automata. Theor. Comput. Sci. 363(2), 224–233 (2006)
Arnold, A.: Rational omega-languages are non-ambiguous. Theor. Comput. Sci. 26, 221–223 (1983)
Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Logic, Methodology, and Philosophy of Science: Proc. of the 1960 International Congress, pp. 1–11. Stanford University Press, Stanford (1962)
Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Information and Control 61(3), 175–201 (1984)
Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851–868 (2006)
Gurevich, Y., Harrington, L.: Trees, automata, and games. In: 14th ACM Symposium on the Theory of Computing, San Francisco, Calif, pp. 60–65. ACM, New York (1982)
Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic Büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)
Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, pp. 358–367. IEEE, Los Alamitos (1991)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Logic 2(3), 408–429 (2001)
Kähler, D.: Determinisierung von ω-Automaten. Diploma thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel (2001)
McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9, 521–530 (1966)
Michel, M.: Complementation is more difficult with automata on infinite words (unpublished notes) (1988)
Muller, D.E.: Infinite sequences and finite machines. In: Proceedings of the 4th Annual IEEE Symposium on Switching Circuit Theory and Logical Design, pp. 3–16 (1963)
Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. Theor. Comput. Sci. 141(1&2), 69–107 (1995)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic Parity automata. In: 21th IEEE Symposium on Logic in Computer Science, Seattle, WA, USA, Proceedings, pp. 255–264. IEEE, Los Alamitos (2006)
Ozer Rabin, M.: Decidability of second-order theories and finite automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)
Safra, S.: On the complexity of ω-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, pp. 319–327. IEEE, Los Alamitos (1988)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with appplications to temporal logic. Theor. Comput. Sci. 49, 217–237 (1987)
Thomas, W.: Complementation of Büchi automata revised. In: Karhumäki, J., Maurer, H.A., Paun, G., Rozenberg, G. (eds.) Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pp. 109–120. Springer, Heidelberg (1999)
Vardi, M.Y., Wilke, Th.: Automata: from logics to algorithms. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives. Texts in Logic and Games, vol. 2, pp. 629–736. Amsterdam University Press, Amsterdam (2007)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37
Yan, Q.: Lower bounds for complementation of ω-automata via the full automata technique. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 589–600. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kähler, D., Wilke, T. (2008). Complementation, Disambiguation, and Determinization of Büchi Automata Unified. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds) Automata, Languages and Programming. ICALP 2008. Lecture Notes in Computer Science, vol 5125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70575-8_59
Download citation
DOI: https://doi.org/10.1007/978-3-540-70575-8_59
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70574-1
Online ISBN: 978-3-540-70575-8
eBook Packages: Computer ScienceComputer Science (R0)