Skip to main content
SpringerLink
Log in

Finite horizon analysis of Markov Chains with the Murϕ verifier

  • Special section on Recent Advances in Hardware Verification
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Murϕ verifier. We call the resulting probabilistic model checker FHP-Murϕ (Finite Horizon ProbabilisticMurϕ). We present experimental results comparing FHP-Murϕ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Murϕ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: ICCAD ’93: Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, pp. 188–191. IEEE Computer Society Press, Los Alamitos, CA, USA (1993)

  2. Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, P., Marchetti-Spaccamela, A. (eds.) Automata, Languages and Programming, 24th International Colloquium, ICALP’97, Bologna, Italy, Proceedings, vol. 1256 of Lecture Notes in Computer Science, pp. 430–440. Springer, Berlin (1997)

  3. Behrends, E.: Introduction to Markov Chains, Vieweg. Germany (2000)

    MATH  Google Scholar 

  4. Bianco, de Alfaro: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) Foundations of Software Technology and Theoretical Computer Science, 15th Conference, Bangalore, India, Proceedings, vol. 1026 of Lecture Notes in Computer Science, pp. 499–513. Springer, Berlin (1995)

  5. Bobbio, A., Ciancamerla, E., Franceschinis, G., Gaeta, R., Minichino, M., Portinale, L.: Methods of increasing modelling power for safety analysis, applied to a turbine digital control system. In: Anderson, S., Bologna, S., Felici, M. (eds.) Computer Safety, Reliability and Security 21st International Conference, SAFECOMP 2002, Catania, Italy, Proceedings, vol. 2434 of Lecture Notes in Computer Science, pp. 212–223. Springer, Berlin (2002)

  6. Bobbio, A., Ciancamerla, E., Gribaudo, M., Horvath, A., Minichino, M., Tronci, E.: Model Checking based on fluid petri nets for the temperature control system of the icaro co-generative Planti. In: Anderson, S., Bologna, S., Felici, M. (eds.) Computer Safety, Reliability and Security, 21st International Conference, SAFECOMP 2002, Catania, Italy, Proceedings, vol. 2434 of Lecture Notes in Computer Science, pp. 273–283. Springer, Berlin (2002)

  7. Bobbio, A., Bologna, S., Minichino, M., Ciancamerla, E., Incalcaterra, P., Kropp, C., Tronci, E.: Advanced techniques for safety analysis applied to the gas turbine control system of Icaro co generative plant. In: Proceedings of X Convegno TESEC, Genova, Italy (2001)

  8. Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35 (8), 677–691 (1986)

    Google Scholar 

  9. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98 (2), 142–170 (1992)

    Article  MathSciNet  Google Scholar 

  10. Clarke, E.M., McMillan, K.L., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large Boolean functions with applications to technology mapping. In: Proceedings of the 30th International on Design automation conference, pp. 54–60. ACM Press, New York (1993)

  11. Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of the IEEE Conference on Decision and Control, pp. 338–345. IEEE Press, Piscataway, NJ (1988)

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

    Article  MathSciNet  Google Scholar 

  13. CUDD Web Page: http://vlsi.colorado.edu/~fabio/ (2004)

  14. de Alfaro, L.: Formal verification of performance and reliability of real-time systems. Technical Report STAN-CS-TR-96-1571, Stanford University (1996)

  15. Della Penna, G., Intrigila, B., Melatti, I., Minichino, M., Ciancamerla, E., Parisse, A., Tronci, E., Venturini Zilli, M.: Automatic verification of a turbogas control system with the murφ verifier. In: Maler, O., Pnueli, A. (eds.) Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, Proceedings, vol. 2623 of Lecture Notes in Computer Science, pp. 141–155. Springer, Berlin (2003)

  16. Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M.: Finite horizon analysis of markov chains with the Murφ verifier. In: Geist, D., Tronci, E. (eds.) Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L’Aquila, Italy, Proceedings, vol. 2860 of Lecture Notes in Computer Science, pp. 394–409. Springer (2003)

  17. Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer and Processors, pp. 522–525. IEEE Computer Society, Washington, DC (1992)

  18. ENEA: Proprietary ICARO Documentation (2001)

  19. Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)

    Google Scholar 

  20. Hansson, H., Jonsson, B.: A logic for reasoning about time and probability. Formal Aspects Comput 6(5), 512–535 (1994)

    Article  Google Scholar 

  21. Hart, S., Sharir, M.: Probabilistic temporal logics for finite and bounded models. In: Proceedings of the sixteenth annual ACM symposium on Theory of computing, pp. 1–13. ACM Press, New York (1984)

  22. Holzmann,G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Upper Saddle River, NJ (1991)

    Google Scholar 

  23. Holzmann, G.J.: The spin model checker. IEEE Trans. Software Eng. 23(5), 279–295, (1997)

    Article  MathSciNet  Google Scholar 

  24. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J.T., Harder, U. (eds.) Computer Performance Evaluation, Modelling Techniques and Tools 12th International Conference, TOOLS 2002, London, UK, Proceedings, vol. 2324 of Lecture Notes in Computer Science, pp. 200–204. Springer, Berlin (2002)

  25. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8–12, 2002, Proceedings, vol. 2280 of Lecture Notes in Computer Science, pp. 52–66. Springer, Berlin (2002)

  26. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  Google Scholar 

  27. Lehmann, D., Rabin, M.: On the advantages of free choice: A symmetric fully distributed solution to the dining philosophers problem (extended abstract). In: Proceedings of 8th Symposium on Principles of Programming Languages, pp. 133–138 (1981)

  28. Lynch, N., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, pp. 314–323. ACM Press, New York (1994)

  29. Murphi Web Page: http://sprout.stanford.edu/dill/murphi.html (2004)

  30. Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53–72 (1986)

    Article  Google Scholar 

  31. Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. Comput. 103(1), 1–29 (1993)

    Article  MathSciNet  Google Scholar 

  32. PRISM Web Page: http://www.cs.bham.ac.uk/~dxp/prism/ (2004)

  33. Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR ’94, Concurrency Theory, 5th International Conference, Uppsala, Sweden, Proceedings, vol. 836 of Lecture Notes in Computer Science, pp. 481–496. Springer, Berlin (1994)

  34. SPIN Web Page: http://spinroot.com (2004)

  35. Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M.: Exploiting transition locality in automatic verification. In: Margaria, T., Melham, T.F. (eds.) Correct Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, Proceedings, vol. 2144 of Lecture Notes in Computer Science, pp. 259–274. Springer, Berlin (2001)

  36. Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, pp. 327–338, IEEE CS Press, Portland, OR (1985)

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di L’Aquila, Coppito, 67100, L’Aquila, Italy

    Giuseppe Della Penna & Igor Melatti

  2. Dipartimento di Informatica, Università di Roma “La Sapienza”, Via Salaria 113, 00198, Rome, Italy

    Enrico Tronci & Marisa Venturini Zilli

  3. Dipartimento di Matematica Pura ed Applicata, Università di Roma “Tor Vergata”, Via della Ricerca Scientifica 1, 00133, Rome, Italy

    Benedetto Intrigila

Authors
  1. Giuseppe Della Penna
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benedetto Intrigila
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Igor Melatti
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Enrico Tronci
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Marisa Venturini Zilli
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Giuseppe Della Penna.

Additional information

This research has been partially supported by MURST projects MEFISTO and SAHARA.

This paper is a journal version of the conference paper [16].

Rights and permissions

Reprints and permissions

About this article

Cite this article

Penna, G.D., Intrigila, B., Melatti, I. et al. Finite horizon analysis of Markov Chains with the Murϕ verifier. Int J Softw Tools Technol Transfer 8, 397–409 (2006). https://doi.org/10.1007/s10009-005-0216-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-005-0216-7

Keywords

Search

Navigation