## 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