DocumentCode
2111020
Title
A really temporal logic
Author
Alur, Rajeev ; Henzinger, Thomas A.
Author_Institution
Dept. of Comput. Sci., Stanford Univ., CA, USA
fYear
1989
fDate
30 Oct-1 Nov 1989
Firstpage
164
Lastpage
169
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Foundations of Computer Science, 1989., 30th Annual Symposium on
Conference_Location
Research Triangle Park, NC
Print_ISBN
0-8186-1982-1
Type
conf
DOI
10.1109/SFCS.1989.63473
Filename
63473
Link To Document