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

By the second part of Lemma 7.1 ,( ʔ | ʘ ) may be written as t ∈ ʘ ʘ ( t ) · ( ʔ | t ) and

−ₒ t ∈ ʘ

ʱ

( ʔ |

therefore another application of linearity gives ʔ | ʘ ʘ ( t ) · t ) and

by the same result this residual coincides with ( ʔ |

ʘ ) .

Lemma 7.3 In a pLTS,

ʔ implies ʔ ʔ |

(i) ʔ ⃒ | ʘ ⃒ ʘ ;

ʱ
⃒

ʱ
⃒ ʔ implies ʔ ʔ |

(ii) ʔ | ʘ ʘ , for ʱ ∈ Act ˄ ;

a
⃒

a
⃒

˄
⃒ ʔ 1 and ʔ 2 ʔ 2 implies ʔ 1 | ʔ 1 | ʔ 2 , for a

(iii) ʔ 1 ʔ 2 ∈ Act .

Proof Parts (ii) and (iii) follow from (i) and the corresponding result in the previous

lemma.
For (i) suppose ʔ ʔ . First note that a weak move from ʔ to k = 0 ʔ k =

⃒

ʔ ,

as in Definit i on 6.4, can easily be transformed into a weak tr a nsition fro m ( ʔ | t )to

k = 0 ( ʔ k | t ). This means that for any state t we have a ( ʔ | t )

( ʔ | t ).
By the second part of Lemma 7.1 ,( ʔ | ʘ ) can be written as t ∈ ʘ ʘ ( t )

⃒

· ( ʔ | t ) ,

⃒ t ∈ ʘ ʘ ( t ) ( ʔ | t ) and since ⃒ is linear, Theorem 6.5(i), this means ( ʔ | ʘ ) ·

and again Lemma 7.1 renders this residual to be ( ʔ | ʘ ).

Theorem 7.4 (Compositionality of ≈ s ) L e t s , t be states and ʘ a distribution in

an arbitrary pLTS, if s ≈ s ʘ then s | t ≈ s ʘ | t.

Proof We construct the following relation

R ={ ( s | t , ʘ | t ) | s ≈ s ʘ }

and check that R is a simple bisimulation in the associated pLTS. This will imply

that R ↆ≈ s , from which the result follows. Note that by construction we have that

(a) ʔ 1 (

†

≈ s ) † ʔ 2 , which implies ( ʔ 1 |

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

We use this pro p erty throughout the proof.
Let ( s

. We first prove property (ii) in Definition 7. 2 , which turns
out to be straightforward. Since s

| t , ʘ | t ) ∈ R

˄
⃒ ≈ s ʘ , there is so me ʔ su c h that s ʔ and

˄
⃒

≈ s ) † ʔ . A n application of Lemma 7.3 (ii) gives s ʘ ( | t ʔ | t and property (a) that

†

( ʘ | t ).

Let us concentrate on property (i) where we must prove that every transition from

t ) R ( ʔ |

ʱ
−ₒ s | t has a matching weak transition from ʘ | t . Assume that s | t ʓ for some action

ʱ and distribution ʓ . There are three possibilities:

ʱ
−ₒ ʓ is ʔ | t for some action ʱ and distribution ʔ with s ʔ . Here we have

•

ʱ
⃒

≈ s ) † ʘ , since s

ʘ suc h that ʔ (

ʘ ≈ s ʘ . Mor e over b y Lemma 7.3 (ii), we

ʱ
⃒

† , and therefore

ʘ | t . Again by (a), we have ( ʔ | t , ʘ |

can deduce ʘ | t t ) ∈ R

a matching transition.

ʱ
−ₒ ʔ , where t ʔ . Here a symmetric version of Lemma 7.2 (i)

• Suppose ʓ is s |

ʱ
−ₒ

ʔ . This is the required matching transition since we can use
(a) above to deduce ( s

| |

gives ʘ t ʘ

† .

|

ʔ , ʘ

|

ʔ )

∈ R