Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

Paper: Complete Proof Systems for First Order Interval Temporal Logic (at LICS 1995)

Authors: Bruno Dutertre


Different interval modal logics have been proposed for reasoning about the temporal behavior of digital systems. Some of them are purely propositional and only enable the specification of qualitative time requirements. Others, such as ITL and the duration calculus, are first order logics which support the expression of quantitative, real-time requirements. These two logics have in common the presence of a binary modal operator `chop' interpreted as the action of splitting an interval into two parts. Proof systems for ITL or the duration calculus have been proposed but little is known about their power. This paper present completeness results for a variant of ITL where `chop' is the only modal operator. We consider several classes of models for ITL which make different assumptions about time and we construct a complete and sound proof system for each class.


    author = 	 {Bruno Dutertre},
    title = 	 {Complete Proof Systems for First Order Interval Temporal Logic},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {36-46},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}