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

≈ s ) † ʘ .
First suppose ʔ

(a) ʔ (

⃒ i ∈ I p i · ʔ i . By Corollary 7.1 there is some distribution ʘ

ʱ

ʘ and ( i ∈ I p i ·

ʱ
⃒ ʔ i )( ≈ s ) † ʘ . But by Proposition 6.2 we know

with ʘ

≈ s ) † is left-decomposable. This means that ʘ = i ∈ I p i ·

ʘ i

that the relation (

for some distributions ʘ i such that ʔ i ≈ s ) † ʘ i ( for each i ∈ I . We, hence, have

the required matching move from ʘ .
For the converse, suppose ʘ

⃒ i ∈ I p i ·

ʱ

ʘ i . We have to find a matching

⃒ i ∈ I p i ·

ʱ

ʔ i , such that ʔ i R ʘ i . In fact it is sufficient to find

transition, ʔ

ʔ , such that i ∈ I p i ·

ʱ
⃒ ʘ i ≈ s ) † ʔ , since ( ( ≈ s ) † ) − 1

a transition ʔ ( ↆ R

and the deconstruction of ʔ into the required sum i ∈ I p i ·

ʔ i will again

≈ s ) † is left-decomposable. To this end let us abbreviate follow from the fact that (

i ∈ I p i ·

ʘ i to simply ʘ .
We know from ʔ ( ≈ s ) † ʘ , using the left-decomposability of ( ≈ s ) † , the convexity

= s ∈ ʔ

of ≈ s and Remark 6.1, that ʘ ʔ ( s ) · ʘ s for some ʘ s with s ≈ s ʘ s .

˄
⃒ ≈ s ) † ʔ s .

Now using Theorem 6.5(ii) it is easy to show the left-decomposability of weak
actions

Then, by the definition of ≈ s , s ʔ s for some ʔ s such that ʘ s (

ʘ , we can derive that ʘ = s ∈ ʔ

ʱ
⃒

ʱ
⃒ ʘ s ,

. Then from ʘ ʔ ( s ) ·

ʱ
⃒ ʘ s , for each s in the support of ʔ . Applying Corollary 7.1

such that ʘ s

≈ s ) † to ʘ s ( ʔ s we have, again for each s in the supp o rt of ʔ , a matching

ʱ
⃒

˄
⃒ ʔ s such that ʘ s ( ≈ s ) † ʔ s . But, since s

move ʔ s ʔ s , this gives

ʱ
⃒ ʔ s

ʱ
⃒

s , these

moves from the states s in the support of ʔ can be combined to obtain the action
ʔ

for each s ∈ ʔ ; using the linearity of weak actions

⃒ s ∈ ʔ ʔ ( s ) · ʔ s . The required ʔ is this sum, s ∈ ʔ ʔ ( s )

ʱ

· ʔ s , since

≈ s ) † ) − 1 ʘ .
(b) The second possibility is that ʔ ((

≈ s ) † gives ʔ (( linearity of (

≈ s ) † ʔ . But in this
case the proof that the relevant moves from ʘ and ʔ can be properly matched
is exactly the same as in case (a).

≈ s ) † ) − 1 ʘ , that is ʘ (

We also have a partial converse to Theorem 7.3 :

Proposition 7.2 In a finitary pLTS, s ≈ ʘ implies s ≈ s ʘ.

bis be the restriction of bis ʘ

Proof Le t ≈ ≈ to S × D ( S ), in the sense that s ≈

bis is a simple bisimulation. Suppose s bis ʘ .

whenever s ≈ ʘ . We show that ≈ ≈

ʱ
−ₒ

ʱ
⃒ ʔ . Then, since s ʘ (i) First suppose s ≈ ʘ there must exist some ʘ

⃒ t ∈ ʔ

˄

such that ʔ ≈ ʘ . Now consider the degenerate action ʔ ʔ ( t ) · t .

ʘ = t ∈ ʔ

˄
⃒

There mu s t be a matching move from ʘ , ʘ ʔ ( t ) ʘ t ·

ʘ t , that is t

s

bis ʘ t

ʔ

such that t ≈ ≈ for each t ∈ .

bis ) † ʘ and by the transitivity of

By linearity, this means ʔ (

s

≈ ⃒ we have

ʱ
⃒ ʘ .

the required matching move ʘ

˄
⃒ (ii) T o establish the second requirement, consider the tr ivial move ʘ ʘ . Since

˄
⃒

s ≈ ʘ , there must exist a corresponding move s ʔ such that ʔ ≈ ʘ .

Since ≈ is a symmetric relation, we also have ʘ ≈ ʔ . Now by an argument