Interval Temporal Logics over Strongly Discrete Linear Orders: the Complete Picture

TL;DR

This paper provides a comprehensive classification of all decidable fragments of Halpern and Shoham's interval temporal logic over strongly discrete linear orders, detailing their expressive power and complexity, and analyzing the special case of natural numbers.

Contribution

It identifies all decidable fragments of HS over strongly discrete linear orders, classifies their complexity, and highlights the unique case of natural numbers with some undecidable fragments becoming decidable.

Findings

44 decidable fragments with complexity from NP to EXPSPACE

Some previously undecidable fragments are now decidable over natural numbers

The number of decidable fragments increases to 47 for natural numbers, with some becoming non-primitive recursive in complexity

Abstract

Interval temporal logics provide a general framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. In this paper, we identify all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the class of strongly discrete linear orders. We classify them in terms of both their relative expressive power and their complexity. We show that there are exactly 44 expressively different decidable fragments, whose complexity ranges from NP to EXPSPACE. In addition, we identify some new undecidable fragments (all the remaining HS fragments were already known to be undecidable over strongly discrete linear orders). We conclude the paper by an analysis of the specific case of natural numbers, whose behavior slightly differs from that of the whole class of strongly discrete linear orders. The number of decidable fragments over natural numbers raises up to 47: three undecidable fragments become decidable with a non-primitive recursive complexity.