The How and Why of Interactive Markov Chains

H. Hermanns, Joost P. Katoen

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

27 Citations (Scopus)
100 Downloads (Pure)

Abstract

This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees.
Original languageUndefined
Title of host publicationSymposium on Formal Methods for Components and Objects, FMCO 2009
EditorsF.S de Boer, S.H. Bonsangue, M Leuschel
Place of PublicationBerlin
PublisherSpringer
Pages311-337
Number of pages27
ISBN (Print)978-3-642-17070-6
DOIs
Publication statusPublished - 2010

Publication series

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

Keywords

  • IR-73120
  • EWI-18444
  • METIS-271027

Cite this

Hermanns, H., & Katoen, J. P. (2010). The How and Why of Interactive Markov Chains. In F. S. de Boer, S. H. Bonsangue, & M. Leuschel (Eds.), Symposium on Formal Methods for Components and Objects, FMCO 2009 (pp. 311-337). (Lecture Notes in Computer Science; Vol. 6286). Berlin: Springer. https://doi.org/10.1007/978-3-642-17071-3_16
Hermanns, H. ; Katoen, Joost P. / The How and Why of Interactive Markov Chains. Symposium on Formal Methods for Components and Objects, FMCO 2009. editor / F.S de Boer ; S.H. Bonsangue ; M Leuschel. Berlin : Springer, 2010. pp. 311-337 (Lecture Notes in Computer Science).
@inproceedings{93e714e7d6864dcbb514dfad7b6899e9,
title = "The How and Why of Interactive Markov Chains",
abstract = "This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees.",
keywords = "IR-73120, EWI-18444, METIS-271027",
author = "H. Hermanns and Katoen, {Joost P.}",
note = "10.1007/978-3-642-17071-3_16",
year = "2010",
doi = "10.1007/978-3-642-17071-3_16",
language = "Undefined",
isbn = "978-3-642-17070-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "311--337",
editor = "{de Boer}, F.S and S.H. Bonsangue and M Leuschel",
booktitle = "Symposium on Formal Methods for Components and Objects, FMCO 2009",

}

Hermanns, H & Katoen, JP 2010, The How and Why of Interactive Markov Chains. in FS de Boer, SH Bonsangue & M Leuschel (eds), Symposium on Formal Methods for Components and Objects, FMCO 2009. Lecture Notes in Computer Science, vol. 6286, Springer, Berlin, pp. 311-337. https://doi.org/10.1007/978-3-642-17071-3_16

The How and Why of Interactive Markov Chains. / Hermanns, H.; Katoen, Joost P.

Symposium on Formal Methods for Components and Objects, FMCO 2009. ed. / F.S de Boer; S.H. Bonsangue; M Leuschel. Berlin : Springer, 2010. p. 311-337 (Lecture Notes in Computer Science; Vol. 6286).

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

TY - GEN

T1 - The How and Why of Interactive Markov Chains

AU - Hermanns, H.

AU - Katoen, Joost P.

N1 - 10.1007/978-3-642-17071-3_16

PY - 2010

Y1 - 2010

N2 - This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees.

AB - This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees.

KW - IR-73120

KW - EWI-18444

KW - METIS-271027

U2 - 10.1007/978-3-642-17071-3_16

DO - 10.1007/978-3-642-17071-3_16

M3 - Conference contribution

SN - 978-3-642-17070-6

T3 - Lecture Notes in Computer Science

SP - 311

EP - 337

BT - Symposium on Formal Methods for Components and Objects, FMCO 2009

A2 - de Boer, F.S

A2 - Bonsangue, S.H.

A2 - Leuschel, M

PB - Springer

CY - Berlin

ER -

Hermanns H, Katoen JP. The How and Why of Interactive Markov Chains. In de Boer FS, Bonsangue SH, Leuschel M, editors, Symposium on Formal Methods for Components and Objects, FMCO 2009. Berlin: Springer. 2010. p. 311-337. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-17071-3_16