Title :
A complete axiomatization of interval temporal logic with infinite time
Author :
Moszkowski, B.C.
Author_Institution :
Software Technol. Res. Lab., De Montfort Univ., Leicester, UK
Abstract :
Interval temporal logic (ITL) is a formalism for reasoning about time periods. To date no one has proved completeness of a relatively simple ITL deductive system supporting infinite time and permitting infinite sequential iteration comparable to ω-regular expressions. We give a complete axiomatization for such a version of quantified ITL over finite domains and can show completeness by representing finite-state automata in ITL and then translating ITL formulas into them. The axiom system (and completeness) is extended to infinite time
Keywords :
computational complexity; finite state machines; temporal logic; temporal reasoning; theorem proving; ω-regular expressions; ITL formulas; axiom system; complete axiomatization; completeness proving; finite domains; finite-state automata; infinite sequential iteration; infinite time; interval temporal logic; quantified ITL; simple ITL deductive system; temporal reasoning; time periods; Automata; Calculus; Chaos; Logic; Reactive power; Real time systems;
Conference_Titel :
Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on
Conference_Location :
Santa Barbara, CA
Print_ISBN :
0-7695-0725-5
DOI :
10.1109/LICS.2000.855773
