Information Technology Reference
In-Depth Information
where
a.
0
is the process with the only behaviour of performing action
a
before
halting.
Example 4.5
Consider the pLTS from Fig.
4.4
resulting from the application of the
h
max
test
T
=
a.ˉ
to the process
Q
. It is easy to see that the function
V
satisfies
max
1
2
h
(
ˉ
),
x
h
V
max
(
s
0
)
=
(4.12)
1
2
h
(
ˉ
)
1
2
· V
h
x
=
+
max
(
s
0
)
.
max
(
s
0
)
It is not difficult to show that this has a unique solution, namely
V
=
h
(
ˉ
).
With further analysis, one can conclude that
er
may
a.
0
.
Q
If
max
is replaced by
min
in (
4.12
) above, then the resulting equation also has a
unique solution, giving
min
(
s
0
)
1
V
=
2
h
(
ˉ
). It follows that
a.
0
er
must
Q
h
because
V
min
([[
T
|
Act
a.
0
]] )
=
h
(
ˉ
). Again further analysis will show
Q
er
must
a.
0
4.6
Extremal Reward Testing Versus Resolution-Based
Reward Testing
In this section we compare two approaches of testing introduced in the previous two
subsections. Our first result is that in the most general setting, they lead to different
testing preorders.
Example 4.6
Consider the infinite-state pLTS in Fig.
4.5
.
We compare the state
s
1
with the process
a.
0
. With the test
a.ˉ
using resolutions,
we get:
0,
1
2
h
(
ˉ
),
...
,
1
2
k
h
(
ˉ
),
...
1
1
A
h
(
a.ˉ
,
s
1
)
=
−
−
(4.13)
h
(
a.ˉ
,
a.
0
)
A
={
h
(
ˉ
)
}
,
which means that
a.
0
pmay
s
1
.
However when we use extremal testing, the test
a.ˉ
cannot distinguish these
processes. It is straightforward to see that
max
(
a.ˉ
V
|
Act
a.
0
)
=
h
(
ˉ
). To see that
Search WWH ::
Custom Search