Non interleaving semantics of mobile processes

This paper studies causality in the π-calculus. Our notion of causality combines the dependencies given by the syntactic structure of processes with those originated by passing names. Our studies show that two transitions not causally related may however occur in a fixed ordering in any computation, i.e., the π-calculus may implicitly express a precedence between actions. The same partial order of transitions is associated with all the computations that are obtained by shuffling transitions that are concurrent (i.e. related neither by causality nor by precedence). Other non-interleaving semantics 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 extend our approach to higher-order π-calculus, enriched with a spawn operation.