A behavioural theory for a π-calculus with preorders

• We study the behavioural theory of πPπP, an π-calculus based on a preorder between names.
• πPπP supports i/o-types and subtyping, contrarily to related calculi like Fusions or Chi.
• Barbed congruence in πPπP is first characterised using a compositional labelled transition system.
• A set of laws provides an axiomatisation of barbed congruence, which gives a second characterisation.

We study the behavioural theory of πPπP, a π  -calculus in the tradition of Fusions and Chi calculi. In contrast with such calculi, reduction in πPπP generates a preorder on names rather than an equivalence relation. We present two characterisations of barbed congruence in πPπP: the first is based on a compositional LTS, and the second is an axiomatisation. The results in this paper bring out basic properties of πPπP, mostly related to the interplay between the restriction operator and the preorder on names.Consequently, πPπP is a calculus in the tradition of Fusion calculi, in which both types and behavioural equivalences can be exploited in order to reason rigorously about concurrent and mobile systems.