BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-89-1267
       ENTRY:: September 27, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: A really temporal logic.
        TYPE:: Technical Report
      AUTHOR:: Alur, Rajeev
      AUTHOR:: Henzinger, Thomas A.
        DATE:: July 1989
       PAGES:: 29
    ABSTRACT:: We introduce a real-time temporal logic for the specification
               of reactive systems. The novel feature of our logic, TPTL, is
               the adoption of temporal operators as quantifiers over time
               variables; every modality binds a variable to the time(s) it
               refers to.

               TPTL is demonstrated to be both a natural specification
               language as well as a suitable formalism for verification and
               synthesis. We present a tableau-based decision procedure and
               model-checking algorithm for TPTL. Several generalizations of
               TPTL are shown to be highly undecidable.
       NOTES:: [Adminitrivia V1/RAM/19940927]
         END:: STAN//CS-TR-89-1267