On the Axiomatisation of Branching Bisimulation Congruence over CCS

TL;DR

This paper explores the equational theory of CCS under rooted branching bisimilarity, demonstrating non-finite axiomatizability and providing a finite basis with additional operators for finite actions.

Contribution

It proves CCS is not finitely axiomatizable under rooted branching bisimilarity and introduces a finite basis with merge operators for finite action sets.

Findings

CCS is not finitely based modulo rooted branching bisimilarity.

Unique parallel decomposition exists for all CCS processes.

Finite equational basis exists with merge operators when actions are finite.

Abstract

In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.