A Really Temporal Logic

12 years 1 months ago
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.
Rajeev Alur, Thomas A. Henzinger
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1989
Where FOCS
Authors Rajeev Alur, Thomas A. Henzinger
Comments (0)