Information Technology Reference
In-Depth Information
˄
1/
3
2
/3
r
r
s
1
1
2
˄
˄
˄
˄
s
1/4
3/4
2
ˉ
r
4
r
5
r
3
1
1/2
1/2
˄
˄
s
s
4
ˉ
2
r
6
3
ˉ
1
1/
2
1/2
ˉ
1
r
7
r
8
ˉ
2
(a)
(b)
Fig. 4.1
A resolution
Lemma 4.1
For any test T and process P ,ifo
1
,
o
2
∈
A
(
T
,
P
)
, then their weighted
average o
1
p
↕
o
2
is also in
A
(
T
,
P
)
for any p
∈
[0, 1]
.
Proof
|
Act
P
]] that give rise
to
o
1
,
o
2
. We take their disjoint union, except initially we let
ʘ
:
Let
R
1
,
ʘ
1
,
ₒ
1
,
R
2
,
ʘ
2
,
ₒ
2
be the resolutions of [[
T
=
ʘ
1
p
↕
ʘ
2
,to
define the new resolution
R
1
∪
R
2
,
ʘ
,
ₒ
1
∪ₒ
2
. It is easy to see that the new
resolution generates the interpolated tuple
o
1
p
↕
o
2
as required.
Definition 4.4 (Probabilistic Testing Preorders)
pmay
Q
if for every
ʩ
test
T
,
(i)
P
A
(
T
,
P
)
≤
Ho
A
(
T
,
Q
).
pmust
Q
if for every
ʩ
test
T
,
(ii)
P
A
(
T
,
P
)
≤
Sm
A
(
T
,
Q
).
These preorders are abbreviated to
P
pmay
Q
and
P
pmust
Q
, when
|
ʩ
|=
1, and
their kernels are denoted by
pmay
and
pmust
, respectively.
If
|
ʩ
|=
1, then vector-based testing degenerates into scalar testing. In general, if
|
>
1, then vector-based testing appears more discriminating than scalar testing.
Surprisingly, if we restrict ourselves to finitary processes, then scalar testing is equally
powerful as vector-based testing. A key ingredient of the proof is to exploit a method
of testing called
reward testing
, which will be introduced in Sect.
4.4
.
ʩ
|
Search WWH ::
Custom Search