Explicit Algorithms for Probabilistic Model Checking

In this Thesis we present two explicit algorithms for the verification of finite horizon properties of Probabilistic Systems modeled by Discrete Time Markov Chains. The first algorithm deals with finite horizon safety properties only. Thus, given a Markov Chain M and an integer k (horizon), this algorithm is able to check whether the probability of reaching an error state of M in at most k steps is below a given threshold. On the other hand, the second algorithm is able to handle generic BPCTL (Bounded PCTL) formulas, i.e. PCTL formulas in which all Until operators are bounded, possibly with different bounds. This entails that we consider only system runs (paths) of bounded length. Thus, given a Markov Chain M and a BPCTL formula F, our algorithm checks if F is satisfied in M. This allows to verify important properties, which is not possible to check with the first algorithm, such as e.g. robustness in Discrete Time Stochastic Hybrid Systems. We present an implementation of our algorithms within a suitable extension of the Murphi verifier. We call FHP-Murphi (Finite Horizon Probabilistic Murphi) such extension of the Murphi verifier. Finally, we give experimental results comparing FHP-Murphi with PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Murphi can effectively handle verifications for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables. However, PRISM is a more general verifier than Murphi, since it handles also other Markov Chain based models, and is able to verify also unbounded PCTL formulas.