Information Technology Reference
In-Depth Information
As a consequence, the finite generability result, Theorem
6.9
, specialises to
extreme derivatives.
Corollary 6.4
Let
{
ep
1
,
...
,
ep
k
}
be the finite set of extreme policies of a finitary
ˉ
-respecting pLTS
S
,
ʩ
˄
,
ₒ
R
. For any state s and subdistribution ʔ in the pLTS,
s
⃒
ʔ if and only if ʔ
∈{
Der
ep
i
(
s
)
|
1
≤
i
≤
k
}
.
Proof
O
n
e direction follows immediately from the previous lemma. Conversely,
suppose
s
=
1
≤
i
≤
n
p
i
·
Der
dp
i
(
s
) for some finite
collection of derivative policies
dp
i
, where we can assume that each
p
i
≥
⃒
ʔ
. By Theorem
6.9
,
ʔ
0. Because
˄
−ₒ
ʔ
is stable, that is
s
, we show that each derivative policy
dp
i
can be transformed into an extreme policy
ep
i
such that
Der
ep
i
(
s
)
for every
s
∈
ʔ
=
Der
dp
i
(
s
),
from which the result will follow.
First, note it is sufficient to define
ep
i
on the set of states
t
accessible from
s
via
the policy
dp
i
; on the remaining states in
S
ep
i
can be defined arbitrarily, so as to
satisfy the requirements of Definition 4.8. So consider the derivation of
Der
dp
i
(
s
)as
in Definition
6.4
, determined by
dp
i
and suppose
t
∈
ʔ
k
for some
k
≥
0. There
are three cases:
(i) Suppose
t
˄
−ₒ
ʔ
k
, and therefore by definition
dp
i
(
t
) is defined. So in this case we let
ep
i
(
t
) be the same as
dp
i
(
t
).
(ii) Suppose
t
. Since
ʔ
is stable we know
t
∈
ˉ
−ₒ
˄
−ₒ
,
and therefore
dp
i
(
t
) is not defined. Here we choose
ep
i
(
t
) arbitrarily so as to
satisfy
t
, in which case, since the pLTS is
ˉ
-respecting, we know
t
ˉ
−ₒ
ep
i
(
t
).
(iii) Otherwise we leave
ep
i
(
t
) undefined.
By definition,
ep
i
is an extreme policy since it satisfies conditions (a) and (b) in
Definition 4.8 and by construction
Der
ep
i
(
s
)
This corollary gives a useful method for calculating the set of extreme derivatives
of a given state, and therefore of the result of applying a test to a process.
=
Der
dp
i
(
s
).
Example 6.11
Consider again Fig. 4.4, discussed in Example
6.9
, where we have
the
ˉ
-respecting pLTS obtained by applying the test
a.ˉ
to the process
Q
2
. There are
only two extreme policies for this pLTS, denoted by
ep
0
and
ep
1
. They differ only
for the state
s
1
, with
ep
0
(
s
1
)
=
ʘ
0
and
ep
1
(
s
1
)
=
ʘ
1
. The discussion in Example
6.9
explained how
1
2
ˉ.
0
By Corollary
6.4
, we know that every possible extreme derivative of [[[
T
1
2
s
3
+
Der
ep
0
(
s
1
)
=
ˉ.
0
Der
ep
1
(
s
1
)
=
|
Act
Q
2
]] ]
takes the form
1
2
s
3
+
2
ˉ.
0
1
q
·
ˉ.
0
+
(1
−
q
)
·
ˉ
and $(
2
s
3
+
2
ˉ
it follows that
1
1
for some 0
≤
q
≤
1. Since $(
ˉ
)
=
2
ˉ
)
=
q ˉ
1
2
,1
.
d
(
T
,
Q
2
)
A
=
|
q
∈
Search WWH ::
Custom Search