Information Technology Reference
In-Depth Information
ʴ
n
k
,
h
max
(
f
0
(
t
)) for all
t
ʴ
n
k
,
h
(
t
)
V
= V
∈
=
f
0
such that
T
and
k
1, 2,
...
. By Lemma
4.7
,
∈
we have that, for every
t
T
,
=
k
∈N
V
h
(
t
)
ʴ
n
k
,
h
(
t
)
V
=
k
∈N
V
ʴ
n
k
,
h
max
(
f
0
(
t
))
max
(
f
0
(
t
))
.
= V
h
(
ʘ
ⓦ
)
max
(
ʔ
ⓦ
).
It follows that
V
= V
nr
may
Q.
Proof
Similar to that of Theorem
4.2
but employing Theorem
4.3
in place of
Proposition
4.5
.
er
may
Q, if and only if P
Theorem 4.4
For finite-state processes, P
4.7
Vector-Based Testing Versus Scalar Testing
In this section we show that for finitary processes, scalar testing is as powerful as
vector-based testing. As a stepping stone, we use resolution-based reward testing,
which is shown to be equivalent to vector-based testing.
Theorem 4.5
For any ʩ and finitary processes P
,
Q, we have
ʩ
ʩ
P
pmay
Q
iff
P
nr
may
Q
pmust
Q
nr
must
Q.
P
iff
P
Proof
Given test
T
, process
P
and reward vector
h
, we introduce the following
notation:
A
f
(
T
,
P
):
={
Exp
ʘ
(
V
)
|
R
,
ʘ
,
ₒ
is a static resolution of [[
T
|
Act
P
]]
}
h
h
)
A
f
(
T
,
P
):
={
Exp
ʘ
(
V
|
R
,
ʘ
,
ₒ
is a static resolution of [[
T
|
Act
P
]]
}
.
We have the following two claims:
Claim 1
For any test
T
, process
P
, and reward vector
h
, we always have that
A
f
(
T
,
P
)
ↆ
A
A
f
(
T
,
P
)is
p
-closed.
(
T
,
P
). Moreover, if
P
and
T
are finitary, then
Claim 2
Let
h
∈
[0, 1]
m
be a reward tuple,
T
∈ T
m
and
P
are finitary test and
process, respectively.
h
h
(
T
,
P
)
A
f
(
T
,
P
)
=
A
f
(
T
,
P
)
h
(
T
,
P
)
.
A
=
A
Search WWH ::
Custom Search