Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking

In this paper, we describe the dual-processor parallelisation of a symbolic (BDD-based) implementation of probabilistic model checking. We use multi-terminal BDDs, which allow a compact representation of large, structured Markov chains. We show that they also provide a convenient block decomposition of the Markov chain which we use to implement a parallelised version of the Gauss-Seidel iterative method. We provide experimental results on a range of case studies to illustrate the effectiveness of the technique,

• Type: Conference
• Year: 2004
• Where: MASCOTS
• Authors: Marta Z. Kwiatkowska, David Parker, Yi Zhang, Rashid Mehmood
• Keywords: Markov Chain, MASCOTS 2004, MASCOTS 2007, Probabilistic Model Checking, Structured Markov Chains