Information Technology Reference
In-Depth Information
applications of various domains, ranging from dynamic fault trees [11,10,12],
architectural description languages such as AADL (Architectural Analysis and
Design Language) [9,15,13,14], generalised stochastic Petri nets [40] and State-
mate [8] to GALS (Globally Asynchronous Locally Synchronous) hardware de-
sign [22,19,23]. The availability of CTMC-based tool support [31] for IMCs has
led to several of these applications. On the other hand, a rich set of algorith-
mic advances for the analysis and minimisation of IMCs have been recently
developed that enable the analysis of large IMCs [49,66]. Whereas so far the
analysis trajectory was restricted to CTMC models obtained from IMCs whose
weak bisimulation quotient is free of nondeterminism, with the work of [66] this
restriction has become obsolete. In addition, recent developments in composi-
tional abstraction techniques for IMCs are promising means to analyse huge,
and even infinite IMCs. This paper provides a survey of IMCs, some of their
recent applications and algorithmic advancements.
Organization of this paper.
Section 2 introduces IMCs, explains their seman-
tics, defines some basic composition operators and considers (bi)simulation.
Section 3 focuses on the analysis of measures-of-interest on IMCs, such as reduc-
tion to CTMCs and reachability probabilities of various kinds. Section 4 reports
on compositional minimisation techniques for IMCs, including recent progress
in aggressive abstraction. Section 5 describes the usage of IMCs as semantical
backbone for industrially relevent formalisms such as fault trees and AADL, as
well as of other modeling formalisms. Finally, section 6 concludes the paper and
gives some propects for future research directions.
2
Interactive Markov Chains
What are IMCs?
IMCs are basically labeled transition systems with a denu-
merable state space, action-labeled transitions, as well as Markovian transitions
that are labeled with rates of exponential distributions. In the remainder of this
paper, we assume the existence of a denumerable set of actions, ranged over by
α
and
β
, and which includes a distinguished action, denoted
τ
.Actions
τ
models
internal, i.e., unobservable activity, whereas all other actions model observable
activities.
Definition 1 (Interactive Markov chain).
An
interactive Markov chain
is
atuple
I
=(
S,
Act
,
−→
,
⇒
,s
0
)
where
-
S
is a nonempty set of states with
initial state
s
0
∈
S
.
-
Act
is a set of actions,
-
−→⊆
S
× Act ×
S
is a set of
interactive
transitions, and
-
⇒⊆
S
×
R
>
0
×
S
is a set of
Markovian
transitions.
α
−−→
We abbreviate (
s, α, s
)
s
and similarly, (
s, λ, s
)
∈→
as
s
∈ ⇒
by
λ
⇒
s
. States are by the type of their outgoing transitions. Let:
s
