Information Technology Reference
In-Depth Information
max
In a similar fashion, we can define the function
[0, 1])
that uses the
max
function in place of
min
. Both these functions are monotone and
therefore have least fixed points, which we abbreviate to
C
:(
S
ₒ
[0, 1])
ₒ
(
S
ₒ
h
max
, respectively.
V
min
and
V
Lemma 4.4
For any finitely branching pLTS and reward vector h,
h
h
(a) both functions
C
min
and
C
max
are continuous;
h
min
h
max
(b) both results functions
V
and
V
are continuous.
Proof
Again the proof of part (a) is nontrivial. See Lemma
4.3
for the continuity of
min
and
min
can be similarly shown. However part (b) is an
C
. The continuity of
C
C
immediate consequence.
So in analogy with the evaluation function
h
, these results functions can be captured
V
by a chain of approximants:
=
n
∈N
V
=
n
∈N
V
h
,
n
min
min
max
h
,
n
max
V
and
V
(4.11)
h
,0
min
(
s
)
h
,0
where
V
= V
max
(
s
)
=
0 for every state
s
∈
S
, and
h
,(
k
+
1)
h
,
k
min
)
•
V
=
C
min
(
V
min
h
,(
k
+
1)
h
,
k
•
max
).
Now for a test
T
, a process
P
, and a reward vector
h
, we have two ways of defining
the outcome of the application of
T
to
P
:
V
=
C
max
(
V
max
min
(
T
,
P
)
min
([[
T
A
= V
|
Act
P
]] )
max
(
T
,
P
)
max
([[
T
A
= V
|
Act
P
]] )
.
Here
A
min
(
T
,
P
) returns a single probability
p
, estimating the minimal probability
of success; it is a pessimistic estimate. On the other hand,
A
max
(
T
,
P
) is optimistic,
in that it gives the maximal probability of success.
er
may
and
er
must
are defined
Definition 4.7
The extremal reward testing preorders
as follows:
er
may
Q
if for every
ʩ
test
T
and nonnegative reward tuple
h
[0, 1]
ʩ
,
(i)
P
∈
h
h
A
max
(
T
,
P
)
≤
A
max
(
T
,
Q
).
ʩ
[0, 1]
ʩ
,
(ii)
P
er
must
Q
if for every
ʩ
test
T
and nonnegative reward tuple
h
∈
h
h
min
(
T
,
Q
).
These preorders are abbreviated to
P
A
min
(
T
,
P
)
≤
A
er
may
Q
and
P
er
must
Q
when
|
ʩ
|=
1. We
use the obvious notation for the kernels of these preorders.
Example 4.4
Let
T
be the test
a.ˉ
. By applying it to the process
P
in Fig.
4.3
a,
we obtain the pLTS in (b) that is deterministic and therefore all three functions
V
max
,
min
and
h
max
(
a.ˉ
,
P
)
min
(
T
,
P
)
V
V
coincide, giving
A
=
A
=
h
(
ˉ
).
Again it is straightforward to establish
P
er
may
a.
0
P
er
must
a.
0
Search WWH ::
Custom Search