bisimulation (original) (raw)

Given two labelled state transition systems (LTS) M=(S1,Σ,→1), N=(S2,Σ,→2), a binary relation ≈⊆S1×S2 is called a simulation if whenever p≈q and p→α1p′, then there is a q′ such that p′≈q′ and q→α2q′. An LSTS M=(S1,Σ,→1) is similar to an LTS N=(S2,Σ,→2) if there is a simulation ≈S1×S2.

For example, any LTS is similar to itself, as the identity relation on the set of states is a simulation. In addition,

1. 1. if M is similar to N and N is similar to P, then M is similar to P:

Proof.

Let M=(S1,Σ,→1), N=(S2,Σ,→2), and P=(S3,Σ,→3) be LSTS, and suppose p≈1∘≈2q with p→α1p′, where ≈1 and ≈2 are simulations. Then there is an r such that p≈1r and r≈2q. Since ≈1 is a simulation, there is an r′ such that r→α2r′. But then since ≈2 is a simulation, there is a q′ such that q→α3q′. As a result, ≈1⁣∘⁣≈2 is a simulation. ∎ 2. 2.
a union of simulations is a simulation.

Proof.

Let ≈ be the union of simulations ≈i, where i∈I, and suppose p≈q, with p→αp′. Then p≈iq for some i. Since ≈i is a simulation, there is a state q′ such that p′≈iq′ and q→αq′. So p′≈q′ and therefore ≈ is a simulation. ∎

A binary relation ≈ between S1 and S2 is a bisimulation if both ≈ and its converse ≈-1 are simulations. A bisimulation is also called a strong bisimulation, in contrast with weak bisimulation. When there is a bisimulation between the state sets of two LTS, we say that the two systems are bisimilar, or strongly bisimilar. By abuse of notation, we write M≈N to denote that M is bisimilar to N.

An equivalent formulation of bisimulation is given by extending the binary relation on the sets to a binary relation on the corresponding power sets. Here’s how: let ≈⊆S1×S2. For any A⊆S1 and B⊆S2, define

Then the binary relation ≈ can be extended to a binary relation from P⁢(S1) to P⁢(S2), still denoted by ≈, as

for any A⊆S1 and B⊆S2. In other words, A≈B iff for any a∈A, there is a b∈B such that a≈b and for any b∈B, there is an a∈A such that a≈b. Now, for any p∈S1 and α∈Σ, let

We can similar define function δ2:S2×Σ→P⁢(S2). So a binary relation ≈ between S1 and S2 is a bisimilation iff for any (p,q)∈S1×S2 such that p≈q, we have δ1⁢(p,a)≈δ2⁢(q,a) for any a∈Σ.

Let M=(S1,Σ,→1), N=(S2,Σ,→2), and P=(S3,Σ,→3) be LTS. The following are some basic properties of bisimulation:

1. 1. The identity relation = is a bisimilation on any LTS, since = is a simulation and =-1 is just =.
2. 1. If M is bisimilar to N via ≈, then N is bisimilar to M via ≈-1, since both ≈-1 and (≈-1)-1=≈ are simulations.
3. 1. If M≈1 and N≈2P, then M≈1∘≈2P, since ≈1⁣∘⁣≈2 and (≈1∘≈2)-1=≈21-∘≈1-1 are both simulations according to the argument above.
4. 1. A union of bisimilations is a bisimilation.

Proof.

Let ≈ be the union of bisimulations ≈i, where i∈I. Then ≈ is a simulation by the argument above. Now, suppose p≈-1q and p→αp′, then q≈p. Then q≈ip for some i∈I. So p≈i-1q. Since ≈i is a bisimulation, so is ≈i-1, and therefore for some state q′, p′≈i-1q′ and q→αq′. This means that p′≈-1q′, implying that ≈-1 is a simulation. Hence ≈ is a bisimulation. ∎ 5. 5.
The union of all bisimilations on an LTS is a bisimulation that is also an equivalence relation.

For an LTS M=(S,Σ,→), let ≈M be the maximal bisimulation on M as defined above. Since ≈M is an equivalence relation, we can form an equivalence class [p] for each state p∈S. Let [S] be the set of all such equivalence classes: [S]:={[p]∣p∈S}. Define [→] on S×Σ×S by

This is a well-defined ternary relation, for if p≈Mp′ and q≈Mq′, we have p′→αq′. Now, [M]:=([S],Σ,[→]) is an LSTS, and M is bisimilar to it, with bisimulation given by the relation {(p,[p])∣p∈S}.