一句话：在 BCCSP 中为交错并行组合的多种模拟与踪迹语义给出有限完备公理化，并证明嵌套踪迹/模拟语义不可有限公理化。
本文研究交错并行组合算子在 van Glabbeek 线性时间—分支时间谱系中各行为等价下的有限等式公理化问题。作者在有限动作集上的进程代数 BCCSP 中，为多种模拟语义及（带装饰的）踪迹语义构造了有限且 ground-complete 的等式公理系统；同时证明，任何包含 bisimilarity 且被 possible futures 等价包含的 BCCSP 同余关系都不具有有限 ground-complete 公理化。该否定结果覆盖所有嵌套踪迹与嵌套模拟语义，从而划定了并行组合可有限公理化的边界。
This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek's linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. We also show that no congruence over BCCSP that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation; this negative result applies to all the nested trace and nested simulation semantics.
@article{paperbot1740,
title = {On the Axiomatisability of Parallel Composition},
author = {Luca Aceto and Valentina Castiglioni and Anna Ingolfsdottir and Bas Luttik and Mathias R. Pedersen},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:15)2022}
}