Abstract

We introduce the pi_F-calculus, a pi-calculus based on explicit fusions. The explicit fusion x=y is a process which declares that two names can be used interchangeably. In contrast, the fusion calculus of Parrow and Victor treats fusions implicitly as part of the reaction relation. We give simple embeddings of the pi, the pi_I and the fusion calculus, and prove a full abstraction result which connects bisimulation for the pi-calculus with bisimulation for its embedding in the pi_F-calculus.

We will explore two equivalent bisimulation congruences. One arises from a standard labelled transition system (LTS), in which a label can be regarded as an offer of a synchronisation with an external process. The other arises from a new form of LTS, in which a label denotes a small context necessary to create a redex. Both definitions of bisimulation provide a natural analysis of the graphical structure of processes.

This talk describes joint work with Lucian Wischik, and arose from our previous work on process frameworks. A basic knowledge of the pi-calculus is assumed.