@Article{DellaPenna_etal2006,
author="Della Penna, Giuseppe
and Intrigila, Benedetto
and Melatti, Igor
and Tronci, Enrico
and Venturini Zilli, Marisa",
title="Finite horizon analysis of Markov Chains with the Mur{\$}{\backslash}varphi{\$} verifier",
journal="Int. J. Softw. Tools Technol. Transf.",
year="2006",
publisher="Springer-Verlag",
address="Berlin, Heidelberg",
volume="8",
number="4",
pages="397--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=78), last updated on Thu, 22 Nov 2012 14:59:18 +0100",
issn="1433-2779",
doi="10.1007/s10009-005-0216-7",
opturl="https://doi.org/10.1007/s10009-005-0216-7",
file=":http://mclab.di.uniroma1.it/publications/papers/papers/Della Penna2006a.pdf:PDF"
}