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.