Advertisement

From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata

  • Simon Jantsch
  • David MüllerEmail author
  • Christel Baier
  • Joachim Klein
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool Duggi and discuss experimental results that compare the automata sizes and computation times of Duggi with the tableau-based LTL-to-UBA translation of the SPOT tool set. Our experiments also cover the analysis of Markov chains under LTL specifications, which is an important application of UBA.

References

  1. 1.
    Arnold, A.: Deterministic and non ambiguous rational \(\omega \)-languages. In: Nivat, M., Perrin, D. (eds.) LITP 1984. LNCS, vol. 192, pp. 18–27. Springer, Heidelberg (1985).  https://doi.org/10.1007/3-540-15641-0_20CrossRefGoogle Scholar
  2. 2.
    Babiak, T., et al.: The Hanoi omega-automata format. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 479–486. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_31CrossRefGoogle Scholar
  3. 3.
    Babiak, T., Křetínský, M., Řehák, V., Strejček, J.: LTL to Büchi automata translation: fast and more deterministic. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95–109. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_8CrossRefzbMATHGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  5. 5.
    Baier, C., Kiefer, S., Klein, J., Klüppelholz, S., Müller, D., Worrell, J.: Markov chains and unambiguous Büchi automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 23–42. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41528-4_2CrossRefGoogle Scholar
  6. 6.
    Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 32–46. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_3CrossRefzbMATHGoogle Scholar
  7. 7.
    Bousquet, N., Löding, C.: Equivalence and inclusion problem for strongly unambiguous Büchi automata. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 118–129. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13089-2_10CrossRefzbMATHGoogle Scholar
  8. 8.
    Carton, O., Michel, M.: Unambiguous Büchi automata. Theor. Comput. Sci. 297(1–3), 37–81 (2003)CrossRefGoogle Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)CrossRefGoogle Scholar
  10. 10.
    Colcombet, T.: Unambiguity in automata theory. In: Shallit, J., Okhotin, A. (eds.) DCFS 2015. LNCS, vol. 9118, pp. 3–18. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-19225-3_1CrossRefGoogle Scholar
  11. 11.
    Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48119-2_16CrossRefGoogle Scholar
  12. 12.
    Couvreur, J.-M., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 361–375. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-39813-4_26CrossRefGoogle Scholar
  13. 13.
    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
  14. 14.
    Duret-Lutz, A.: Contributions to LTL and \(\omega \)-automata for model checking. Habilitation thesis, Université Pierre et Marie Curie (Paris 6), February 2017Google Scholar
  15. 15.
    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
  16. 16.
    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
  17. 17.
    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
  18. 18.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiński, P., Średniawa, M. (eds.) Protocol Specification, Testing and Verification XV, PSTV 1995. IFIP Advances in Information and Communication Technology, vol. 38, pp. 3–18. Springer, Boston (1996).  https://doi.org/10.1007/978-0-387-34892-6_1CrossRefGoogle Scholar
  19. 19.
    Grädel, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-36387-4CrossRefzbMATHGoogle Scholar
  20. 20.
    Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: 26th International Conference on Concurrency Theory (CONCUR 2015), Leibniz International Proceedings in Informatics (LIPIcs), vol. 42, pp. 354–367. SchlossDagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl (2015)Google Scholar
  21. 21.
    Haverkort, B.R., Hermanns, H., Katoen, J.P.: On the use of model checking techniques for dependability evaluation. In: 19th IEEE Symposium on Reliable Distributed Systems (SRDS), pp. 228–237. IEEE Computer Society (2000)Google Scholar
  22. 22.
    Isaak, D., Löding, C.: Efficient inclusion testing for simple classes of unambiguous \(\omega \)-automata. Inf. Process. Lett. 112(14–15), 578–582 (2012)Google Scholar
  23. 23.
    Jantsch, S., Müller, D., Baier, C., Klein, J.: From LTL to unambiguous Büchi automata via disambiguation of alternating automata. Technical report, Technische Universität Dresden (2019). https://arxiv.org/abs/1907.02887/
  24. 24.
    Karmarkar, H., Joglekar, M., Chakraborty, S.: Improved upper and lower bounds for Büchi disambiguation. In: Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 40–54 (2013)Google Scholar
  25. 25.
    Kretínský, J., Meggendorfer, T., Sickert, S.: LTL store: repository of LTL formulae from literature and case studies. CoRR abs/1807.03296 (2018). http://arxiv.org/abs/1807.03296
  26. 26.
    Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of the 9th International Conference on Quantitative Evaluation of SysTems (QEST), pp. 203–204. IEEE Computer Society (2012)Google Scholar
  27. 27.
    Löding, C.: Efficient minimization of deterministic weak \(\omega \)-automata. Inf. Process. Lett. 79(3), 105–109 (2001)Google Scholar
  28. 28.
    Loding, C., Thomas, W.: Alternating automata and logics over infinite words. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44929-9_36CrossRefGoogle Scholar
  29. 29.
    Mohri, M.: On the disambiguation of finite automata and functional transducers. Int. J. Found. Comput. Sci. 24(6), 847–862 (2013)MathSciNetCrossRefGoogle Scholar
  30. 30.
    Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF). Electronic Proceedings in Theoretical Computer Science, vol. 256, pp. 180–194. Open Publishing Association (2017)Google Scholar
  31. 31.
    Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS), pp. 422–427 (1988)Google Scholar
  32. 32.
    Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theor. Comput. Sci. 54, 267–276 (1987)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000).  https://doi.org/10.1007/10722167_21CrossRefGoogle Scholar
  34. 34.
    Stearns, R.E., Hunt, H.B.: On the equivalence and containment problem for unambiguous regular expressions, grammars, and automata. SIAM J. Comput. 14, 598–611 (1985)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the 26th IEEE Symposium on Foundations of Computer Science (FOCS), pp. 327–338. IEEE Computer Society (1985)Google Scholar
  36. 36.
    Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-57887-0_116CrossRefGoogle Scholar
  37. 37.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the 1st Symposium on Logic in Computer Science (LICS), pp. 332–344. IEEE Computer Society Press (1986)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Technische Universität DresdenDresdenGermany

Personalised recommendations