Bisimulation
A term that denotes a kind of relationship on the carrier of a coalgebra and which is dual to congruence. The concept of bisimulation has been defined by Park and Milner and is commonly used in the field of operational semantics. Bisimulations are used to define a concept of equality on the states of some transition system or automaton, thus as a flexible theory stating in which sense two automata "behave the same way". It is used with formal models for concurrent systems like the pi calculus, where computations usually have no final state nor "result" and thus we cannot say that two automata behave the same way if they produce the same result, as we would do, for instance, in the lambda calculus.
Let us consider a relationship ^ between the states of two automata A1 and A2. We say that ^ is a simulation of A1 in A2 if it obeys a law stating that for every s1, s2:
if s1 ^ s2 and s1 -[a] s1' then a state s2' exists such as s2 -[a] s2' and s1' ^ s2'.
With [a] we indicate that the state transition bringing s1 in s1' is labelled with a label a. Labels are used to indicate both the cause of the state transition (for instance, the input of some value from the environment) and its observable effects (for instance, the output towards the environment of another value). The two aspects are often unified. The above property means that A2 can "simulate step by step" any behavior of A1:
s2 -[a1] s2' -[a2] s2'' -[a3] ...
^ ^ ^ ...
s1 -[a1] s1' -[a2] s1'' -[a3] ...
every instance of the lower row can be matched by some instance of the upper one.
The relation ^ is a bisimulation if and only if it is a simulation of A1 in A2, and at the same time its inverse is a simulation of A2 in A1. This means not only that every computation of A1 can be matched by an analogous computation of A2 and vice versa, but also that this match can be done through just one relation. In a word: a bisimulation is something more than a pair of simulations!
The category-theoretic definition of bisimulation is the following. A bisimulation between two coalgebras A1 and A2 is a coalgebra A3 such as there is a span of homomorphisms from A3 to both A1 and A2. Intuitively, this means that there is an automaton A3 that can be simulated contemporarily by A1 and by A2, and this formalizes the previous definition.
Different flavours of "bisimulation" can be defined for a same formal model of computation by varying the definition of the transitions, of the labels, and by discarding or aggregating the labels. Being the union of two bisimulations again a bisimulation, it turns out that there is a bisimulation which is the biggest of all. Precisely, the biggest of all the bisimulation is the union of all the bisimulations, and we indicate as ~.~. ~.~ is commonly called bisimilarity, so that two states s1, s2 such as s1 ~.~ s2 can be said to be bisimilar tout court. Bisimilarity is always a reflexive (every state is bisimilar to itself) and symmetric (if s1 is bisimilar to s2, then s2 is bisimilar to s1) relationship, and for most of, but not for all, the coalgebra signatures (functors, in category-theoretic terms) it is also transitive (if s1 is bisimilar to s2 and s2 to s3, then s1 is also bisimilar to s3). In the latter case bisimilarity has almost all the features of an equality theory on states.
Why "almost"? In every formal models of computation like the pi calculus, the join calculus, the fusion calculus et cetera, computing unit (usually called processes) can be composed by means of a series of operators, like parallel, choice, continuation... in a word, processes and these operators form an algebra. A true equality theory on processes should therefore have an additional desirable property: it should respect all the composition operations, so that we can "replace equals with equals" anywhere, and obtain equals: In a word, it must be a congruence. "Bisimulation as congruence" is a very desirable feature of a calculus for distributed, concurrent processes. Alas, the common case is that your favourite bisimilarity for your favourite computational model is not a congruence. For instance, if your favourite bisimilarity relation equates the inert process (which does nothing) with a process that waits to read on channel x and then terminates (perhaps because no other process is around to write on channel x, and so also this process is stuck), you can be sure that in this case bisimilarity is not a congruence. In facts, when both processes are composed in parallel with another process which writes on channel x we obtain two processes which behave differently: The first remains inert because the inert process does not read channel x, thus the writer is stuck altogether, while the second is composed by a reader and a writer for x, and therefore it may perform a computational step where the two components exchange a value on x. So you cannot safely replace under every context the inert process with a process that reads on a channel and then stops.
For this reason a true equality theory in process calculi is usually a suitable congruence ~ contained in ~.~, rather than ~.~ itself. Which ~ should we choose among the many possible? Well, we have some degrees of freedom according to any additional desirable feature we want for ~. Typically we want it to be big (the bigger the ~, the more processes we can equate by means of it), better if it is the biggest congruence contained in bisimilarity. Other desirable features are decidability and axiomatizability. On the first side, there are algorithms to verify bisimilarity which are polynomial in the number of states of the automaton.
Note for the mathematician: according to Rocco de Nicola, bisimilarity is a slight generalization of isomorphism of automata, abstracting from replica of equivalent states. Bisimilarity has also been used by Abramski to define equivalences for the lazy lambda calculus
This page is linked from: Congruence Fusion Calculus Induction and Co-induction