Locality and interleaving semantics in calculi for mobile processes

Reviewer: D. John Cooke

Unlike many papers that appear as “Fundamental Studies” in Theoretical Computer Science , this paper is not primarily a tutorial, nor is it a rationalization of an established body of knowledge. It does include a brief summary of the polyadic pi-calculus, but only to provide the necessary foundations for the research results presented. The basic idea is to extend this calculus to incorporate the notion of located processes. This naturally leads to the concept of location bisimulation, which can also be expressed in terms of interleaving observation equivalence using a fully abstract encoding; the encoding allows the simpler theory (of observation equivalence) to be used to reason about location bisimulation. This is of interest because it contributes to the understanding of the links between interleaving and noninterleaving semantics in process algebras, and between the more intuitive ideas and those that are arguably easier to reason about. The paper is dense, though not unreasonably so. Although it is quite detailed, the reader is left to fill in many gaps. On the other hand, being clearly for the specialist process algebraist, it is easy to follow and, with the exception of a few confusing sentences, well explained. Much of the content of the paper deals with the intricacies of “up-to” techniques (not unlike the notion of similarity in other algebraic contexts) and the problems in dealing with silent—internal, unobservable—actions. This paper is not for the fainthearted, but is a useful addition to the literature on process algebra.