Introduction to Bisimulation and Coinduction

Introduction to Bisimulation and Coinduction
Davide Sangorgi
Cambridge University Press, 2012

Bisimulation is a natural notion of equivalence for process algebras, and arises naturally in modal logic, graph theory and other settings.  Suppose we have a labeled transition system $(X,\stackrel{a}{\to})$, then a bisimulation $R$ is a relation satisfying:

• for all $x~R~y$, if $x \stackrel{a}{\to} x'$ then there exists $y'$ such that $y \stackrel{a}{\to} y'$
• for all $x~R~y$, if $y \stackrel{a}{\to} y'$ then there exists $x'$ such that $x \stackrel{a}{\to} x'$

Then bisimilarity is defined as the largest relation $\approx$ that contains every bisimulation.  Equivalently, the largest relation closed under the above two rules.

Bisimulation is defined coinductively, that is, in terms of the greatest fixed point of a monotone operator, in contrast to inductive definitions (least fixed-points) that are more familiar to computer scientists.  Bisimulation and coinduction are general concepts, but they have generally been covered in the context of process calculi such as CCS or the $\pi$-calculus, or for reasoning about infinite streams or other infinite behaviors in functional programming.  This book provides an accessible treatment of both topics in their own right, rather than as a secondary matter arising in the study of process calculus or streams.
Read more »