Abstract
In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas(BPCTL), that is, PCTL formulas in which all Until operators arebounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain \({\cal M}\) and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in \({\cal M}\). This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems.
We present an implementation of our algorithm within a suitable extension of the Murφ verifier. We call FHP-Murφ (Finite Horizon Probabilistic Murφ) such extension of the Murφ verifier.
We give 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 effectively handle verification of BPCTL formulas for 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 chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430–440. Springer, Heidelberg (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), 677–691 (1986)
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)
Cached murphi web page: http://www.dsi.uniroma1.it/~tronci/cached.murphi.html
Clarke, E.M., McMillan, K.L.: 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)
Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of the IEEE Conference on Decision and Control, Piscataway, NJ, pp. 338–345. IEEE Press, Los Alamitos (1988)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
Cudd web page: http://vlsi.colorado.edu/~fabio/
de Alfaro, L.: Formal verification of performance and reliability of real-time systems. Technical Report STAN-CS-TR-96-1571, Stanford University (1996)
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 & Processors, pp. 522–525. IEEE Computer Society, Los Alamitos (1992)
Online appendices: http://www.di.univaq.it/melatti/FMCAD04/
Jonsson, B., Hansson, H.: A logic for reasoning about time and probability. Formal Aspects of Computing 6(5), 512–535 (1994)
Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)
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)
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A tool for modelchecking markov chains. Software Tools for Technology Transfer 4(2), 153–172 (2003)
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: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)
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, pp. 52–66. Springer, Heidelberg (2002)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 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)
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)
Murphi web page: http://sprout.stanford.edu/dill/murphi.html
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 murϕ verifier. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 141–155. Springer, Heidelberg (2003)
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, and M. V. Zilli. Finite horizon analysis of markov chains with the murϕ verifier. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 394–409. Springer, Heidelberg (2003)
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite horizon analysis of stochastic systems with the murϕ verifier. In: Blundo, C., Laneve, C. (eds.) ICTCS 2003. LNCS, vol. 2841, pp. 58–71. Springer, Heidelberg (2003)
Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53–72 (1986)
Prism web page: http://www.cs.bham.ac.uk/~dxp/prism/
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)
Spin web page: http://spinroot.com
Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, pp. 327–338. IEEE CS Press, Los Alamitos (1985)
Clarke, E.M., Hartonas-Garmhausen, V., Aguiar Campos, S.V.: Probverus: Probabilistic symbolic model checking. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 96–110. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V. (2004). Bounded Probabilistic Model Checking with the Murφ Verifier. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-30494-4_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23738-9
Online ISBN: 978-3-540-30494-4
eBook Packages: Springer Book Archive