GLOBAN 2006 - The Global Computing Approach to Analysis of Systems

Equality of processes: equivalences and proof techniques

Lectures by Davide Sangiorgi, University of Bologna, Italy

Abstract

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

In the lectures I will review the main forms of behavioural equivalence. I will devote more time to bisimulation, for its importance and mathematical properties. In particular, I will discuss the bisimulation proof method. This is an instance of a general proof technique called co-induction that is today widely used also outside concurrency theory.