TY  - CONF
AU  - Della Penna, Giuseppe
AU  - Intrigila, Benedetto
AU  - Melatti, Igor
AU  - Tronci, Enrico
AU  - Venturini Zilli, Marisa
ED  - Geist, D.
ED  - Tronci, E.
PY  - 2003
DA  - 2003//
TI  - Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier
BT  - Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings
T3  - Lecture Notes in Computer Science
SP  - 394
EP  - 409
VL  - 2860
PB  - Springer
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  - 3-540-20363-X
L1  - http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2003a.pdf
UR  - https://doi.org/10.1007/978-3-540-39724-3_34
DO  - 10.1007/978-3-540-39724-3_34
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=84), last updated on Sat, 24 Nov 2012 14:21:40 +0100
ID  - DellaPenna_etal2003
ER  -