Information Technology Reference
In-Depth Information
Proof
The next two sections are devoted to proving the converse of Theorems
5.2
and
5.3
.
That is, we will establish:
Similar to the proof of Theorem
5.2
, using (
5.10
)-(
5.12
).
Theorem 5.4
Let P and Q be
pCSP
processes.
•
P
pmay
Q implies P
S
Q and
•
P
FS
Q.
Because of Theorem 4.7, it will suffice to show that
pmust
Q implies P
pmay
Q
implies
P
•
P
S
Q
and
pmust
Q
implies
P
FS
Q
.
This shift from scalar testing to vector-based testing is motivated by the fact that
the latter enables us to use more informative tests, allowing us to discover more
intensional properties of the processes being tested.
The crucial characteristics of
•
P
needed for the above implications are summarised
in Lemmas
5.9
and
5.10
. For convenience of presentation, we write
ˉ
for the vector
in [0, 1]
ʩ
A
defined by
ˉ
(
ˉ
)
1 and
ˉ
(
ˉ
)
0 for
ˉ
=
=
=
ˉ
. We also have the vector
0
[0, 1]
ʩ
with 0(
ˉ
)
∈
=
0 for all
ˉ
∈
ʩ
. Sometimes we treat a distribution
ʔ
of finite
support as the
pCSP
expression
s
∈
ʔ
ʔ
(
s
)
·
s
, so that
A
(
T
,
ʔ
):
=
Exp
ʔ
A
(T, __).
Lemma 5.9
Let P be a
pCSP
process, and T
,
T
i
be tests.
ˉ
.
1. o
∈
A
(
ˉ
,
P
)
,iffo
=
2.
0
∈
A
X
−ₒ
˄
⃒
.
3. Suppose the action ˉ does not occur in the test T . Then o
(
a
∈
X
a.ˉ
,
P
)
,iff
∃
ʔ
: [
P
]]
ʔ
∈
A
(
˄.ˉ
a.T
,
P
)
a
⃒
with o
(
ˉ
)
=
0
, iff there is a ʔ
∈
D
(sCSP)
with
[[
P
]]
ʔ and o
∈
A
(
T
,
ʔ
)
.
4. o
∈
A
(
T
1
p
↕
T
2
,
P
)
,iffo
=
p
·
o
1
+
(1
−
p
)
·
o
2
for some o
i
∈
A
(
T
i
,
P
)
.
5. o
∈
A
(
T
1
T
2
,
P
)
if there are some probability q
∈
[0, 1]
and ʔ
1
,
ʔ
2
∈
˄
⃒
D
(
sCSP
)
such that
[[
P
]]
q
·
ʔ
1
+
(1
−
q
)
·
ʔ
2
and o
=
q
·
o
1
+
(1
−
q
)
·
o
2
for some o
i
∈
A
(
T
i
,
ʔ
i
)
.
Proof
The converse of Lemma
5.9
(5) also holds, as the following lemma says. However,
the proof is less straightforward.
Straightforward, by induction on the structure of
P
.
Let P be a
pCSP
process, and T
i
be tests. If o
∈
A
Lemma 5.10
(
i
∈
I
T
i
,
P
)
then
(
sCSP
)
with
i
∈
I
q
i
=
∈
I there are probabilities q
i
∈
[0, 1]
and ʔ
i
∈
D
for all i
1
⃒
i
∈
I
q
i
·
=
i
∈
I
q
i
o
i
for some o
i
∈
A
˄
such that
[[
P
]]
(
T
i
,
ʔ
i
)
.
Proof
Given that the states of our pLTS are
sCSP
expressions, there exists a well-
founded order on the combination of states in
sCSP
and distributions in
ʔ
i
and o
D
(
sCSP
),
ʱ
−ₒ
such that
s
ʔ
implies that
s
is larger than
ʔ
, and any distribution is larger than
the states in its support. Intuitively, this order corresponds to the usual order on natural
numbers if we graphically depict a
pCSP
process as a finite tree (cf. Sect.
5.2.4
) and
Search WWH ::
Custom Search