The How and Why of Interactive Markov Chains

11 years 3 months ago
The How and Why of Interactive Markov Chains
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 aggrestraction 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.
Holger Hermanns, Joost-Pieter Katoen
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where FMCO
Authors Holger Hermanns, Joost-Pieter Katoen
Comments (0)