Paper Details

A Symbolic Out-of-Core Solution Method for Markov Models
Marta Kwiatkowska, Rashid Mehmood, Gethin Norman and David Parker

Despite much effort state-space explosion problem remains an issue in the analysis of Markov models. Symbolic representation of the state space, for example can result in very compact encoding of the matrices given structure. However, a major obstacle for symbolic methods is the need to store the probability vector(s) explicitly in the 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. 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.