On the Axiomatisation of Branching Bisimulation Congruence over CCS

Luca Aceto; Valentina Castiglioni; Anna Ingólfsdóttir; Bas Luttik

doi:10.4230/LIPIcs.CONCUR.2022.6

On the Axiomatisation of Branching Bisimulation Congruence over CCS

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

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.

Original language	English
Title of host publication	33rd International Conference on Concurrency Theory, CONCUR 2022
Editors	Bartek Klin, Slawomir Lasota, Anca Muscholl
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Pages	6:1-6:18
Number of pages	18
ISBN (Electronic)	978-3-95977-246-4
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2022.6
Publication status	Published - 6 Sept 2022
Event	33rd International Conference on Concurrency Theory, CONCUR 2022 - Warsaw, Poland Duration: 12 Sept 2022 → 16 Sept 2022

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	243
ISSN (Print)	1868-8969

Conference

Conference	33rd International Conference on Concurrency Theory, CONCUR 2022
Country/Territory	Poland
City	Warsaw
Period	12/09/22 → 16/09/22

Funding

Funding This work has been partially supported by the project “Open Problems in the Equational Logic of Processes” (OPEL) of the Icelandic Research Fund (grant No. 196050-051). V. Castiglioni has been supported by the project “Programs in the wild: Uncertainties, adaptabiLiTy and veRificatiON” (ULTRON) of the Icelandic Research Fund (grant No. 228376-051).

Keywords

CCS
Equational basis
Parallel composition
Weak semantics

Access to Document

10.4230/LIPIcs.CONCUR.2022.6

pdfFinal published version, 838 KBLicence: CC BY

Cite this

Aceto, L., Castiglioni, V., Ingólfsdóttir, A., & Luttik, B. (2022). On the Axiomatisation of Branching Bisimulation Congruence over CCS. In B. Klin, S. Lasota, & A. Muscholl (Eds.), 33rd International Conference on Concurrency Theory, CONCUR 2022 (pp. 6:1-6:18). Article 6 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 243). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.6

Aceto, Luca ; Castiglioni, Valentina ; Ingólfsdóttir, Anna et al. / On the Axiomatisation of Branching Bisimulation Congruence over CCS. 33rd International Conference on Concurrency Theory, CONCUR 2022. editor / Bartek Klin ; Slawomir Lasota ; Anca Muscholl. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. pp. 6:1-6:18 (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{ba92872ec7a4429090ca38879a215c3e,

title = "On the Axiomatisation of Branching Bisimulation Congruence over CCS",

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.",

keywords = "CCS, Equational basis, Parallel composition, Weak semantics",

author = "Luca Aceto and Valentina Castiglioni and Anna Ing{\'o}lfsd{\'o}ttir and Bas Luttik",

note = "Funding Information: Funding This work has been partially supported by the project “Open Problems in the Equational Logic of Processes” (OPEL) of the Icelandic Research Fund (grant No. 196050-051). V. Castiglioni has been supported by the project “Programs in the wild: Uncertainties, adaptabiLiTy and veRificatiON” (ULTRON) of the Icelandic Research Fund (grant No. 228376-051). Publisher Copyright: {\textcopyright} Luca Aceto, Valentina Castiglioni, Anna Ing{\'o}lfsd{\'o}ttir, and Bas Luttik; licensed under Creative Commons License CC-BY 4.0.; 33rd International Conference on Concurrency Theory, CONCUR 2022 ; Conference date: 12-09-2022 Through 16-09-2022",

year = "2022",

month = sep,

day = "6",

doi = "10.4230/LIPIcs.CONCUR.2022.6",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

pages = "6:1--6:18",

editor = "Bartek Klin and Slawomir Lasota and Anca Muscholl",

booktitle = "33rd International Conference on Concurrency Theory, CONCUR 2022",

}

Aceto, L, Castiglioni, V, Ingólfsdóttir, A & Luttik, B 2022, On the Axiomatisation of Branching Bisimulation Congruence over CCS. in B Klin, S Lasota & A Muscholl (eds), 33rd International Conference on Concurrency Theory, CONCUR 2022., 6, Leibniz International Proceedings in Informatics, LIPIcs, vol. 243, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 6:1-6:18, 33rd International Conference on Concurrency Theory, CONCUR 2022, Warsaw, Poland, 12/09/22. https://doi.org/10.4230/LIPIcs.CONCUR.2022.6

On the Axiomatisation of Branching Bisimulation Congruence over CCS. / Aceto, Luca; Castiglioni, Valentina; Ingólfsdóttir, Anna et al.
33rd International Conference on Concurrency Theory, CONCUR 2022. ed. / Bartek Klin; Slawomir Lasota; Anca Muscholl. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. p. 6:1-6:18 6 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 243).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - On the Axiomatisation of Branching Bisimulation Congruence over CCS

AU - Aceto, Luca

AU - Castiglioni, Valentina

AU - Ingólfsdóttir, Anna

AU - Luttik, Bas

N1 - Funding Information: Funding This work has been partially supported by the project “Open Problems in the Equational Logic of Processes” (OPEL) of the Icelandic Research Fund (grant No. 196050-051). V. Castiglioni has been supported by the project “Programs in the wild: Uncertainties, adaptabiLiTy and veRificatiON” (ULTRON) of the Icelandic Research Fund (grant No. 228376-051). Publisher Copyright: © Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik; licensed under Creative Commons License CC-BY 4.0.

PY - 2022/9/6

Y1 - 2022/9/6

N2 - 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.

AB - 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.

KW - CCS

KW - Equational basis

KW - Parallel composition

KW - Weak semantics

UR - http://www.scopus.com/inward/record.url?scp=85138712764&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CONCUR.2022.6

DO - 10.4230/LIPIcs.CONCUR.2022.6

M3 - Conference contribution

AN - SCOPUS:85138712764

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 6:1-6:18

BT - 33rd International Conference on Concurrency Theory, CONCUR 2022

A2 - Klin, Bartek

A2 - Lasota, Slawomir

A2 - Muscholl, Anca

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 33rd International Conference on Concurrency Theory, CONCUR 2022

Y2 - 12 September 2022 through 16 September 2022

ER -

Aceto L, Castiglioni V, Ingólfsdóttir A, Luttik B. On the Axiomatisation of Branching Bisimulation Congruence over CCS. In Klin B, Lasota S, Muscholl A, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2022. p. 6:1-6:18. 6. (Leibniz International Proceedings in Informatics, LIPIcs). doi: 10.4230/LIPIcs.CONCUR.2022.6

On the Axiomatisation of Branching Bisimulation Congruence over CCS

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this