Sciweavers

ENTCS
2002

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

13 years 3 months ago
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.
Marta Z. Kwiatkowska, Rashid Mehmood, Gethin Norma
Added 18 Dec 2010
Updated 18 Dec 2010
Type Journal
Year 2002
Where ENTCS
Authors Marta Z. Kwiatkowska, Rashid Mehmood, Gethin Norman, David Parker
Comments (0)