Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, and Marisa Venturini Zilli. "Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier." In Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 2124, 2003, Proceedings, edited by D. Geist and E. Tronci, 394–409. Lecture Notes in Computer Science 2860. Springer, 2003. ISSN: 354020363X. DOI: 10.1007/9783540397243_34.
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$\varphi$ verifier. We call the resulting probabilistic model checker FHPMur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHPMur$\varphi$ with (a finite horizon subset of) PRISM, a stateoftheart symbolic model checker for Markov Chains. Our experimental results show that FHPMur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
