Expressiveness, decidability, and undecidability of Interval Temporal Logic

Dario Della Monica
Università di Udine
1 Aprile 2011


Interval Temporal Logics are formalisms particularly suitable to express temporal properties. Unlike standard temporal logics, they use intervals, instead of points, as primitive ontological entities. The most studied propositional interval temporal logic is Halpern and Shoham’s Modal Logic of Time Intervals (HS for short). It features a modal operator for each possible ordering relation between pairs of intervals (the so-called Allen’s relations). HS is very expressive, but its satisfiability problem turns out to be highly undecidable (over most classes of linear orders). The three main contributions of this thesis are the following ones. First, we provide a complete classification of HS fragments with respect to their relative expressive power in the class of all linear orders. Second, we systematically investigate the decidable/undecidable status of the satisfiability problem for a number of previously unclassified HS fragments, showing that, once more, undecidability is the rule and decidability the exception. Pairing the results given here with existing ones, the long-standing goal of obtaining a complete classification of all HS fragments with respect to their satisfiability problem is now almost achieved. Third, we study metric, hybrid, and first-order extensions of Propositional Neighborhood Logic (over natural numbers), a meaningful and well-studied decidable fragment of HS.