Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier
Della Penna
Giuseppe
author
Intrigila
Benedetto
author
Melatti
Igor
author
Tronci
Enrico
author
Venturini Zilli
Marisa
author
2006
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).
exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=78), last updated on Thu, 22 Nov 2012 14:59:18 +0100
text
http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2006a.pdf
10.1007/s10009-005-0216-7
DellaPenna_etal2006
Sapienza @ mari @ Dimtz06
Int. J. Softw. Tools Technol. Transf.
2006
Springer-Verlag
Berlin, Heidelberg
continuing
periodical
academic journal
8
4
397
409
1433-2779