Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach

In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision pro-cesses using specifications in the probabilistic tempo-ral logics PCTL and CSL. Motivated by the success of model checkers such as SMV, which use BDDs (binary decision diagrams), we have developed an implementa-tion of PCTL and CSL model checking based on MTB-DDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit meth-ods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of sym-bolic and explicit approaches to overcome these perfor-mance problems. For typical examples, we achieve a dra-matic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of mag-nitude larger than with sparse matrices, whilst almost matching or even beating them for speed