2026-07-24T05:02:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17069 2024-03-06T10:58:40Z ddc:004 open_access

On the Axiomatisation of Branching Bisimulation Congruence over CCS Aceto, Luca Castiglioni, Valentina Ingólfsdóttir, Anna Luttik, Bas Equational basis Weak semantics CCS Parallel composition 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Luca Aceto and Valentina Castiglioni and Anna Ingólfsdóttir and Bas Luttik 2022 Is Part Of LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2022.6 urn:nbn:de:0030-drops-170692 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.6 eng https://creativecommons.org/licenses/by/4.0/legalcode