DocumentCode
2717732
Title
Explicit clock temporal logic
Author
Harel, Eyal ; Lichtenstein, Orna ; Pnueli, Amir
Author_Institution
Dept. of Appl. Math., Weizmann Inst. of Sci., Rehobot, Israel
fYear
1990
fDate
4-7 Jun 1990
Firstpage
402
Lastpage
413
Abstract
The authors present a single exponent decision procedure for the validity of XCTL formulas, and a double exponent decision procedure for the validity of XCTL formulas over finite state programs (model checking). The expressive power of XCTL is compared with that of some other logics proposed for the expression of real time properties. It is shown that it is incomparable with the expressive power of the recently proposed logic TPTL (timed propositional temporal logic)
Keywords
computational complexity; finite automata; program verification; temporal logic; XCTL formulas; double exponent decision procedure; explicit clock temporal logic; finite state programs; model checking; single exponent decision procedure; timed propositional temporal logic; validity checking; Clocks; Delay; Logic; Mathematics; Real time systems; Scattering; Timing; Upper bound;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
Conference_Location
Philadelphia, PA
Print_ISBN
0-8186-2073-0
Type
conf
DOI
10.1109/LICS.1990.113765
Filename
113765
Link To Document