Location equivalence has been presented in [5] as a bisimulation-based equivalence able to take into account the spatial distribution of processes. In this work, the parametric approach of [12] is applied to location equivalence. An observation domain for localities is identified and the associated equivalence is shown to coincide with the equivalence introducted in [6, 16]. 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 sublocation 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 [6, 16] to obtain the last observation. The equivalence induced by this observation corresponds to the very intuitive assumption that different locations cannot share a common clock, and hence the ordering between events occurring in different places cannot be determined. Thanks to the general results proved in [12] for the parametric approach, all the observation equivalences described in this paper come equipped with sound and complete axiomatizations.
LOCATION EQUIVALENCE IN A PARAMETRIC SETTING
MONTANARI, UGO GIOVANNI ERASMO;
1995-01-01
Abstract
Location equivalence has been presented in [5] as a bisimulation-based equivalence able to take into account the spatial distribution of processes. In this work, the parametric approach of [12] is applied to location equivalence. An observation domain for localities is identified and the associated equivalence is shown to coincide with the equivalence introducted in [6, 16]. 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 sublocation 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 [6, 16] to obtain the last observation. The equivalence induced by this observation corresponds to the very intuitive assumption that different locations cannot share a common clock, and hence the ordering between events occurring in different places cannot be determined. Thanks to the general results proved in [12] for the parametric approach, all the observation equivalences described in this paper come equipped with sound and complete axiomatizations.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
