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

H. Hermanns, Marta Kwiatkowska, Gethin Norman, David Parker, Markus Siegle

    Research output: Contribution to journalArticleAcademic

    45 Citations (Scopus)
    18 Downloads (Pure)

    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.
    Original languageEnglish
    Pages (from-to)23-67
    JournalJournal of logic and algebraic programming
    Volume56
    Issue number1-2
    DOIs
    Publication statusPublished - 2003

    Keywords

    • Markov Chain
    • Binary Decision Diagrams
    • Performability analysis
    • Markov decision process
    • Multi-terminal binary decision diagrams
    • Model Checking

    Fingerprint Dive into the research topics of 'On the use of MTBDDs for performability analysis and verification of stochastic systems'. Together they form a unique fingerprint.

  • Cite this