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

˄

˄ t

q 1 a

q 2

a

a a

1/2 1/2

b

b ˉ 1 b

ˉ 2

Fig. 6.5 Two processes with divergence and a test. Reprinted from [ 13 ], with kind permission from
Elsevier

We will show that for real-reward testing may and must preorders are the inverse
of each other, that is, for any processes P and Q ,

rr may Q iff Q rr must P.

P (6.27)

A more surprising result is that for finitary convergent processes real-reward must
preorder coincides with nonnegative-reward must preorder, that is, for any finitary
convergent processes P and Q ,

rr must Q iff P nr must Q.

P (6.28)

Here by convergence we mean that in the pLTS generated by a process there is no
infinite sequence of internal transitions between distributions like

˄
−ₒ

˄
−ₒ···

ʔ 0 ʔ 1

Although, it is easy to see that in ( 6.28 ) the former is included in the latter, to prove
that the latter is included in the former is far from being trivial. Our proof strategy is to
make use of failure simulation preorder as a stepping stone, and adapt the soundness
proof of failure simulation with respect to must testing (Theorem 6.13 ).
We now recall our testing framework. A test is simply a finite process in the lan-
guage pCSP , except that it may in addition use special success actions for reporting
outcomes; these are drawn from a set ʩ of fresh actions not already in Act ˄ . Here, we
require tests to be finite processes because we will consider convergent processes; if
P , T are finitary convergent then their parallel composition P

| Act T is not necessarily
convergent unless T is very finite. As we have seen from Remark 6.4 , restricting to
finite tests does not weaken our testing semantics, as far as finitary processes are
concerned. As in Sect. 4.2, to apply test T to process P , we form the process T | Act P

in which all visible actions of P must synchronise with T . The resulting composition