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

    38 Citations (Scopus)
    80 Downloads (Pure)

    Abstract

    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
    PublisherSpringer
    Pages8-23
    Number of pages15
    ISBN (Electronic)978-3-642-28891-3
    ISBN (Print)978-3-642-28890-6
    DOIs
    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
    Volume7226
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference4th International Symposium on NASA Formal Methods, NFM 2012
    Abbreviated titleNFM
    CountryUnited States
    CityNorfolk
    Period3/04/125/04/12

      Fingerprint

    Keywords

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

    Cite this

    Guck, D., Han, T., Katoen, J-P., & Neuhäußer, M. R. (2012). Quantitative timed analysis of interactive Markov chains. In A. E. Goodloe, & S. Person (Eds.), NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings (pp. 8-23). (Lecture Notes in Computer Science; Vol. 7226). Berlin: Springer. https://doi.org/10.1007/978-3-642-28891-3_4