A tutorial on interactive Markov chains

Florian Arnold; Daniel Gebler; Dennis Guck; Hassan Hatefi

doi:10.1007/978-3-662-45489-3_2

A tutorial on interactive Markov chains

Florian Arnold, Daniel Gebler, Dennis Guck, Hassan Hatefi

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

409 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 language	Undefined
Title of host publication	Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems
Editors	A.K.I. Remke, Anne Katharina Ingrid Remke, M.I.A. Stoelinga, Mariëlle Ida Antoinette Stoelinga
Place of Publication	Berlin
Publisher	Springer
Pages	26-66
Number of pages	41
ISBN (Print)	978-3-662-45488-6
DOIs	https://doi.org/10.1007/978-3-662-45489-3_2
Publication status	Published - Jun 2014
Event	Stochastic Model Checking: Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems - Vahrn, Italy Duration: 22 Oct 2012 → 26 Oct 2012

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	8453
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	Stochastic Model Checking
Country/Territory	Italy
City	Vahrn
Period	22/10/12 → 26/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

Access to Document

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

http://eprints.eemcs.utwente.nl/secure2/25350/02/chp%253A10.1007%252F978-3-662-45489-3_2.pdf

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). Springer. https://doi.org/10.1007/978-3-662-45489-3_2

Arnold, Florian ; Gebler, Daniel ; Guck, Dennis et al. / 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 ;; null ; Conference date: 22-10-2012 Through 26-10-2012",

year = "2014",

month = jun,

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 et al.

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 proceeding › Conference contribution › Academic › peer-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

Y2 - 22 October 2012 through 26 October 2012

ER -