Locality and interleaving semantics in calculi for mobile processes

Process algebra semantics can be categorised into noninterleaving 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 noninterleaving semantics in the framework of process algebras for mobile systems, like pi-calculus [19, 17]. We focus on location bisimulation (approximate to sic), in our opinion one of the most convincing non-interleaving equivalences, which aims to describe the spatial dependencies on processes. We introduce approximate to sic in pi-calculus following the definition for CCS given in [5]. Our main contribution is to show that in pi-calculus approximate to sic can be expressed, or implemented, within the ordinary interleaving observation equivalence [16, 19] 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 approximate to sic. We illustrate this with a few examples, including the proof of the congruence properties of approximate to sic. We show that in pi-calculus approximate to sic 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.