[KPZM04]
M. Kwiatkowska, D. Parker, Y. Zhang and R. Mehmood.
Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking.
In Proc. 12th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 123-130, IEEE CS Press.
October 2004.
[ps.gz]
[pdf]
[bib]
|
Abstract.
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,
observing an average speed-up of 1:8 with two processors.
Furthermore, we present an optimisation for our method based on preconditioning.
|