BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-87-1186
       ENTRY:: April 24, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: A Hierarchy of Temporal Properties
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: October 1987
       PAGES:: 46
    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.
       NOTES:: [Adminitrivia V1/Prg/19950424]
         END:: STAN//CS-TR-87-1186