%0 Journal Article
%T Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier
%A Della Penna, Giuseppe
%A Intrigila, Benedetto
%A Melatti, Igor
%A Tronci, Enrico
%A Venturini Zilli, Marisa
%J Int. J. Softw. Tools Technol. Transf.
%D 2006
%V 8
%N 4
%I Springer-Verlag
%C Berlin, Heidelberg
%@ 1433-2779
%F DellaPenna_etal2006
%O exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=78), last updated on Thu, 22 Nov 2012 14:59:18 +0100
%X 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 FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ 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$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
%R 10.1007/s10009-005-0216-7
%U http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2006a.pdf
%U https://doi.org/10.1007/s10009-005-0216-7
%P 397-409