Introduction to bisimulation and coinduction.

*(English)*Zbl 1252.68008
Cambridge: Cambridge University Press (ISBN 978-1-107-00363-7/hbk; 978-1-139-15378-2/ebook). xii, 247 p. (2012).

The book is a gentle introduction to the basics of bisimulation and other notions of behavioral equivalences over (weak) labelled transitions systems (LTS). The notion of bisimulation is set in the proper context of coinduction and the duality with induction is illustrated in the text.

There is a companion volume, [D. Sangiorgi (ed.) and J. Rutten (ed.), Advanced Topics in Bisimulation and Coinduction. Cambridge: Cambridge University Press (2012)] that deals with more specialized material.

The book is organized in seven chapters.

The first chapter introduces LTS and discusses how to represent processes using them. The concept of bisimulation as “equivalence of behavior” is developed in a detailed manner with many examples.

Chapter 2 discusses coinduction as a dual of induction, first intuitively through examples (notably convergence/divergence, finite/infinite lists) and then in a rigorous manner by setting the mathematical foundation of complete lattices and fixed points of monotone functions. Several useful versions of fixed point principles are presented. With these tools ready, examples and respective concepts of bisimulation are revisited. Game characterizations are also discussed, but only briefly.

Chapter 3 studies a version of the calculus of communicating systems (CCS) of R. Milner [Communication and concurrency. New York etc.: Prentice Hall (1989; Zbl 0683.68008)] and the concept of congruence is presented. Then bisimilarity on finite processes is axiomatized in an equational setting.

Chapter 4 surveys the various bisimulations over weak LTS, which is continued in the next two chapters where testing equivalences and those that emerge from simulation relations are studied.

The final chapter introduces barbed bisimilarity \(\dot\sim\), which takes only into account internal (\(\tau\)) actions and “observables” (available actions). This equivalence is presented only to define barbed congruence, the congruence contextually defined from \(\dot\sim\). Since barbed congruence is very robust and versatile, the author claims that it may prove helpful to decide which is the correct behavioral equivalence to choose in some contexts. The author discusses, for example, cases in which this notion could be particularly useful, but the concrete technical details are omitted.

There are plenty of exercises in the body of the text, chosen and organized with great care. Most students will have great benefit from them. A large fraction of the exercises is solved in an appendix.

The book fulfills very neatly the goal of providing a detailed, nicely paced and well written introduction to the concepts of bisimulation, coinduction and congruence. The only, if any, weak point of this work is that it barely misses being a self-contained textbook for a first graduate course. In this direction, it is acknowledged in the introduction that some parts of the companion book should supplement the lectures. In any case, it is perfectly suited for advanced undergraduate students: they may go through the details with little need of supervision.

There is a companion volume, [D. Sangiorgi (ed.) and J. Rutten (ed.), Advanced Topics in Bisimulation and Coinduction. Cambridge: Cambridge University Press (2012)] that deals with more specialized material.

The book is organized in seven chapters.

The first chapter introduces LTS and discusses how to represent processes using them. The concept of bisimulation as “equivalence of behavior” is developed in a detailed manner with many examples.

Chapter 2 discusses coinduction as a dual of induction, first intuitively through examples (notably convergence/divergence, finite/infinite lists) and then in a rigorous manner by setting the mathematical foundation of complete lattices and fixed points of monotone functions. Several useful versions of fixed point principles are presented. With these tools ready, examples and respective concepts of bisimulation are revisited. Game characterizations are also discussed, but only briefly.

Chapter 3 studies a version of the calculus of communicating systems (CCS) of R. Milner [Communication and concurrency. New York etc.: Prentice Hall (1989; Zbl 0683.68008)] and the concept of congruence is presented. Then bisimilarity on finite processes is axiomatized in an equational setting.

Chapter 4 surveys the various bisimulations over weak LTS, which is continued in the next two chapters where testing equivalences and those that emerge from simulation relations are studied.

The final chapter introduces barbed bisimilarity \(\dot\sim\), which takes only into account internal (\(\tau\)) actions and “observables” (available actions). This equivalence is presented only to define barbed congruence, the congruence contextually defined from \(\dot\sim\). Since barbed congruence is very robust and versatile, the author claims that it may prove helpful to decide which is the correct behavioral equivalence to choose in some contexts. The author discusses, for example, cases in which this notion could be particularly useful, but the concrete technical details are omitted.

There are plenty of exercises in the body of the text, chosen and organized with great care. Most students will have great benefit from them. A large fraction of the exercises is solved in an appendix.

The book fulfills very neatly the goal of providing a detailed, nicely paced and well written introduction to the concepts of bisimulation, coinduction and congruence. The only, if any, weak point of this work is that it barely misses being a self-contained textbook for a first graduate course. In this direction, it is acknowledged in the introduction that some parts of the companion book should supplement the lectures. In any case, it is perfectly suited for advanced undergraduate students: they may go through the details with little need of supervision.

Reviewer: Pedro Sánchez Terraf (Córdoba)

##### MSC:

68-01 | Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science |

03B70 | Logic in computer science |

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |