Action Structures for the Pi-Calculus

Robin Milner

Abstract: In a previous paper, action structures were proposed as a variety of algebra to underlie concrete models of concurrent computation and interaction. That work is summarised here, to make the paper self-contained. In particular, the uniform construction of a process calculus upon an arbitrary action structure is reviewed. Another relevant concept from the previous paper is recalled, namely the notion of incident set. Its importance is that, in the process calculus uniformly constructed upon any action structure, a bisimulation equivalence which rests upon an incident set is guaranteed to be a congruence for the calculus.

The main purpose of this paper is to give a family of action structures for the Pi-calculus. Using one of these, the original Pi-calculus is obtained by the uniform construction. The most substantial technical element here is the construction of an appropriate incident set for this action structure, yielding a bisimulation congruence for the Pi-calculus.

Another action structure is used to provide (again via the uniform construction) a synchronous version of the Pi-calculus, in the sense that MEIJE or SCCS is a synchronous version of CCS. The natural version of this action structure contains an anomaly which appears to prevent the existence of the appropriate incident set. However, a so-called reflexive version of the action structure does indeed yield a natural incident set, and thereby again a bisimulation congruence.

Two innovations are noteworthy. One is the definition of reflexive substitution. With this new kind of substitution, restricting a port-name x (in the sense of CCS) amounts to ``making x denote itself'' -- i.e. reflexively substituting x for itself. This notion simplifies the action structure for the synchronous Pi-calculus. The second innovation is that the action structures are presented graphically, giving a new perspective on the Pi-calculus. Indeed, both definition and proof of the incident set for the reflexive Pi-calculus are in terms of a simple graph-theoretic notion of reachability.

LFCS report ECS-LFCS-93-264, May 1993.

Previous | Index | Next