Alur, Rajeev; Henzinger, Thomas AIST Austria
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.
164 - 169
FOCS: Foundations of Computer Science
Alur R, Henzinger TA. A really temporal logic. In: IEEE; 1989:164-169. doi:10.1109/SFCS.1989.63473
Alur, R., & Henzinger, T. A. (1989). A really temporal logic (pp. 164–169). Presented at the FOCS: Foundations of Computer Science, IEEE. https://doi.org/10.1109/SFCS.1989.63473
Alur, Rajeev, and Thomas A Henzinger. “A Really Temporal Logic,” 164–69. IEEE, 1989. https://doi.org/10.1109/SFCS.1989.63473.
R. Alur and T. A. Henzinger, “A really temporal logic,” presented at the FOCS: Foundations of Computer Science, 1989, pp. 164–169.
Alur R, Henzinger TA. 1989. A really temporal logic. FOCS: Foundations of Computer Science, 164–169.
Alur, Rajeev, and Thomas A. Henzinger. A Really Temporal Logic. IEEE, 1989, pp. 164–69, doi:10.1109/SFCS.1989.63473.
Link(s) to Main File(s)