|
David ParkerLecturerSchool of Computer Science University of Birmingham Edgbaston, Birmingham, B15 2TT Email: d.a.parker@cs.bham.ac.uk Tel: +44 (0) 121 41 47264 Office: 107 Office hours: Wed 12.30-1.30, Thu 3-4 |
<< NEWS >>
|
|
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.
|