Skip to main content
SpringerLink
Log in

New Optimizations and Heuristics for Determinization of Büchi Automata

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

A. Pirogov—This work is supported by the German research council (DFG) Research Training Group 2236 UnRAVeL.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Notes

  1. 1.

    Our prototype can be obtained at https://github.com/apirogov/nbautils.

References

  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_22

    Chapter  MATH  Google Scholar 

  2. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  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_50

    Chapter  Google Scholar 

  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. Carton, O., Maceiras, R.: Computing the Rabin index of a parity automaton. RAIRO-Theoret. Inform. Appl. 33(6), 495–505 (1999)

    Article  MathSciNet  Google Scholar 

  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_13

    Chapter  MATH  Google Scholar 

  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_31

    Chapter  Google Scholar 

  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_8

    Chapter  Google Scholar 

  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_25

    Chapter  Google Scholar 

  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_13

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  12. Fisman, D., Lustig, Y.: A modular approach for Büchi determinization. In: CONCUR 2015. LIPIcs (2015)

    Google Scholar 

  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)

    Article  Google Scholar 

  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_6

    Chapter  Google Scholar 

  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_4

    Chapter  MATH  Google Scholar 

  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. Jacobs, S., et al.: The 4th reactive synthesis competition (syntcomp 2017): benchmarks, participants & results. arXiv preprint arXiv:1711.11439 (2017)

  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_59

    Chapter  MATH  Google Scholar 

  19. Klein, J.: Linear time logic and deterministic omega-automata. Diploma thesis, University of Bonn (2005)

    Google Scholar 

  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_7

    Chapter  MATH  Google Scholar 

  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_30

    Chapter  Google Scholar 

  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_6

    Chapter  Google Scholar 

  23. Kupferman, O., Vardi, M.Y.: From linear time to branching time. TOCL 6, 273–294 (2005)

    Article  MathSciNet  Google Scholar 

  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. McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Inf. Control 9(5), 521–530 (1966)

    Article  MathSciNet  Google Scholar 

  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_31

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  29. Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: GandALF 2017

    Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  31. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: LICS 2006. IEEE (2006)

    Google Scholar 

  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. Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae 119(3–4), 393–406 (2012)

    MathSciNet  MATH  Google Scholar 

  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. 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_13

    Chapter  MATH  Google Scholar 

  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_33

    Chapter  Google Scholar 

  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. 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_7

    Chapter  Google Scholar 

  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_35

    Chapter  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. RWTH Aachen University, Templergraben 55, 52062, Aachen, Germany

    Christof Löding & Anton Pirogov

Authors
  1. Christof Löding
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anton Pirogov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Christof Löding or Anton Pirogov .

Editor information

Editors and Affiliations

  1. Institute of Information Science, Academia Sinica, Taipei, Taiwan

    Yu-Fang Chen

  2. DENSO AUTOMOTIVE Deutschland GmbH, Eching, Germany

    Chih-Hong Cheng

  3. Institute of Computer Science, TU München, Munich, Germany

    Javier Esparza

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Löding, C., Pirogov, A. (2019). New Optimizations and Heuristics for Determinization of Büchi Automata. In: Chen, YF., Cheng, CH., Esparza, J. (eds) Automated Technology for Verification and Analysis. ATVA 2019. Lecture Notes in Computer Science(), vol 11781. Springer, Cham. https://doi.org/10.1007/978-3-030-31784-3_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31784-3_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31783-6

  • Online ISBN: 978-3-030-31784-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation