Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Towards a Grand Unification of Büchi Complementation Constructions

  • Chapter
  • First Online:
Principles of Systems Design

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13660))

  • 833 Accesses

Abstract

The complementation construction for nondeterministic word automata has numerous applications in formal verification. In particular, the language-containment problem, to which many verification problems are reduced, involves complementation. For automata on finite words, which correspond to safety properties, complementation is typically done by determinization using the subset construction. For Büchi automata on infinite words, which are required for the modeling of liveness properties, optimal complementation constructions are quite complicated, as the subset construction is not sufficient. Over the years, three different constructions have been developed for Büchi complementation, based on congruence relations (via Ramsey analysis), progress ranks, and profiles. In this work we unify the three constructions, by showing how profiles can also yield both optimal congruence relations and progress ranks.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Abdulla, P.A., et al.: Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 132–147. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_14

    Chapter  Google Scholar 

  2. Abdulla, P.A., et al.: Advanced Ramsey-based Büchi automata inclusion testing. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 187–202. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23217-6_13

    Chapter  Google Scholar 

  3. Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for Büchi automata. In: Dawar, A., Grädel, E. (ed.) LICS, pp. 46–55. ACM (2018)

    Google Scholar 

  4. Angluin, D., Fisman, D.: Learning regular omega languages. Theor. Comput. Sci. 650, 57–72 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  5. Breuers, S., Löding, C., Olschewski, J.: Improved Ramsey-based Büchi complementation. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 150–164. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28729-9_10

    Chapter  Google Scholar 

  6. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of International Congress on Logic, Method, and Philosophy of Science, pp. 1–12. Stanford University Press (1962)

    Google Scholar 

  7. Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational \(\omega \)-languages. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 554–566. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58027-1_27

    Chapter  MATH  Google Scholar 

  8. Chen, Y.-F., Havlena, V., Lengál, O.: Simulations in rank-based Büchi automata complementation. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 447–467. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-34175-6_23

    Chapter  Google Scholar 

  9. Allen Emerson, E., Lei, C.-L.: Temporal reasoning under generalized fairness constraints. In: Monien, B., Vidal-Naquet, G. (eds.) STACS 1986. LNCS, vol. 210, pp. 21–36. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-16078-7_62

    Chapter  Google Scholar 

  10. Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 420–434. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_29

    Chapter  Google Scholar 

  11. Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile trees for Büchi word automata, with application to determinization. Inf. Comput. 245, 136–151 (2015)

    Article  MATH  Google Scholar 

  12. Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.Y.: Unifying Büchi complementation constructions. Log. Methods Comput. Sci. 9(1), 1–26 (2013)

    Google Scholar 

  13. 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). https://doi.org/10.1007/978-3-642-12002-2_17

    Chapter  Google Scholar 

  14. Fogarty, S., Vardi, M.Y.: Büchi complementation and size-change termination. Log. Methods Comput. Sci. 8(1), 1–33 (2012)

    Google Scholar 

  15. Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851–868 (2006)

    Article  MATH  Google Scholar 

  16. 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). https://doi.org/10.1007/978-3-540-39724-3_10

    Chapter  Google Scholar 

  17. Havlena, V., Lengál, O.: Reducing (to) the ranks: efficient rank-based Büchi automata complementation (technical report). CoRR, abs/2010.07834 (2020)

    Google Scholar 

  18. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation, 2nd edn. Addison-Wesley, Reading (2000)

    MATH  Google Scholar 

  19. 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. LNCS, vol. 5125, pp. 724–735. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70575-8_59

    Chapter  MATH  Google Scholar 

  20. Karmarkar, H., Chakraborty, S.: On minimal odd rankings for Büchi complementation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 228–243. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04761-9_18

    Chapter  MATH  Google Scholar 

  21. Klarlund, N.: Progress measures for complementation of omega-automata with applications to temporal logic. In: FOCS, pp. 358–367. IEEE Computer Society (1991)

    Google Scholar 

  22. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001)

    Article  MATH  Google Scholar 

  23. Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Log. 2(3), 408–429 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  24. Li, Y., Tsay, Y.-K., Turrini, A., Vardi, M.Y., Zhang, L.: Congruence relations for Büchi automata. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 465–482. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_25

    Chapter  Google Scholar 

  25. Löding, C., Pirogov, A.: Determinization of Büchi automata: unifying the approaches of Safra and Muller-Schupp. In: Baier, C., Chatzigiannakis, I., Flocchini, P., Leonardi, S. (eds.) ICALP. LIPIcs, vol. 132, pp. 120:1–120:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

    Google Scholar 

  26. Maler, O., Staiger, L.: On syntactic congruences for omega-languages. Theor. Comput. Sci. 183(1), 93–112 (1997)

    Article  MATH  Google Scholar 

  27. Michel, M.: Complementation is more difficult with automata on infinite words. Technical report, CNET, Paris (Manuscript) (1988)

    Google Scholar 

  28. Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321–330 (1984)

    Article  MATH  Google Scholar 

  29. 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)

    Article  MathSciNet  MATH  Google Scholar 

  30. Myhill, J.: Finite automata and the representation of events. Technical report, WADD TR-57-624, pp. 112–137 (1957)

    Google Scholar 

  31. Nerode, A.: Linear automaton transformations. Am. Math. Soc. 9, 541–544 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  32. Safra, S.: On the complexity of \(\omega \)-automata. In: FOCS, pp. 319–327. IEEE (1988)

    Google Scholar 

  33. Schewe, S.: Büchi complementation made tight. In: STACS. LIPIcs, vol. 3, pp. 661–672. Schloss Dagstuhl, Germany (2009)

    Google Scholar 

  34. Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theor. Comput. Sci. 49(2–3), 217–237 (1987)

    Article  MATH  Google Scholar 

  35. Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133–191. Elsevier and MIT Press (1990)

    Google Scholar 

  36. Tsai, M.-H., Fogarty, S., Vardi, M.Y., Tsay, Y.-K.: State of Büchi complementation. Log. Methods Comput. Sci. 10(4), 1–27 (2014)

    Google Scholar 

  37. Vardi, M.Y.: Expected properties of set partitions. Technical report, The Weizmann Institute of Science (1980)

    Google Scholar 

  38. Vardi, M.Y.: Verification of concurrent programs: the automata-theoretic framework. Ann. Pure Appl. Log. 51(1–2), 79–98 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  39. 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). https://doi.org/10.1007/978-3-540-70918-3_2

    Chapter  Google Scholar 

  40. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332–344. IEEE (1986)

    Google Scholar 

  41. Yan, Q.: Lower bounds for complementation of \(\omega \)-automata via the full automata technique. Log. Methods Comput. Sci. 4(1:5), 1–20 (2008)

    Google Scholar 

Download references

Acknowledgements

We thank the anonymous reviewers for their valuable suggestions to this paper. This work is supported in part by the National Natural Science Foundation of China (Grant Nos. 62102407 and 61836005), CAS grant QYZDB-SSW-SYS019, NSF grants IIS-1527668, CCF-1704883, IIS-1830549, CNS-2016656, DoD MURI grant N00014-20-1-2787, and an award from the Maryland Procurement Office.

Author information

Authors and Affiliations

  1. Department of Computer Science, Rice University, Houston, USA

    Moshe Y. Vardi

  2. Department of Computer Science, Trinity University, San Antonio, USA

    Seth Fogarty

  3. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Yong Li

  4. National Taiwan University, Taipei, Taiwan

    Yih-Kuen Tsay

Authors
  1. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Seth Fogarty
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yong Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yih-Kuen Tsay
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yong Li .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Jean-François Raskin

  2. Institute of Science and Technology Austria, Klosterneuburg, Austria

    Krishnendu Chatterjee

  3. École Normale Supérieure Paris-Saclay, Gif-sur-Yvette, France

    Laurent Doyen

  4. MPI for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Vardi, M.Y., Fogarty, S., Li, Y., Tsay, YK. (2022). Towards a Grand Unification of Büchi Complementation Constructions. In: Raskin, JF., Chatterjee, K., Doyen, L., Majumdar, R. (eds) Principles of Systems Design. Lecture Notes in Computer Science, vol 13660. Springer, Cham. https://doi.org/10.1007/978-3-031-22337-2_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-22337-2_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-22336-5

  • Online ISBN: 978-3-031-22337-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation