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
N1 - Funding Information: This work has been supported by the project ‘Open Prob- Publisher Copyright: © 2021 IEEE.
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 - CCS
KW - Equational logic
KW - bisimilarity
KW - linear time-branching time spectrum
KW - parallel composition
UR - https://www.scopus.com/pages/publications/85113825289
U2 - 10.1109/LICS52264.2021.9470526
DO - 10.1109/LICS52264.2021.9470526
M3 - Conference contribution
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 -