分布式系统活性性质的精化
On the Refinement of Liveness Properties of Distributed Systems
摘要：
我们提出了一种新的方法来推理分布式系统的活性特性，表示为自动机。我们的方法是基于模拟关系，只需要推理有限的执行片段。当前基于模拟关系的自动机活性属性推理方法需要对整个执行进行推理，因为它们涉及以下形式的证明义务：如果具体和抽象执行通过模拟“对应”，并且具体执行是活的，那么抽象执行也是活的。我们的贡献包括（1）定义活性性质的形式，（2）基于该形式的活性性质的证明方法，和（3）两个表达完备性结果：第一，我们的形式可以表示任何满足自然"鲁棒性“条件的活性性质，第二，我们的形式可以表示任何活性性质，只要历史变量可以使用
英文摘要：
We present a new approach for reasoning about liveness properties of distributed systems, represented as automata. Our approach is based on simulation relations, and requires reasoning only over finite execution fragments. Current simulation-relation based methods for reasoning about liveness properties of automata require reasoning over entire executions, since they involve a proof obligation of the form: if a concrete and abstract execution ``correspond'' via the simulation, and the concrete execution is live, then so is the abstract execution. Our contribution consists of (1) a formalism for defining liveness properties, (2) a proof method for liveness properties based on that formalism, and (3) two expressive completeness results: firstly, our formalism can express any liveness property which satisfies a natural ``robustness'' condition, and secondly, our formalism can express any liveness property at all, provided that history variables can be used
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
