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

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

=

ʔ ( s ) . =

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

b) Similarly, we have ʘ t .

∈ R

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

c) For each ( s , t ) I ,wehave s

† ʘ .

The lifting operation given in Definition 3.2 is monotone and also preserves the
transitivity of the relation being lifted. Moreover, it is distributive with respect to the
composition of relations.

Proposition 3.4

R 1 † ↆ R 2 † 1. If R 1 ↆ R 2 then

R 1 · R 2 ) † = R 1 † · R 2 † 2. (

† .

3. If R is a transitive relation, then so is R

Proof
1. By Definition 3.2 , it is straightforward to show that if ʔ 1 R 1 † ʔ 2 and

R 1 ↆ R 2

then ʔ 1 R 2 † ʔ 2 .
2. We first show that ( R 1 · R 2 ) † ↆ R 1 † · R 2 † . Suppose there are two distributions

R 1 · R 2 ) † ʔ 2 . Then we have that ʔ 1 , ʔ 2 such that ʔ 1 (

ʔ 1 = p i · s i , s i R 1 · R 2 t i , ʔ 2 = p i · t i . (3.1)

i ∈ I i ∈ I

The middle part of ( 3.1 ) implies the existence o f some states s i such that s i R 1 s i

and s i R 2 t i . Let ʘ be the distribution i ∈ I p i · s i . It is clear that ʔ 1 R 1 † ʘ and

· R 2 † ʔ 2 .
Then we show the inverse inclusion

R 2 † ʔ 2 . It follows that ʔ 1 R 1 † ʘ

R 1 † · R 2 † R 1 · R 2 ) † . Given any three ↆ (

R 1 † R 2 †

distributions ʔ 1 , ʔ 2 and ʔ 3 , we show that if ʔ 1 ʔ 2 and ʔ 2 ʔ 3 then

R 1 · R 2 ) † ʔ 3 .
First ʔ 1 R 1 † ʔ 2 means that
ʔ 1 =

ʔ 1 (

s i R 1 s i , s i p i · s i , ʔ 2 = p i · ; (3.2)

i ∈ I i ∈ I

also ʔ 2 R 2 † ʔ 3 means that
ʔ 2 = t j , t j R 2 t j , q j · ʔ 3 = q j · t j ; (3.3)

j ∈ J j ∈ J

and we can assume without loss of generality that all the coefficients p i , q j are
nonzero. Now define I j ={

s i = t j } t j = s i }

i ∈ I | and J i ={ j ∈ J | , so that

trivially

{ ( i , j ) | i ∈ I , j ∈ J i } ={ ( i , j ) | j ∈ J , i ∈ I j } (3.4)