Information Technology Reference
In-Depth Information
The above definition is obtained by factoring out divergence from Clause 1 in
Definition
6.20
and conservatively extends Definition 5.4 to compare processes that
might not be finite. We first note that the relation
S
FS
is not interesting for infinitary
FS
)
†
is not a transitive relation for those processes.
processes since its lifted form (
Example 6.21
C
onsider the p
ro
cess defined by the following two transitions:
˄
−ₒ
˄
−ₒ
t
0
(
0
1
/
2
↕
t
1
) and
t
1
t
1
. We compar
e
state
t
0
with state
s
in Example
6.1
5
˄
−ₒ
S
1
and have
th
at
t
0
FS
s
. The tr
an
sition
t
0
(
0
1
/
2
↕
t
1
) can be matched by
s
⃒
2
0
FS
)
†
S
1
S
because (
0
1
/
2
↕
t
1
)(
2
0
by noticing that
t
1
FS
ʵ
.
S
FS
It also holds that
s
0
beca
us
e the relation
{
(
s
,
0
), (
0
,
0
)
}
is a simple fai
lu
re
˄
−ₒ
k
(
0
k
2
↕
s
) for any
k
≥
simulation. The transition
s
2 is matched by
0
⃒
0
.
FS
Howe
v
er, we do not have
t
0
0
. The only cand
id
ate to simulate
t
he transition
˄
−ₒ
FS
)
†
S
t
0
(
0
1
/
2
↕
t
1
)is
0
⃒
0
, but we do not have (
0
2
↕
t
1
)(
0
because the
divergent state
t
1
cann
ot
be simulated by
0
.
Therefore, we have
t
0
(
FS
)
†
s
(
FS
)
†
FS
)
†
0
but not
t
0
(
0
, thus transitivity of
FS
)
†
fails. Here the state
s
is not finitely branching. As a matter of fact,
transitivity of (
S
the relation (
FS
)
†
also fails for finitely branching but infinite state processes.
Consider an infinite state pLTS consisting of a collection of states
s
k
for
k
S
≥
2
such that
˄
−ₒ
s
k
0
k
2
↕
s
k
+
1
.
(6.22)
This pLTS
is
obtained from that
in
Example
6.5
by replacing
a
.
0
with
0
.
One can
check that
t
0
(
FS
)
†
FS
)
†
FS
)
†
s
2
(
0
but we already know that
t
0
(
0
does not
FS
)
†
.
If we restrict our attention to finitary processes, then
S
hold. Again, we loose the transitivity of (
S
FS
provides a simpler
characterisation of failure similarity.
Theorem 6.12 (Equivalence of Failure- and Simple Failure Similarity)
For fini-
tary distributions ʔ
,
ʘ
S
∈
D
sub
(
S
)
inapLTS
S
,
Act
˄
,
ₒ
we have ʔ
FS
ʘ if and
e
only if ʔ
FS
ʘ.
ʱ
−ₒ
ʱ
−ₒ
A
A
ʔ
implies
s
ʔ
and
s
Proof
Because
s
−ₒ
implies
s
⃒
−ₒ
it is trivial
e
e
S
that
FS
satisfies the conditions of Definition
6.21
, so that
FS
ↆ
FS
.
S
FS
For the other direction,
we need to show that
satisfies Clause 1 of
Definition
6.20
with
ʱ
=
˄
, that is
ʔ
then there is some
ʘ
∈
D
sub
(
S
) with
ʘ
ʘ
and
S
if
s
FS
ʘ
and
s
⃒
⃒
FS
)
†
ʘ
.
ʔ
(
S
FS
Once we have this, the relation
clearly satisfies both clauses of Definition
6.20
,
FS
e
FS
.
ↆ
so that we have
FS
ʘ
and that
s
ʔ
where—for the moment—we assume
So suppose that
s
⃒
|
ʔ
|=
1. Referring to Definition
6.4
, there must be
ʔ
k
,
ʔ
k
and
ʔ
k
for
k
≥
0 such
Search WWH ::
Custom Search