Editing Bisimulation (section)

=== 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>.