Title :
A really temporal logic
Author :
Alur, Rajeev ; Henzinger, Thomas A.
Author_Institution :
Dept. of Comput. Sci., Stanford Univ., CA, USA
fDate :
30 Oct-1 Nov 1989
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
Keywords :
formal logic; formal specification; specification languages; TPTL; formalism; model-checking algorithm; natural specification language; quantifiers; reactive systems; really temporal logic; specification; synthesis; tableau-based decision procedure; temporal operators; verification; Computer science; Contracts; Logic; Real time systems; Specification languages;
Conference_Titel :
Foundations of Computer Science, 1989., 30th Annual Symposium on
Conference_Location :
Research Triangle Park, NC
Print_ISBN :
0-8186-1982-1
DOI :
10.1109/SFCS.1989.63473
