A really temporal logic Alur, Rajeev Henzinger, Thomas A ; https://orcid.org/0000−0002−2985−7724 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. IEEE 1989 info:eu-repo/semantics/conferenceObject doc-type:conferenceObject text http://purl.org/coar/resource_type/c_5794 https://research-explorer.ista.ac.at/record/4596 Alur R, Henzinger TA. A really temporal logic. In: <i>30th Annual Symposium on Foundations of Computer Science</i>. FCOS. IEEE; 1989:164-169. doi:<a href="https://doi.org/10.1109/SFCS.1989.63473">10.1109/SFCS.1989.63473</a> eng info:eu-repo/semantics/altIdentifier/doi/10.1109/SFCS.1989.63473 info:eu-repo/semantics/altIdentifier/issn/0018-9162 info:eu-repo/semantics/altIdentifier/e-issn/1558-0814 info:eu-repo/semantics/altIdentifier/isbn/0-8186-1982-1 info:eu-repo/semantics/closedAccess