Weak Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 240

Proof Without loss of generality, we assume that p i = 0 for all i ∈ I . Suppose that

( i ∈ I p i · ʔ i ) b. 0 ), where

all a i and b are fresh and pairwise different actions. By the compositionality of

≈ rbc ʘ . Consider the testing process T =

i ∈ I ( a i . 0

≈ rbc ,

we have ( i ∈ I p i · ʔ i ) | T ≈ rbc ʘ | T .Now( i ∈ I p i · ʔ i ) ⃒ i ∈ I p i ·

˄

| T ( ʔ i | a i . 0 ).

Since ≈ rbc is reduction-closed, there must exist some ʓ such that ʘ | T ⃒ ʓ and

i ∈ I p i ·

( ʔ i | a i . 0 ) ≈ rbc ʓ .

The barbs of i ∈ I p i · ( ʔ i | a i . 0 ) constrain severely the possible structure of ʓ .

≡ k ∈ K q k ·

> 0
b

For example, since ʓ ⇓ ,wehave ʓ ( ʘ k | a k i . 0 ) for some index set

⃒ k q k ·

˄

K , where ʘ ʘ k and k i ∈ I . For any indices k 1 and k 2 ,if a k 1 = a k 2 ,

we can combine the two summands q k 1 · ʘ k 1 and q k 2 · ʘ k 2 into one ( q k 1 + q k 2 ) · ʘ k 12

q k 1
q k 1 +

q k 2
q k 1 +

where ʘ k 12 = (

q k 2 ·

ʘ k 1 +

q k 2 ·

ʘ k 2 ). In this way, we see that ʓ can be written

as i ∈ I q i · p i and i ∈ I p i = ⇓ ≥ p i

( ʘ i | a i . 0 ). Since ʓ , q i ≥ 1, we have p i = q i

a i

for each i I .

Therefore, the required matching move is ʘ

∈

⃒ i ∈ I p i ·

˄

ʘ i . This follows

because i ∈ I p i · ≈ rbc i ∈ I p i ·

( ʔ i | a i . 0 ) ( ʘ i | a i . 0 ), from which Lemma 7.4 implies

the required ʔ i ≈ rbc ʘ i for each i ∈ I .

ʱ
⃒ ʔ with ʱ

Proposition 7.5 Suppose that ʔ ≈ rbc ʘ in rpCSP .Ifʔ ∈ Act ˄

ʱ
⃒ ʘ such that ʔ ≈ rbc ʘ .

then ʘ

Proof We can distinguish two cases.

(1) ʱ is ˄ . This case is trivial because ≈ rbc is reduction-closed.

(2) ʱ is a , for some a ∈ Act . Let T be the process b. 0 a.c. 0 where b and c are fresh

ʔ |

actions. Then ʔ | T ⃒ c. 0 by Lemma 7.3 (iii). Since ʔ ≈ rbc ʘ , it follows

that ʔ | T ≈ rbc ʘ | T . Since ≈ rbc is reduction-closed, there is some ʓ such

ʓ and ʔ | that ʘ | T ⃒ c. 0 ≈ rbc ʓ .

≈ rbc is barb-preserving, we have ʓ ⇓

> 0
b

⇓ ≥ 1
c

Since and ʓ . By the construction

of the test T it must be the case that ʓ has the form ʘ | c. 0 for some ʘ with

a
⃒ ʘ ʘ . By Lemma 7.4 and ʔ | c. 0 ≈ rbc ʘ | c. 0 , it follows that ʔ ≈ rbc ʘ .

Theorem 7.7 (Completeness) In rpCSP , ʔ ≈ rbc ʘ implies ʔ ≈ ʘ.
Proof

We show that ≈ rbc is a bisimulation. Because of symmetry it is sufficient to

⃒ i ∈ I p i · ʔ i with i ∈ I p i =

ʱ

show that if ʔ 1, where ʱ ∈ Act ˄ and I is a

⃒ i ∈ I p i ·

ʱ

finite index set, there is a matching move ʘ ʘ i for some ʘ i such that

ʔ i ≈ rbc ʘ i .
In fact , because of Proposition 7.4 it is sufficient to match a simple move ʔ

ʱ
⃒ ʔ

ʱ
⃒

ʘ such that ʔ ≈ rbc ʘ . But this can easily be established with a simple move ʘ

using Propositions 7.5 .