Editing Bisimulation (section)

== Alternative definitions ==

=== Relational definition ===
Bisimulation can be defined in terms of [[composition of relations]] as follows.

Given a [[state transition system|labelled state transition system]] <math>(S, \Lambda, \rightarrow)</math>, a ''bisimulation'' [[Relation (mathematics)|relation]] is a [[binary relation]] {{mvar|R}} over {{mvar|S}} (i.e., {{math|{{var|R}} &sube; {{var|S}} &times; {{var|S}}}}) such that <math>\forall\lambda\in\Lambda</math>

<math display="block">R\ ;\ \overset{\lambda}{\rightarrow}\quad {\subseteq}\quad \overset{\lambda}{\rightarrow}\ ;\ R</math>
and
<math display="block">R^{-1}\ ;\ \overset{\lambda}{\rightarrow}\quad {\subseteq}\quad \overset{\lambda}{\rightarrow}\ ;\ R^{-1}</math>

From the monotonicity and continuity of relation composition, it follows immediately that the set of bisimulations is closed under unions ([[join (order theory)|join]]s 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]].

=== Fixpoint definition ===

Bisimilarity can also be defined in [[Order theory|order-theoretical]] fashion, in terms of [[Knaster&ndash;Tarski theorem|fixpoint theory]], more precisely as the greatest fixed point of a certain function defined below.

Given a [[state transition system|labelled state transition system]] (<math>S</math>, &Lambda;, &rarr;), define <math>F:\mathcal{P}(S \times S) \to \mathcal{P}(S \times S)</math> to be a function from binary relations over <math>S</math> to binary relations over <math>S</math>, as follows:

Let <math>R</math> be any binary relation over <math>S</math>. <math>F(R)</math> is defined to be the set of all pairs <math>(p,q)</math> in <math>S</math> &times; <math>S</math> such that:

<math display="block">
\forall \lambda\in \Lambda. \, \forall p' \in S. \,
p \overset{\lambda}{\rightarrow} p' \, \Rightarrow \, 
\exists q' \in S. \, q \overset{\lambda}{\rightarrow} q' \,\textrm{ and }\, (p',q') \in R
</math>
and
<math display="block">
\forall \lambda\in \Lambda. \, \forall q' \in S. \,
q \overset{\lambda}{\rightarrow} q' \, \Rightarrow \, 
\exists p' \in S. \, p \overset{\lambda}{\rightarrow} p' \,\textrm{ and }\, (p',q') \in R
</math>

Bisimilarity is then defined to be the [[greatest fixed point]] of <math>F</math>.

===  Ehrenfeucht–Fraïssé game definition  ===
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, <math>\lambda</math>, from <math>(p,q)</math>. That is,
<math display="block">
(p,q) \overset{\lambda}{\rightarrow} (p',q)
</math>
or 
<math display="block">
(p,q) \overset{\lambda}{\rightarrow} (p,q')
</math>

The "Defender" must then attempt to match that transition, <math>\lambda</math> from either <math>(p',q)</math> or <math>(p,q')</math> depending on the attacker's move.
I.e., they must find an  <math>\lambda</math> such that:
<math display="block">
(p',q) \overset{\lambda}{\rightarrow} (p',q')
</math>
or 
<math display="block">
(p,q') \overset{\lambda}{\rightarrow} (p',q')
</math>

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 <math>(p,q)</math> 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 <math>(p,q)</math>, 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.

=== Coalgebraic definition ===

A bisimulation for state transition systems is a special case of [[F-coalgebra|coalgebraic]] bisimulation for the type of covariant powerset [[functor]].
Note that every state transition system <math>(S, \Lambda, \rightarrow)</math> can be mapped [[Bijection|bijectively]] to a function <math>\xi_{\rightarrow} </math> from <math>S</math> to the [[Power set|powerset]] of <math>S</math> indexed by <math>\Lambda</math> written as <math>\mathcal{P}(\Lambda \times S)</math>, defined by
<math display="block"> p \mapsto \{ (\lambda, q) \in \Lambda \times S : p \overset{\lambda}{\rightarrow} q \}.</math>

Let <math>\pi_i \colon S \times S \to S</math> be <math>i</math>-th [[Product (category theory)|projection]], mapping
<math>(p, q)</math> to <math>p</math> and <math>q</math> respectively for <math>i = 1, 2</math>; and
<math>\mathcal{P}(\Lambda \times \pi_1)</math> the forward image of <math>\pi_1</math> defined by dropping the third component
<math display="block"> P \mapsto \{ (\lambda, p) \in \Lambda \times S : \exists q . (\lambda, p, q) \in P \}</math>
where <math>P</math> is a subset of <math>\Lambda \times S \times S</math>. Similarly for <math>\mathcal{P}(\Lambda \times \pi_2)</math>.

Using the above notations, a relation <math>R \subseteq S \times S </math> is a '''bisimulation''' on a transition system <math>(S, \Lambda, \rightarrow)</math> if and only if there exists a transition system <math>\gamma \colon R \to \mathcal{P}(\Lambda \times R)</math> on the relation <math>R</math> such that the [[Commutative diagram|diagram]]

[[Image:Coalgebraic bisimulation.svg|frameless|upright=1.5]]

commutes, i.e. for <math>i = 1, 2</math>, the equations
<math display="block"> \xi_\rightarrow \circ \pi_i = \mathcal{P}(\Lambda \times \pi_i) \circ \gamma </math>
hold
where <math>\xi_{\rightarrow}</math> is the functional representation of <math>(S, \Lambda, \rightarrow)</math>.