Information Technology Reference
In-Depth Information
interactive transitions by a single such transition. This acts exactly the same as
for labeled transition systems. The treatment of Markovian transitions is a bit
more involved, however. First, let us remark that the probability distribution
of a sequence of exponential distributions is not an exponential distribution but
constitutes a phase-type distribution. Therefore, it is not possible to define a
weak version of the transition relation
⇒
as is done for weak bisimulation in
labeled transition systems. The solution is to demand that Markovian transitions
have to be mimicked in the strong sense, while they can be preceded and/or fol-
lowed by arbitrary sequences of internal interactive transitions. The treatment of
sequences of internal interactive transitions is similar to that of branching bisim-
ulation [62]. As for strong bisimulation, rate equality is only required if a state
has no outgoing internal transitions (maximal progress). Let
s
τ
∗
s
denote
that
s
can be reached from
s
solely via zero or more
τ
-transitions; in particular
s
−−→
τ
∗
−−→
s
for any state
s
. For state
s
,action
α
and
C
⊆
S
,let
W
(
s, α, C
)=1if
τ
∗
τ
∗
α
{
s
∈
C
|
s
−−→
−−→
−−→
s
}
and only if
is non-empty.
Definition 6 (Weak bisimulation).
Let
I
=(
S,
Act
,
−→
,
⇒
,s
0
)
be an IMC.
An equivalence relation
R
⊆
S
×
S
is a
weak bisimulation
on
I
if for any
(
s, t
)
∈
R
and equivalence class
C
∈
S/R
, the following holds:
1. for any
α
∈
Act
,
W
(
s, α, C
)=
W
(
t, α, C
)
,and
τ
∗
s
and
s
τ
τ
∗
t
and
t
τ
2.
s
−−→
−−→
/
implies
t
−−→
−−→
/
and
R
(
s
,C
)=
R
(
t
,C
)
for some
t
∈
S
.
States
s
and
s
are weakly bisimilar, denoted
s
s
,if
(
s, s
)
≈
∈
R
for some weak
bisimulation
R
.
Theorem 2.
[35]
≈
is a congruence wrt. parallel composition and hiding.
Bisimulation relations are equivalences requiring two bisimilar states to exhibit
identical stepwise behaviour. On the contrary, simulation relations [46] are pre-
orders on the state space requiring that whenever
s
s
(
s
simulates
s
) state
s
can mimic all stepwise behaviour of
s
; the converse is not guaranteed, so state
s
may perform steps that cannot be matched by
s
.
Definition 7 (Strong simulation).
For IMC
I
=(
S,
Act
,
−→
,
⇒
,s
0
)
,
R
⊆
S
×
S
is a
simulation relation
, iff for any
(
s, t
)
∈
R
it holds:
and
s
∈
α
s
implies
t
α
t
and
(
s
,t
)
1. for any
α
∈ Act
S
,
s
−−→
−−→
∈
R
for some
t
∈
S
τ
−−→
2.
s
/
implies
E
(
s
)
≤
E
(
t
)
τ
−−→
)
and
μ
=
P
(
s
,
3.
s
/
implies for distributions
μ
=
P
(
s,
·
·
)
there exists
[0
,
1]
such that for all
u, u
∈
Δ
:
S
×
S
→
S
:
(a)
Δ
(
u, u
)
>
0=
(
u, u
)
(c)
Δ
(
S, u
)=
μ
(
u
)
⇒
∈
R
(b)
Δ
(
u, S
)=
μ
(
u
)
s
if (
s, s
)
II
for IMCs
We write
s
∈
R
for some simulation
R
and
I
I
.
The last constraint requires the existence of a weight function
Δ
that basically
I
with initial states
s
0
and
s
0
,if
s
0
s
0
in the disjoint union of
and
I
and
