www.prismmodelchecker.org
[ZPK05a] Yi Zhang, David Parker and Marta Kwiatkowska. A Wavefront Parallelisation of CTMC Solution using MTBDDs. In Proc. International Conference on Dependable Systems and Networks (DSN'05), pages 732-742, IEEE CS Press. June 2005. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (74 KB)  pdf pdf (168 KB)  bib bib
Links: [Google] [Google Scholar]
Abstract. In this paper, we present a parallel implementation for the steady-state analysis of continuous-time Markov chains (CTMCs). This analysis is performed via solution of a linear equation system, which is carried out using the Gauss-Seidel iterative method. We apply wavefront techniques, which are used to create an efficient parallel execution schedule based on dependencies between subtasks. Our implementation uses symbolic data structures - multi-terminal binary decision diagrams (MTBDDs) - which provide a compact representation for large, structured CTMCs. MTBDDs prove to be very well suited to this application; firstly, by providing a significant reduction in inter-processor communication; and secondly, by allowing easy access to task dependency information. We demonstrate the effectiveness of our technique by presenting experimental results from a cluster of 32 nodes which exhibit speedups of between 9.7 and 16.5, comparable with existing parallelisations of similar CTMC analysis techniques. Thanks to the low space complexity and good convergence rate of the Gauss-Seidel method, our implementation represents an excellent candidate for parallel steady-state solution of CTMCs.

Publications