Advertisement

New Optimizations and Heuristics for Determinization of Büchi Automata

  • Christof LödingEmail author
  • Anton PirogovEmail author
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11781)

Abstract

In this work, we present multiple new optimizations and heuristics for the determinization of Büchi automata that exploit a number of semantic and structural properties, most of which may be applied together with any determinization procedure. We built a prototype implementation where all the presented heuristics can be freely combined and evaluated them, comparing our implementation with the state-of-the-art tool spot on multiple data sets with different characteristics. Our results show that the proposed optimizations and heuristics can in some cases significantly decrease the size of the resulting deterministic automaton.

Keywords

Büchi Parity Automata Determinization Heuristics 
This is a preview of subscription content, log in to check access.

References

  1. 1.
    Althoff, C.S., Thomas, W., Wallmeier, N.: Observations on determinization of Büchi automata. In: Farré, J., Litovsky, I., Schmitz, S. (eds.) CIAA 2005. LNCS, vol. 3845, pp. 262–272. Springer, Heidelberg (2006).  https://doi.org/10.1007/11605157_22CrossRefzbMATHGoogle Scholar
  2. 2.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  3. 3.
    Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 611–625. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45744-5_50CrossRefGoogle Scholar
  4. 4.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Studies in Logic and the Foundations of Mathematics, vol. 44, pp. 1–11. Elsevier (1966)Google Scholar
  5. 5.
    Carton, O., Maceiras, R.: Computing the Rabin index of a parity automaton. RAIRO-Theoret. Inform. Appl. 33(6), 495–505 (1999)MathSciNetCrossRefGoogle Scholar
  6. 6.
    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. LNCS, vol. 5556, pp. 151–162. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02930-1_13CrossRefzbMATHGoogle Scholar
  7. 7.
    Duret-Lutz, A.: Manipulating LTL formulas using spot 1.0. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 442–445. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-02444-8_31CrossRefGoogle Scholar
  8. 8.
    Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46520-3_8CrossRefGoogle Scholar
  9. 9.
    Esparza, J., Křetínský, J., Raskin, J.-F., Sickert, S.: From LTL and limit-deterministic Büchi automata to deterministic parity automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 426–442. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54577-5_25CrossRefGoogle Scholar
  10. 10.
    Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–168. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44618-4_13CrossRefGoogle Scholar
  11. 11.
    Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Fisman, D., Lustig, Y.: A modular approach for Büchi determinization. In: CONCUR 2015. LIPIcs (2015)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44585-4_6CrossRefGoogle Scholar
  15. 15.
    Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 53–70. Springer, Heidelberg (2006).  https://doi.org/10.1007/11691617_4CrossRefzbMATHGoogle Scholar
  16. 16.
    Hopcroft, J.: An n log n algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations, pp. 189–196. Elsevier (1971)Google Scholar
  17. 17.
    Jacobs, S., et al.: The 4th reactive synthesis competition (syntcomp 2017): benchmarks, participants & results. arXiv preprint arXiv:1711.11439 (2017)
  18. 18.
    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_59CrossRefzbMATHGoogle Scholar
  19. 19.
    Klein, J.: Linear time logic and deterministic omega-automata. Diploma thesis, University of Bonn (2005)Google Scholar
  20. 20.
    Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic \(\omega \)-automata. In: Holub, J., Žd’árek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 51–61. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-76336-9_7CrossRefzbMATHGoogle Scholar
  21. 21.
    Křetínský, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: from LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 567–577. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_30CrossRefGoogle Scholar
  22. 22.
    Kupferman, O., Rosenberg, A.: The blow-up in translating LTL to deterministic automata. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt 2010. LNCS (LNAI), vol. 6572, pp. 85–94. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-20674-0_6CrossRefGoogle Scholar
  23. 23.
    Kupferman, O., Vardi, M.Y.: From linear time to branching time. TOCL 6, 273–294 (2005)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Löding, C., Pirogov, A.: Determinization of Büchi automata: unifying the approaches of Safra and Muller-Schupp. ICALP 2019 https://arxiv.org/abs/1902.02139
  25. 25.
    McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9(5), 521–530 (1966)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back!. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578–586. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_31CrossRefGoogle Scholar
  27. 27.
    Michel, M.: Complementation is more difficult with automata on infinite words. Manuscript, CNET, Paris (1988)Google Scholar
  28. 28.
    Miyano, S., Hayashi, T.: Alternating finite automata on \(\omega \)-words. Theoret. Comput. Sci. 32(3), 321–330 (1984)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: GandALF 2017Google Scholar
  30. 30.
    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. Theoret. Comput. Sci. 141(1–2), 69–107 (1995)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: LICS 2006. IEEE (2006)Google Scholar
  32. 32.
    Pnueli, A.: The temporal logic of programs. In: 1977 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)Google Scholar
  33. 33.
    Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae 119(3–4), 393–406 (2012)MathSciNetzbMATHGoogle Scholar
  34. 34.
    Safra, S.: On the complexity of omega-automata. In: 1988 29th Annual Symposium on Foundations of Computer Science, pp. 319–327. IEEE (1988)Google Scholar
  35. 35.
    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).  https://doi.org/10.1007/978-3-642-00596-1_13CrossRefzbMATHGoogle Scholar
  36. 36.
    Tabakov, D., Vardi, M.Y.: Optimized temporal monitors for systemC. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 436–451. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16612-9_33CrossRefGoogle Scholar
  37. 37.
    Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B, pp. 133–192. Elsevier Science Publishers, Amsterdam (1990)Google Scholar
  38. 38.
    Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 389–455. Springer, Heidelberg (1997).  https://doi.org/10.1007/978-3-642-59126-6_7CrossRefGoogle Scholar
  39. 39.
    Thomas, W.: Church’s problem and a tour through automata theory. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 635–655. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78127-1_35CrossRefGoogle Scholar
  40. 40.
    Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Logic and Automata - History and Perspectives, Texts in Logic and Games, vol. 2, pp. 629–724. Amsterdam University Press (2007)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.RWTH Aachen UniversityAachenGermany

Personalised recommendations

Cite paper

Buy options