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

Despite 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.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Marta Z. Kwiatkowska, Rashid Mehmood, Gethin Norman, David Parker
• Keywords: Considerable Effort, ENTCS 2002, Probability Vector, State-space Explosion Problem