Skip to main content
SpringerLink
Log in

Abstraction Refinement for Probabilistic Software

  • Conference paper
Book cover Verification, Model Checking, and Abstract Interpretation (VMCAI 2009)

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

Abstract

We present a methodology and implementation for verifying ANSI-C programs that exhibit probabilistic behaviour, such as failures or randomisation. We use abstraction-refinement techniques that represent probabilistic programs as Markov decision processes and their abstractions as stochastic two-player games. Our techniques target quantitative properties of software such as “the maximum probability of file-transfer failure” or “the minimum expected number of loop iterations” and the abstractions we construct yield lower and upper bounds on these properties, which then guide the refinement process. We build upon state-of-the-art techniques and tools, using SAT-based predicate abstraction, symbolic implementations of probabilistic model checking and components from GOTO-CC, SATABS and PRISM. Experimental results show that our approach performs very well in practice, successfully verifying actual networking software whose complexity is significantly beyond the scope of existing probabilistic verification tools.

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. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  2. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proc. QEST 2006, pp. 157–166. IEEE, Los Alamitos (2006)

    Google Scholar 

  4. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD 25(2-3), 105–127 (2004)

    MATH  Google Scholar 

  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. D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 72–86. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. de Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 325–338. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Roy, P., Parker, D., Norman, G., de Alfaro, L.: Symbolic magnifying lens abstraction in Markov decision processes. In: Proc. QEST 2008. IEEE, Los Alamitos (2008)

    Google Scholar 

  10. Chatterjee, K., Henzinger, T., Jhala, R., Majumdar, R.: Counterexample-guided planning. In: Proc. UAI 2005, pp. 104–111 (2005)

    Google Scholar 

  11. McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  12. Huth, M.: On finite-state approximants for probabilistic computation tree logic. Theoretical Computer Science 346(1), 113–134 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Game-based probabilistic predicate abstraction in PRISM. In: Proc. QAPL 2008(2008)

    Google Scholar 

  14. Pierro, A.D., Wiklicky, H.: Concurrent constraint programming: Towards probabilistic abstract interpretation. In: Proc. PPDP 2000, pp. 127–138. ACM Press, New York (2000)

    Google Scholar 

  15. Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Science of Computer Programming 58(1-2), 179–205 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  16. Smith, M.: Probabilistic abstract interpretation of imperative programs using truncated normal distributions. In: Proc. QAPL 2008 (2008)

    Google Scholar 

  17. Legay, A., Murawski, A., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 173–187. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. QEST 2006, pp. 131–132. IEEE, Los Alamitos (2006)

    Google Scholar 

  19. Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Springer, Heidelberg (1976)

    Book  MATH  Google Scholar 

  20. Shapley, L.: Stochastic games. Proc. Nat. Acad. Science 39, 1095–1100 (1953)

    Article  MathSciNet  MATH  Google Scholar 

  21. de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis (1997)

    Google Scholar 

  22. Condon, A.: On algorithms for simple stochastic games. Advances in computational complexity theory 13, 51–73 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  23. GOTO-CC, http://www.verify.ethz.ch/goto-cc/

  24. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. PLDI 2001, pp. 203–213 (2001)

    Google Scholar 

  25. Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  26. Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Technical Report RR-08-06, Oxford University Computing Laboratory (2008)

    Google Scholar 

  27. Jhala, R., McMillan, K.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  28. Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: Proc. POPL 2004, pp. 232–244. ACM Press, New York (2004)

    Google Scholar 

  29. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  30. Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Parks Road, Oxford, OX1 3QD

    Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman & David Parker

Authors
  1. Mark Kattenbelt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gethin Norman
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. David Parker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. (Emeritus University of Copenhagen), Bukkeballevej 88, 2960, Rungsted, Denmark

    Neil D. Jones

  2. Institut für Informatik, Fachbereich Mathematik und Informatik, Westfälische Wilhelms-Universität, 48149, Münster, Germany

    Markus Müller-Olm

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D. (2008). Abstraction Refinement for Probabilistic Software. In: Jones, N.D., Müller-Olm, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2009. Lecture Notes in Computer Science, vol 5403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93900-9_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-93900-9_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-93899-6

  • Online ISBN: 978-3-540-93900-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation