[HKN+03]
H. Hermanns, M. Kwiatkowska, G. Norman, D. Parker and M. Siegle.
On the use of MTBDDs for Performability Analysis and Verification of Stochastic Systems.
Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, 56, pages 23-67, Elsevier.
June 2003.
[ps.gz]
[pdf]
[bib]
|
Abstract.
This paper describes how to employ Multi-Terminal Binary
Decision Diagrams (MTBDDs)
for the construction and analysis of a general class of models that
exhibit stochastic, probabilistic and non-deterministic behaviour. It
is shown how the notorious problem of state space explosion can be
circumvented by compositionally constructing symbolic (i.e.
MTBDD-based) representations of complex systems from small-scale
components. We emphasise, however, that compactness of the
representation can only be achieved if heuristics are applied with
insight into the structure of the system under investigation. We
report on our
experiences concerning compact representation,
performance analysis and
verification of performability properties.
|