18th Estonian Winter School in Computer Science (EWSCS)
XVIII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 3 - 8, 2013

Davide Sangiorgi

Dip. di Scienze dell'Informazione
Università di Bologna

Introduction to Bisimulation and Coinduction


A fundamental concern in concurrency theory is establishing when two processes are "the same", i.e., indistinguishable to an external observer interacting with them. This notion, called, behavioural equivalence, is the basis upon which a theory of processes can be developed.

In the lectures will introduce bisimulation, one of the most studied forms of behavioural equivalence for processes. Bisimulation has a number of elegant mathematical properties. I will focus in particular on the bisimulation proof method. This is an instance of a general proof technique, called coinduction, that is today widely used also outside concurrency theory. I will review the basics of coinduction and its duality with induction.

If time allows, I will also consider enhancements of the bisimulation proof method. Enhancements of the methods are often extremely useful for proving non-trivial equalities; they seem to be even essential in languages for mobility such as the π-calculus, and higher-order languages such λ-calculus or Higher-Order π-calculus.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed April 17, 2016 21:09 EET by local organizers, ewscs13(at)cs.ioc.ee
EWSCS'13 page: http://cs.ioc.ee/ewscs/2013/