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.


The first chapter gives motivation, leading from the question of how to define the behavior of interactive processes to the notion of bisimulation.  The second chapter presents both induction and coinduction from a variety of perspectives (e.g. fixed points, rules, games, continuity) and revisits the notion of bisimulation formally.

Starting in chapter 3, it uses a (somewhat simplified) variant of Milner's Calculus of Communicating Systems (CCS) as a source of running examples, and contains an introduction to CCS, making it self-contained for readers with a reasonable mathematics or CS background that might not already be familiar with it or other process calculi.  Algebraic properties of bisimilarity in the context of CCS are studied, particularly the conditions when bisimilarity is a congruence.

The book initially focuses on so-called "strong" labeled transition systems where all actions are treated equally.  Chapter 4 investigates the case of weak LTSs where there is a certain "internal action" $\tau$, and considers bisimilarity where we only ask that an $\stackrel{a}{\to}$ transition on one side can be matched by first doing zero or more $\tau$ transitions, then $\stackrel{a}{\to}$, then zero or more more $\tau$ transitions. 

Chapter 5 considers other notions of behavioral equivalence, including the testing equivalences employed in the CSP family of process algebras, and relates them to bisimilarity and to each other. Chapter 6 considers variants of simulation (the asymmetric form of bisimulation) and establishes relationships among them.  Chapter 7 considers the problems that arise once transitions do not just have atomic labels but might record communicated values, and covers "observables" (sometimes called barbs) and associated notions of bisimulation.

Chapters 1-4 would form the basis of a good graduate-level course on bisimulation or coinduction, with the remaining chapters providing advanced material that could be covered optionally.