• People
• Events
• Research

A fully abstract semantics for causality in the pi-calculus

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 each calculi.

We separate two forms of causal depoendencies on actions of pi-calculus processes, called subject and object dependencies: The former originate from the meeting of prefixes and are propagated through interactions among processes (they are the only forms 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, 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.

LFCS report ECS-LFCS-94-297, August 1994.