A Really Temporal Logic

We introduce a temporal logic for the speci cation of real-time systems. Our logic, TPTL, employs a novel quanti er construct for referencing time: the freeze quanti er binds a variable to the time of the local temporal context. TPTL is both a natural language for speci cation and a suitable formalism for veri cation. We present a tableau-based decision procedure and a model checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.

• Type: Conference
• Year: 1989
• Where: FOCS
• Authors: Rajeev Alur, Thomas A. Henzinger
• Keywords: FOCS 1989, Quanti Er, Quanti Er Construct, Speci Cation, Theoretical Computer Science