TY  - JOUR
AU  - Della Penna, Giuseppe
AU  - Intrigila, Benedetto
AU  - Melatti, Igor
AU  - Tronci, Enrico
AU  - Venturini Zilli, Marisa
PY  - 2006
DA  - 2006//
TI  - Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier
JO  - Int. J. Softw. Tools Technol. Transf.
SP  - 397
EP  - 409
VL  - 8
IS  - 4
PB  - Springer-Verlag
CY  - Berlin, Heidelberg
AB  - 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).
SN  - 1433-2779
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2006a.pdf
UR  - https://doi.org/10.1007/s10009-005-0216-7
DO  - 10.1007/s10009-005-0216-7
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=78), last updated on Thu, 22 Nov 2012 14:59:18 +0100
ID  - DellaPenna_etal2006
ER  -