Abstract
In this paper, Nondeterministic Büchi Automata (NBA) are equivalently transformed as a new kind of deterministic omega automata, Deterministic Partitioned Automata (DPA). Different from the existing automata, at most three different transitions may occur between two states of a DPA. This leads to a determinization construction of NBA with smaller state complexity but larger transition complexity. Compared with the existing determinization constructions of NBA, the new one is intuitive and easily implementable since it is completely based on subset construction. In addition, we have proved that both nondeterministic and deterministic partitioned automata share the same expressive power with NBA.
This research is supported by the NSFC Grant No. 61003078, 61133001, and 61272117, 973 Program Grant No. 2010CB328102 and ISN Lab Grant No. ISN1102001.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clark, M., Gremberg, O., Peled, A.: Model Checking. The MIT Press (2000)
Katoen, J.-P.: Concepts, Algorithms and Tools for Model Checking. Arbeitsberichte der Informatik, Friedrich-Alexander-Universitaet Erlangen-Nuernberg 32(1) (1999)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pp. 1–12. Stanford University Press (1962)
Thomas, W.: Languages, automata and logic. In: Handbook of Formal Languages, vol. 3, pp. 389–455. Springer, Berlin (1997)
Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Jain, H.: Automata on Infinite Objects. B.Tech Seminar Report, India, internal report (1996)
Vardi, M.Y.: The Büchi Complementation Saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12–22. Springer, Heidelberg (2007)
Safra, S.: On the complexity of omega-automata. In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science, FOCS 1988, pp. 319–327. IEEE Computer Society Press (1988)
Muller, D.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)
Boker, U., Kupferman, O.: Co-ing Büchi Made Tight and Useful. In: LICS 2009, pp. 245–254 (2009)
Boker, U., Kupferman, O.: The Quest for a Tight Translation of Büchi to co-Büchi Automata. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 147–164. Springer, Heidelberg (2010)
Boker, U., Kupferman, O.: Co-Büching Them All. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 184–198. Springer, Heidelberg (2011)
Friedgut, E., Kupderman, O., Vardi, M.Y.: Büchi complementation made tighter. International Journal of Foundations of Computer Science 17(4), 851–863 (2006)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)
Muller, D.E.: Infinite sequences and finite machines. In: Proceedings of the 4th IEEE Symposioum on Switching Circuit Theory and Logical Design, pp. 3–16 (1963)
McNaughton: Testing and generating infinite sequences by a finite automaton. Information and Control 9(5), 521–530 (1966)
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)
Schewe, S.: Büchi Complementation Made Tight. In: STACS 2009, pp. 661–672 (2009)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Journal of Logical Methods in Computer Science 3 (2007)
Liu, W., Wang, J.: A tighter analysis of Piterman’s Büchi determinization. Inf. Process. Lett. 109(16), 941–945 (2009)
Schewe, S.: Tighter Bounds for the Determinisation of Büchi Automata. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 167–181. Springer, Heidelberg (2009)
Colcombet, T., Zdanowski, K.: A Tight Lower Bound for Determinization of Transition Labeled Büchi Automata. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 151–162. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tian, C., Duan, Z., Yang, M. (2013). Deternimization of Büchi Automata as Partitioned Automata. In: Du, DZ., Zhang, G. (eds) Computing and Combinatorics. COCOON 2013. Lecture Notes in Computer Science, vol 7936. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38768-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-38768-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38767-8
Online ISBN: 978-3-642-38768-5
eBook Packages: Computer ScienceComputer Science (R0)