一句话：为有限状态行为提出保持发散分支同余的完备等式公理化，解决1993年以来的公开问题。
本文研究有限状态进程表达式的语义等价公理化问题。自1993年以来，保持发散的分支同余一直缺少完备的等式公理化。作者构造了一个等式推理系统：以van Glabbeek关于分支互模拟同余的简洁完备公理化为基础，删除在更精细的发散敏感语义下不健全的一条公理，再加入四条简单公理。论文证明该推理系统相对于保持发散的分支同余既是可靠的又是完备的，从而解决了这一长期公开问题，并为发散敏感的进程等价提供了一套完整而简洁的代数证明方法。
We present an equational inference system for finite-state expressions, and prove that the system is sound and complete with respect to divergence preserving branching congruence, closing a problem that has been open since 1993. The inference system refines Rob van Glabbeek's simple and elegant complete axiomatisation for branching bisimulation congruence of finite-state behaviours by joining four simple axioms after dropping one axiom which is unsound under the more refined divergence sensitive semantics.
DOI 原文 ·
@inproceedings{paperbot6180,
title = {A Complete Axiomatisation for Divergence Preserving Branching Congruence of Finite-State Behaviours},
author = {Xinxin Liu and Tingting Yu},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470647}
}