Information Technology Reference
In-Depth Information
˄
−ₒ⃒
ʓ
⃒
ʵ
,
(a)
s
|
A
t
⃒
˄
−ₒ⃒
†
ʨ
.
(b)
ʘ
|
A
t
⃒
ʨ
and
ʓ
R
˄
−ₒ
p
ʓ
By Lemma
6.29
, there are
ʔ
,
ʓ
ʔ
and
ʔ
|
A
t
∈
D
sub
(
S
) with
s
⃒
⃒
ʵ
.
FS
coincides with
FS
and
e
FS
by Lemma
6.26
and
Since for finitary processes
FS
)
†
ʘ
.
Theorem
6.12
, there must be a
ʘ
∈
D
sub
(
S
) such that
ʘ
ʘ
and
ʔ
(
C
⃒
˄
−ₒ⃒
ʨ
for some
ʨ
such that
ʓ
By Proposition
6.10
,wehave
ʘ
|
A
t
⃒
†
ʨ
.
R
˄
−ₒ
˄
−ₒ⃒
ʔ
|
A
t
ʘ
|
A
t
Now,
s
|
A
t
⃒
ʓ
⃒
ʵ
and
ʘ
|
A
t
⃒
⃒
ʨ
with
†
ʨ
, which had to be shown.
Therefore, we have shown that
ʓ
R
FS
. Now let us focus our attention on the
statement of the proposition, which involves
R
ↆ
FS
.
FS
ʔ
. By Proposition
6.7
, this means that there is some
ʘ
match
Suppose
ʘ
such
e
FS
)
†
⃒
ʘ
match
ʘ
match
. By Theorem
6.12
and Lemma
6.26
,we
that
ʘ
and
ʔ
(
FS
)
†
ʘ
match
. Then Lemma
6.27
(5) yields (
ʔ
†
C
(
ʘ
match
have
ʔ
(
|
A
Φ
)
R
|
A
Φ
). There-
FS
)
†
C
(
ʘ
match
e
FS
)
†
(
ʘ
match
fore, we have (
ʔ
|
A
Φ
)
by Lemma
6.26
and Theorem
6.12
. By using Lemma
6.27
(1), we also have that
(
ʘ
|
A
Φ
)(
|
A
Φ
), that is, (
ʔ
|
A
Φ
)(
(
ʘ
match
|
A
Φ
)
⃒
|
A
Φ
), which had to be established according to Proposi-
tion
6.7
.
e
FS
S
In the proof of Proposition
6.11
, we use the characterisation of
as
FS
,
S
FS
which assumes the pLTS to be finitary. In general, the relation
is not closed
under parallel composition.
Example 6.23
We use a modification of the infinite state pLTS's in Example
6.5
that as before has states
s
k
with
k
≥
2, but we add an extra
a
-looping state
s
a
to give
all together the system
˄
−ₒ
a
−ₒ
s
a
.
for
k
≥
2
s
k
(
s
a
k
2
↕
s
k
+
1
)
and
s
a
1
FS
There is a failure simulation so that
s
k
(
s
a
k
↕
0
) because from state
s
k
the
˄
−ₒ
transition
s
k
(
s
a
k
2
↕
s
k
+
1
) can be matched by a transition to (
s
a
k
2
↕
(
s
a
1
k
+
↕
0
))
1
that simplifies to just (
s
a
k
↕
0
) again, that is, a sufficient simulating transition would
be the identity instance of
.
Now
s
2
|
{
a
}
s
a
wholly
di
verges even
th
ough
s
2
itself does not, and (recall from
above)wehave
s
2
⃒
S
FS
(
s
a
2
↕
0
). Yet (
s
a
2
↕
0
)
|
{
a
}
s
a
does not diverge, and therefore
S
FS
s
2
|
{
a
}
s
a
|
{
a
}
S
a
.
Note that this counter-example does not go through if we
us
e failure similarity
(
S
a
2
↕
0
)
e
S
e
FS
instead of simple failure similarity
FS
, since
s
2
FS
(
s
a
2
↕
0
)—the former
has the transition
s
2
⃒
s
a
2
↕
ʵ
, which cannot be matched by
s
a
2
↕
0
.
Proposition 6.12 (Precongruence)
In a finitary pLTS, if P
FS
Q then it holds
FS
ʱ.Q for any ʱ
∈
Act
, and similarly if P
1
FS
Q
1
and P
2
FS
Q
2
then
that ʱ.P
P
1
P
2
FS
Q
1
,
p
↕
|
A
.
Q
2
for
being any of the operators
,
and
Search WWH ::
Custom Search