A parametric approach to localities

Abstract

Location equivalence has been presented in [3] as a bisimulation based equivalence able to take into account the spatial distribution of processes. In this work, the parametric approach of [9] is applied to location equivalence. An observation domain for localities is identified and the resulting equivalence is shown to coincide with the equivalence introduced in [4, 13]. The observation of a computation is a forest (defined up to isomorphism) whose nodes are the events (labeled by observable actions) and where the arcs describe the sub-location relation. We show in the paper that our approach is really parametric. By performing minor changes in the definitions, many equivalences are captured: partial and mixed ordering causal semantics, interleaving, and a variation of location equivalence where the generation ordering is not evidenced. It seems difficult to modify the definitions of [4, 13] to obtain the last observation. The equivalence induced by this observation corresponds to the very intuitive assumption that different locations cannot share any common clock, and hence the ordering between events occurring in different places cannot be determined. Thanks to the general results proved in [9] for the parametric approach, all the observation equivalences described in the paper come equipped with sound and complete axiomatizations.