Locality and Non-Interleaving Semantics in Calculi for Mobile Processes

Davide Sangiorgi

Abstract: Process algebra semantics can be categorised into non-interleaving semantics, where parallel composition is considered a primitive operator, and interleaving semantics, where concurrency is reduced to sequentiality plus nondeterminism. The former have an appealing intuitive justification, but the latter are mathematically more tractable.

This paper addresses the study of non-interleaving semantics in the framework of process algebras for mobile systems, like pi-calculus [Milner 91]. We focus on location bisimulation, in our opinion one of the most convincing non-interleaving equivalences, which aims to describe the spatial dependencies on processes. We introduce location bisimulation in pi-calculus following the definition for CCS given in [Boudol, Castellani, Hennesey and Kiehn 1991]. Our main contribution is to show that in pi-calculus location bisimulation can be expressed, or implemented, within the ordinary interleaving observation equivalence by means of a fairly simple and fully abstract encoding. Thus, we can take advantage of the easier theory of observation equivalence to reason about location bisimulation. We illustrate this with a few examples, including the proof of the congruence properties of location bisimulation. We show that in pi-calculus location bisimulation is not a congruence, and that the full abstraction of the encoding extends to the induced congruence.

The results in the paper also shed more light on the expressive power of the pi-calculus.

An extract from this paper will appear in the Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS'94), Japan, 1994. The proceedings will be published in the Springer-Verlag series of Lecture Notes in Computer Science.

LFCS report ECS-LFCS-94-282, January 1994.

Previous | Index | Next