Report Number: CS-TR-89-1267
Institution: Stanford University, Department of Computer Science
Title: A really temporal logic.
Author: Alur, Rajeev
Author: Henzinger, Thomas A.
Date: July 1989
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
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.