The How and Why of Interactive Markov Chains

H. Hermanns, Joost P. Katoen

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    31 Citations (Scopus)
    817 Downloads (Pure)


    This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees.
    Original languageUndefined
    Title of host publicationSymposium on Formal Methods for Components and Objects, FMCO 2009
    EditorsF.S de Boer, S.H. Bonsangue, M Leuschel
    Place of PublicationBerlin
    Number of pages27
    ISBN (Print)978-3-642-17070-6
    Publication statusPublished - 2010
    EventSymposium on Formal Methods for Components and Objects, FMCO 2009 - Eindhoven, the Netherlands
    Duration: 4 Nov 20096 Nov 2009

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    ConferenceSymposium on Formal Methods for Components and Objects, FMCO 2009
    Other4 - 6 November 2009


    • IR-73120
    • EWI-18444
    • METIS-271027

    Cite this