Testing Finite Probabilistic Processes - Semantics of Probabilistic Processes: An Operational Approach - page 115

In this section we substantiate these claims by proving that P pmust Q implies
Q pmay P , and by providing a counterexample that shows the implication is strict.
We are only able to obtain the implication since our language is for finite processes
and does not feature divergence , infinite sequences of ˄ actions. It is well-known
from the nonprobabilistic theory of testing [ 3 , 4 ] that in the presence of divergence
may and must are incomparable.

To establish a relationship between must testing and may testing, we define the
context C [__]

ʽ )) so that for every test T we obtain a new test
C [ T ], by considering ʽ instead of ˉ as success action.

= __ | { ˉ } ( ˉ ( ʽ

Lemma 5.2 For any process P and test T , it holds that

1. if p ∈ A ( T , P ) , then (1 − p ) ∈ A ( C [ T ], P )

2. if p ∈ A ( C [ T ], P ) , then there exists some q ∈ A ( T , P ) such that 1 − q ≤ p.

Proof | Act t can always do a ˄ move, and never directly

a success action ʽ . The ˄ steps that C [ s ]

A state of the form C [ s ]

| Act t can do fall into three classes: the

resulting distribution is either

ʽ
−ₒ

• a point distribution u with u ; we call this a successful ˄ step, because it

contributes 1 to the s e t V f ( C [ s ] | Act t )

• a point distribution u with u , a state from which the success action ʽ is un-

reachable; we call this an unsuccessful ˄ step, because it contributes 0 to the set
V f ( C [ s ]

| Act t )

• or a distribution of form C [ ʘ ] | Act ʔ .

Note that

• C [ s ] | Act t can always do a successful ˄ step

• C [ s ] | Act t can do an unsuccessful ˄ step, iff s | Act t can do a ˉ step

˄
−ₒ

˄
−ₒ • | Act ʔ .

Using this, both claims follow by a straightforward induction on T and P .

and C [ s ] | Act t C [ ʘ ] | Act ʔ ,iff s | Act t ʘ

Proposition 5.1 If P pmust Q then Q pmay P .

Proof Suppose P pmust Q . We must show that, for any test T ,if p ∈ A ( T , Q ) then

there exists a q ∈ A ( T , P ) such that p ≤ q . So suppose p ∈ A ( T , Q ). By the first

clause of Lemma 5.2 ,wehave(1 − p ) ∈ A ( C [ T ], Q ). Given that P pmust Q , there

must be an x ∈ A ( C [ T ], P ) such that x ≤ 1 − p . By the second clause of Lemma 5.2 ,

there exists a q ∈ A ( T , P ) such that 1 − q ≤ x . It follows that p ≤ q . Therefore

Q pmay P .

Example 5.12 To show that must testing is strictly more discriminating than may
testing, consider the processes a b and a b , and expose them to test a.ˉ .Itis

not hard to see that A ( a.ˉ , a b ) ={ 1 } , whereas A ( a.ˉ , a b ) ={ 0, 1 } . Since

A = A =

min ( ( a.ˉ , a b )) 1 and min ( ( a.ˉ , a b )) 0, using Proposition 4.1 we

pmust ( a

obtain that ( a b ) b ).