A fully abstract semantics for causality in the \pi-calculus |
| |
Authors: | Michele Boreale Davide Sangiorgi |
| |
Affiliation: | (1) Dipartimento di Scienze dell'Informazione, Università di Roma “La Sapienza”, Roma, Italy , IT;(2) INRIA Sophia-Antipolis, 2004, route des Lucioles, B.P. 93, F-06902 Sophia Antipolis Cedex, France (e-mail: davide.sangiorgi@sophia.inria.fr) , FR |
| |
Abstract: | We examine the meaning of causality in calculi for mobile processes like the -calculus, and we investigate the relationship between interleaving and causal semantics for such calculi. We separate two
forms of causal dependencies on actions of -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.
Received 11 December 1995 / 16 June 1997 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|