Information Technology Reference
In-Depth Information
Proof
We reason as follows.
P
S
Q
implies
[
P
|
Act
T
]
S
[
Q
|
Act
T
]
the counterpart of Lemma
6.30
for simulation
implies
V
([
P
|
Act
T
])
≤
Ho
V
([
Q
|
Act
T
])
[
·
]is
ˉ
-respecting; Lemma
6.46
d
(
T
,
P
)
d
(
T
,
Q
)
iff
A
≤
Ho
A
Definition
6.24
iff
P
pmay
Q.
Definition
6.11
6.8.2
Completeness
Let
by skipping the
div
and
ref
(
X
) clauses. In other words, the
formulae are exactly the same as those in the logic for characterising the simulation
preorder in Sect. 5.6. The semantic interpretation is different now because the weak
transition relation
˄
L
be the subclass of
F
⃒
used there has been replaced in this chapter by a more general
L
Q
just when [[
P
]]
form
⃒
given in Definition
6.4
. We continue to write
P
|=
˕
implies [[
Q
]]
.
We have the counterparts of Theorems
6.16
and
6.17
, with similar proofs.
|=
˕
for all
˕
∈
L
L
ʘ if and only if ʔ
Theorem 6.19
In a finitary pLTS ʔ
S
ʘ.
pmay
ʘ then ʔ
L
ʘ.
Theorem 6.20
If ʔ
Corollary 6.14
Suppose P and Q are finitary
r
pCSP
processes. If P
pmay
Q then
P
S
Q.
Proof
pmay
Q
then
P
S
Q
.
Theorem 4.7 says that
ʩ
-testing is reducible to scalar testing. So the required result
follows.
From Theorems
6.19
and
6.20
we know that if
P
As one would expect, the completeness result in Corollary
6.14
would fail for
infinitary processes.
Example 6.26
Consider the state
s
2
that we saw in Example
6.5
. It turns out that
˄.
(
0
2
↕
a.
0
)
pmay
s
2
However, we do not have
˄.
(
0
2
↕
a.
0
)
s
s
2
because the transition
˄
−ₒ
˄.
(
0
2
↕
a.
0
)
(
0
2
↕
a.
0
)
cannot be matched by a transition from
s
2
as there is no
full distribution ʔ
such that
s
2
⃒
ʔ
and (
0
2
↕
a.
0
)(
s
)
†
ʔ
.
Search WWH ::
Custom Search