On the use of MTBDDs for performability analysis and verification of stochastic systems

Share/Save/Bookmark

Hermanns, Holger and Kwiatkowska, Marta and Norman, Gethin and Parker, David and Siegle, Markus (2003) On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming, 56 (1-2). pp. 23-67. ISSN 1567-8326

[img] PDF
Restricted to UT campus only
: Request a copy
773kB
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.
Item Type:Article
Copyright:© 2003 Elsevier
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/75029
Official URL:http://dx.doi.org/10.1016/S1567-8326(02)00066-8
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page