方程的分歧和唯一解
摘要：基于方程的唯一解决方法，我们研究了等价性的证明技术。我们从Roscoe在CSP的含义设置中得出的结果中汲取灵感，并针对失败语义，基本上是指一个方程（或一组方程）的无限展开永远不会产生发散，具有唯一解决性质。我们将这个结果转移到CCS的操作设置和等价性上。然后，我们利用操作方法来：完善定理，区分不同形式的发散；导出定理的抽象形式，适用于一般的LTS；将定理调整为其他等价性，如跟踪等价性，以及预序如跟踪包含。我们将所得到的技术与等价性证明方法的增强（“up-to技术”）进行比较。最后，我们在异步π-演算等通过命名的计算中探讨了这些定理，并将它们用于重新审视Milner对将λ-演算编码到π-演算的完全抽象性证明的Levy-Longo树部分的完整性。
作者：Adrien Durier, Daniel Hirschkoff, Davide Sangiorgi
论文ID：1806.11354
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22