Information Technology Reference
In-Depth Information
d
(
T
i
,
ʔ
i
) with
o
i
≤
v
i
. Hence, there are
o
i
∈
A
d
(
T
i
,
ʔ
i
)
i
=
1, 2 there are
o
i
∈
A
with
o
i
≤
v
i
. Thus,
o
:
=
p
·
o
1
+
·
o
2
∈
A
d
(
T
˕
,
ʔ
) by Lemma
6.39
(6),
(1
−
p
)
and
o
≤
v
˕
.
Now, suppose
d
(
T
˕
,
ʔ
):
o
∃
o
∈
A
≤
v
˕
. Then, by Lemma
6.42
, there are
q
∈
[0, 1] and
ʔ
1
,
ʔ
2
∈
D
sub
(
sCSP
) such that
ʔ
⃒
q
·
ʔ
1
+
(1
−
q
)
·
ʔ
2
and
o
1
+
o
2
for certain
o
i
∈
A
d
(
T
i
,
ʔ
i
). Now
i
:
o
i
(
ˉ
i
)
v
i
(
ˉ
i
)
1
o
=
q
·
(1
−
q
)
·
∀
=
=
2
,
so, using that
T
1
,
T
2
are
ʩ
-disjoint tests,
1
2
q
1
2
p
o
1
(
ˉ
1
)
v
1
(
ˉ
1
)
=
q
·
=
o
(
ˉ
1
)
≤
v
˕
(
ˉ
1
)
=
p
·
=
and likewise
1
2
(1
1
2
(1
o
2
(
ˉ
2
)
v
2
(
ˉ
2
)
−
q
)
=
(1
−
q
)
·
=
o
(
ˉ
2
)
≤
v
˕
(
ˉ
2
)
=
(1
−
p
)
·
=
−
p
)
.
Together, these inequalities say that
q
=
p
. Exactly as in the previous case one
obtains
o
i
≤
v
i
for both
i
=
1, 2. Given that
T
i
=
T
i
2
↕
ˉ
i
, using Lemma
6.39
(5),
it must be that
o
i
=
1
1
2
o
i
+
2
ˉ
i
for some
o
i
∈
A
d
(
T
i
,
ʔ
i
) with
o
i
≤
v
i
. By induction,
ʔ
i
|=
˕
i
for
i
=
1, 2, and hence
ʔ
|=
˕
.
pmust
ʔ then ʘ
F
ʔ.
Theorem 6.17
If ʘ
pmust
ʔ
and
ʔ
Proof
. Let
T
˕
be a characteristic
test of
˕
with target value
v
˕
. Then Proposition
6.14
yields
Suppose
ʘ
|=
˕
for some
˕
∈
F
d
(
T
˕
,
ʔ
):
o
∃
o
∈
A
≤
v
˕
,
pmust
ʔ
, by the Smyth preorder we are guaranteed to have
and hence, given that
ʘ
o
∈
A
d
(
T
˕
,
ʘ
):
o
≤
∃
v
˕
. Thus
ʘ
|=
˕
by Proposition
6.14
again.
Corollary 6.13
For any finitary processes P and Q,ifP
pmust
Q then P
FS
Q.
pmust
Q
then
P
FS
Q
.
Theorem 4.7 tells us that
ʩ
-testing is reducible to scalar testing. So the required
result follows.
Proof
From Theorems
6.17
and
6.16
, we know that if
P
Remark 6.4
Note that in our testing semantics we have allowed tests to be finitary.
The proof of Proposition
6.14
actually tells us that if two processes are behaviourally
different they can be distinguished by some characteristic tests that are always finite.
Therefore, Corollary
6.13
still holds if tests are required to be finite.
6.8
Simulations and May Testing
In this section, we follow the same strategy as for failure simulations and testing
(Sect.
6.6
) except that we restrict our treatment to full distributions; this is possible
because partial distributions are not necessary for this case; and it is desirable because
the approach becomes simpler as a result.
Search WWH ::
Custom Search