关于 CCS 上分支互模拟同余的公理化
计算机科学中的逻辑
2022-06-29 v1
摘要
本文研究 CCS（去除限制、重标记与递归的片段）模以根分支互模拟（rooted branching bisimilarity）的等式理论，这是一种经典的、基于互模拟的等价概念，可抽象掉进程行为中的内部计算步骤。首先，我们证明 CCS 在所给同余下不是有限基的。作为该否定性结果证明中一个具有独立意义的关键步骤，我们证明每个 CCS 进程在分支互模拟意义下都具有唯一的并行分解为不可分解进程。作为第二主要贡献，我们证明当动作集合有限时，根分支互模拟在 enriched with left merge 与 communication merge 算子（来自 ACP）的 CCS 上具有有限等式基。
引用
@article{arxiv.2206.13927,
title = {On the Axiomatisation of Branching Bisimulation Congruence over CCS},
author = {Luca Aceto and Valentina Castiglioni and Anna Ingolfsdottir and Bas Luttik},
journal= {arXiv preprint arXiv:2206.13927},
year = {2022}
}