Project suggestion (2004): Bisimulation checking for the
pi-calculus
There are various little languages for describing concurrency and
communication. Milner's Calculus of Communicating Systems
(CCS) is a good example. One important aspect of such systems is
observational equivalence -- identifying processes which appear
identical to the observer even if they are internally different.
Bisimilarity is one particularly important form of
observational equivalence.
The method of partition refinement has been used to check the
bisimilarity of processes. Optimisations of the algorithms there are
quite well understood. Furthermore, it relates well to a more abstract
approach to modelling systems, called coalgebra.
The pi-calculus adds to languages such as CCS a concept of
mobility, so that processes can learn new names and establish private
channels on which to communicate. For example, it has been used to
model mobile telephony. I have recently been working with some
coalgebraic models of the pi-calculus, and am interested to develop
bisimulation checking algorithms for the pi-calculus based on the
method of partition refinement.
Please contact me (ss368) if you are interested in this project.