Fifteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2000)

Paper: A Complete Axiomatization of Interval Temporal Logic with Infinite Time (at LICS 2000)

Authors: B.C. Moszkowski


Interval Temporal Logic (ITL) is formalism for reasoning about times. To date no one has proved completeness of a relatively simple ITL deductive system supporting infinite time and permitting infinite sequential iteration comparable to omega-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 full paper (and another conference paper) presents the basic framework for finite time. Here and in the full paper the axiom system (and completeness) is extended to infinite time.


    author = 	 {B.C. Moszkowski},
    title = 	 {A Complete Axiomatization of Interval Temporal Logic with Infinite Time},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {241--252},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}