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).