LOCATION EQUIVALENCE IN A PARAMETRIC SETTING

Location equivalence has been presented in [5] as a bisimulation-based equivalence able to take into account the spatial distribution of pro cesses. In this work, the parametric approach of [12] is applied to lo cation equivalence. An observation domain for localities is identified and the associated equivalence is shown to coincide with the equivale nce introducted in [6, 16]. The observation of a computation is a fore st (defined up to isomorphism) whose nodes are the events (labeled by observable actions) and where the arcs describe the sublocation relati on. We show in the paper that our approach is really parametric. By pe rforming minor changes in the definitions, many equivalences are captu red: 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 [6, 16] to obtain the last observation. The equivalence induced by this observat ion corresponds to the very intuitive assumption that different locati ons cannot share a common clock, and hence the ordering between events occurring in different places cannot be determined. Thanks to the gen eral results proved in [12] for the parametric approach, all the obser vation equivalences described in this paper come equipped with sound a nd complete axiomatizations.