A tutorial on interactive Markov chains

Florian Arnold, Daniel Gebler, Dennis Guck, Hassan Hatefi

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

    334 Downloads (Pure)

    Abstract

    Interactive Markov chains (IMCs) constitute a powerful sto- chastic model that extends both continuous-time Markov chains and labelled transition systems. IMCs enable a wide range of modelling and analysis techniques and serve as a semantic model for many industrial and scientific formalisms, such as AADL, GSPNs and many more. Applications cover various engineering contexts ranging from industrial system-on-chip manufacturing to satellite designs. We present a survey of the state-of-the-art in modelling and analysis of IMCs. We cover a set of techniques that can be utilised for compositional modelling, state space generation and reduction, and model checking. The significance of the presented material and corresponding tools is highlighted through multiple case studies.
    Original languageUndefined
    Title of host publicationStochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems
    EditorsA.K.I. Remke, Anne Katharina Ingrid Remke, M.I.A. Stoelinga, Mariëlle Ida Antoinette Stoelinga
    Place of PublicationBerlin
    PublisherSpringer
    Pages26-66
    Number of pages41
    ISBN (Print)978-3-662-45488-6
    DOIs
    Publication statusPublished - Jun 2014
    EventStochastic Model Checking: Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems - Vahrn, Italy
    Duration: 22 Oct 201226 Oct 2012

    Publication series

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

    Other

    OtherStochastic Model Checking
    CountryItaly
    CityVahrn
    Period22/10/1226/10/12

    Keywords

    • stochastic
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/318003
    • EWI-25350
    • IR-93332
    • Interactive Markov chains
    • Abstraction
    • Model Checking
    • METIS-309682
    • logic

    Cite this