提出两种新等价关系，解决可逆进程演算中弱同步的匹配难题。
On Weak Bisimilarities in CCSK
- 区分方向性与混合型弱可逆等价，基于τ动作方向设计匹配规则。
- 混合等价是同余关系，能完全隐藏τ动作的影响。
- 适合形式化验证与并发系统建模的研究者阅读。
在可逆扩展的CCSK（即可逆的通信系统演算）背景下，研究了强/弱、单向/可逆等多种等价关系，并揭示其异同。针对此前未被研究的弱可逆情形，提出了两种变体：方向性等价与混合等价，区别在于τ动作是否需与被匹配动作保持相同方向（前向或后向）。特别地，证明了混合等价是同余关系，且能完全抽象掉τ动作的影响。
原文摘要 · Abstract (English)
In the context of CCSK, a reversible extension of CCS, we study different notions of bisimilarity (strong/weak, forward-only/reversible) and highlight their differences and commonalities. In particular, for the weak reversible case, not previously studied in the literature, we propose two variants, dubbed directional and mixed bisimilarity, depending on whether $τ$ actions should be in the same direction (forward/backward) as the action being matched or not. We show, in particular, that mixed bisimilarity is a congruence and completely abstracts away from $τ$ actions.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。