Bisimulation is one of the most important ideas of theoretical computer science. I was wondering whether bisimilarity is used/known outside of computer science/modal logic? I am aware that it corresponds more or less to back and forth techniques from model theory, but are there any other areas where it finds application?
For those not in the know, here is a definition:
Given a labelled transition system $(S,\Lambda,\to)$, a bisimulation relation is a binary relation $R$ over $S$ (that is, $R\subseteq S\times S$) such that for all pairs of elements $p,q\in S$ with $(p,q)\in R$, and for all $\alpha\in\Lambda$, we have
- $p\to^\alpha p'$ implies that there is a $q'$ such that $q\to^\alpha q'$ and $(p',q')\in R$, and
- symmetrically for $q$, namely, $q\to^\alpha q'$ implies that there is a $p'$ such that $p\to^\alpha p'$ and $(p',q')\in R$.
Applications collected thus far in answers include:
- process equivalence in concurrency theory
- model logic: expressiveness characterisations, modal correspondence theory
- coinduction, for example in Game Theory
- non-well founded set theory
- Algebraic
- algebraic set theory
- geometric topology
