Links:
[Google]
[Google Scholar]
|
Abstract.
In recent years, disk-based approaches to the analysis of Markov
models have proved to be an effective method of combating the
state space explosion problem. Coupled with parallel and symbolic techniques,
disk-based methods have demonstrated impressive performance
for numerical solution. In an earlier paper, we presented a novel, symbolic
out-of-core algorithm which used MTBDD-based data structures
for matrix storage in RAM and disk-based storage for solution vectors.
This extended the size of models which could be solved on a standard
workstation. This paper reports on a significant improvement to our
earlier work obtained by using an alternative scheme for decomposing the
matrix into blocks. We present experimental results for three benchmark
models, a Kanban manufacturing system, a cyclic server polling system
and a flexible manufacturing system, and analyse the performance of our
implementation. In general, we double the speed of numerical solution.
We report results for models as large as 216 million states and 2.1 billion
transitions on a workstation with 512MB RAM.
|