Editing Bisimulation

{{Short description|Relation between transition systems in computer science}}
{{More citations needed|date=February 2017}}
In [[theoretical computer science]] a '''bisimulation''' is a [[binary relation]] between state [[transition system]]s, associating systems that behave in the same way in that one system simulates the other and vice versa.

Intuitively two systems are bisimilar if they, assuming we view them as playing a ''game'' according to some rules, match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.

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

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

== Variants of bisimulation ==
In special contexts the notion of bisimulation is sometimes refined by adding additional requirements or constraints. An example is that of [[stutter bisimulation]], in which one transition of one system may be matched with multiple transitions of the other, provided that the intermediate states are equivalent to the starting state ("stutters").<ref>{{cite book |last1=Baier |first1=Christel|author1-link= Christel Baier |last2=Katoen |first2=Joost-Pieter|author2-link=Joost-Pieter Katoen |title=[[Principles of Model Checking]] |date=2008 |publisher=MIT Press |isbn=978-0-262-02649-9 |page=527}}</ref>

A different variant applies if the state transition system includes a notion of ''silent'' (or ''internal'') action, often denoted with <math>\tau</math>, i.e. actions that are not visible by external observers, then bisimulation can be relaxed to be ''weak bisimulation'', in which if two states <math>p</math> and <math>q</math> are bisimilar and there is some number of internal actions leading from <math>p</math> to some state <math>p'</math> then there must exist state <math>q'</math> such that there is some number (possibly zero) of internal actions leading from <math>q</math> to <math>q'</math>. A relation <math>\mathcal{R}</math> on processes is a weak bisimulation if the following holds (with <math>\mathcal{S} \in \{ \mathcal{R}, \mathcal{R}^{-1} \}</math>, and <math>a,\tau</math> being an observable and mute transition respectively):

<math display="block">\forall p, q. \quad (p,q) \in \mathcal{S} \Rightarrow p \stackrel{\tau}{\rightarrow} p' \Rightarrow \exists q' . \quad q \stackrel{\tau^\ast}{\rightarrow} q' \wedge (p',q') \in \mathcal{S} </math>
<math display="block">\forall p, q. \quad (p,q) \in \mathcal{S} \Rightarrow p \stackrel{a}{\rightarrow} p' \Rightarrow \exists q' . \quad q \stackrel{\tau^\ast a \tau^\ast}{\rightarrow} q' \wedge (p',q') \in \mathcal{S} </math>

This is closely related{{how|date=September 2023}} to the notion of bisimulation "[[up to]]" a relation.<ref name="Pous2005">{{cite journal |author=Damien Pous |title=Up-to techniques for weak bisimulation |journal=Proc. 32nd ICALP |series=[[Lecture Notes in Computer Science]] |volume=3580 |publisher=Springer Verlag |year=2005 |pages=730–741}}</ref>

Typically, if the [[state transition system]] gives the [[operational semantics]] of a [[programming language]], then the precise definition of bisimulation will be specific to the restrictions of the programming language. Therefore, in general, there may be more than one kind of bisimulation (respectively bisimilarity) relationship depending on the context.

== Bisimulation and modal logic ==

Since [[Kripke semantics|Kripke models]] are a special case of (labelled) state transition systems, bisimulation is also a topic in [[modal logic]]. In fact, modal logic is the fragment of [[first-order logic]] invariant under bisimulation ([[Johan van Benthem (logician)|van Benthem's theorem]]).

== Algorithm ==
Checking that two finite transition systems are bisimilar can be done in [[polynomial time]].{{sfnp|Baier|Katoen|2008|loc=Corollary 7.45, p. 486}} The fastest algorithms are [[quasilinear time]] using [[partition refinement]] through a reduction to the coarsest [[partition problem]].

== See also ==
* [[Simulation preorder]]
* [[Congruence relation]]
* [[Probabilistic bisimulation]]

== Notes ==
{{reflist|group=Note}}
== References ==
{{Reflist}}

==Further reading==
* {{Cite conference
 | first = David
 | last = Park
 | year = 1981
 | title = Concurrency and Automata on Infinite Sequences
 | conference = Proceedings of the 5th GI-Conference, Karlsruhe
 | book-title = Theoretical Computer Science
 | series = [[Lecture Notes in Computer Science]]
 | editor = Deussen, Peter
 | pages = 167–183
 | volume = 104
 | publisher = [[Springer-Verlag]]
 | isbn = 978-3-540-10576-3
 | doi = 10.1007/BFb0017309
}}
* {{Cite book
 | last = Milner
 | first = Robin
 | title = Communication and Concurrency
 | year = 1989
 | publisher = [[Prentice Hall]]
 | isbn = 0-13-114984-9
 }}
*{{Cite book |last=Sangiorgi |first=Davide |authorlink = Davide Sangiorgi|url=https://www.worldcat.org/oclc/773040572 |title=An introduction to Bisimulation and Coinduction |date=2011 |publisher=Cambridge University Press |isbn = 9781107003637 |location=Cambridge, UK |oclc=773040572}}

==External links==

=== Software tools ===
* [[CADP]]: [http://cadp.inria.fr 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
* [http://www.brics.dk/bisim/ The Bisimulation Game Game]

{{Authority control}}

[[Category:Theoretical computer science]]
[[Category:Formal methods]]
[[Category:Logic in computer science]]
[[Category:Transition systems]]