Information Technology Reference
In-Depth Information
s
1
s
s
˄
2
˄
3
˄
. . . . . .
˄
˄
˄
1/2
1/2
1/4
3/4
1/8
7/8
a
a
a
Fig. 4.5
An infinite-state pLTS
max
(
a.ˉ
|
Act
s
1
) also evaluates to
h
(
ˉ
), we let
x
k
= V
max
(
a.ˉ
|
Act
s
k
), for all
k
≥
V
1,
and we have the following infinite equation system.
max
2
h
(
ˉ
),
x
2
x
1
=
max
(1
4
)
h
(
ˉ
),
x
3
1
x
2
=
−
.
x
k
=
max
1
2
k
h
(
ˉ
),
x
k
+
1
1
−
.
We have
x
k
=
h
(
ˉ
) for all
k
≥
1 as the least solution of the above equation system.
With some more work one can go on to show that no test can distinguish between
these processes using optimistic extremal testing, meaning that
a.
0
er
may
s
1
.
In the remainder of this section, we show that provided some finitary constraints
are imposed on the pLTS, extremal reward testing and resolution-based reward testing
coincide. First we examine
must
testing, which is easier than the
may
case; this in
turn is treated in the following section.
4.6.1
Must Testing
Here we show that provided we restrict our attention to finitely branching pro-
cesses, there is no difference between extremal
must
testing and resolution-based
must
testing.
Let us consider a pLTS
S
,
ʩ
˄
,
ₒ
, obtained perhaps from applying a test
T
to
|
Act
P
). We have two ways of obtaining a result for a distribution
of states from
S
, by applying the function
a process
P
in (
T
min
, or by using resolutions of the pLTS
V
to realise
h
. Our first result says that regardless of the actual resolution used, the
value obtained from the latter will always dominate the former.
V
Search WWH ::
Custom Search