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
2003
Springer
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=84), last updated on Sat, 24 Nov 2012 14:21:40 +0100
text
http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2003a.pdf
10.1007/978-3-540-39724-3_34
DellaPenna_etal2003
Sapienza @ mari @ Dimtz03
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
Geist
D.
editor
Tronci
E.
editor
2003
Springer
conference publication
394
409
3-540-20363-X
Lecture Notes in Computer Science
2860