www.prismmodelchecker.org
[KMNP02] Marta Kwiatkowska, Rashid Mehmood, Gethin Norman and David Parker. A Symbolic Out-of-Core Solution Method for Markov Models. In Proc. Workshop on Parallel and Distributed Model Checking (PDMC'02), volume 68.4 of ENTCS. August 2002. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (131 KB)  pdf pdf (491 KB)  bib bib
Notes: ENTCS is available at www.sciencedirect.com/science/journal/15710661.
Links: [Google] [Google Scholar]
Abstract. 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.

Publications