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