Causality for mobile processes

We study causality in the π-calculus. Our notion of causality combines the dependencies given by the syntactic structure of processes with those originated by passing names. It turns out that two transitions not causally related may although occur in a fixed ordering in any computation, i.e., π-calculus may express implicitly a priority between actions. Our causality relation still induces the same partial order of transitions for all the computations that are obtained by shuffling transitions that are concurrent (= related neither by causality nor by priority). The presentation takes advantage from a parametric definition of process behaviour that highlights the essence of the topic. All the results on bisimulation based equivalences, congruences, axiomatizations and logics axe taken (almost) for free from the interleaving theory