Abstract

The copying of processes is limited in the context of distributed computation, either as a fact of life, often because remote networks are simply too complicated to have control over, or deliberately, as in the design of security protocols. Roughly, linearity is about how to manage without a presumed ability to copy. The meaning and mathematical consequences of linearity are studied for path-based models of processes which are also models of affine-linear logic. This connection yields an affine-linear language for processes in which processes are typed according to the kind of computation paths they can perform. One consequence is that the affine-linear language automatically respects open-map bisimulation. A range of process operations (from CCS, CCS with process-passing, mobile ambients, and dataflow) can be expressed within the affine-linear language showing the ubiquity of linearity. Of course, process code can be sent explicitly to be copied. Following the discipline of linear logic, suitable nonlinear maps are obtained as linear maps whose domain is under an exponential. Different ways to make assemblies of processes lead to different choices of exponential; the nonlinear maps of only some of which will respect bisimulation.

Introduction

In the film “Groundhog Day” the main character comes to relive and remember the same day repeatedly, until finally he gets it right (and the girl). Real life isn't like that. The world moves on and we cannot rehearse, repeat or reverse the effects of the more important decisions we take.