Information Technology Reference
In-Depth Information
e
Proposition 6.8
The relation
FS
is convex.
[0, 1] for
i
∈
I
, with
i
∈
I
p
i
=
e
Proof
Suppose
s
FS
ʘ
i
and
p
i
∈
1. We need to
FS
i
∈
I
p
i
·
e
show that
s
ʘ
i
.
ʱ
⃒
ʱ
⃒
ʔ
, then there exist
ʘ
i
ʘ
i
If
s
for each
i
∈
I
such that
ʘ
i
and
FS
)
†
ʘ
i
. By Corollary
6.7
and Theorem
6.4
, we obtain that
i
∈
I
p
i
·
ʱ
⃒
ʔ
(
e
ʘ
i
i
∈
I
p
i
·
FS
)
†
i
∈
I
p
i
·
ʘ
i
and
ʔ
(
e
ʘ
i
.
A
A
ʘ
i
If
s
⃒
−ₒ
for some
A
ↆ
Act
, then
ʘ
i
⃒
−ₒ
for all
i
∈
I
. By definition
we have
i
∈
I
p
i
·
ʘ
i
. Theorem
6.5
(i) yields
i
∈
I
p
i
·
ʘ
i
⃒
i
∈
I
p
i
·
ʘ
i
.
So we have checked that
s
A
−ₒ
FS
i
∈
I
p
i
·
ʘ
i
. It follows that
e
e
FS
is convex.
e
FS
)
†
Proposition 6.9
The relation
(
ↆ
D
sub
(
S
)
×
D
sub
(
S
)
is reflexive and
transitive.
e
Proof
Reflexivity is easy; it relies on the fact that
s
FS
s
for every state
s
.
e
e
FS
)
†
For transitivity, we first show that
FS
·
(
is a failure simulation. Suppose
ʱ
⃒
ʱ
⃒
FS
)
†
e
e
ʔ
, then there is a
ʘ
such that
ʘ
ʘ
that
s
FS
ʘ
(
Φ
.If
s
ʱ
⃒
FS
)
†
and
ʔ
(
e
ʘ
. By Lemma
6.21
, there exists a
Φ
such that
Φ
Φ
and
e
FS
)
†
Φ
. Hence,
ʔ
(
e
FS
)
†
e
FS
)
†
Φ
. By Lemma
6.3
we know that
ʘ
(
·
(
e
FS
)
†
e
FS
)
†
e
FS
e
FS
))
†
(
·
(
=
(
·
(
(6.21)
Therefore, we obtain
ʔ
(
e
FS
e
FS
)
†
)
†
Φ
.
·
(
A
A
A
If
s
⃒
−ₒ
for some
A
ↆ
Act
, then
ʘ
⃒
−ₒ
and hence
Φ
⃒
−ₒ
by
applying Lemma
6.22
.
So we established that
FS
)
†
e
e
e
FS
·
(
ↆ
FS
. It now follows from the monotonicity
FS
)
†
FS
)
†
FS
)
†
.
e
e
e
of the lifting operation and (
6.21
) that (
·
(
ↆ
(
6.6.2
A Simple Failure Similarity for Finitary Processes
Here, we present a simpler characterisation of failure similarity, valid when consider-
ing finitary processes only. It is in terms of this characterisation that we will establish
soundness and completeness of the failure simulation preorder with respect to the
must testing preorder; consequently we have these results for finitary processes only.
Definition 6.21 (Simple Failure Similarity)
Let
F
be the function on
S
×
D
sub
(
S
)
such that for any binary relation
R
∈
S
×
D
sub
(
S
), state
s
and subdistribution
ʘ
,if
s
F
(
R
)
ʘ
then
1. whenever
s
⃒
ʵ
then also
ʘ
⃒
ʵ
, otherwise
ʱ
−ₒ
ʱ
⃒
ʔ
, for some
ʱ
Act
˄
, then there is a
ʘ
with
ʘ
ʘ
and
2. whenever
s
∈
†
ʘ
and
3. whenever
s
ʔ
R
A
A
−ₒ
then
ʘ
⃒
−ₒ
.
S
FS
Let
be the greatest fixed point of
F
.
Search WWH ::
Custom Search