Advertisement

Owl: A Library for \(\omega \)-Words, Automata, and LTL

  • Jan KřetínskýEmail author
  • Tobias Meggendorfer
  • Salomon Sickert
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

We present the library Owl (Omega-Words, automata, and LTL) for \(\omega \)-automata and linear temporal logic. It forms a backbone of several translations from LTL to automata and related tools by different authors. We describe the functionality of the library and the recent experience, which has already shown the library is apt for easy prototyping of new tools in this area.

References

  1. 1.
    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
  2. 2.
    Babiak, T., Blahoudek, F., Křetínský, M., Strejček, J.: Effective translation of LTL to deterministic Rabin automata: beyond the (F,G)-fragment. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 24–39. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-02444-8_4CrossRefGoogle 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.: Principles of Model Checking. MIT Press, Cambridge (2008)Google Scholar
  5. 5.
    Blahoudek, F., Duret-Lutz, A., Klokočka, M., Křetínský, M., Strejček, J.: Seminator: a tool for semi-determinization of omega-automata. In: LPAR (2017)Google Scholar
  6. 6.
    Chatterjee, K., Gaiser, A., Křetínský, J.: Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559–575. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_37CrossRefGoogle Scholar
  7. 7.
    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
  8. 8.
    Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48683-6_23CrossRefGoogle Scholar
  9. 9.
    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
  10. 10.
    Emerson, E.A., Lei, C.: Modalities for model checking: branching time strikes back. In: POPL (1985)Google Scholar
  11. 11.
    Esparza, J., Křetínský, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192–208. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08867-9_13CrossRefGoogle Scholar
  12. 12.
    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
  13. 13.
    Esparza, J., Křetínský, J., Sickert, S.: From LTL to deterministic automata - a safraless compositional approach. Form. Methods Syst. Des. (2016)Google Scholar
  14. 14.
    Esparza, J., Křetínský, J., Sickert, S.: One theorem to rule them all: a unified translation of LTL into \(\omega \)-automata. In: LICS (2018)Google Scholar
  15. 15.
    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
  16. 16.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: CAV (2001). Tool accessible at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/
  17. 17.
    Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-36135-9_20CrossRefGoogle Scholar
  18. 18.
    Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Fifth Workshop on Synthesis (SYNT\(@\)CAV) (2016)Google Scholar
  19. 19.
    Kini, D., Viswanathan, M.: Limit deterministic and probabilistic automata for LTL \(\setminus \) GU. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 628–642. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_57Google Scholar
  20. 20.
    Kini, D., Viswanathan, M.: Optimal translation of LTL to limit deterministic automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 113–129. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54580-5_7CrossRefGoogle Scholar
  21. 21.
    Klein, J.: ltl2dstar - LTL to deterministic Streett and Rabin automata. http://www.ltl2dstar.de/
  22. 22.
    Komárková, Z., Křetínský, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 235–241. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_17CrossRefGoogle Scholar
  23. 23.
    Křetínský, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7–22. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_7CrossRefGoogle Scholar
  24. 24.
    Křetínský, J., Meggendorfer, T., Sickert, S.: Owl: a library for \(\omega \)-words, automata, and LTL. https://owl.model.in.tum.de. Accessed July 2018
  25. 25.
    Křetínský, J., Meggendorfer, T., Sickert, S.: LTL store: repository of LTL formulae from literature and case studies. CoRR, abs/1807.03296 (2018)Google Scholar
  26. 26.
    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
  27. 27.
    Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 88–98. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27660-6_8CrossRefGoogle Scholar
  28. 28.
    Křetínský, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7–22. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_7CrossRefGoogle Scholar
  29. 29.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  30. 30.
    Meggendorfer, T.: JBDD: a java BDD library. https://github.com/incaseoftrouble/jbdd. Accessed July 2018
  31. 31.
    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
  32. 32.
    Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Gandalf (2017)Google Scholar
  33. 33.
    Pnueli, A.: The temporal logic of programs. In: FOCS (1977)Google Scholar
  34. 34.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL (1989)Google Scholar
  35. 35.
    Rodger, S.H., Qin, H., Su, J.: Changes to JFLAP to increase its use in courses. In: SIGCSE (2011)Google Scholar
  36. 36.
    Safra, S.: On the complexity of omega-automata. In: FOCS (1988)Google Scholar
  37. 37.
    Sickert, S., Esparza, J., Jaax, S., Křetínský, J.: Limit-deterministic Büchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 312–332. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_17CrossRefGoogle Scholar
  38. 38.
    Sickert, S., Křetínský, J.: MoChiBA: probabilistic LTL model checking using limit-deterministic Büchi automata. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 130–137. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-46520-3_9CrossRefGoogle Scholar
  39. 39.
    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
  40. 40.
    Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15297-9_9CrossRefzbMATHGoogle Scholar
  41. 41.
    Tsai, M.-H., Tsay, Y.-K., Hwang, Y.-S.: GOAL for games, omega-automata, and logics. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 883–889. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_62CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Technical University of MunichMunichGermany

Personalised recommendations