Non-interleaving semantics for mobile processes

This paper studies causality in the pi-calculus. Our notion of causality co mbines the dependencies given by the syntactic structure of processes with those originated by passing names. Our studies show that two transitions no t causally related may however occur in a fixed ordering in any computation , i.e., the pi-calculus may implicitly express a precedence between actions . The same partial order of transitions is associated with all the computat ions that are obtained by shuffling transitions that are concurrent (i.e. r elated neither by causality nor by precedence). Other non-interleaving sema ntics are investigated and compared. The presentation takes advantage of a parametric definition of process behaviour given in SOS style that permits us to take almost for free the interleaving theory and tools. Finally, we e xtend our approach to higher-order pi-calculus, enriched with a spawn opera tion. (C) 1999-Elsevier Science B.V. All rights reserved.