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

with the possibility that P is a.P . Thus suppose that a.P s [[ Q ]]. We proceed
by a case analysis on the structure of Q .
•

Q is a.Q . We know from a.P s [[ a.Q ]] that [[ P ]] ( s ) † ʘ for some ʘ with

˄
⃒ [[ Q ]] ʘ , thus P S Q . Therefore, we have P E may Q by induction. It

follows that a.P E may a.Q .

• Q is j ∈ I a j .Q j with at least two elements in J . We use ( May0 ) and then

proceed as in the next case.

Q 2 . We know from a.P s [[ Q 1 Q 2 ]] that [[ P ]] ( s ) † ʘ for some • Q is Q 1

ʘ such that one of the following two conditions holds
a) [[ Q i ]]

a
⃒ 1 or 2. In this case, a.P s [[ Q i ]], hence a.P S Q i .

By induction we have a.P E may Q i ; then we apply ( May1 ).
b) [[ Q 1 ]]

ʘ for i =

a
⃒

a
⃒

ʘ 1 and [[ Q 2 ]] ʘ 2 such that ʘ = p · ʘ 1 + (1 − p ) · ʘ 2 for

[[ Q i ]] for i

some p 1, 2. By the Derivative Lemma,

we have a.Q 1 E may Q 1 and a.Q 2 E may Q 2 . Clearly, [[ Q 1 p ↕ Q 2 ]]

∈ (0, 1). Let ʘ i = =

ʘ , thus
we have P S Q 1 p ↕ Q 2 . By induction, we infer that P E may Q 1 p ↕ Q 2 .So

=

a.P E may a. ( Q 1 p ↕ Q 2 )

E may a.Q 1 p ↕ a.Q 2

( May3 )

E may Q 1 p ↕ Q 2
E may Q 1 Q 2 ( May4 )

Q is Q 1 p ↕ Q 2 . We know from a.P s [[ Q 1 p ↕ Q 2 ]] that [[ P ]] ( s ) † ʘ for some •

a
⃒ ʘ . From Lemma 5.4 we know that ʘ must take

ʘ such that [[ Q 1 p ↕ Q 2 ]]

a
⃒ [[ Q 1 ]] [[ Q 2 ]], where [[ Q i ]] [[ Q i ]] for i

1, 2.
Hence P S Q 1 p ↕ Q 2 , and by induction we get P E may Q 1 p ↕ Q 2 . Then we
can derive a.P E may Q 1 p ↕ Q 2 as in the previous case.
Now we use ( 5.29 ) to show that P

the form p · + (1 − p ) · =

S Q implies P E may Q . Suppose P S Q . Applying

Definition 5.5 with the understanding that any distribution ʘ ∈ D ( sCSP ) can be

written as [[ Q ]] for some Q ∈ s ) † [[ Q ]] for

pCSP , this basically means that [[ P ]] (

˄
⃒ [[ Q ]]. The Derivative Lemma yields Q E may Q . So it suffices to

some [[ Q ]]

E may Q . We know that [[ P ]] ( s ) † [[ Q ]] means that show P

t k s [[ Q k ]] [[ Q ]] [[ Q k ]] [[ P ]] = r k · t k = r k ·

k ∈ K k ∈ K

sCSP and Q k ∈

for some K , r k ∈ (0, 1], t k ∈ pCSP .Now

[[ k ∈ K r k · = prob k ∈ K r k · 1. [[ P ]] = t k ]]. By Lemma 5.14 we have P t k .

[[ k ∈ K r k · Q k ]]. Again Lemma 5.14 yields Q = prob k ∈ K r k · 2. [[ Q ]] Q k .

=

3. t k s [[ Q k ]] implies t k E may Q k by ( 5.29 ). Therefore, k ∈ K r k · t k E may k ∈ K r k · Q k .

E may Q , hence P E may Q .

Combining (1), (2) and (3) above we obtain P