Name
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1109/MASCOT.2004.1348189 | MASCOTS |
Keywords | Field | DocType |
parallel processing,systems analysis,iterative methods,markov processes,markov chain,gauss seidel,model checking | Markov process,Iterative method,Markov model,Computer science,Parallel processing,Systems analysis,Markov chain,Binary decision diagram,Theoretical computer science,Probabilistic model checking | Conference |
ISSN | ISBN | Citations |
1526-7539 | 0-7695-2251-3 | 6 |
PageRank | References | Authors |
0.60 | 10 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marta Z. Kwiatkowska | 1 | 6118 | 322.21 |
| David Parker | 2 | 4018 | 184.00 |
| Yi Zhang | 3 | 214 | 10.52 |
| Rashid Mehmood | 4 | 355 | 45.46 |