Reference

[HermannsMS99] Hermanns, H; Meyer-Kayser, J and Siegle, M Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. In NSMC, pages 188-207, 1999.
Downloads: bibAbstract. Binary Decision Diagrams (BDDs) have gained high attention in the context of design and verification of digital circuits. They have successfully been employed to encode very large state spaces in an efficient, symbolic way. Multi terminal BDDs (MTBDDs) are generalisations of BDDs from Boolean values to values of any finite domain. In this paper, we investigate the applicability of MTBDDs to the symbolic representation of continuous time Markov chains, derived from high-level formalisms, such as queueing networks or process algebras. Based on this data structure, we discuss iterative solution algorithms to compute the steady-state probability vector that work in a completely symbolic way. We highlight a number of lessons learned, using a set of small examples.