Bisimulation

Bisimulation can be defined in terms of composition of relations as follows.

Given a labelled state transition system ${\displaystyle (S,\Lambda ,\rightarrow )}$, a bisimulation relation is a binary relation ${\displaystyle R}$ over ${\displaystyle S}$ (i.e., ${\displaystyle R}$ ⊆ ${\displaystyle S}$ × ${\displaystyle S}$) such that ${\displaystyle \forall \alpha \in \Lambda }$

$${\displaystyle R\$$ ;\ {\overset {\alpha }{\rightarrow }}\quad {\subseteq }\quad {\overset {\alpha }{\rightarrow }}\ ;\ R}

and

$${\displaystyle R^{-1}\$$ ;\ {\overset {\alpha }{\rightarrow }}\quad {\subseteq }\quad {\overset {\alpha }{\rightarrow }}\ ;\ R^{-1}}

From the monotonicity and continuity of relation composition, it follows immediately that the set of bisimulations is closed under unions (joins in the poset of relations), and a simple algebraic calculation shows that the relation of bisimilarity—the join of all bisimulations—is an equivalence relation. This definition, and the associated treatment of bisimilarity, can be interpreted in any involutive quantale.

Bisimilarity can also be defined in order-theoretical fashion, in terms of fixpoint theory, more precisely as the greatest fixed point of a certain function defined below.

Given a labelled state transition system (${\displaystyle S}$, Λ, →), define ${\displaystyle F:{\mathcal {P}}(S\times S)\to {\mathcal {P}}(S\times S)}$ to be a function from binary relations over ${\displaystyle S}$ to binary relations over ${\displaystyle S}$, as follows:

Let ${\displaystyle R}$ be any binary relation over ${\displaystyle S}$. ${\displaystyle F(R)}$ is defined to be the set of all pairs ${\displaystyle (p,q)}$ in ${\displaystyle S}$ × ${\displaystyle S}$ such that:

$${\displaystyle \forall \alpha \in \Lambda .\,\forall p'\in S.\,p{\overset {\alpha }{\rightarrow }}p'\,\Rightarrow \,\exists q'\in S.\,q{\overset {\alpha }{\rightarrow }}q'\,{\textrm {and}}\,(p',q')\in R}$$

and

$${\displaystyle \forall \alpha \in \Lambda .\,\forall q'\in S.\,q{\overset {\alpha }{\rightarrow }}q'\,\Rightarrow \,\exists p'\in S.\,p{\overset {\alpha }{\rightarrow }}p'\,{\textrm {and}}\,(p',q')\in R}$$

Bisimilarity is then defined to be the greatest fixed point of ${\displaystyle F}$.

Bisimulation can also be thought of in terms of a game between two players: attacker and defender.

"Attacker" goes first and may choose any valid transition, ${\displaystyle \alpha }$, from ${\displaystyle (p,q)}$. That is,

$${\displaystyle (p,q){\overset {\alpha }{\rightarrow }}(p',q)}$$

or

$${\displaystyle (p,q){\overset {\alpha }{\rightarrow }}(p,q')}$$

The "Defender" must then attempt to match that transition, ${\displaystyle \alpha }$ from either ${\displaystyle (p',q)}$ or ${\displaystyle (p,q')}$ depending on the attacker's move. I.e., they must find an ${\displaystyle \alpha }$ such that:

$${\displaystyle (p',q){\overset {\alpha }{\rightarrow }}(p',q')}$$

or

$${\displaystyle (p,q'){\overset {\alpha }{\rightarrow }}(p',q')}$$

Attacker and defender continue to take alternating turns until:

• The defender is unable to find any valid transitions to match the attacker's move. In this case the attacker wins.
• The game reaches states ${\displaystyle (p,q)}$ that are both 'dead' (i.e., there are no transitions from either state) In this case the defender wins
• The game goes on forever, in which case the defender wins.
• The game reaches states ${\displaystyle (p,q)}$, which have already been visited. This is equivalent to an infinite play and counts as a win for the defender.

By the above definition the system is a bisimulation if and only if there exists a winning strategy for the defender.

A bisimulation for state transition systems is a special case of coalgebraic bisimulation for the type of covariant powerset functor. Note that every state transition system ${\displaystyle (S,\Lambda ,\rightarrow )}$ is bijectively a function ${\displaystyle \xi _{\rightarrow }}$ from ${\displaystyle S}$ to the powerset of ${\displaystyle S}$ indexed by ${\displaystyle \Lambda }$ written as ${\displaystyle {\mathcal {P}}(\Lambda \times S)}$, defined by

$${\displaystyle p\mapsto \{(\alpha ,q)\in \Lambda \times S:p{\overset {\alpha }{\rightarrow }}q\}.}$$

Let ${\displaystyle \pi _{i}\colon S\times S\to S}$ be ${\displaystyle i}$-th projection mapping ${\displaystyle (p,q)}$ to ${\displaystyle p}$ and ${\displaystyle q}$ respectively for ${\displaystyle i=1,2}$; and ${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{1})}$ the forward image of ${\displaystyle \pi _{1}}$ defined by dropping the third component

$${\displaystyle P\mapsto \{(\alpha ,p)\in \Lambda \times S:\exists q.(\alpha ,p,q)\in P\}}$$

where ${\displaystyle P}$ is a subset of ${\displaystyle \Lambda \times S\times S}$. Similarly for ${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{2})}$.

Using the above notations, a relation ${\displaystyle R\subseteq S\times S}$ is a bisimulation on a transition system ${\displaystyle (S,\Lambda ,\rightarrow )}$ if and only if there exists a transition system ${\displaystyle \gamma \colon R\to {\mathcal {P}}(\Lambda \times R)}$ on the relation ${\displaystyle R}$ such that the diagram

commutes, i.e. for ${\displaystyle i=1,2}$, the equations

$${\displaystyle \xi _{\rightarrow }\circ \pi _{i}={\mathcal {P}}(\Lambda \times \pi _{i})\circ \gamma }$$

hold where ${\displaystyle \xi _{\rightarrow }}$ is the functional representation of ${\displaystyle (S,\Lambda ,\rightarrow )}$.

• CADP: tools to minimize and compare finite-state systems according to various bisimulations
• mCRL2: tools to minimize and compare finite-state systems according to various bisimulations
• The Bisimulation Game Game