Weak Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 238

Definition 7.4 ≈ rbc be the largest relation over the states that is

barb-preserving, reduction-closed and compositional.

In a pLTS, let

Theorem 7.6 (Soundness) In a finitary pLTS, if ʔ ≈ ʘ then ʔ ≈ rbc ʘ.

Proof Theorem 7.5 says that ≈ is compositional. It is also easy to see that ≈ is

reduction-closed. So it is sufficient to prove that ≈ is barb-preserving.

⇓ ≥ p Suppose ʔ ≈ ʘ and ʔ , for any action a and probability p , we need to show

a

⇓ ≥ p ⇓ ≥ p ʔ for some ʔ with V a ( ʔ )

that ʘ . We see from ʔ that ʔ ⃒ ≥ p . Since

a a

is reduction-closed, there exists ʘ such t ha t ʘ ʘ and ʔ ≈ ʘ .

the relation ≈ ⃒

⃒ s ∈ ʔ

˄

The degenerate weak transition ʔ ʔ ( s )

· s must be matched by some

transition

˄
⃒ ʘ ʔ ( s ) ʘ s · (7.1)

s ∈ ʔ

ʘ s . By Proposition 7.2 we know that s ≈ s ʘ s for each s ʔ such that s ≈ ∈ .

a
−ₒ

˄
⃒

a
−ₒ

˄
⃒ ʓ s for some distribution ʓ s , then ʘ s ʘ s ʘ

s

Now, if s for some

distributions ʘ s and ʘ

s

≈ s ) ʘ ʘ s |≥| ʘ s |=|

with ʓ s ( . It follows that | ʓ s |= 1.

s

a
−ₒ}

ʔ | , and ʘ be the distribution Let S a be the set of states { s ∈ s

⊛
⊝
s ∈ S a

⊞ ⊛

⊝
s

⊞

⊠ + ⊠ .

ʔ ( s ) · ʘ s ʔ ( s ) · ʘ s

∈ ʔ \ S a

˄
⃒

By the linearity and reflexivity of , Theorem 6.6, we have

⊛
⊝
s

⊞

˄
⃒

⊠

ʔ ( s ) ʘ s ʘ

· (7.2)

ʔ

∈

˄
⃒

˄
⃒

, we obtain ʘ ʘ , thus ʘ

⃒

ʘ . By ( 7.1 ), ( 7.2 ) and the transitivity of

V a ( ʘ ) ≥

It remains to show that p .

a
−ₒ S a we have ʘ s V a ( ʘ s ) Note that for each s ∈ , which means that = 1. It

follows that

= s ∈ S a ʔ ( s ) + s ∈ ʔ \ S a ʔ ( s )

V a ( ʘ ) · V a ( ʘ s ) · V a ( ʘ s )

≥ s ∈ S a ʔ ( s )

· V a ʘ s

= s ∈ S a ʔ ( s )
= V a ( ʔ )
≥

p.

In order to establish a converse to Theorem 7.6 , completeness , we need to work in
a pLTS that is expressive enough to provide appropriate contexts and barbs in order