Interval Temporal Logic

Interval Temporal Logic

Howard Bowman and Simon Thompson

Interval Temporal Logic (ITL) is an important class of temporal logic which was initally devised by Ben Moskowski in the 1980's.

Standard temporal logics (see e.g. this page) are defined over infinite state models, for example, the models for Manna and Pnueli Linear Time Temporal Logic are infinite state sequences. However, in interval temporal logic the model theory is restricted to finite state sequences, called intervals (although, supporting infinite state sequences is currently being investigated).

There are a number of reasons for being interested in such logics. One reason is that interval temporal logic lends itself to execution. This is apparent from Moskowski's initial work. In addition, a number of interesting and powerful operators arise naturally from ITL. In fact, it is straightforward to derive operators very like the constructs of imperative programming (e.g. assignment, conditionals, iteration etc). This then yields the possibility that abstract specifications and concrete implementations can be realised in the same notation, with refinement mappings between.

An additional aspect of interval temporal logic is that it provides a very simple real-time model in which one unit of time is past when moving from state to state. Consequently, timings can be obtained by measuring interval lengths.

Two operators which are characteristic of interval temporal logic are the Chop operator ; and the projection operator Proj. The former of these implements a form of sequential composition, while the projection operator yields repetitive behaviour.

A further reason for being interested in logics containing chop and repetition operators (such as projection) is that they address the problem of the limited expressiveness of classic point based temporal logics such as linear and branching time temporal logics. It is well known that propositional temporal logic is expressively limited. In fact, propositional temporal logics are only as expressive as F1S (the first order theory of linear orders). In addition, logics with chop, such as Rosner and Pnueli's Choppy logic, are similarly expressive. However, addition of the star operator brings the expressive power of S1S (the second order theory of linear orders), i.e. omega regular languages. Furthermore, projection is at least as expressive as star.

Our initial work in this area, which was in collaboration with Helen Cameron, and Peter King, investigated how multimedia documents could be specified using ITL. The following conference paper outlines our work on the topic, while the journal paper gives a more indepth explanation of our work.

Following on from our initial work on interval temporal logic, we have become interested in more theoretical aspects of the ITL approach. In particular, the following two papers (of which the second is the more comprehensive) present a tableau method for checking satisfiability of ITL formulae, and give a proof of completeness of an axiomatisation of ITL, which uses tableaux.

Back to Howard Bowman's home page.

Last modified August 2003.