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

† ʘ iff s R t for all t ∈ ʘ

Proposition 3.2 s R .

The lifting construction satisfies the following useful property.

T and i ∈ I p i = Proposition 3.3 (Left-Decomposable) Suppose R ↆ S × 1 .If

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

† ʘ then ʘ

ʔ i ) R ʘ i for some set of distributions { ʘ i } i ∈ I

† ʘ i for each i

such that ʔ i R ∈ I .

= i ∈ I p i ·

† ʘ . We have to find a family of ʘ i such

Proof Suppose ʔ ʔ i and ʔ R

that

† ʘ i for each i

(i) ʔ i R ∈ I .

= i ∈ I p i ·

(ii) ʘ i .

From the alternative characterisation of lifting, Proposition 3.1 , we know that

ʘ

ʔ = q j · s j s j R t j ʘ = q j · t j

j ∈ J j ∈ J

Define ʘ i to be

⊛ ⊞

q j
ʔ ( s ) ·

⊝ ⊠

ʔ i ( s ) · t j

s ∈ ʔ i { j ∈ J | s = s j }

Note that ʔ ( s ) can be written as { j ∈ J | s = s j } q j and therefore

⊛ ⊞

q j
ʔ ( s ) ·

⊝ ⊠

ʔ i = ʔ i ( s ) · s j

s ∈ ʔ i { j ∈ J | s = s j }

Since s j R t j this establishes (i) above.

To establish (ii) above let us first abbreviate the sum { j ∈ J | s = s j }

q j
ʔ ( s ) ·

t j to X ( s ).

Then i ∈ I p i · ʘ i can be written as

p i · ʔ i ( s ) · X ( s )

s ∈ ʔ i ∈ I

ʔ i ( s ) = p i · · X ( s )

s ∈ ʔ i ∈ I

= ʔ ( s ) · X ( s )

s ∈ ʔ

= i ∈ I p i · ʔ i ( s ).

The last equation is justified by the fact th at ʔ ( s )

= { j ∈ J | s = s j } q j · t j and therefore we have Now ʔ ( s ) · X ( s )

p i · ʘ i = q j ·

t j

i ∈ I s ∈ ʔ { j ∈ J | s = s j }

= q j · t j

j ∈ J

= ʘ