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

Proof is closed under countable

disjoint unions because probability distributions are ˃ -additive. Since ʔ and ʘ are
distributions, we have ʔ ( S )

Let X ={ A ∈ A | ʔ ( A ) = ʘ ( A ) } . Then X

= ʘ ( S ) = 1. It follows that if A ∈ X then ʔ ( S \ A ) =

ʔ ( S ) − ʔ ( A ) = ʘ ( S ) − ʘ ( A ) = ʘ ( S \ A ), i.e. S \ A ∈ X . Thus X is closed under

complementation as well. It follows that X is a ʻ -class. Note that A 0 is a ˀ -class

in view of the equation [[ ˕ 1 ∧ ˕ 2 ]] = [[ ˕ 1 ]] ∩ [[ ˕ 2 ]]. Since A 0 ↆ X , we can apply

the ˀ - ʻ Theorem to obtain that A = ˃ ( A 0 ) ↆ X ↆ A , i.e. A = X . Therefore,

ʔ ( B )

The following theorem has appeared in [ 51 ], which is obtained by simplifying
the results of [ 46 ] in reactive pLTSs with countable state spaces.

= ʘ ( B ) for any B ∈ A .

= L rhm t.

Theorem 3.8 Let s and t be two states in a reactive pLTS. Then s ∼ t iff s

Proof The proof of soundness is carried out by a routine induction on the structure
of formulae. Below we focus on the completeness. It suffices to show that

= L rhm

is

= L rhm

a bisimulation. Note that is clearly an equivalence relation. For any u ∈ S the

equivalence class in S/ = L rhm that contains u is

[ u ] = { [[ ˕ ]] | u |= ˕ }∩ { S \ [[ ˕ ]] | u |= ˕ } . (3.17)

In ( 3.17 ) only countable intersections are used because the set of all the formulae
in the logic

A 0 be defined as in Proposition 3.9 . Then each
equivalence class of S/ = L rhm is a member of ˃ (

L rhm is countable. Let

A 0 ).

a
−ₒ ʔ implies that some distribution ʘ exists On the other hand, s = L rhm t and s

a
−ₒ

with t ʘ and for any ˕ ∈ L rhm , ʔ ([[ ˕ ]] ) = ʘ ([[ ˕ ]]) by Lemma 3.4 . Thus by

Proposition 3.9 we have

ʔ ([ u ]) = ʘ ([ u ]) (3.18)

where [ u ] is any equivalence class of S/ = L rhm . Then it follows from Theorem 3.1 (2)
that ʔ (

= L rhm ) † ʘ . Symmetrically, any transition of t can be mimicked by a
transition from s . Therefore, the relation = L rhm

is a bisimulation.

L rhm can characterise bisimulation for reactive pLTSs,
and this logic has neither negation nor infinite conjunction. Moreover, the above
result holds for general reactive pLTSs that may have countable state space and are
not necessarily finitely branching.

Theorem 3.8 tells us that

3.6.2 An Expressive Logic

In this section we add the probabilistic-choice modality introduced in Sect. 3.6.1
to the modal mu-calculus, and show that the resulting probabilistic mu-calculus is
expressive with respect to probabilistic bisimilarity.