一句话：综述并推进 CCS 并行组合公理化：解决有限可公理化边界及 rooted weak bisimilarity 无有限完全公理化等开放问题。
本文综述进程代数中并行组合公理化的若干最新与经典成果，聚焦不含递归、重标号和限制的 CCS 片段。文章讨论三个长期开放的问题。首先，针对 Bergstra 和 Klop 的辅助算子 left merge 与 communication merge 在模 bisimilarity 的有限公理化中的地位，作者论证：在若干自然假设下，向 CCS 添加单个辅助二元算子并不能得到 bisimilarity 的有限公理化。其次，文章刻画了 van Glabbeek 线性时间—分支时间谱中各种同余在 CCS 上有限可公理化与不可公理化之间的边界。最后，作者给出新结果：rooted weak bisimilarity 在 CCS 上不存在有限完全公理化。
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.
@inproceedings{paperbot6199,
title = {In search of lost time: Axiomatising parallel composition in process algebras},
author = {Luca Aceto and Elli Anastasiadi and Valentina Castiglioni and Anna Ingolfsdottir and Bas Luttik},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470526}
}