www.prismmodelchecker.org
[MPK03b] Rashid Mehmood, David Parker and Marta Kwiatkowska. An Efficient BDD-Based Implementation of Gauss-Seidel for CTMC Analysis. Technical report CSR-03-13, School of Computer Science, University of Birmingham. December 2003. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (111 KB)  pdf pdf (243 KB)  bib bib
Links: [Google] [Google Scholar]
Abstract. Symbolic approaches to the analysis of Markov models, i.e. those that use BDD-based data structures, have proved to be an effective method of combating the state space explosion problem. One such example is the use of offset-labelled MTBDDs (multi-terminal BDDs). However, a major disadvantage of this data structure is that it cannot be used with efficient iterative methods, in particular, Gauss-Seidel. In this paper, we propose a solution that permits the use of this numerical method by introducing a data structure derived from an offset-labelled MTBDD. This approach provides significant improvements in terms of both time and memory consumption. We present and analyse experimental results for both in-core and out-of-core versions of this implementation on a standard workstation, and successfully perform steady-state probability computation for CTMCs with as many as 600 million states and 7.7 billion transitions.

Publications