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

a
−ₒ ʔ 1 and t

a
−ₒ ʔ 2

• The final possibility for ʱ is ˄ and ʓ is ( ʔ 1 | ʔ 2 ) , where s

a
⃒ ∈ ≈ s ʘ , we have a transition ʘ

ʘ such that

for some a A . Here, since s

≈ s ) † ʔ 1 ( ʘ . By combining these transitions using part (iii) of Lemma 7.3 we

˄
⃒ |

ʘ |

obtain ʘ ʔ 2 . Again this is the required matching transition since an

application of (a) above gives ( ʔ 1 |

t

† .

ʔ 2 , ʘ | ʔ 2 ) ∈ R

≈ s ) † ʘ implies ( ʔ | ʓ )( ≈ s ) †

Corollary 7.4 In an arbitrary pLTS, ʔ ( ( ʘ | ʓ )

Proof A simple consequence of the previous compositionality result, using a
straightforward linearity argument.

Theorem 7.5 (Compositionality of ≈ ) Let ʔ , ʘ and ʓ be any distributions in a

finitary pLTS. If ʔ ≈ ʘ then ʔ | ʓ ≈ ʘ | ʓ .

Proof We show that the relation

R ={ ( ʔ | ʓ , ʘ | ʓ ) | ʔ ≈ ʘ }∪ ≈

is a bisimulation, from which the result follows.
Suppose ( ʔ | ʓ , ʘ | ʓ ) ∈ R . Since ʔ ≈ ʘ , we know from Theorem 7.1 that some

˄
⃒ ʘ exists such that ʘ ʘ and ʔ ( ≈ s ) † ʘ and the previous corollary implies

≈ s ) † ( ʘ | ʓ ); by Theorem 7.1 this gives ( ʔ | ʓ ) ( ʘ | ʓ ). that ( ʔ | ʓ )( ≈

is a weak bisimulation. Consider the transitions from both
( ʔ | ʓ ) and ( ʘ | ʓ ); by symmetry it is sufficient to show that the transitions of the
former can be matched by the latter. Suppose that ( ʔ | ʓ )

We now show that R

( i p i · ʔ i ). Then,

ʱ
⃒

( i p i ·

ʱ
⃒ ( ʘ | ʘ i ) with ʔ i ≈ ʘ i

ʓ ) for each i . But by part (i) of Lemma 7.3

˄
⃒

˄
⃒

( ʘ | ( ʘ | ʓ ) ʓ ) and therefore by the transitivity of we have the required

( i p i ·

ʱ
⃒ ʘ i ).

matching transition ( ʘ | ʓ )

7.4 Reduction Barbed Congruence

We now introduce an extensional behavioural equivalence called reduction barbed
congruence and show that weak bisimilarity is both sound and complete for it.

∈ D ∈ Act V a ( ʔ ) =

Definition 7.3 (Barbs) For ʔ ( S ) and a let

{

a
−ₒ} ⇓ ≥ p ʔ , where V a ( ʔ )

ʔ ( s ) | s . We write ʔ whenever ʔ ⃒ ≥ p .

a

⇓ ≥ p

> 0
a

We also we use the notation ʔ ⇓ to mean that ʔ does not hold for any p> 0.

a

⇓ ≥ p ⇓ ≥ p

Then we say a relation R is barb-preserving if ʔ iff ʘ whenever ʔ R ʘ .

a a

It is reduction-closed if ʔ R ʘ implies

⃒

ʔ , there is a ʘ

⃒

ʘ such that ʔ R ʘ (i) whenever ʔ

⃒

ʘ , there is a ʔ

⃒

ʔ such that ʔ R ʘ . (ii) whenever ʘ

Finally, we say that in a binary relation R is compositional if ʔ 1 R ʔ 2 implies

( ʔ 1 | ʘ ) R ( ʔ 2 | ʘ ) for any distribution ʘ .