We examine the meaning of causality in calculi for mobile processes like the pi-calculus, and we investigate the relationship between interleaving and causal semantics for such calculi. We separate two forms of causal dependencies on actions of pi-calculus processes, called subject and object dependencies: The former originate from the nesting of prefixes and are propagated through interactions among processes (they are the only form of causal dependencies present in CCS-like languages); the latter originate from the binding mechanisms on names. We propose a notion of causal bisimulation which distinguishes processes which differ for the subject or for the object dependencies. We show that this causal equivalence can be reconducted to, or implemented into, the ordinary interleaving observation equivalence. We prove that our encoding is fully abstract w.r.t. the two behavioural equivalences. This allows us to exploit the simpler theory of the interleaving semantics to reason about the causal one. In [San94b] a similar programme is carried out for location bisimulation [BCHK91], a non-interleaving spatial-sensitive (as opposed to causal-sensitive) behavioural equivalence. The comparison between the encodings of causal bisimulation in this paper, and of location bisimulation in [San94b], evidences the similarities and the differences between these two equivalences.

A Fully Abstract Semantics for Causality in the pi-Calculus / M. Boreale; D. Sangiorgi. - In: ACTA INFORMATICA. - ISSN 0001-5903. - STAMPA. - 35:(1998), pp. 353-400. [10.1007/s002360050124]

A Fully Abstract Semantics for Causality in the pi-Calculus

BOREALE, MICHELE;
1998

Abstract

We examine the meaning of causality in calculi for mobile processes like the pi-calculus, and we investigate the relationship between interleaving and causal semantics for such calculi. We separate two forms of causal dependencies on actions of pi-calculus processes, called subject and object dependencies: The former originate from the nesting of prefixes and are propagated through interactions among processes (they are the only form of causal dependencies present in CCS-like languages); the latter originate from the binding mechanisms on names. We propose a notion of causal bisimulation which distinguishes processes which differ for the subject or for the object dependencies. We show that this causal equivalence can be reconducted to, or implemented into, the ordinary interleaving observation equivalence. We prove that our encoding is fully abstract w.r.t. the two behavioural equivalences. This allows us to exploit the simpler theory of the interleaving semantics to reason about the causal one. In [San94b] a similar programme is carried out for location bisimulation [BCHK91], a non-interleaving spatial-sensitive (as opposed to causal-sensitive) behavioural equivalence. The comparison between the encodings of causal bisimulation in this paper, and of location bisimulation in [San94b], evidences the similarities and the differences between these two equivalences.
1998
35
353
400
M. Boreale; D. Sangiorgi
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/607809
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 53
  • ???jsp.display-item.citation.isi??? 40
social impact