In search of lost time: Axiomatising parallel composition in process algebras

Luca Aceto; Elli Anastasiadi; Valentina Castiglioni; Anna Ingolfsdottir; Bas Luttik

doi:10.1109/LICS52264.2021.9470526

In search of lost time: Axiomatising parallel composition in process algebras

Luca Aceto, Elli Anastasiadi, Valentina Castiglioni, Anna Ingolfsdottir, Bas Luttik

Department of Computer Science

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

Abstract

This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS does not yield a finite axiomatisation of bisimilarity. Then we delineate the boundary between finite and non-finite axiomatisability of the congruences in van Glabbeek's linear time-branching time spectrum over CCS. Finally, we present a novel result to the effect that rooted weak bisimilarity has no finite complete axiomatisation over CCS.

Original language	English
Title of host publication	2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
Publisher	Institute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)	9781665448956
DOIs	https://doi.org/10.1109/LICS52264.2021.9470526
Publication status	Published - 29 Jun 2021
Event	36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 - Virtual, Online Duration: 29 Jun 2021 → 2 Jul 2021

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
Volume	2021-June
ISSN (Print)	1043-6871

Conference

Conference	36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021
City	Virtual, Online
Period	29/06/21 → 2/07/21

Bibliographical note

Funding Information:
This work has been supported by the project ‘Open Prob-

Publisher Copyright:
© 2021 IEEE.

Other keywords

bisimilarity
CCS
Equational logic
linear time-branching time spectrum
parallel composition

Access to Document

10.1109/LICS52264.2021.9470526

Cite this

Aceto, L., Anastasiadi, E., Castiglioni, V., Ingolfsdottir, A., & Luttik, B. (2021). In search of lost time: Axiomatising parallel composition in process algebras. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 Article 9470526 (Proceedings - Symposium on Logic in Computer Science; Vol. 2021-June). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/LICS52264.2021.9470526

@inproceedings{c97a751865854caabb58389f9c676719,

title = "In search of lost time: Axiomatising parallel composition in process algebras",

abstract = "This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS does not yield a finite axiomatisation of bisimilarity. Then we delineate the boundary between finite and non-finite axiomatisability of the congruences in van Glabbeek's linear time-branching time spectrum over CCS. Finally, we present a novel result to the effect that rooted weak bisimilarity has no finite complete axiomatisation over CCS.",

keywords = "bisimilarity, CCS, Equational logic, linear time-branching time spectrum, parallel composition",

author = "Luca Aceto and Elli Anastasiadi and Valentina Castiglioni and Anna Ingolfsdottir and Bas Luttik",

note = "Funding Information: This work has been supported by the project {\textquoteleft}Open Prob- Publisher Copyright: {\textcopyright} 2021 IEEE.; 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021 ; Conference date: 29-06-2021 Through 02-07-2021",

year = "2021",

month = jun,

day = "29",

doi = "10.1109/LICS52264.2021.9470526",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

booktitle = "2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021",

address = "United States",

}

Aceto, L, Anastasiadi, E, Castiglioni, V, Ingolfsdottir, A & Luttik, B 2021, In search of lost time: Axiomatising parallel composition in process algebras. in 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021., 9470526, Proceedings - Symposium on Logic in Computer Science, vol. 2021-June, Institute of Electrical and Electronics Engineers Inc., 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Virtual, Online, 29/06/21. https://doi.org/10.1109/LICS52264.2021.9470526

In search of lost time: Axiomatising parallel composition in process algebras. / Aceto, Luca; Anastasiadi, Elli; Castiglioni, Valentina et al.
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. Institute of Electrical and Electronics Engineers Inc., 2021. 9470526 (Proceedings - Symposium on Logic in Computer Science; Vol. 2021-June).

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

TY - GEN

T1 - In search of lost time

T2 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021

AU - Aceto, Luca

AU - Anastasiadi, Elli

AU - Castiglioni, Valentina

AU - Ingolfsdottir, Anna

AU - Luttik, Bas

PY - 2021/6/29

Y1 - 2021/6/29

N2 - This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS does not yield a finite axiomatisation of bisimilarity. Then we delineate the boundary between finite and non-finite axiomatisability of the congruences in van Glabbeek's linear time-branching time spectrum over CCS. Finally, we present a novel result to the effect that rooted weak bisimilarity has no finite complete axiomatisation over CCS.

AB - This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS does not yield a finite axiomatisation of bisimilarity. Then we delineate the boundary between finite and non-finite axiomatisability of the congruences in van Glabbeek's linear time-branching time spectrum over CCS. Finally, we present a novel result to the effect that rooted weak bisimilarity has no finite complete axiomatisation over CCS.

KW - bisimilarity

KW - CCS

KW - Equational logic

KW - linear time-branching time spectrum

KW - parallel composition

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

U2 - 10.1109/LICS52264.2021.9470526

DO - 10.1109/LICS52264.2021.9470526

M3 - Conference contribution

AN - SCOPUS:85113825289

T3 - Proceedings - Symposium on Logic in Computer Science

BT - 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 29 June 2021 through 2 July 2021

ER -

Aceto L, Anastasiadi E, Castiglioni V, Ingolfsdottir A, Luttik B. In search of lost time: Axiomatising parallel composition in process algebras. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021. Institute of Electrical and Electronics Engineers Inc. 2021. 9470526. (Proceedings - Symposium on Logic in Computer Science). doi: 10.1109/LICS52264.2021.9470526

In search of lost time: Axiomatising parallel composition in process algebras

Abstract

Publication series

Conference

Bibliographical note

Other keywords

Access to Document

Fingerprint

Cite this