Testing Finitary Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 227

{ $ Φ | [[ P | Act T ]] ⃒ Φ }

d ( T , P ), is also convex and compact. By Corollary 6.3 , the set

that is, ( T , P )

is, thus, convex and compact. Combining this with ( 6.31 ), and using the Separation
theorem, Theorem 2.7, we infer the existence of some hyperplane whose normal is
h

A A

ʩ

o >h o for all o ∈ A

∈ R such that h · · ( T , P ). By scaling h , we obtain without

1, 1] ʩ . It follows that loss of generality that h ∈ [ −

h · A ( T , P ) >h · o ≥ h · A ( T , Q )

rr must Q .

which is a contradiction to the assumption that P

Note that in the above proof the normal of the separating hyperplane belongs
to [ 1, 1] ʩ rather than [0, 1] ʩ . So we cannot repeat the above proof for

nr must .

−

ʩ

In general, we do not have that P ( T , Q ) for any

ʩ -test T and for arbitrary finitary processes P and Q , that is finitary processes that
might not be convergent. However, when we restrict ourselves to finitary convergent
processes, this property does indeed hold, as can be seen from the first five lines in
the proof of Theorem 6.22 . Note that in that proof there is an essential use of the
failure simulation preorder, in particular the pleasing property stated in Lemma 6.48 .
Even for finitary convergent processes we cannot give a direct and simple proof of
that property for

nr must Q implies

A ( T , P ) ↇ A

nr must , analogous to that of Theorem 6.24 .
Although for finitary convergent processes, real-reward must testing is no more
powerful then nonnegative-reward must testing, a similar result does not hold for may
testing. This follows immediately from our result that (the inverse of) real-reward
may testing is as powerful as real-reward must testing, that is known not to hold for
nonnegative-reward may and must testing. Thus, real-reward may testing is strictly
more discriminating than nonnegative-reward may testing, even in the absence of
divergence.

6.10 Summary

We have generalised the results in Chap. 5 of characterising the may preorder as
a simulation relation and the must preorder as a failure-simulation relation, from
finite processes to finitary processes. Although the general proof schema is inherited
from Chap. 5, the details here are much more complicated. One important reason
is the inapplicability of structural induction, an important proof principle used in
proving some fundamental properties for finite processes, when we shift to finitary
processes. So we have to make use of more advanced mathematical tools such as
fixed points on complete lattices, compact sets in topological spaces, especially in
complete metric spaces, etc. Technically, we develop weak transitions between prob-
abilistic processes, elaborate their topological properties and capture divergence in
terms of partial distributions. In order to obtain the characterisation results of testing
preorders as simulation relations, we found it necessary to investigate fundamental