Finite Horizon Analysis of Markov Chains with the Murphi Verifier

In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given aMarkov 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? verifier. We call the resulting probabilistic model checker FHP-Mur? (Finite Horizon Probabilistic Mur?).We present experimental results comparing FHP-Mur? with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHPMur? can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).