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

Note that ( Must2 ) can be used, together with ( I1 ), to derive the dual of ( May3 )
via the following inference:

a.P p ↕ a.Q = E ( a.P p ↕ a.Q ) ( a.P p ↕ a.Q )

E must a. ( P p ↕ Q ) .

An important inequation that follows from ( May1 ) and ( P1 )is

( May4 ) P p ↕ Q E may P Q

saying that any probabilistic choice can be simulated by an internal choice. It is
derived as follows:

P p ↕ Q

E may ( P Q ) p ↕ ( P Q )

= E ( P Q ) .

Likewise, we have

P Q E must P p ↕ Q.

Theorem 5.7 Fo r P , Q in nCSP , it holds that

(i) P S Q iff P E may Q
(ii) P FS Q iff P E must Q.

Proof For one direction it is sufficient to check that the inequations, and the inequa-
tional schema in Fig. 5.8 are sound. The converse, completeness, is established in
the next section.

5.10 Completeness

The completeness proof of Theorem 5.7 depends on the following variation on the
Derivative lemma of [ 15 ]:

Lemma 5.15 (Derivative Lemma) Let P , Q ∈ nCSP .

˄
⃒ (i) If [[ P ]] [[ Q ]] then P E must Q and Q E may P .

a
⃒

(ii) If [[ P ]] [[ Q ]] then a.Q E may P .

Proof The proof of (i) proceeds in four stages. We only deal with E may , as the proof

for E must is entirely analogous.

First we show by structural induction on s

˄
−ₒ

∈ sCSP ∩ nCSP that s [[ Q ]]

˄
−ₒ

implies Q P 2 it follows

by the operational semantics of pCSP that Q = P 1 or Q = P 2 . Hence, Q E may s by

E may s . So suppose s [[ Q ]]. In case s has the form P 1