Information Technology Reference
In-Depth Information
n
ʔ
k
= V
by continuity of
V
n
≥
0
k
=
0
∞
ʔ
k
= V
k
=
0
= V
ʔ
We are now ready to compare the two methods for calculating the set of outcomes
associated with a subdistribution:
•
using extreme derivatives and the reward function $ from Definition
6.9
; and
V
•
using resolutions and the evaluation function
from Sect. 4.2.
Corollary 6.2
In an ˉ-respecting pLTS
S
,
ʩ
˄
,
ₒ
, the following statements hold.
(a) If ʔ
⃒
ʔ
then there is a resolution
$(
ʔ
)
.
R
,
ʘ
,
ₒ
R
of ʔ such that
V
(
ʘ
)
=
of ʔ, there exists an extreme derivative ʔ
such
(b) For any resolution
R
,
ʘ
,
ₒ
R
ʔ
and
$(
ʔ
)
.
that ʔ
⃒
V
(
ʘ
)
=
ʔ
. By Theorem
6.7
, there is a resolution
Proof
Suppose
ʔ
⃒
R
,
ʘ
,
ₒ
R
ʘ
and,
of
ʔ
with resolving function
f
and subdistribution
ʘ
such that
ʘ
⃒
moreover,
ʔ
=
(
ʘ
).
Since
ʘ
and
ʔ
are extreme derivatives, all the states in their supports are stable.
Therefore, a simple calculation, using the fact that
ʔ
=
Img
f
(
ʘ
). By Lemma
6.8
,wehave
V
(
ʘ
)
= V
Img
f
(
ʘ
), will show that
(
ʘ
)
$(
ʔ
), from which the required
$(
ʔ
) follows.
V
=
V
(
ʘ
)
=
To prove part (b), suppose that
R
,
ʘ
,
ₒ
R
is a resolution of
ʔ
with resolving
function
f
, so that
ʔ
Img
f
(
ʘ
). We know from Lemma
6.7
that there exists a
(unique) subdistribution
ʘ
such that
ʘ
=
ʘ
. By Proposition
6.5
, we have that
⃒
Img
f
(
ʘ
). The same arguments as in the other direction show
ʔ
=
Img
f
(
ʘ
)
⃒
$(Img
f
(
ʘ
)).
that
V
(
ʘ
)
=
d
(
T
,
P
)
Corollary 6.3
For any process P and test T , we have
A
=
A
(
T
,
P
)
.
6.5
Generating Weak Derivatives in a Finitary pLTS
Now let us restrict our attention to a finitary pLTS whose state space is assumed to
be
S
ʱ
−ₒ
are finite, for every
state
s
and label
ʱ
. This of course is no longer true for the weak arrows; the sets
{
={
s
1
,
...
,
s
n
}
. Here by definition the sets
{
ʘ
|
s
ʘ
}
ʱ
⃒
are in general not finite, because of the infinitary nature of the weak
derivative relation
ʘ
|
s
ʘ
}
. The purpose of this section is to show that, nevertheless,
they can be finitely represented, at least for finitary pLTSs.
This is explained in Sect.
6.5.1
and the ramifications are then explored in the
following subsection. These include a very useful topological property of these sets
⃒
Search WWH ::
Custom Search