Bisimulation and Coinduction


Introduction to Bisimulation and Coinduction Advanced Topics in Bisimulation and Coinduction
Davide Sangiorgi Davide Sangiorgi and Jan Rutten (eds)


The two books treat bisimulation and coinduction. They books analyse the most fundamental aspects of bisimulation and coinduction, exploring concepts and techniques that can be transported to many areas. Bisimulation is a special case of coinduction, by far the most studied coinductive concept. Bisimulation has been discovered in Concurrency Theory and processes remain the main application area. This explains the special emphasis on bisimulation and processes that one finds throughout the two volumes.

The introduction volume treats basic topics. It explains coinduction, and its duality with induction, from various angles, starting from some simple results of fixed-point theory. It then goes on to bisimulation, as a tool for defining behavioural equality among processes (bisimilarity), and for proving such equalities. It compares bisimulation to other notions of behavioural equivalence. It also presents a simple process calculus, both to show algebraic techniques for bisimulation and to illustrate the combination of inductive and coinductive reasoning.

The advanced volume deals with more specialised topics. A chapter recalls the history of the discovery of bisimulation and coinduction. Another chapter unravels the duality between induction and coinduction, both as defining principles and as proof techniques, in terms of the duality between the mathematical notions of algebra and coalgebra and properties such as initiality and finality. A third chapter analyses the profound implications of the concept of bisimulation in modal logics, with some beautiful results on the expressiveness of the logics. Two further chapters are devoted to the bisimulation proof method, a major ingredient for success of bisimulation: the algorithmic content of the method, showing striking separation results between bisimilarity and other behavioural equivalences; and enhancements of the bisimulation proof method, whose goal is to further facilitate the proof of bisimilarity results. Finally, separate chapters discuss two important refinements of bisimulation, which have to do with probabilities and higher-order linguistic constructs.

Bisimulation and coinduction offer us powerful tools for defining, understanding, and reasoning about objects and structures that are common in Computer Science. Today, bisimulation and coinduction are also used in other fields, e.g., Artificial Intelligence, Cognitive Science, Mathematics, Modal Logics, Philosophy, Physics.

Follow the links above for details on the single books, including order information.