Paper: A Propositional Model Logic of Time Intervals (at LICS 1986)

Authors: Joseph Y. Halpern Yoav Shoham

Abstract

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 we develop a modal temporal logic based on time intervals, a logic which can be viewed as a generalization of point-based modal temporal logic. We discuss related logics, give an intuitive presentation of the new logic, and define its formal syntax and semantics. We make no assumption about the underlying nature of time, allowing it to be discrete (such as the integers) or continuous (such as the rationals or the reals), linear or branching, complete (such as the reals) or not (such as the rationals). We show, however, that there are formulas in the logic that allow us to distinguish all these situations. We also show a translation of our logic into first-order logic, which allows us to apply some results on the first-order logic to our modal one. Finally, we consider the difficulty of validity problem for the logic. This turns out to depend critically, and in surprising ways, on our assumptions about time. For example, if we take our underlying temporal structure to be the rationals, we can show that the validity problem is r.e.-complete, if it is the reals then we can show that validity is Π¹₁-hard, and if it is the integers then validity is Π¹₁-complete.

BibTeX

  @InProceedings{HalpernShoham-APropositionalModel,
    author = 	 {Joseph Y. Halpern and Yoav Shoham},
    title = 	 {A Propositional Model Logic of Time Intervals},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {279--292},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }