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 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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/89/1267/CS-TR-89-1267.pdf