An Efficient Symbolic Out-of-Core Solution Method for Markov Models

In recent years, disk-based approaches to the analysis of Markov models have proved to be an effective method of combating the state space explosion problem. Coupled with parallel and symbolic techniques, disk-based methods have demonstrated impressive performance for numerical solution. In an earlier paper, we presented a novel, symbolic out-of-core algorithm which used MTBDD-based data structures for matrix storage in RAM and disk-based storage for solution vectors. This extended the size of models which could be solved on a standard workstation. This paper reports on a significant improvement to our earlier work obtained by using an alternative scheme for decomposing the matrix into blocks. We present experimental results for three benchmark models, a Kanban manufacturing system, a cyclic server polling system and a flexible manufacturing system, and analyse the performance of our implementation. In general, we double the speed of numerical solution. We report results for models as large as 216 million states and 2.1 billion transitions on a workstation with 512MB RAM