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