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

• preserves barbs ; barbs are simple experiments which observers may perform on
systems
• s reduction-closed ; this is a natural condition on the reduction semantics of
systems which ensures that nondeterministic choices are in some sense preserved.

The three criteria chosen above are very robust because they can be formalised in a
similar way across different process description languages. In our setting, compo-
sitions of pLTSs and reduction semantics can be easily defined. For barbs, we use
predicates like P ⇓ ≥ a , which means that process P can expose the visible action a

with probability at least p . The details are given in Sect. 7.4 .

7.2 A Simple Bisimulation

Due to the use of weak arrows and the quantification over sets of probabilities, it
is difficult to directly apply Definition 7.1 and exhibit witness bisimulations. We,
therefore, give an alternative characterisation of

≈ in terms of a relation between

states and distributions by adapting Definition 6.29.

R ↆ × D

Definition 7.2 (Simple Bisimulation) A relation S ( S )isa simple (weak

probabilistic) bisimulation, if s R ʘ implies, for each ʱ ∈ Act ˄ ,

ʱ
−ₒ

ʱ
⃒ ʔ , there is some ʘ ʘ , such that ʔ R

† ʘ ;

(i) whenever s

˄
⃒

† ʔ .

(ii) there exists some ʔ ∈ D ( S ) such that s ʔ and ʘ R

We use ≈ s to denote the largest simple bisimulation. As in Remark 6.5, the bisimu-

lation game is implicitly limited to weak transitions that simulate by producing full
distributions only.
The precise relationship between the two forms of bisimulations is given by:

Theorem 7.1 Let ʔ and ʘ be two distributions in a finitary pLTS.

˄
⃒

≈ s ) † ʘ .

≈

ʘ then there is some ʘ with ʘ ʘ and ʔ (

(i) If ʔ

≈ s ) † ʘ then ʔ ≈

(ii) ʘ .

The remainder of this subsection is devoted to the proof of this theorem; it involves
first developing a number of subsidiary results.

If ʔ (

ʱ
−ₒ ≈ s ) † ʔ in an arbitrary pLTS. Then Proposition 7.1 Suppose ʔ ( ʘ and ʔ

ʱ
⃒ there exists some ʘ such that ʘ ʘ and ʔ ( ≈ s ) † ʘ .

ʱ
−ₒ ≈ s ) † ʔ . By Lemma 6.1 there is a finite index

Proof Suppose ʔ ( ʘ an d ʔ

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

set I such that (i) ʔ s i , (ii) ʘ ʘ i and (iii) s i ≈ s ʘ i for each

ʱ
−ₒ ʔ , (i) and Proposition 6.2, we can decompose ʔ into i ∈ I . By the condition ʔ

i ∈ I p i ·

ʱ
−ₒ ʔ i for some ʔ i such that s i ʔ i . By Lemma 6.1 again, for each i

∈ I ,

there is an index set J i such that ʔ i = j ∈ J i q ij ·

ʱ
−ₒ

ʔ ij ʔ ij and s i for each j ∈ J i

and j ∈ J i q ij =

ʱ
⃒

1. By (iii) there is some ʘ ij ʘ ij and ʔ ij ≈ s ) † ʘ ij . such that ʘ i (