Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking
In this paper, the authors describe the dual-processor parallelization of a symbolic (BDD-based) implementation of probabilistic model checking. They use multi-terminal BDDs, which allow a compact representation of large, structured Markov chains. They show that they also provide a convenient block decomposition of the Markov chain which they use to implement a parallelized version of the Gauss-Seidel iterative method. They provide experimental results on a range of case studies to illustrate the effectiveness of the technique, observing an average speed-up of 1.8 with two processors.