Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 29

a) We have ʔ = ( s , t ) ∈ I p ( s , t ) · s because, for any s ∈ S ,
( s , t ) ∈ I p ( s , t ) ·

s ( s )

( s , t ) ∈ I w ( s , t )

=

= { w ( s , t ) | w ( s , t ) > 0, t ∈ T }

= { w ( s , t ) | t ∈ T }

= ʔ ( s ) .

= ( s , t ) ∈ I b) Similarly, we have ʘ w ( s , t ) · t .

c) For each ( s , t ) ∈ I ,wehave w ( s , t ) > 0, which implies s R t .

Hence, the above decompositions of ʔ and ʘ meet the requirement of the lifting
ʔ

† ʘ .

R

† ʘ . By Propos it ion 3.1 , we can decompose ʔ and ʘ such that

2. ( ⃒ ) Suppose ʔ R

= i ∈ I p i · = i ∈ I p i · ʔ s i , ʘ t i , and s i R t i for all i ∈ I . For any equivalence

class C ∈ S/ R , we have that

s ∈ C ʔ ( s ) s ∈ C

ʔ ( C ) = = { p i | i ∈ I , s i = s }

= { p i | i ∈ I , s i ∈ C }

= { p i | i ∈ I , t i ∈ C }

= ʘ ( C )

where the equality in the third line is justified by the fact that s i ∈ C iff t i ∈ C
since s i R t i and C ∈ S/ R .

( ⃐ ) Suppose ʔ ( C ) = ʘ ( C ) for each equivalence class C ∈ S/ R . We construct

ʔ ( s ) ʘ ( t )
ʔ ([ s ])

the index set I ={ ( s , t ) | s R t and s , t ∈ S } and probabilities p ( s , t ) = for

each ( s , t ) ∈ I , where [ s ] stands for the equivalence class that contains s .

= ( s , t ) ∈ I p ( s , t ) ·

s because, for any s ∈

a) We have ʔ S ,

( s , t ) ∈ I p ( s , t ) ·

s ( s )

( s , t ) ∈ I p ( s , t )

=

ʔ ( s ) ʘ ( t )
ʔ ([ s ]) |

S s R

= t , t ∈

ʔ ( s ) ʘ ( t )
ʔ ([ s ]) |

[ s ]

= ∈

t

ʔ ([ s ])

ʔ ( s )

[ s ]

= { ʘ ( t ) | t ∈ }

ʔ ( s )
ʔ ([ s ]) ʘ ([ s ])

=