论文标题
在CCS上的分支分支一致性的公理化
On the Axiomatisation of Branching Bisimulation Congruence over CCS
论文作者
论文摘要
在本文中，我们调查了（限制，重新布置和递归片段的平等理论）CCS Modulo扎根分支双性恋，这是一种经典的，基于双分裂的等效概念，从过程行为中的内部计算步骤中抽象出来。首先，我们表明CCS不是基于有限的Modulo。作为对该负面结果证明的独立兴趣的关键步骤，我们证明每个CCS过程在不可分解的过程中都有独特的并行分解模型分支双向分支。作为第二个主要贡献，我们表明，当一组动作是有限的时，植根的分支双相似性在CCS上具有有限的方程式，而CCS富含ACP的左合并和通信合并操作员。
In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.
