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

From Definition 3.2 , the next two properties follow. In fact, they are sometimes
used in the literature as definitions of lifting relations instead of being properties (see
e.g. [ 6 , 23 ]).

Theorem 3.1

† ʘ if and only

1. Let ʔ and ʘ be distributions over S and T , respectively. Then ʔ R

if there is a probability distribution on S , such

that ʔ and ʘ are its marginal distributions. In other words, there exists a weight
function w : S

× T , with support a subset of R

× T ₒ [0, 1] such that

S : t ∈ T

a) ∀ s ∈ w ( s , t ) = ʔ ( s ) .

T : s ∈ S w ( s , t )

b) ∀ t ∈ = ʘ ( t ) .

c) ∀ ( s , t ) ∈ S × T : w ( s , t ) > 0 ⃒ s R t.

2. Let ʔ and ʘ be distributions over S and R be an equivalence relation. Then

† ʘ if and only if ʔ ( C )

ʔ R = ʘ ( C ) for all equivalence classes C ∈ S/ R , where

ʔ ( C ) stands for the accumulation probability s ∈ C ʔ ( s ) .

Proof

†

⃒ R

1. ( ) Suppose ʔ ʘ . By Propositio n 3.1 , we can decompose ʔ and ʘ such

= i ∈ I p i · = i ∈ I p i ·

t i , and s i R

∈

that ʔ s i , ʘ t i for all i I . We define the

weight function w by letting

w ( s , t ) = { p i | s i = s , t i = t , i ∈ I }

for any s ∈ S , t ∈ T . This weight function can be checked to meet our

requirements.

a) For any s ∈ S ,wehave

t ∈ T

w ( s , t ) = { p i | s i = s , t i = t , i ∈ I }

t ∈ T

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

ʔ ( s ) .
b) Similarly, we have s ∈ S w ( s , t )

=

= ʘ ( t ).

c) For any s ∈ S , t ∈ T ,if w ( s , t ) > 0 then there is some i ∈ I such that p i > 0,

s i = s , and t i = t . It follows from s i R t i that s R t .

( ) Suppose there is a weight function w satisfying the three conditions in the

hypothesis. We construct the index set I

⃐

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

and probabilities p ( s , t ) = w ( s , t ) for each ( s , t ) ∈ I .