Title:
Finite Horizon Analysis of Markov Chains with the Mur$\varphi$ Verifier


Authors:
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti,
Enrico Tronci, Marisa Venturini Zilli 

Proceedings of: 
12th Advanced Research Working Conference on
Correct Hardware Design and Verification Methods (CHARME),
21-24 October 2003, L'Aquila (Italy),
LNCS, Springer-Verlag <br>
Co-sponsored by the IFIP TC10/WG10.5 Working Group on:
Design and Engineering of Electronic Systems <



Abstract

In this paper we present an explicit disk based verification algorithm
for Probabilistic Systems defining
{\em discrete time}/{\em 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$ ({\em 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).