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

( May1 ). The only other possibility is that s has the form s 1 s 2 . In that case there
must be a distribution ʔ such that either s 1

˄
−ₒ

˄
−ₒ

ʔ and [[ Q ]] = ʔ s 2 ,or s 2 ʔ

and [[ Q ]] ʔ . Using symmetry, we may restrict attention to the first case. Let

R be a term such that [[ R ]]

= s 1

= ʔ . Then [[ R s 2 ]] = ʔ s 2 = [[ Q ]], so Lemma 5.14

yields Q = prob R s 2 . By induction we have R E may s 1 , hence R s 2 E may s 1 s 2 ,

and thus Q E may s .

Now we show that s

˄
−ₒ

˄
−ₒ

[[ Q ]] implies Q E may s . This follows because s [[ Q ]]

˄
−ₒ

means that either s [[ Q ]] o r [[ Q ]] = s , and in the latter case Lemma 5.14 yields

Q = prob s .

Next we show that [[ P ]]

˄
−ₒ

˄
−ₒ [[ Q ]] implies Q E may P . So suppose [[ P ]] [[ Q ]] ,

that is

˄
−ₒ

ˆ

[[ P ]] = p i · s i s i [[ Q i ]] [[ Q ]] = p i · [[ Q i ]]

i ∈ I i ∈ I

for some I , p i ∈ (0, 1], s i ∈ sCSP ∩ nCSP and Q i ∈ nCSP .Now

[[ i ∈ I p i · = prob i ∈ I p i · 1. [[ P ]] = s i ]]. By Lemma 5.14 we have P s i .

[[ i ∈ I p i · = prob i ∈ I p i ·

2. [[ Q ]] = Q i ]]. Again Lemma 5.14 yields Q Q i .

[[ Q i ]] implies Q i E may s i . Therefore, i ∈ I p i · Q i E may i ∈ I p i · s i .
Combining (1), (2) and (3) we obtain Q E may P .
Finally, the general case, when [[ P ]]

˄
−ₒ

3. s i

˄
⃒

ʔ , is now a simple inductive argument

on the length of the derivation.
The proof of (ii) is similar: first we treat the case when s

a
−ₒ

[[ Q ]] by structural

a
−ₒ

induction, using ( May2 ); then the case [[ P ]] [[ Q ]], exactly as above; and finally

use part (i) to derive the general case.

The completeness result now follows from the following two propositions.

Proposition 5.8 E may Q.

Proof The proof is by structural induction on P and Q , and we may assume that
both P and Q are in normal form because of Proposition 5.7 . So take P , Q

Let P and Q be in nCSP . Then P S Q implies P

pCSP
and suppose the claim has been established for all subterms P of P and Q of Q ,of
which at least one of the two is a strict subterm. We start by proving that if P

∈

∈ sCSP

then we have

P s [[[ Q ]]] implies P E may Q. (5.29)

There are two cases to consider.

1. P has the form P 1 S Q . We use induction

to obtain P i E may Q , from which the result follows using ( I1 ).
2. P has the form

P 2 . Since P i E may P we know P i S P

i ∈ I a i .P i .If I contains two or more elements then P may also

be written as i ∈ I a i .P i , using ( May0 ) and ( D2 ), and we may proceed as in case

(1) above. If I is empty, that is P is 0 , then we can use ( May2 ). So we are left