Skip to main content
SpringerLink
Log in
Book cover

International Conference on Language and Automata Theory and Applications

LATA 2014: Language and Automata Theory and Applications pp 453–465Cite as

Are Good-for-Games Automata Good for Probabilistic Model Checking?

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8370))

Abstract

The potential double exponential blow-up for the generation of deterministic ω-automata for linear temporal logic formulas motivates research on weaker forms of determinism. One of these notions is the good-for-games property that has been introduced by Henzinger and Piterman together with an algorithm for generating good-for-games automata from nondeterministic Büchi automata. The contribution of our paper is twofold. First, we report on an implementation of this algorithms and exhaustive experiments. Second, we show how good-for-games automata can be used for the quantitative analysis of systems modeled by Markov decision processes against ω-regular specifications and evaluate this new method by a series of experiments.

Funded by the DFG through the Graduiertenkolleg 1763 (QuantLA), the CRC 912 HAEC, the cluster of excellence cfAED and the project QuaOS and by the ESF young researcher group IMData 100098198 and the EU-FP-7 grant 295261 (MEALS).

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

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: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 24–39. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

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

    Google Scholar 

  3. Benedikt, M., Lenhardt, R., Worrell, J.: Two variable vs. linear temporal logic in model checking and games. Logical Methods in Computer Science 9(2) (2013)

    Google Scholar 

  4. Boker, U., Kuperberg, D., Kupferman, O., Skrzypczak, M.: Nondeterminism in the presence of a diverse or unknown future. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 89–100. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  5. Bustan, D., Rubin, S., Vardi, M.Y.: Verifying ω-regular properties of Markov chains. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 189–201. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2000)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  8. 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, vol. 2850, pp. 361–375. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: ICSE 1999, pp. 411–420. ACM (1999)

    Google Scholar 

  10. Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  12. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  13. Henzinger, T., Piterman, N.: Solving games without determinization. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395–410. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Klein, J., Baier, C.: Experiments with deterministic ω-automata for formulas of linear temporal logic. Theoretical Computer Science 363(2), 182–195 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  15. Klein, J., Baier, C.: On-the-fly stuttering in the construction of deterministic ω-automata. In: Holub, J., Žďárek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 51–61. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Klein, J., Müller, D., Baier, C., Klüppelholz, S.: Are good-for-games automata good for probabilistic model checking (extended version). Tech. rep., Technische Universität Dresden (2013), http://wwwtcs.inf.tu-dresden.de/ALGI/PUB/LATA14/

  17. Křetínský, J., Garza, R.L.: Rabinizer 2: Small deterministic automata for LTL ∖  GU. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 446–450. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  18. Kupferman, O., Piterman, N., Vardi, M.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. 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, vol. 6572, pp. 85–94. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Kupferman, O., Vardi, M.: From linear time to branching time. ACM Transactions on Computational Logic 6(2), 273–294 (2005)

    Article  MathSciNet  Google Scholar 

  21. Kupferman, O., Vardi, M.: Safraless decision procedures. In: FOCS 2005, pp. 531–542. IEEE Computer Society (2005)

    Google Scholar 

  22. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT) 6(2), 128–142 (2004)

    Google Scholar 

  23. Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 169–187. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  24. Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 74–88. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  25. Löding, C.: Optimal bounds for transformations of ω-automata. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

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

    Google Scholar 

  27. Morgenstern, A., Schneider, K.: From LTL to symbolically represented deterministic automata. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 279–293. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  28. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science 3(3:5), 1–21 (2007)

    Google Scholar 

  29. Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS 2006, pp. 275–284. IEEE (2006)

    Google Scholar 

  30. Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)

    Book  MATH  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  34. Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS 1986, pp. 332–344. IEEE Computer Society (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Theoretical Computer Science, Technische Universität Dresden, 01062, Dresden, Germany

    Joachim Klein, David Müller, Christel Baier & Sascha Klüppelholz

Authors
  1. Joachim Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Müller
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christel Baier
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sascha Klüppelholz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Group on Mathematical Linguistics, Rovira i Virgili University, Avinguda Catalunya, 35, 43002, Tarragona, Spain

    Adrian-Horia Dediu  & Carlos Martín-Vide  & 

  2. School of Computer Science, Department of Software Engineering and Artificial Intelligence, Complutense University of Madrid, Professor José Garcia Santesmases, 9, 28040, Madrid, Spain

    José-Luis Sierra-Rodríguez

  3. Fakultät für Informatik, Institut für Wissens- und Sprachverarbeitung, Otto-von-Guericke-Universität Magdeburg, Universitätsplatz 2, 39106, Magdeburg, Germany

    Bianca Truthe

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Klein, J., Müller, D., Baier, C., Klüppelholz, S. (2014). Are Good-for-Games Automata Good for Probabilistic Model Checking?. In: Dediu, AH., Martín-Vide, C., Sierra-Rodríguez, JL., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2014. Lecture Notes in Computer Science, vol 8370. Springer, Cham. https://doi.org/10.1007/978-3-319-04921-2_37

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-04921-2_37

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-04920-5

  • Online ISBN: 978-3-319-04921-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation