Notes:
ENTCS is available at www.sciencedirect.com/science/journal/15710661.
|
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.
|