@InProceedings{DellaPenna_etal2003,
author="Della Penna, Giuseppe
and Intrigila, Benedetto
and Melatti, Igor
and Tronci, Enrico
and Venturini Zilli, Marisa",
editor="Geist, D.
and Tronci, E.",
title="Finite Horizon Analysis of Markov Chains with the Mur{\$}{\backslash}varphi{\$} Verifier",
booktitle="Correct Hardware Design and Verification Methods, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L{\textquoteright}Aquila, Italy, October 21-24, 2003, Proceedings",
series="Lecture Notes in Computer Science",
year="2003",
publisher="Springer",
volume="2860",
pages="394--409",
abstract="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{\$}{\backslash}varphi{\$} verifier. We call the resulting probabilistic model checker FHP-Mur{\$}{\backslash}varphi{\$} (Finite Horizon Probabilistic Mur{\$}{\backslash}varphi{\$}). We present experimental results comparing FHP-Mur{\$}{\backslash}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{\$}{\backslash}varphi{\$} can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).",
optnote="exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=84), last updated on Sat, 24 Nov 2012 14:21:40 +0100",
issn="3-540-20363-X",
doi="10.1007/978-3-540-39724-3_34",
opturl="https://doi.org/10.1007/978-3-540-39724-3_34",
file=":http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2003a.pdf:PDF"
}