The Pi-Calculus and MONSTR

Richard Banach

(University of Manchester)

The pi-calculus is a process algebra in which channel names can act both as transmission medium and as transmitted data. Its basic atomic actions are individual point to point communications which are nondeterministically selected and globally sequentialised. MONSTR is a term graph rewriting language designed to be easily implementable on distributed architectures and features limited synchronisation facilities. The talk describes a translation of a version of the pi-calculus, into MONSTR. It confronts the rather different synchronisation abilities of the two systems, which are resolved by using a suitable communication protocol in the MONSTR system. The issue of the correctness of the translation raises a number of problems, not the least of which is "what does correctness mean?", which is resolved by demanding that a pi-calculus system and its translation are capable of the same sequences of communications. One direction of the correctness proof is then a relatively straightforward simulation, while the converse becomes a substantial exercise in serialisability. The translation thus provides a non-trivial case study in verification.
Tuesday 5th December 1995, 14:30
Seminar Room 322
Department of Computer Science