A PROPOSITIONAL MODAL LOGIC OF TIME INTERVALS

In certain areas of artificial intelligence there is need to represent continuous change and to make statements that are interpreted with respect to time intervals rather than time points. To this end, a modal temporal logic based on time intervals is developed, a logic that can be viewed as a generalization of point-based modal temporal logic. Related logics are discussed, an intuitive presentation of the new logic is given, and its formal syntax and semantics are defined. No assumption is made about the underlying nature of time, allowing it to be discrete (such as the natural numbers) or continuous (such as the rationals or the reals), linear or branching, complete (such as the reals), or not (such as the rationals). It is shown, however, that there are formulas in the logic that allow us to distinguish all these situations. A translation of our logic into first-order logic is given, which allows the application of some results on first-order logic to our modal logic. Finally, the difficulty of validity problems for the logic is considered. This turns out to depend critically, and in surprising ways, on our assumptions about time. For example, if our underlying temporal structure is the rationals, then, the validity problem is r.e.-complete; if it is the reals, then validity is PI-1(1)-hard; and if it is the natural numbers, then validity is PI-1(1)-complete.