分布式系统活性属性的细化
摘要：基于有限执行片段的模拟关系论证是一种新的用于推理分布式系统的活力属性的方法。目前基于模拟关系的方法需要整个执行过程进行推理，因为它们涉及到一种证明义务：如果一个具体和抽象执行经过模拟“对应”，并且具体执行是活跃的，则抽象执行也是活跃的。本文的贡献包括（1）定义活力属性的形式化，（2）基于该形式化的活力属性的证明方法，以及（3）两个表达完备性的结果：首先，我们的形式化可以表达满足自然“健壮性”条件的任何活力属性，其次，只要可以使用历史变量，我们的形式化可以表达任何活力属性。
作者：Paul C. Attie
论文ID：0801.0949
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-01-08