A hierarchy of temporal properties
A hierarchy of temporal properties
复制标题
时间属性的层次结构
DOI：
10.1145/41840.41857
复制
发表时间：
1987
期刊：
影响因子：
--
通讯作者：
A. Pnueli
中科院分区：
文献类型：
--
作者：
Z. Manna;A. Pnueli
我们提出了一个分类的时间属性到一个层次结构，完善了已知的安全活性分类的属性。新的分类识别安全、保证、持久性、公平和超公平的类别。这里建议的分类是基于有限计算的性质可以扩展到无限计算的性质的不同方式。对于可由时态逻辑和谓词自动机表示的属性，我们提供了指定不同类中属性的公式和自动机的语法特征。我们考虑了一个给定的程序的属性的验证，并为每个类提供了一个唯一的证明原则。
We propose a classification of temporal properties into a hierarchy which refines the known safety-liveness classification of properties. The new classification recognizes the classes of safety, guarantee, persistence, fairness, and hyper-fairness. The classification suggested here is based on the different ways a property of finite computations can be extended into a property of infinite computations. For properties that are expressible by temporal logic and predicate automata, we provide a syntactic characterization of the formulae and automata that specify properties in the different classes. We consider the verification of properties over a given program, and provide a unique proof principle for each class.