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

3.5 Probabilistic Bisimulation

With a solid base of the lifting operation, we can proceed to define a probabilistic
version of bisimulation.
Let s and t be two states in a pLTS. We say t can simulate the behaviour of s if
whenever the latter can exhibit action a and lead to distribution ʔ then the former can
also perform a and lead to a distribution, say ʘ , which then in turn can mimic ʔ in
successor states. We are interested in a relation between two states, but it is expressed
by invoking a relation between two distributions. To formalise the mimicking of one
distribution by the other, we make use of the lifting operation investigated in Sect. 3.3 .

Definition 3.5 A relation R ↆ S × S is a probabilistic simulation if s R t implies

a
−ₒ

a
−ₒ

• f s ʔ then there exists some ʘ such that t ʘ and ʔ R

† ʘ .

R − 1 If both R and are probabilistic simulations, then R is a probabilistic bisimu-

lation . The largest probabilistic bisimulation, denoted by ∼ , is called probabilistic

bisimilarity .
As in the nonprobabilistic setting, probabilistic bisimilarity can be approximated
by a family of inductively defined relations.

Definition 3.6 Let S be the state set of a pLTS. We define:

• ∼ 0 : = S × S

• s ∼ n + 1 t , for n ≥ 0, if

a
−ₒ

a
−ₒ ∼ n ) † ʘ ;

1. whenever s ʔ , there exists some ʘ such that t ʘ and ʔ (

a
−ₒ

a
−ₒ ∼ n ) † ʘ . 2. whenever t ʘ , there exists some ʔ such that s ʔ and ʔ (

= n ≥ 0 ∼ n
In general,

• ∼ ˉ :

∼ ˉ . However, the two relations coin-
cide when limited to image-finite pLTSs where for any state s and action a , the set
{

∼ is a strictly finer relation than

a
−ₒ

ʔ ∈ D ( S ) | s ʔ } is finite.

Proposition 3.8 On image-finite pLTSs, ∼ ˉ coincides with ∼ .

Proof It is trivial to show by induction that s ∼ t implies s ∼ n t for all n ≥ 0, and

thus that s ∼ ˉ t .

Now we show that

a
−ₒ

∼ ˉ is a bisimulation. Suppose s ∼ ˉ t and s ʔ .By

a
−ₒ ∼ n ) † ʘ n .

Since we are considering image-finite pLTSs, there are only finitely many different
ʘ n 's. Then for at least one of them, say ʘ ,wehave ʔ (

≥

assumption for all n 0 there exists some ʘ n with t ʘ n and ʔ (

∼ n ) † ʘ for infinitely many
different n 's. By a straightforward induction we can show that s ∼ n t implies s ∼ m t
for all m , n ≥ ∼ n ) † ʘ for all n ≥ 0 with n>m . It follows that ʔ ( 0. We now claim

that

∼ ˉ ) † ʘ (3.12)
To see this, let A be any subset of the whole state space that may be countable. For any
n ≥

ʔ (

∼ n ) † ʘ we know from Theorem 3.5 (1) that ʔ ( A )

0, since ʔ ( ≤ ʘ ( ∼ n ( A )) .