Information Technology Reference
In-Depth Information
The How and Why
of Interactive Markov Chains
Holger Hermanns
1
,
2
and Joost-Pieter Katoen
3
,
4
1
Dependable Systems and Software, Universitat des Saarlandes, Germany
2
VASY Team, INRIA Grenoble - Rhone-Alpes, France
3
MOVES Group, RWTH Aachen University, Germany
4
FMT Group, University of Twente, The Netherlands
Abstract.
This paper reviews the model of interactive Markov chains
(IMCs, for short), an extension of labelled transition systems with expo-
nentially delayed transitions. We show that IMCs are closed under paral-
lel composition and hiding, and show how IMCs can be compositionally
aggregated prior to analysis by e.g., bisimulation minimisation or aggres-
sive 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 pro-
cess algebras and generalised stochastic Petri nets and can be used for
engineering formalisms such as AADL and dynamic fault trees.
1
Introduction
Designing correct and ecient distributed systems is a dicult task. As a chal-
lenging case take an offshore wireless sensor network that is designed to identify
tsunami situations and relay tsunami warnings [61]. Once fully operational, will
this network help to save human life? Can we guarantee its correct functioning,
or is there a risk of failure at the very moment when it is seriously needed?
To say it with Barendregt, correct systems for information processing are more
valuable than gold [4]. In the tsunami context, a correct system is one that
guarantees certain time bounds for the tasks it needs to perform, even in the
presence of message losses or component failures. Correctness, performance and
dependability are intertwined here, and so they are in many other contemporary
IT applications. These applications ask for quantitative correctness properties
such as: The frequency of system downtime is below one hour per year, and
packets arrive timely in at least 99.96% of all cases.
This research has been funded by NWO under grant 612
.
000
.
420 (QUPES) and
DFG-NWO grant Dn 63-257 (ROCKS), by the EU under FP7-ICT-2007-1 grant
214755 (Quasimodo), and by the German Research Council (DFG) as part of the
Transregional Collaborative Research Center “Automatic Verification and Analysis
of Complex Systems” SFB/TR 14 AVACS.
