A tutorial on interactive Markov chains

Florian Arnold, Daniel Gebler, Dennis Guck, Hassan Hatefi

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

307 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

Arnold, F., Gebler, D., Guck, D., & Hatefi, H. (2014). A tutorial on interactive Markov chains. In A. K. I. Remke, A. K. I. Remke, M. I. A. Stoelinga, & M. I. A. Stoelinga (Eds.), Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems (pp. 26-66). (Lecture Notes in Computer Science; Vol. 8453). Berlin: Springer. https://doi.org/10.1007/978-3-662-45489-3_2
Arnold, Florian ; Gebler, Daniel ; Guck, Dennis ; Hatefi, Hassan. / A tutorial on interactive Markov chains. Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. editor / A.K.I. Remke ; Anne Katharina Ingrid Remke ; M.I.A. Stoelinga ; Mariëlle Ida Antoinette Stoelinga. Berlin : Springer, 2014. pp. 26-66 (Lecture Notes in Computer Science).
@inproceedings{d9f9ed3d3b7047e5b391c0cc367aab17,
title = "A tutorial on interactive Markov chains",
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.",
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",
author = "Florian Arnold and Daniel Gebler and Dennis Guck and Hassan Hatefi",
note = "Foreground = 25{\%} ; Type of activity = publication in tutorial volume ; Main leader = UT ; Type of audience = Scientific community ; Size of audience = n.a. ; Countries addressed = international ;",
year = "2014",
month = "6",
doi = "10.1007/978-3-662-45489-3_2",
language = "Undefined",
isbn = "978-3-662-45488-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "26--66",
editor = "A.K.I. Remke and Remke, {Anne Katharina Ingrid} and M.I.A. Stoelinga and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
booktitle = "Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems",

}

Arnold, F, Gebler, D, Guck, D & Hatefi, H 2014, A tutorial on interactive Markov chains. in AKI Remke, AKI Remke, MIA Stoelinga & MIA Stoelinga (eds), Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. Lecture Notes in Computer Science, vol. 8453, Springer, Berlin, pp. 26-66, Stochastic Model Checking, Vahrn, Italy, 22/10/12. https://doi.org/10.1007/978-3-662-45489-3_2

A tutorial on interactive Markov chains. / Arnold, Florian; Gebler, Daniel; Guck, Dennis; Hatefi, Hassan.

Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. ed. / A.K.I. Remke; Anne Katharina Ingrid Remke; M.I.A. Stoelinga; Mariëlle Ida Antoinette Stoelinga. Berlin : Springer, 2014. p. 26-66 (Lecture Notes in Computer Science; Vol. 8453).

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

TY - GEN

T1 - A tutorial on interactive Markov chains

AU - Arnold, Florian

AU - Gebler, Daniel

AU - Guck, Dennis

AU - Hatefi, Hassan

N1 - Foreground = 25% ; Type of activity = publication in tutorial volume ; Main leader = UT ; Type of audience = Scientific community ; Size of audience = n.a. ; Countries addressed = international ;

PY - 2014/6

Y1 - 2014/6

N2 - 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.

AB - 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.

KW - stochastic

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/318003

KW - EWI-25350

KW - IR-93332

KW - Interactive Markov chains

KW - Abstraction

KW - Model Checking

KW - METIS-309682

KW - logic

U2 - 10.1007/978-3-662-45489-3_2

DO - 10.1007/978-3-662-45489-3_2

M3 - Conference contribution

SN - 978-3-662-45488-6

T3 - Lecture Notes in Computer Science

SP - 26

EP - 66

BT - Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems

A2 - Remke, A.K.I.

A2 - Remke, Anne Katharina Ingrid

A2 - Stoelinga, M.I.A.

A2 - Stoelinga, Mariëlle Ida Antoinette

PB - Springer

CY - Berlin

ER -

Arnold F, Gebler D, Guck D, Hatefi H. A tutorial on interactive Markov chains. In Remke AKI, Remke AKI, Stoelinga MIA, Stoelinga MIA, editors, Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems. Berlin: Springer. 2014. p. 26-66. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-662-45489-3_2