## A Really Temporal Logic

*Rajeev Alur and
Thomas A. Henzinger*
We introduce a temporal logic for the specification of real-time systems.
Our logic, TPTL, employs a novel quantifier construct for referencing time:
the "freeze" quantifier binds a variable to the time of the local temporal
context.
TPTL is both a natural language for specification and a suitable formalism
for verification.
We present a tableau-based decision procedure and a model-checking algorithm
for TPTL.
Several generalizations of TPTL are shown to be highly undecidable.

*Journal of the ACM* 41:181-204, 1994.
A preliminary version appeared in the
*Proceedings of the
30th Annual IEEE Symposium on Foundations of Computer Science*
(FOCS 1989), pp. 164-169.