Report Number: CS-TR-87-1186
Institution: Stanford University, Department of Computer Science
Title: A Hierarchy of Temporal Properties
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: October 1987
Abstract: 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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/87/1186/CS-TR-87-1186.pdf