A Symbolic Out-of-Core Solution Method for Markov Models

AbstractDespite considerable effort, the state-space explosion problem remains an issue in the analysis of Markov models. Given structure, symbolic representations can result in very compact encoding of the models. However, a major obstacle for symbolic methods is the need to store the probability vector(s) explicitly in main memory. In this paper, we present a novel algorithm which relaxes these memory limitations by storing the probability vector on disk. The algorithm has been implemented using an MTBDD-based data structure to store the matrix and an array to store the vector. We report on experimental results for two benchmark models, a Kanban manufacturing system and a flexible manufacturing system, with models as large as 133 million states