A Distribution Law for CCS and a New Congruence Result for the pi-calculus

TL;DR

This paper presents an axiomatisation of strong bisimilarity for a fragment of CCS without sum, and extends the result to the finite pi-calculus, establishing congruence in a nontrivial subcalculus.

Contribution

It introduces the first congruence result for strong bisimilarity in a subcalculus of the pi-calculus that includes full output prefix without sum.

Findings

Axiomatisation of strong bisimilarity for a CCS fragment without sum

Derivation of congruence of strong bisimilarity in the finite pi-calculus without sum

Identification of a unique subcalculus with full output prefix where bisimilarity is a congruence

Abstract

We give an axiomatisation of strong bisimilarity on a small fragment of CCS that does not feature the sum operator. This axiomatisation is then used to derive congruence of strong bisimilarity in the finite pi-calculus in absence of sum. To our knowledge, this is the only nontrivial subcalculus of the pi-calculus that includes the full output prefix and for which strong bisimilarity is a congruence.