  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.
