@inproceedings{4596,
  abstract     = {A real-time temporal logic for the specification of reactive systems is introduced. The novel feature of the 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 and a suitable formalism for verification and synthesis. A tableau-based decision procedure and model-checking algorithm for TPTL are presented. Several generalizations of TPTL are shown to be highly undecidable.},
  author       = {Alur, Rajeev and Henzinger, Thomas A},
  booktitle    = {30th Annual Symposium on Foundations of Computer Science},
  isbn         = {0-8186-1982-1},
  issn         = {1558-0814},
  location     = {Research Triangle Park, NC, USA},
  pages        = {164 -- 169},
  publisher    = {IEEE},
  title        = {{A really temporal logic}},
  doi          = {10.1109/SFCS.1989.63473},
  year         = {1989},
}