一句话：将CSP中基于方程唯一解的双相似证明方法迁移到CCS等操作语义，并区分发散、推广到迹等价与π演算。
论文研究基于方程唯一解证明双相似性的技术。作者受 Roscoe 在 CSP 失败语义中的结果启发：若方程（组）的无限展开永不产生发散，则具有唯一解性质，并将该结果从指称语义迁移到 CCS 的操作语义与双相似性。借助操作视角，作者细化定理以区分不同发散形式，在一般 LTS 上给出抽象表述，并把结论推广到迹等价、迹包含等前序关系。文中还将新技术与双模拟证明方法的 up-to 技术相比较，并在异步 π 演算等传名演算中考察定理，用它重新审视 Milner 将 λ 演算编码到 π 演算、针对 Lévy-Longo 树的全抽象证明的完备性部分。
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the `up-to techniques'). Finally, we study the theorems in name-passing calculi such as the asynchronous $\pi$-calculus, and use them to revisit the completeness part of the proof of full abstraction of Milner's encoding of the $\lambda$-calculus into the $\pi$-calculus for L\'evy-Longo Trees. Comment: This is an extended version of the paper with the same title published in the proceedings of CONCUR'17
@article{paperbot773,
title = {Divergence and unique solution of equations},
author = {Adrien Durier and Daniel Hirschkoff and Davide Sangiorgi},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:12)2019}
}