Skip to main content
SpringerLink
Log in

Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains

  • Conference paper
Book cover Quantitative Evaluation of Systems (QEST 2014)

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

Included in the following conference series:

Abstract

We present a novel technique to analyze the bounded reachability probability problem for large Markov chains. The essential idea is to incrementally search for sets of paths that lead to the goal region and to choose the sets in a way that allows us to easily determine the probability mass they represent. To effectively analyze the system dynamics using an SMT solver, we employ a finite-precision abstraction on the Markov chain and a custom quantifier elimination strategy. Through experimental evaluation on PRISM benchmark models we demonstrate the feasibility of the approach on models that are out of reach for previous methods.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Kwiatkowska, M.Z., Norman, G., Parker, D.: Using probabilistic model checking in systems biology. SIGMETRICS Performance Evaluation Review 35(4) (2008)

    Google Scholar 

  2. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  4. Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: Proc. of QEST, pp. 167–176. IEEE Computer Society (2009), www.mrmc-tool.org

  5. Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 162–175. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Fränzle, M., Teige, T., Eggers, A.: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. Journal of Logic and Algebraic Programming 79(7), 436–466 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  7. Teige, T.: Stochastic Satisfiability Modulo Theories: A Symbolic Technique for the Analysis of Probabilistic Hybrid Systems. Doctoral dissertation, Carl von Ossietzky Universität Oldenburg, Department of Computing Science, Germany (2012)

    Google Scholar 

  8. Teige, T., Fränzle, M.: Generalized Craig interpolation for stochastic Boolean satisfiability problems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 158–172. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234–248. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Dehnert, C., Katoen, J.-P., Parker, D.: SMT-based bisimulation minimisation of Markov models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 28–47. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time markov chains using bounded model checking. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366–380. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Braitling, B., Wimmer, R., Becker, B., Jansen, N., Ábrahám, E.: Counterexample generation for Markov chains using SMT-based bounded model checking. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE 2011. LNCS, vol. 6722, pp. 75–89. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Jansen, N., Ábrahám, E., Zajzon, B., Wimmer, R., Schuster, J., Katoen, J.-P., Becker, B.: Symbolic counterexample generation for discrete-time Markov chains. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 134–151. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  15. Ash, R., Doléans-Dade, C.: Probability and Measure Theory. Harcourt/Academic Press (2000)

    Google Scholar 

  16. Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. Proc. of FMSD 42(1) (2013)

    Google Scholar 

  17. Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Helmink, L., Sellink, M., Vaandrager, F.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127–165. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  19. Reiter, M., Rubin, A.: Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security (TISSEC) 1(1), 66–92 (1998)

    Article  Google Scholar 

  20. Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Communications of the ACM 28(6), 637–647 (1985)

    Article  MathSciNet  Google Scholar 

  21. Herman, T.: Probabilistic self-stabilization. Information Processing Letters 35(2), 63–67 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  22. von Neumann, J.: Probabilistic logics and synthesis of reliable organisms from unreliable components. In: Shannon, C., McCarthy, J. (eds.) Proc. of Automata Studies, pp. 43–98. Princeton University Press (1956)

    Google Scholar 

  23. Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and Computation 88(1) (1990)

    Google Scholar 

  24. Rabe, M.N., Wintersteiger, C.M., Kugler, H., Yordanov, B., Hamadi, Y.: Symbolic approximation of the bounded reachability probability in large Markov chains. Technical Report MSR-TR-2014-74, Microsoft Research (2014)

    Google Scholar 

  25. Bellman, R.: Dynamic programming. Princeton University Press (1957)

    Google Scholar 

  26. Shapley, L.S.: Stochastic games. Proceedings of the National Academy of Sciences 39(10) (1953)

    Google Scholar 

  27. Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: A web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  28. Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Bounded probabilistic model checking with the Murϕ verifier. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 214–229. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  29. de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  30. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL. ACM (1977)

    Google Scholar 

  31. Esparza, J., Gaiser, A.: Probabilistic abstractions with arbitrary domains. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 334–350. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  32. Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 182–197. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  33. Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322–340. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  34. Fränzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172–186. Springer, Heidelberg (2008)

    Google Scholar 

  35. Andrés, M.E., D’Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 129–148. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  36. Han, T., Katoen, J.P., Berteun, D.: Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering 35(2), 241–257 (2009)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Saarland University, Germany

    Markus N. Rabe

  2. Microsoft Research, U.S.A.

    Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov & Youssef Hamadi

Authors
  1. Markus N. Rabe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph M. Wintersteiger
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hillel Kugler
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Boyan Yordanov
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Youssef Hamadi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing Science, University of Glasgow, G12 8RZ, Glasgow, UK

    Gethin Norman

  2. University of Illinois, 61801-2918, Urbana, IL, USA

    William Sanders

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Rabe, M.N., Wintersteiger, C.M., Kugler, H., Yordanov, B., Hamadi, Y. (2014). Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains. In: Norman, G., Sanders, W. (eds) Quantitative Evaluation of Systems. QEST 2014. Lecture Notes in Computer Science, vol 8657. Springer, Cham. https://doi.org/10.1007/978-3-319-10696-0_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10696-0_30

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10695-3

  • Online ISBN: 978-3-319-10696-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation