Quantitative timed analysis of interactive Markov chains

Dennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer

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

    40 Citations (Scopus)
    100 Downloads (Pure)


    This paper presents new algorithms and accompanying tool support for analyzing interactive Markov chains (IMCs), a stochastic timed 1 1/2-player game in which delays are exponentially distributed. IMCs are compositional and act as semantic model for engineering formalisms such as AADL and dynamic fault trees. We provide algorithms for determining the extremal expected time of reaching a set of states, and the long-run average of time spent in a set of states. The prototypical tool Imca supports these algorithms as well as the synthesis of ε-optimal piecewise constant timed policies for timed reachability objectives. Two case studies show the feasibility and scalability of the algorithms.
    Original languageEnglish
    Title of host publicationNASA Formal Methods
    Subtitle of host publication4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings
    EditorsAlwyn E. Goodloe, Suzette Person
    Place of PublicationBerlin
    Number of pages15
    ISBN (Electronic)978-3-642-28891-3
    ISBN (Print)978-3-642-28890-6
    Publication statusPublished - Apr 2012
    Event4th International Symposium on NASA Formal Methods, NFM 2012 - Norfolk, United States
    Duration: 3 Apr 20125 Apr 2012
    Conference number: 4

    Publication series

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


    Conference4th International Symposium on NASA Formal Methods, NFM 2012
    Abbreviated titleNFM
    Country/TerritoryUnited States


    • expected time
    • interactive Markov chain
    • EWI-22672
    • METIS-296168
    • Reachability
    • Quantitative analysis
    • IR-83449
    • Long-run average


    Dive into the research topics of 'Quantitative timed analysis of interactive Markov chains'. Together they form a unique fingerprint.

    Cite this