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

Proof We first consider the case for S .

˄
⃒

1. Since P 1 S Q 1 , there must b e a ʔ 1 such that [[ Q 1 ]] ʔ 1 and [[ P 1 ]] ( s ) † ʔ 1 .Itis

a
−ₒ eas y to se e that a.P 1 s a.Q 1 because the transiti on a .P 1 [[ P 1 ]] can be matched

a
−ₒ

˄
⃒

s ) † a.Q 1 = by a.Q 1 [[ Q 1 ]] ʔ 1 . Thus [[ a.P 1 ]] = a.P 1 ( [[ a.Q 1 ]] .

˄
⃒

s ) † ʔ i .It 2. Since P i S Q i , there must be a ʔ i suc h that [[ Q i ]] ʔ i and [[ P i ]] (

˄
−ₒ

is easy to see that P 1 P 2 s Q 1 Q 2 because the transition P 1 P 2 [[ P i ]] ,

˄
−ₒ

˄
⃒ ʔ i . Thus, we

for i = 1or i = 2, can be mat ched by Q 1 Q 2 [[ Q i ]]

s ) † Q 1 Q 2 = have that [[ P 1 P 2 ]] = P 1 P 2 ( [[ Q 1 Q 2 ]] .

3. Let R ↆ sCSP × D ( sCSP ) be defined by s R ʔ , iff either s s ʔ or s = s 1 s 2

and ʔ = ʔ 1 ʔ 2 with s 1 s ʔ 1 and s 2 s ʔ 2 . We show that R is a simulation.

a
−ₒ

a
−ₒ Suppose s 1 s ʔ 1 , s 2 s ʔ 2 and s 1 s 2 ʘ with a ∈ Act . Then s i ʘ for

a
⃒ i = 1or i = 2. Thus ʔ i ʔ for some ʔ with ʘ ( s ) † ʔ , and hence ʘ R

† ʔ .

a
⃒

ˆ

By Lemma 5.7 we have ʔ 1 ʔ .

Now suppose that s 1 s ʔ 1 , s 2 s ʔ 2 and s 1

ʔ 2

˄
−ₒ

s 2 ʘ . Then we have

˄
−ₒ

˄
−ₒ

s 1 Φ and ʘ = Φ s 2 or s 2 Φ and ʘ = s 1 Φ . By symmetry we

˄
⃒ ʔ for some ʔ with Φ (

may restrict attention to the first case. Thus ʔ 1 s ) † ʔ .

˄
−ₒ

†

By Lemma 5.7 we have ( Φ s 2 ) R ( ʔ ʔ 2 ) and ʔ 1 ʔ 2 ʔ ʔ 2 .

The case that s s ʔ is trivial, so we have checked that R is a simulation indeed.

Using this, we proceed to show that P 1 P 2 S Q 1 Q 2 .

˄
⃒

ˆ

s ) † ʔ i .By

Since P i S Q i , there must be a ʔ i such that [[ Q i ]] ʔ i and [[ P i ]] (

†

Lemma 5.7 ,wehave [ P 1 P 2 ]] = ([[ P 1 ]] [[ P 2 ]] ) R ( ʔ 1 ʔ 2 ). Therefore, it

s ) † ( ʔ 1

holds that [[ P 1 P 2 ]] ( ʔ 2 ). By Lemma 5.7 we also obtain

˄
⃒

ˆ ˄

⃒

ˆ

[[ Q 1 Q 2 ]] = [[ Q 1 ]] [[ Q 2 ]] ʔ 1 [[ Q 2 ]] ʔ 1 ʔ 2 ,

so the required result is established.
4. Since P i S Q i , there must be a ʔ i such that [[ Q i ]]

˄
⃒ ʔ i and [[ P i ]] (

s ) † ʔ i .

˄
⃒

ˆ

Thus [[ Q 1 p ↕ Q 2 ]] = p · [[ Q 1 ]] + (1 − p ) · [[ Q 2 ]] p · ʔ 1 + (1 − p ) · ʔ 2 by

s ) † p Lemma 5.4 and [[ P 1 p ↕ P 2 ]] = p · [[ P 1 ]] + (1 − p ) · [[ P 2 ]] ( · ʔ 1 + (1 − p ) · ʔ 2

by the linearity of lifting operation. Hence P 1 p ↕ P 2 S Q 1 p ↕ Q 2 .
5. Let R ↆ sCSP × D ( sCSP ) be defined by s R ʔ ,iff s = s 1 | A s 2 and ʔ =

ʔ 1 | A ʔ 2 with s 1 s ʔ 1 and s 2 s ʔ 2 . We show that R is a simulation. There are

three cases to consider.
a) Suppose s 1 s ʔ 1 , s 2 s ʔ 2 and s 1 | A s 2

ʱ
−ₒ ʘ 1 | A s 2 because of the transition

ʱ
−ₒ

ʱ
⃒ ʔ 1 for some ʔ 1 s ) † ʔ 1 . s 1 ʘ 1 with ʱ ∈ A . Then ʔ 1 with ʘ 1 (

ʱ
⃒ ʔ 1 | A ʔ 2 and also it can be seen that

By Le m ma 5.8 we have ʔ 1 | A ʔ 2

† ( ʔ 1 | A ʔ 2 ).
b) The symmetric case can be similarly analysed.
c) Suppose s 1 s ʔ 1 , s 2 s ʔ 2 and s 1 | A s 2

( ʘ 1 | A s 2 ) R

˄
−ₒ ʘ 1 | A ʘ 2 because of the transitions

a
−ₒ

a
−ₒ

s 1 ʘ 1 and s 2 ʘ 2 with a ∈ A . Then for i = 1 and i = 2wehave