Linearity in Distributed Computation

Mikkel Nygaard Hansen Glynn Winskel

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002


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 a path-based model of processes which is also a model 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, ambients, and dataflow) can be expressed within the affine-linear language showing the ubiquity of linearity. An operational semantics is provided for the tensor fragment of the language, and it is indicated how to understand the tensor operation as a parallel composition of event structures. Of course, process code can be sent explicitly to be copied. Different ways to make assemblies of processes lead to different choices of exponential, some of which respect bisimulation.

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:30
Start Conference Manager
Conference Systems