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.
@InProceedings{aceto_et_al:LIPIcs.CONCUR.2022.6, author = {Aceto, Luca and Castiglioni, Valentina and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas}, title = {{On the Axiomatisation of Branching Bisimulation Congruence over CCS}}, booktitle = {33rd International Conference on Concurrency Theory (CONCUR 2022)}, pages = {6:1--6:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-246-4}, ISSN = {1868-8969}, year = {2022}, volume = {243}, editor = {Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.6}, URN = {urn:nbn:de:0030-drops-170692}, doi = {10.4230/LIPIcs.CONCUR.2022.6}, annote = {Keywords: Equational basis, Weak semantics, CCS, Parallel composition} }
Feedback for Dagstuhl Publishing