Uses of bisimulation outside of computer science.

Question

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 set theory
• geometric topology

Answer 1

As you probably know, between choice and foundation, any use of coinductive arguments in ZFC can be eliminated. So you often have cases where coinduction could have been used, but more inductive methods are used instead. So you have to squint a bit to see them.

Aside from CS and modal logic, the place where coinductive arguments show up most commonly is in game theory, in the study of Nash equilibria of infinite games. The reason they show up here is that it's natural to think of a game in terms of a stream or infinite tree of player moves and opponent responses. If you think about it, this is very similar to the situation in process algebra, where you think of the interaction between a process and its environment.

This actually tells you where to look to find coinduction in the central areas of mathematics. In particular, Nash equilibrium can be understood as an application of Brouwer's fixed point theorem, which tells you that any time you see a compactness or completeness requirement, that's something that could be explained coinductively.

Basically, the intuition is that taking an infinite number of steps always takes you to a limit, and "taking an infinite number of steps" is essentially a function $\mathbb{N} \to \mathrm{blah}$, which is isomorphic to a stream of $\mathrm{blah}$s. This fact is of considerable importance in implementations of computable real arithmetic, because Cauchy sequences are streams, too, and it is natural to write corecursive programs to work with them.

EDIT: Here's a really cute paper by Dexter Kozen and Nicholas Ruozzi, "Applications of Metric Coinduction". They exploit the fact that for contractive maps in metric spaces, least and greatest fixed points coincide to simplify some analytic epsilon-delta arguments by just switching to coinductive arguments.

Answer 2

Another area of set theory where bisimulations come up is in the study of models of ZFC minus foundation.

For example, under Peter Aczel's anti-foundation axiom AFA a large class of systems of set equations are given to have unique solutions; equations that would otherwise not have solutions in full ZFC. The equation x={x} has exactly one solution in AFA; there is a set that contains just itself, and there is only one such set. Bisimulations are used as a tool in the analysis of such sets and in identifying them (a nonwellfounded set can be described by a certain system, and two sets will be the same if there is a bisimulation between the systems). Check out Aczel's text Non-wellfounded Sets. There's a link to the text in the references for the wikipedia article

http://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axiom

Part III of the book Vicious Circles by Jon Barwise and Lawrence Moss is also a good reference for this material where they make use of bisimulations to analyze consequences of AFA.

Answer 3

One area of application -- but I am not an expert here -- is in Algebraic Set Theory (see the monograph with that name by Joyal and Moerdijk), where free ZF algebras and related notions are constructed by consideration of bisimulation-equivalence classes of forests. I am dimly aware that bisimulations have been studied and used quite a lot by category theorists; if Tom Leinster sees this he might be able to tell you more (to name just one person).

Answer 4

Let me add another instance, this time involving both set theory and modal logic at the same time. This application involves modal logic fundamentally, but seems very little related to computer science, and rather seems much closer to philosophical issues concerning the nature of mathematical existence.

The idea is to consider a model of set theory in the context of all its forcing extensions, and their forcing extensions, and so on, as a kind of multiverse. This generic multiverse is very naturally viewed as a Kripke model, where each model of set theory accesses exactly its forcing extensions, and it turns out that although the fundamental concepts seem at first to be second order, they are actually first order expressible in set theory. Thus, one defines that $\varphi$ is possible, written $\diamond\varphi$, if $\varphi$ holds in some forcing extension, and necessary, written $\square\varphi$, if $\varphi$ holds in all forcing extensions. The general question was, What are the modal validities of this forcing interpretation of modal logic?

It is easy to see that all the S4 and even the S4.2 axioms of modal logic are provably legitimate under the forcing interpretation. But what exactly are the provable validities?

Theorem.(Hamkins & Loewe, TAMS, 260, 2008) If ZFC is consistent, then the ZFC-provably valid principles of forcing are exactly the modal assertions of S4.2.

The proof makes essential use of an increased understanding of a complete set of Kripke frames for S4.2, using bisumulation at its core, as well as some detailed forcing combinatorics. Benedikt and I proved via bisimulation that the class of finite pre-Boolean algebras is complete for S4.2. Apart from this, the key ideas were the concepts of buttons and switches in set theory. Namely, a statement $\varphi$ is a switch if you can force $\varphi$ or $\neg\varphi$ over any model of set theory, and a button if you can force $\varphi$ in such a way that it remains true in all further extensions. (Once you push a button, you cannot unpush it.) For example, the Continuum Hypothesis is a switch, and the assertion "$\aleph_1^L$ is countable" is a button. By considering larger independent families of buttons and switches, we were able to simulate any Kripke model on a finite pre-Boolean algebra frame within set theory via forcing extensions, and thereby deduce the theorem.

A related question was whether the set theoretic universe could ever be completed with respect to what is possibly necessary. The Maximality Principle is the scheme expressing that every possibly necessary statement is already true: $\diamond\square\varphi\implies\varphi$. Under MP, if one could force any statement $\varphi$ in such a way that $\varphi$ was true in all subsequent forcing extensions, then $\varphi$ should already be true. I proved (also observed independently by Vanaana and Stavi) that this is equiconsistent with ZFC.

Answer 5

It's used in modal logic, where it was invented, and is used to define relations between models and constructions of new models from old models, which are used to show that different classes of model have the same discriminatory power for modal theories. Van Benthem's introduction of bisimulation was in his PhD thesis, 1976, Modal Correspondence Theory.

There'a quite a bit in Blackburn, de Rijke & Venema (2001) Modal Logic on bisimulation; section 2.2 explains the basics of the application to modal logic.

Answer 6

Bisimularity of graphs arises in geometric topology. See "Quasi-isometric classification of graph manifold groups" by Behrstock and Neumann.