事件系统的不带和带公平性假设的不动点语义
摘要：事件系统的不动点语义的的修复方法是以一种通用的框架呈现的，而没有考虑公平性。在这个通用框架中，我们证明了推导“leads-to”属性的规则的准确性和完整性。通用框架被实例化为最小进展和弱公平性假设，并获得了类似的结果。我们通过推导“leads-to”的足够条件来展示这些结果的能力，在不需要对状态跟踪进行推理的情况下，证明了证明义务的准确性。
作者：Hector Ruiz Barradas (LSR - IMAG), Didier Bert (LSR - IMAG)
论文ID：cs/0512082
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23