TITLE: Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier

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

Proceedings of:
Formal Methods in Computer-Aided Design:
5th International Confrence, FMCAD 2004,
Austin, Texas, USA, November 15-17, 2004
LNCS 3312, Springer-Verlag


ABSTRACT

In this paper we present an explicit %disk based 
verification algorithm for
Probabilistic Systems defining {\em discrete time}/{\em finite state} Markov
Chains.  We restrict ourselves to verification of {\em Bounded} PCTL formulas
(BPCTL), that is, PCTL formulas in which all {\em Until} operators are bounded,
possibly with different bounds. This means that we consider only paths (system
runs) of bounded length. 

Given a Markov Chain ${\cal M}$ and a BPCTL formula $\Phi$, our algorithm
checks if $\Phi$ is satisfied in ${\cal M}$. This allows to verify important
properties, such as reliability in {\em Discrete Time Hybrid Systems}.

We present an implementation of our algorithm within  a suitable extension of
the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ ({\em Finite Horizon
Probabilistic} Mur$\varphi$) such extension of the Mur$\varphi$ verifier.

We give 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 effectively  handle
verification of BPCTL formulas for systems that are out of reach for PRISM,
namely those involving arithmetic operations on the state variables (e.g.
hybrid systems).