Title :
Explicit clock temporal logic
Author :
Harel, Eyal ; Lichtenstein, Orna ; Pnueli, Amir
Author_Institution :
Dept. of Appl. Math., Weizmann Inst. of Sci., Rehobot, Israel
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;
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
DOI :
10.1109/LICS.1990.113765
