Comparing the expressiveness of the $\pi$-calculus and CCS

TL;DR

This paper demonstrates that the $ ext{pi}$-calculus with implicit matching is not more expressive than a specific variant of CCS called CCS$ extgamma$, through a compositional translation valid up to strong barbed bisimilarity.

Contribution

It provides a formal translation from the $ ext{pi}$-calculus with implicit matching to CCS$ extgamma$, establishing their equivalence in expressiveness and showing limitations of encodings between these calculi.

Findings

$ ext{pi}$-calculus with implicit matching is no more expressive than CCS$ extgamma$

Full $ ext{pi}$-calculus can be expressed in CCS$ extgamma$ with triggering operation

CCS cannot be encoded in the $ ext{pi}$-calculus

Abstract

This paper shows that the $\pi$-calculus with implicit matching is no more expressive than CCS$\gamma$, 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 CCS$\gamma$ that is valid up to strong barbed bisimilarity. The full $\pi$-calculus can be similarly expressed in CCS$\gamma$ enriched with the triggering operation of Meije. I also show that these results cannot be recreated with CCS in the role of CCS$\gamma$, 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.