[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata

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

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9938))

Abstract

The limiting factor for quantitative analysis of Markov decision processes (MDP) against specifications given in linear temporal logic (LTL) is the size of the generated product. As recently shown, a special subclass of limit-deterministic Büchi automata (LDBA) can replace deterministic Rabin automata in quantitative probabilistic model checking algorithms. We present an extension of PRISM for LTL model checking of MDP using LDBA. While existing algorithms can be used only with minimal changes, the new approach takes advantage of the special structure and the smaller size of the obtained LDBA to speed up the model checking. We demonstrate the speed up experimentally by a comparison with other approaches.

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

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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. 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: ATVA, pp. 24–39 (2013)

    Google Scholar 

  2. 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). doi:10.1007/978-3-642-28756-5_8

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  4. Blahoudek, F., Heizmann, M., Schewe, S., Strejček, J., Tsai, M.-H.: Complementing semi-deterministic Büchi automata. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 770–787. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_49

    Chapter  Google Scholar 

  5. Blahoudek, F., Křetínský, M., Strejček, J.: Comparison of LTL to deterministic Rabin automata translators. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 164–172. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_12

    Chapter  Google Scholar 

  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). doi:10.1007/978-3-642-39799-8_37

    Chapter  Google Scholar 

  7. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  8. 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). doi:10.1007/3-540-48119-2_16

    Google Scholar 

  9. 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). doi:10.1007/978-3-540-39813-4_26

    Chapter  Google Scholar 

  10. 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). doi:10.1007/3-540-48683-6_23

    Chapter  Google Scholar 

  11. Duret-Lutz, A.: Manipulating LTL formulas using Spot 1.0. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 442–445. Springer, Heidelberg (2013). doi:10.1007/978-3-319-02444-8_31

    Chapter  Google Scholar 

  12. Duret-Lutz, A.: LTL translation improvements in Spot 1.0. IJCCBS 5(1–2), 31–54 (2014)

    Article  Google Scholar 

  13. 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, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_13

    Google Scholar 

  14. Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–168. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_13

    Chapter  Google Scholar 

  15. Fritz, C.: Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003). doi:10.1007/3-540-45089-0_5

    Chapter  Google Scholar 

  16. Gaiser, A., Křetínský, J., Esparza, J.: Rabinizer: small deterministic automata for LTL(F, G). In: ATVA, pp. 72–76 (2012)

    Google Scholar 

  17. Gastin, P., Oddoux, D.: Fast LTL to Büchi automatatranslation. In: CAV, pp. 53–65 (2001). http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/

    Google Scholar 

  18. 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). doi:10.1007/3-540-36135-9_20

    Chapter  Google Scholar 

  19. Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazyprobabilistic model checking without determinisation. In: CONCUR. LIPIcs, vol. 42, pp. 354–367 (2015)

    Google Scholar 

  20. Henzinger, T.A., Piterman, N.: Solving games without determinization. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395–410. Springer, Heidelberg (2006). doi:10.1007/11874683_26

    Chapter  Google Scholar 

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

    Google Scholar 

  22. Klein, J.: ltl2dstar - LTL to deterministic Streett and Rabinautomata. http://www.ltl2dstar.de/

  23. Klein, J., Müller, D., Baier, C., Klüppelholz, S.: Are good-for-games automata good for probabilistic model checking? In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 453–465. Springer, Heidelberg (2014). doi:10.1007/978-3-319-04921-2_37

    Chapter  Google Scholar 

  24. 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, Heidelberg (2014). doi:10.1007/978-3-319-11936-6_17

    Google Scholar 

  25. Křetínský, J., Ledesma-Garza, R.: Rabinizer 2: small deterministic automata for LTL\(_{\setminus \mathbf{GU}}\). In: ATVA, pp. 446–450 (2013)

    Google Scholar 

  26. Křetínský, J., Esparza, J.: Deterministic automata for the (F, G)-fragment of LTL. In: CAV, pp. 7–22 (2012)

    Google Scholar 

  27. 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). doi:10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  28. Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203–204 (2012)

    Google Scholar 

  29. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: LICS, pp. 255–264 (2006)

    Google Scholar 

  30. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)

    Google Scholar 

  31. Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53–72 (1986). doi:10.1007/BF01843570

    Article  MATH  Google Scholar 

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

    Google Scholar 

  33. Schewe, S.: Tighter bounds for the determinisation of Büchi automata. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 167–181. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00596-1_13

    Chapter  Google Scholar 

  34. Sickert, S.: MoChiBA. https://www7.in.tum.de/~sickert/projects/mochiba/

  35. 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, Heidelberg (2016). doi:10.1007/978-3-319-41540-6_17

    Chapter  Google Scholar 

  36. 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). doi:10.1007/10722167_21

    Chapter  Google Scholar 

  37. 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). doi:10.1007/978-3-642-39799-8_62

    Chapter  Google Scholar 

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

    Google Scholar 

Download references

Acknowledgements

This work is partially funded by the DFG Research Training Group “PUMA: Programm- und Modell-Analyse” (GRK 1480) and by the Czech Science Foundation, grant No. 15-17564S.

The authors want to thank Ernst Moritz Hahn and Andrea Turrini for providing a private version of IscasMC to compare to and for assistance in using it.

Author information

Authors and Affiliations

  1. Technische Universität München, Munich, Germany

    Salomon Sickert & Jan Křetínský

Authors
  1. Salomon Sickert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jan Křetínský
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Salomon Sickert .

Editor information

Editors and Affiliations

  1. AIST , Osaka, Japan

    Cyrille Artho

  2. Inria Rennes , Rennes, France

    Axel Legay

  3. Bar Ilan University , Ramat Gan, Israel

    Doron Peled

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Sickert, S., Křetínský, J. (2016). MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46520-3_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46519-7

  • Online ISBN: 978-3-319-46520-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation