Correctness proofs of distributed termination algorithms
Correctness proofs of distributed termination algorithms
复制标题
分布式终止算法的正确性证明
DOI：
--
复制
发表时间：
1986
期刊：
影响因子：
--
通讯作者：
K. Apt
中科院分区：
文献类型：
--
作者：
K. Apt
解决了解决方案对法兰西斯分布式终止问题的正确性[7]。正确性标准是在程序正确性的习惯框架中形式化的。提出了一种非常简单的证明方法并应用以显示解决方案的正确性。它使我们能够使用新的总正确性概念来理解时间逻辑的透明性特性（例如，参见Manna和Pnueli [12]）。
The problem of correctness of the solutions to the distributed termination problem of Francez [7] is addressed. Correctness criteria are formalized in the customary framework for program correctness. A very simple proof method is proposed and applied to show correctness of a solution to the problem. It allows us to reason about liveness properties of temporal logic (see, e.g., Manna and Pnueli [12]) using a new notion of weak total correctness.