On characterising strong bisimilarity in a fragment of CCS with replication

TL;DR

This paper characterizes strong bisimilarity in a fragment of CCS with limited replication using a rewriting system, and extends the approach to derive a new congruence result in a sub-calculus of the π-calculus.

Contribution

It introduces a rewriting system for characterizing strong bisimilarity in a CCS fragment and applies this to establish a new congruence result in a π-calculus sub-calculus.

Findings

Rewriting system effectively characterizes strong bisimilarity.

New congruence result established for a π-calculus sub-calculus.

Method provides insights into process equivalences in restricted calculi.

Abstract

We provide a characterisation of strong bisimilarity in a fragment of CCS that contains only prefix, parallel composition, synchronisation and a limited form of replication. The characterisation is not an axiomatisation, but is instead presented as a rewriting system. We discuss how our method allows us to derive a new congruence result in the $\pi$-calculus: congruence holds in the sub-calculus that does not include restriction nor sum, and features a limited form of replication. We have not formalised the latter result in all details.