SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Complete Proof Systems for First Order Interval Temporal Logic
 by Dr. Bruno Dutertre.

Different interval modal logics have been proposed for reasoning about the temporal behaviour 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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2023 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy