Abstract
We consider complementing Büchi automata by applying the Ramsey-based approach, which is the original approach already used by Büchi and later improved by Sistla et al. We present several heuristics to reduce the state space of the resulting complement automaton and provide experimental data that shows that our improved construction can compete (in terms of finished complementation tasks) also in practice with alternative constructions like rank-based complementation. Furthermore, we show how our techniques can be used to improve the Ramsey-based complementation such that the asymptotic upper bound for the resulting complement automaton is \(2^{{\mathcal O}(n {\rm log} n)}\) instead of \(2^{{\mathcal O}(n^2)}\).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., Chen, Y.-F., Clemente, L., Holík, L., Hong, C.-D., Mayr, R., Vojnar, T.: Advanced Ramsey-based Büchi Automata Inclusion Testing. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011 – Concurrency Theory. LNCS, vol. 6901, pp. 187–202. Springer, Heidelberg (2011)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford Univerity Press (1962)
Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Unifying Büchi complementation constructions. In: CSL (2011)
Fogarty, S., Vardi, M.Y.: Efficient Büchi Universality Checking. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 205–220. Springer, Heidelberg (2010)
Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. International Journal of Foundations of Computer Science 17(4), 851–868 (2006)
Kähler, D., Wilke, T.: 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.) ICALP 2008, Part I. LNCS, vol. 5125, pp. 724–735. Springer, Heidelberg (2008)
Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: FOCS, pp. 358–367. IEEE Computer Society (1991)
Michel, M.: Complementation is more difficult with automata on infinite words. Technical report, CNET, Paris (1988)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3) (2007)
Ramsey, F.P.: On a problem of formal logic. Proceedings of the London Mathematical Society 2(1), 264 (1930)
Safra, S.: On the complexity of ω-automata. In: FOCS, pp. 319–327. IEEE (1988)
Schewe, S.: Büchi complementation made tight. In: STACS. LIPIcs, vol. 3, pp. 661–672. Schloss Dagstuhl (2009)
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)
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, pp. 133–192. Elsevier Science Publishers, Amsterdam (1990)
Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of Büchi Complementation. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol. 6482, pp. 261–271. Springer, Heidelberg (2011)
Yan, Q.: Lower bounds for complementation of ω-automata via the full automata technique. Logical Methods in Computer Science 4(1) (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Breuers, S., Löding, C., Olschewski, J. (2012). Improved Ramsey-Based Büchi Complementation. In: Birkedal, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2012. Lecture Notes in Computer Science, vol 7213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28729-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-28729-9_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28728-2
Online ISBN: 978-3-642-28729-9
eBook Packages: Computer ScienceComputer Science (R0)