Editing Bisimulation (section)

== Formal definition ==
Given a [[state transition system|labeled state transition system]] {{math|({{var|S}}, &Lambda;, &rarr;)}},
where {{mvar|S}} is a set of states, <math>\Lambda</math> is a set of labels and &rarr; is a set of labelled transitions (i.e., a subset of <math>S \times \Lambda \times S</math>),
a '''bisimulation''' is a [[binary relation]] <math>R \subseteq S \times S</math>,
such that both {{mvar|R}} and its [[converse relation|converse]] <math>R^T</math> are [[simulation preorder|simulation]]s. From this follows that the [[symmetric relation|symmetric]] closure of a bisimulation is a bisimulation, and that each symmetric simulation is a bisimulation. Thus some authors define bisimulation as a symmetric simulation.<ref>{{Cite journal |last=Jančar, Petr and Srba, Jiří |year=2008 |title=Undecidability of Bisimilarity by Defender's Forcing |url=https://doi.org/10.1145/1326554.1326559 |journal=[[J. ACM]] |location=New York, NY, USA |publisher=Association for Computing Machinery |volume=55 |pages=26 |doi=10.1145/1326554.1326559 |issn=0004-5411 |url-access=subscription |number=1 |s2cid=14878621}}</ref>

Equivalently, {{mvar|R}} is a '''bisimulation''' if and only if for every pair of states <math>(p,q)</math> in {{mvar|R}} and all labels ''&lambda;'' in <math>\Lambda</math>:

* if <math>p \mathrel{\overset{\lambda}{\rightarrow}} p'</math>, then there is <math>q \mathrel{\overset{\lambda}{\rightarrow}} q'</math> such that <math>(p',q') \in R</math>;
* if <math>q \mathrel{\overset{\lambda}{\rightarrow}} q'</math>, then there is <math>p \mathrel{\overset{\lambda}{\rightarrow}} p'</math> such that <math>(p',q') \in R</math>.

Given two states {{mvar|p}} and {{mvar|q}} in {{mvar|S}}, {{mvar|p}} is '''bisimilar''' to {{mvar|q}}, written <math>p \, \sim \, q</math>, if and only if there is a bisimulation {{mvar|R}} such that <math>(p, q) \in R</math>. This means that the bisimilarity relation {{resize|150%|&sim;}} is the union of all bisimulations: <math>(p,q) \in\,\sim\,</math> precisely when <math>(p, q) \in R</math> for some bisimulation {{mvar|R}}.

The set of bisimulations is closed under union;<ref group="Note">Meaning the union of two bisimulations is a bisimulation.</ref> therefore, the bisimilarity relation is itself a bisimulation. Since it is the union of all bisimulations, it is the unique largest bisimulation. Bisimulations are also closed under reflexive, symmetric, and [[transitive closure]]; therefore, the largest bisimulation must be reflexive, symmetric, and transitive. From this follows that the largest bisimulation—bisimilarity—is an [[equivalence relation]].<ref>{{Cite book |last=Milner |first=Robin |title=Communication and Concurrency |publisher=Prentice-Hall, Inc. |year=1989 |isbn=0131149849 |location=USA |authorlink=Robin Milner}}</ref>