BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-89-1296
       ENTRY:: January 05, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Completing the temporal picture
        TYPE:: Technical Report
      AUTHOR:: Manna, Zohar
      AUTHOR:: Pnueli, Amir
        DATE:: December 1989
       PAGES:: 29
    ABSTRACT:: The paper presents a relatively complete proof system for
               proving the validity of temporal properties of reactive
               programs. The presented proof system improves oll previous
               temporal systems, such as [MP83a] and [MP83b], in that it
               reduces the validity of program properties into pure
               assertional reasoning, not involving additional temporal
               reasoning. The proof system is based on the classification of
               temporal properties according to the Borel hierarchy,
               providing an appropriate proof rule for each of the main
               classes, such as safety, response, and progress properties.
       NOTES:: [Adminitrivia V1/RAM/19950105]
         END:: STAN//CS-TR-89-1296