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

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

PDF
Restricted to UT campus only: Request a copy
755Kb

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:	Formal Methods and Tools (FMT)
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

Show download statistics for this publication

Repository Staff Only: item control page