An Efficient BDD-Based Implementation of Gauss-Seidel for CTMC Analysis
Rashid Mehmood, David A. Parker, Marta Kwiatkowska · 2003
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.