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.
- D. Sangiorgi. Introduction to coinduction and bisimulation. EWSCS 2013 course slides. [pdf]
- Videos from the lectures.
- D. Sangiorgi. Introduction to Coinduction and Bisimulation. Cambridge Univ. Press, 2011. [doi link]
April 17, 2016 21:09 EET
local organizers, ewscs13(at)cs.ioc.ee
EWSCS'13 page: http://cs.ioc.ee/ewscs/2013/