Editing Bisimulation (section)

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