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

symmetric to that used in part (i) we can show that this implies the existence
of some ʔ such that ʔ

˄
⃒ ʔ , that is s

˄
⃒ ʔ and ʘ (

bis ) † ʔ .

≈

≈ s ) † do not coincide for arbitrary distributions.
For example, consider the two processes P = a. 0 2 ↕ b. 0 and Q = P P . It is easy
to see that [[ P ]]

But in general the relations ≈ and (

≈ s ) †

≈ [[ Q ]] b u t n o t [[ P ]] ( [[ Q ]]; the latter follows because the point

1 1

distribution [[ Q ]] cannot be decomposed as

2 ·

ʘ a +

2 ·

ʘ b for some ʘ a and ʘ b so

that [[ a. 0 ]] ≈ s ʘ b .

The nearest to a general converse to Theorem 7.3 is the following:

≈ s ʘ a and [[ b. 0 ]]

ʘ in a finitary pLTS. Then there is some ʘ with Proposition 7.3 Suppose ʔ ≈

˄
⃒ ≈ s ) † ʘ .

Proof Now suppose ʔ

ʘ and ʔ (

ʘ

ʘ . We can rewrite ʔ as s ∈ ʔ ≈ ʔ ( s ) · s , and the reflexivity

⃒ s ∈ ʔ

˄
⃒

˄

of gives ʔ ʔ ( s ) · s . Since ≈ is a bisimulation, this move can be

ʘ = s ∈ ʔ

˄
⃒ matched by some ʘ ʔ ( s ) · ʘ s such that s ≈ ʘ s . But we have

just shown in the previous proposition that this means s ≈ s ʘ s .

ʱ
⃒ ≈ s ) † ʘ and therefore ʘ ʘ is the required move. By Definition 6.2, ʔ (

from Definition 7.1 , is our primary behavioural equiv-
alence but we will often develop properties of it via the connection we have just
established with

The weak bisimilarity, ≈

≈ s from Definition 7.2 ; the latter is more amenable as it only re-
quired strong moves to be matched. However, we can also prove properties of ≈ s by

using this connection to weak bisimilarity; a simple example is the following:

˄

≈ s ʘ in a finitary pLTS, where s −ₒ

Corollary 7.2 Suppose s . Then whenever

˄
⃒

ʘ it follows that s

≈ s ʘ .

ʘ

≈ s ) †

Proof Suppose s ≈ s ʘ , which means s ( ʘ and therefore by Theorem 7.3

˄
⃒ ≈

ʘ must be matched by a corresponding m ove from s .

s ʘ . The move ʘ

˄

ʘ .Now

However, since s −ₒ the only possibility is the empty move, giving s ≈

by Proposition 7.2 , we have the required s ≈ s ʘ .

Corollary 7.3 In any finitary pLTS, the relation ≈ is linear.

Consider any collection of probabilities p i with i ∈ I p i = Proof 1, where I is a

finite index set. Suppose further that ʔ i ≈ ʘ i for each i ∈ I . We need to show that

= i ∈ I p i · = i ∈ I p i · ʔ ≈ ʘ , where ʔ ʔ i and ʘ ʘ i .

˄
⃒

By Proposition 7.3 , there is some ʘ i ʘ i ≈ s ) † ʘ i .By with ʘ i and ʔ i (

˄
⃒ ≈ s ) †

Theorem 6.6 (i) and Definition 6.2, both and ( are linear. Therefore, we

ʘ , where ʘ = i ∈ I p i ·

˄
⃒ ʘ and ʔ ( ≈ s ) † ʘ i . It follows from

have ʘ

ʘ .
Now for any transition ʔ

Theorem 7.3 that ʔ ≈

( j ∈ J q j ·

ʱ
⃒

ʔ j ), where J is finite, there is a

( j ∈ J q j ·

ʱ
⃒

matching transition ʘ ʘ j ) such that ʔ j ≈ ʘ j for each j ∈ J . Note

( j ∈ J q j ·

ʱ
⃒

that we also have the transition ʘ ʘ j ) according to the transitivity

( j ∈ J q j ·

˄
⃒

ʱ
⃒

of . By symmetrical arguments, any transition ʘ ʘ j ) can be

( j ∈ J q j ·

ʱ
⃒

matched by some transition ʔ ʔ j ) such that ʔ j ≈ ʘ j for each