在公平性和行为抽象中检查属性
摘要：验证公平条件下的生存性属性通常存在问题，特别是在使用抽象化时。本文表明，使用比公平下的真理更抽象的概念，特别是在公平条件下满足属性的概念，可以带来有趣的可能性。从技术上讲，首先确定了在公平条件下判断满足性的问题是PSPACE完备的，并且证明了在公平条件下满足的属性总是可以由一些公平的实现满足。之后，研究了行为抽象和在公平条件下满足性之间的相互作用，并证明了如果抽象同态是弱连续的，则可以在行为抽象上验证在公平条件下的属性满足性。
作者：Ulrich Ultes-Nitsche and Pierre Wolper
论文ID：cs/0101017
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23