论并行组合的公理化
On the Axiomatisability of Parallel Composition
AI总结：
本文研究 BCCSP 中交错并行组合算子在不同行为等价性下的有限等式公理化，为模拟和迹语义给出有限基完备公理化，并证明包含互模拟且包含于可能未来等价中的同余无有限基完备公理化。
摘要：
本文研究了在 van Glabbeek 的线性时间-分支时间谱系中，交错并行组合算子相对于行为等价性的有限等式公理化存在性问题。在有限动作集上的进程代数 BCCSP 的背景下，我们为各种模拟语义和（装饰）迹语义提供了有限且基完备的公理化。我们还证明了，BCCSP 上任何包含互模拟等价且包含于可能未来等价之中的同余关系都不存在有限基完备的公理化；这一否定结果适用于所有嵌套迹和嵌套模拟语义。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
