Information Technology Reference
In-Depth Information
1, 1]
ʩ
. Clearly,
and
h
be any real-reward tuple in [
−
−
h
is also a real-reward tuple.
Suppose
Q
rr
must
P
, then
(
−
h
)
·
A
(
T
,
Q
)
≤
(
−
h
)
·
A
(
T
,
P
)
(6.30)
Therefore, we can infer that
h
·
A
(
T
,
P
)
by (
6.29
)
(
T
,
P
)
=−
(
−
h
)
·
A
(
T
,
Q
)
by (
6.30
)
≤−
(
−
h
)
·
A
h
=
·
A
(
T
,
Q
)by
6.29
)
ʩ
rr
must
ʩ
nr
must
. The former is included in the
latter, which directly follows from Definition
6.30
. Surprisingly, it turns out that for
finitary convergent processes the latter is also included in the former, thus the two
preorders are in fact the same. The rest of this section is devoted to proving this
result. However, we first show that this result does not extend to divergent processes.
Our next task is to compare
with
Example 6.27
Consider the processes
Q
1
and
Q
2
depicted in Fig.
6.5
. Using the
characterisations of
pmust
in Sects.
6.6
-
6.8
, it is easy to see that these
processes cannot be distinguished by probabilistic may- and must testing, and hence
not by nonnegative-reward testing either. However, let
T
be the test in the right
diagram of Fig.
6.5
that first synchronises on the action
a
, and then with probability
1
2
pmay
and
reaches a state in which a reward of
−
2 is allocated, and with the remaining
1
probability
2
synchronises with the action
b
and reaches a state that yields a reward
of 4. Thus the test employs two success actions
ˉ
1
and
ˉ
2
, and w
e u
se the reward
tuple
h
with
h
(
ˉ
1
)
=−
2 and
h
(
ˉ
2
)
=
4. Then the resolution of
q
1
that does not
1
2
+
1
2
=
involve the
˄
-loop contributes the value
(
T
,
Q
1
),
whereas the resolution that only involves the
˄
-loop contributes the value 0. Due
to interpolation,
h
−
2
·
4
·
1 to the set
h
·
A
(
T
,
Q
1
) is in fact the entire interval [0, 1]. On the other hand,
the resolution corresponding to the
a
-branch of
q
2
contributes the value
·
A
−
1 and
·
A
=
−
·
A
=
−
=
·
A
h
(
T
,
Q
2
)
[
1, 1]. Thus
h
(
T
,
Q
1
)
0
>
1
h
(
T
,
Q
2
), and
hence
q
1
rr
must
q
2
.
For convergent pLTSs, the results in Lemmas
6.31
and
6.33
as well as
Theorem
6.13
can be strengthened.
Lemma 6.47
Let ʔ and ʘ be distributions in an ˉ-respecting convergent pLTS
e
FS
)
†
ʘ, then
$
ʔ
∈
V
S
,
ʩ
˄
,
ₒ
. If distribution ʔ is stable and ʔ
(
(
ʘ
)
.
e
Proof
We first show that if
s
is stable and
s
FS
ʘ
then $
s
∈
V
(
ʘ
). Since
s
is
stable, we have only two cases:
0
. Since
s
e
ʘ
with
ʘ
−ₒ
(i)
s
−ₒ
. Here $
s
=
FS
ʘ
we have
ʘ
⃒
, whence
0
. Thus it holds that $
s
0
∈
V
ʘ
and $
ʘ
=
in fact
ʘ
⃒
=
(
ʘ
).
ˉ
, and since
s
ˉ
−ₒ
ˉ
−ₒ
ʔ
for some
ʔ
. Here $
s
e
FS
ʘ
we have
ʘ
ʘ
(ii)
s
.
As the pLTS we are considering is convergent and
ʘ
is a distribution, we know
=
⃒
Search WWH ::
Custom Search