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

3.3 Lifting Relations

In the probabilistic setting, formal systems are usually modelled as distributions over
states. To compare two systems involves the comparison of two distributions. So we
need a way of lifting relations on states to relations on distributions. This is used,
for example, to define probabilistic bisimulation as we shall see in Sect. 3.5 . A few
approaches of lifting relations have appeared in the literature. We will take the one
from [ 22 ], and show its coincidence with two other approaches.

Definition 3.2 Given two sets S and T and a binary relation R ↆ S × T , the lifted

†

relation R ↆ D ( S ) × D ( T ) is the smallest relation that satisfies:

† t .

(1) s R t implies s R

I implies ( i ∈ I p i · ( i ∈ I p i ·

† ʘ i for all i †

(2) (Linearity) ʔ i R ∈ ʔ i ) R ʘ i ),

where I is a finite index set and i ∈ I p i =

1.

The are alternative presentations of Definition 3.2 . The following is used in many
proofs.

Proposition 3.1 Let ʔ and ʘ be two distributions over S and T , respectively, and

R ↆ × R

† ʘ if and only if there are two collections of states,

{

s i } i ∈ I S T . Then ʔ

{

t i } i ∈ I , and a collection of probabilities

{

p i } i ∈ I , for some finite index set I , such and

that i ∈ I p i = 1 and ʔ , ʘ can be decomposed as follows:

1. ʔ = i ∈ I p i · s i .

2. ʘ = i ∈ I p i · t i .
3. For each i ∈ I we have s i Rt i .

= i ∈ I p i ·

Proof ( ⃐ ) Suppos e we can decompose ʔ and ʘ as follows: (i) ʔ s i ,

= i ∈ I p i · (ii) ʘ t i , a n d (ii i) s i R t i for each i ∈ I . By (iii) and the first rule in

† t i for each i

Definition 3.2 ,wehave s i R ∈ I . By the second rule in Definition 3.2

we obtain that ( i ∈ I p i · ( i ∈ I p i ·

† † ʘ .

s i ) R t i ), that is ʔ R

( ⃒ ) We proceed by rule induction.

† ʘ because ʔ

• f ʔ R = s , ʘ = t and s R t , then we can simply take I to be the

singleton set { i } with p i = 1 and ʘ i = ʘ .

= i ∈ I p i · ʔ i , ʘ i = i ∈ I p i ·

† ʘ because of the conditions ʔ

• f ʔ R ʘ i for

†

some index set I , and ʔ i R ʘ i for each i ∈ I , the n by induction hyp ot hesis

there are index sets J i such that ʔ i = j ∈ J i p ij · s ij , ʘ i = j ∈ J i p ij ·

t ij , and

= i ∈ I j ∈ J i p i p ij ·

s ij R t ij for each i ∈ I an d j ∈ J i . It follows that ʔ s ij ,

= i ∈ I j ∈ J i p i p ij ·

ʘ t ij , and s ij R t ij for each i ∈ I and j ∈ J i . Therefore, it

suffices to take { ij | i ∈ I , j ∈ J i } to be the index set and { p i p ij | i ∈ I , j ∈ J i }

be the collection of probabilities.

An important point here is that in the decomposition of ʔ into i ∈ I p i ·

s i , the states
s i are not necessarily distinct : that is, the decomposition is not in general unique.
Thus when establishing the relationship between ʔ and ʘ , a given state s in ʔ may
play a number of different roles. This is reflected in the following property.