bisimulation


Given two labelled state transition systems (LTS) M=(S1,Σ,1), N=(S2,Σ,2), a binary relationMathworldPlanetmath S1×S2 is called a simulation if whenever pq and pα1p, then there is a q such that pq and qα2q. An LSTS M=(S1,Σ,1) is similarPlanetmathPlanetmath 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 p12q with pα1p, where 1 and 2 are simulations. Then there is an r such that p1r and r2q. 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, 12 is a simulation. ∎

  2. 2.

    a union of simulations is a simulation.

    Proof.

    Let be the union of simulations i, where iI, and suppose pq, with pαp. Then piq for some i. Since i is a simulation, there is a state q such that piq and qαq. So pq and therefore is a simulation. ∎

A binary relation between S1 and S2 is a bisimulation if both and its converseMathworldPlanetmath -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 MN to denote that M is bisimilar to N.

An equivalentMathworldPlanetmathPlanetmathPlanetmath formulation of bisimulation is given by extending the binary relation on the sets to a binary relation on the corresponding power setsMathworldPlanetmath. Here’s how: let S1×S2. For any AS1 and BS2, define

C(A):={bS2ab for some aA} and C(B):={aS1ab for some bB}.

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

ABiffAC(B) and BC(A),

for any AS1 and BS2. In other words, AB iff for any aA, there is a bB such that ab and for any bB, there is an aA such that ab. Now, for any pS1 and αΣ, let

δ1(p,a)={qS1pα1q}.

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 pq, 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. 2.

    If M is bisimilar to N via , then N is bisimilar to M via -1, since both -1 and (-1)-1= are simulations.

  3. 3.

    If M1 and N2P, then M12P, since 12 and (12)-1=21-1-1 are both simulations according to the argument above.

  4. 4.

    A union of bisimilations is a bisimilation.

    Proof.

    Let be the union of bisimulations i, where iI. Then is a simulation by the argument above. Now, suppose p-1q and pαp, then qp. Then qip for some iI. So pi-1q. Since i is a bisimulation, so is i-1, and therefore for some state q, pi-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.

    Proof.

    For an LTS M, let M be the union of all bisimulations on M. Then M is a bisimulation by the previous result. Since = is a bisimulation on M, M is reflexiveMathworldPlanetmathPlanetmathPlanetmathPlanetmath. If pMq, pq for some bisimulation on M. Then -1 is a bisimulation and therefore q-1p implies that qMp, so that M is symmetricPlanetmathPlanetmathPlanetmath. Finally, if pMq and qMr, then p1q and q2r for some bisimulations 1 and 2. So 12 is a bisimulation. Since p12r, pMr and therefore M is transitiveMathworldPlanetmathPlanetmathPlanetmath. ∎

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 classMathworldPlanetmath [p] for each state pS. Let [S] be the set of all such equivalence classes: [S]:={[p]pS}. Define [] on S×Σ×S by

[p][]α[q]  iff  pαq.

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

Title bisimulation
Canonical name Bisimulation
Date of creation 2013-03-22 19:23:14
Last modified on 2013-03-22 19:23:14
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 44
Author CWoo (3771)
Entry type Definition
Classification msc 03B45
Classification msc 68Q85
Classification msc 68Q10
Synonym strong bisimulation
Synonym strongly bisimilar
Related topic PMorphism
Defines simulation
Defines bisimilar