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 Probabilistic Murϕ).
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 research has been partially supported by MURST projects: MEFISTO and SAHARA.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. Automata, Languages and Programming, 430–440 (1997)
Behrends, E.: Introduction to Markov Chains. Vieweg (2000)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers C–35(8) (August 1986)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation, 98 (1992)
Clarke, E.M., McMillan, K.L., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large boolean functions with applications to technology mapping. In: Proc. 30th ACM/IEEE Design Automation Conference, pp. 54–60 (1993)
Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proc. of FOCS 1988, pp. 338–345. IEEE CS Press, Los Alamitos (1988)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
de Alfaro, L.: Formal verification of performance and reliability of real-time systems. Technical report, Stanford University (1996)
Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522–525 (1992)
Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)
Hansson, H., Jonsson, B.: A logic for reasoning about time and probability. Formal Aspects of Computing 6, 512–535 (1994)
Hart, S., Sharir, M.: Probabilistic temporal logic for finite and bounded models. In: Proc. of 16th ACM Symposium on Theory of Computing, pp. 1–13. ACM, New York (1984)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, New Jersey (1991)
Holzmann, G.J.: The spin model checker. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Kemper, P. (ed.) Proc. Tools Session of Aachen 2001 International Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, September 2001, pp. 7–12 (2001); Available as Technical Report 760/2001, University of Dortmund
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with prism: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 52. Springer, Heidelberg (2002)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94, 1–28 (1991)
Lehmann, D., Rabin, M.: On the advantages of free choice: A symmetric fully distributed solution to the dining philosophers problem (extended abstract). In: Proc. 8th Symposium on Principles of Programming Languages, pp. 133–138 (1981)
Della Penna, G., Intrigila, B., Melatti, I., Minichino, M., Ciancamerla, E., Parisse, A., Tronci, E., Zilli, M.V.: Automatic verification of a turbogas control system with the murphi verifier. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 141–155. Springer, Heidelberg (2003)
Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distributed Computing 1(1), 53–72 (1986)
Pnueli, A., Zuck, L.: Probabilistic verification. Information and Computation 103, 1–29 (1993)
Lynchand, N., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: Proc. 13th ACM Symposium on Principles of Distributed Computing, pp. 314–323 (1994)
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 381–496. Springer, Heidelberg (1994)
Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 206–224. Springer, Heidelberg (1995)
Stern, U., Dill, D.L.: A new scheme for memory-efficient probabilistic verification. In: IFIP TC6/WG6.1 Joint International Conference on: Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (1996)
Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M.: Exploiting transition locality in automatic verification. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, p. 259. Springer, Heidelberg (2001)
Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of FOCS 1985, pp. 327–338. IEEE CS Press, Los Alamitos (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V. (2003). Finite Horizon Analysis of Markov Chains with the Murϕ Verifier. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive