Information Technology Reference
In-Depth Information
Proof
The “only if” direction is obvious. Let us consider the “if” direction.
Suppose
P
and
Q
are finitary processes. We reason as follows.
nr
must
Q
P
pmust
Q
iff
P
Theorem 4.5
iff
P
FS
Q
Theorems 4.7 and
6.13
, Corollary
6.13
ʩ
implies
P
rr
must
Q.
Theorem
6.22
nr
must
. For example,
let
P
and
Q
be the processes
rec
xx
and
a.
0
, respectively. It holds that
P
rr
must
is strictly included in
In the presence of divergence,
FS
Q
ʵ
⃒
because
P
and the empty subdistribution can failure simulate any processes.
nr
must
Q
, by recalling the first two steps of reasoning in the proof
of Theorem
6.23
. However, if we apply the test
T
It follows that
P
=
a.ˉ
and reward tuple
h
with
h
(
ˉ
)
=−
1, then
h
·
A
(
T
,
P
)
=
h
·{
ʵ
}=
{
0
}=
0
ˉ
h
·
A
(
T
,
Q
)
=
h
·{
}=
{−
1
}=−
1
rr
must
Q
.
As
h
·
A
(
T
,
P
)
≤
h
·
A
(
T
,
Q
), we see that
P
rr
must
in terms of the set inclusion relation
between testing outcome sets. As a similar characterisation for
Below we give a characterisation of
nr
must
does not hold
in general for finitary (nonconvergent) processes, this indicates the subtle difference
between
nr
must
, and we see more clearly why our proof of Theorem
6.23
involves the failure simulation preorder.
rr
must
and
rr
must
Q if and only
Theorem 6.24
Let P and Q be any finitary processes. Then P
if
A
(
T
,
P
)
ↇ
A
(
T
,
Q
)
for any ʩ-test T .
⃐
∈
−
1, 1]
ʩ
be any real-reward tuple. Suppose
Proof
(
) Let
T
be any
ʩ
-test and
h
[
A
ↇ
A
·
A
ↇ
·
A
(
T
,
P
)
(
T
,
Q
). It is obvious that
h
(
T
,
P
)
h
(
T
,
Q
), from which it
easily follows that
·
A
≤
·
A
h
(
T
,
P
)
h
(
T
,
Q
)
.
rr
must
Q
.
As this holds for an arbitrary real-reward tuple
h
, we see that
P
(
⃒
) Suppose for a contradiction there is some
ʩ
-test
T
with
A
(
T
,
P
)
ↇ
A
(
T
,
Q
).
Then there exists some outcome
o
∈
A
(
T
,
Q
) lying outside
A
(
T
,
P
), i.e.
o
∈
A
(
T
,
P
)
.
(6.31)
Since
T
is finite, it contains only finitely many elements of
ʩ
, so that we may
assume with loss of generality that
ʩ
is finite. Since
P
and
T
are finitary, it is easy
to see that the pruned composition [
P
|
Act
T
] is also finitary. By Theorem
6.1
, the set
{
|
|
Act
T
]]
⃒
}
is convex and compact. With an analogous proof, using
Corollary
6.4
, it can be shown that so is the set
Φ
[[
P
Φ
{
Φ
|
[[
P
|
Act
T
]]
⃒
Φ
}
.
It follows
that the set
Search WWH ::
Custom Search