Aceto, Luca
[VerfasserIn];
Castiglioni, Valentina
[VerfasserIn];
Ingólfsdóttir, Anna
[VerfasserIn];
Luttik, Bas
[VerfasserIn]
;
Luca Aceto and Valentina Castiglioni and Anna Ingólfsdóttir and Bas Luttik
[MitwirkendeR]
On the Axiomatisation of Branching Bisimulation Congruence over CCS
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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.