Abstract
This paper shows that the π-calculus with implicit matching is no more expressive than 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 τ. This is done by exhibiting a compositional translation from the π-calculus with implicit matching to CCSγ that is valid up to strong barbed bisimilarity.
The full π-calculus can be similarly expressed in CCSγ enriched with the triggering operation of MEIJE.
I also show that these results cannot be recreated with CCS in the rôle of CCSγ, not even up to reduction equivalence, and not even for the asynchronous π-calculus without restriction or replication.
Finally I observe that CCS cannot be encoded in the π-calculus.
The full π-calculus can be similarly expressed in CCSγ enriched with the triggering operation of MEIJE.
I also show that these results cannot be recreated with CCS in the rôle of CCSγ, not even up to reduction equivalence, and not even for the asynchronous π-calculus without restriction or replication.
Finally I observe that CCS cannot be encoded in the π-calculus.
| Original language | English |
|---|---|
| Article number | 1 |
| Pages (from-to) | 1-58 |
| Number of pages | 58 |
| Journal | ACM Transactions on Computational Logic |
| Volume | 25 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 18 Nov 2023 |