The How and Why of Interactive Markov Chains

Share/Save/Bookmark

Hermanns, Holger and Katoen, Joost-Pieter (2010) The How and Why of Interactive Markov Chains. In: Symposium on Formal Methods for Components and Objects, FMCO 2009, 4 - 6 November 2009, Eindhoven, the Netherlands.

[img]
Preview
PDF
2183Kb
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.
Item Type:Conference or Workshop Item
Copyright:© 2010 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/73120
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page