Comparing the expressiveness of the π-calculus and CCS

Abstract

Abstract This paper shows that the $$\pi $$ π -calculus with implicit matching is no more expressive than $$\mathrm {CCS}_{\gamma }$$ CCS γ , a variant of CCS in which the result of a synchronisation of two actions is itself an action subject to relabelling or restriction, rather than the silent action $$\tau $$ τ . This is done by exhibiting a compositional translation from the $$\pi $$ π -calculus with implicit matching to $$\mathrm {CCS}_{\gamma }$$ CCS γ that is valid up to strong barbed bisimilarity. The full $$\pi $$ π -calculus can be similarly expressed in $$\mathrm {CCS}_{\gamma }$$ CCS γ enriched with the triggering operation of Meije. I also show that these results cannot be recreated with CCS in the rôle of $$\mathrm {CCS}_{\gamma }$$ CCS γ , not even up to reduction equivalence, and not even for the asynchronous $$\pi $$ π -calculus without restriction or replication. Finally I observe that CCS cannot be encoded in the $$\pi $$ π -calculus.