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

Chapter 7
Weak Probabilistic Bisimulation

Abstract By taking the symmetric form of simulation preorder, we obtain a notion of
weak probabilistic bisimulation. It provides a sound and complete proof methodology
for an extensional behavioural equivalence, a probabilistic variant of the traditional
reduction barbed congruence.

Keywords Weak probabilistic bisimulation · Reduction barbed congruence ·

Compositionality

7.1 Introduction

In Sect. 6.8, we have considered simulation preorder. By taking the symmetric form
of Definition 6.28 we easily obtain a notion of weak probabilistic bisimulation.

Definition 7.1 (Weak Probabilistic Bisimulation) Let S be the set of states in a
probabilistic labelled transitional system (pLTS). A relation R ↆ D ( S ) × D ( S )is

a weak (probabilistic) bisimulation if ʔ R ʘ implies, for each ʱ ∈ Act ˄ and all finite

satisfying i ∈ I p i = sets of probabilities { p i | i ∈ I } 1,

⃒ i ∈ I p i ·

ʱ

(i) whenever ʔ ʔ i , for any distributions ʔ i , there are some

⃒ i ∈ I p i ·

ʱ

distributions ʘ i with ʘ ʘ i , such that ʔ i R ʘ i for each i ∈ I ;

⃒ i ∈ I p i ·

ʱ

(ii) symmetrically, whenever ʘ ʘ i , for any distributions ʘ i , there

⃒ i ∈ I p i ·

ʱ

are some distributions ʔ i with ʔ ʔ i , such that ʔ i R ʘ i for each

i ∈ I .

The largest weak probabilistic bisimulation, which is guaranteed to exist using
standard arguments, is called weak probabilistic bisimilarity and denoted by

≈

.

is an equivalence relation. Moreover, it turns out that
this provides a sound and complete proof methodology for a natural extensional
behavioural equivalence between probabilistic systems, a generalisation of reduction
barbed congruence , the well-known behavioural equivalence for a large variety of
process description languages. Intuitively, reduction barbed congruence is defined
to be the coarsest relation that

It is easy to see that ≈

• s compositional ; that is preserved by some natural operators for constructing
systems