Which fragments of the interval temporal logic HS are tractable in model checking? (Q1731517)

Interval temporal logic is a specialised temporal logic in which the primitives are intervals of some order, typically a linear order. Interval temporal logics can naturally be interpreted over Kripke structures using a linear-time semantics, i.e. all runs of the structure are supposed to satisfiy the formula, here meaning that all intervals which are started on such a run should do so. The operators of interval temporal logics are then the diamond- and box-modalities associated with Allen's relations on intervals. By restricting the set of relations that can be used, one obtains different (fragments) of interval temporal logics with different expressiveness and computational complexities. The paper at hand is concerned with the model checking problem for interval temporal logics over finite Kripke structures. It serves two purposes. First, it provides an overview of known results about the complexity of model checking in terms of upper and lower bounds for interval temporal logics, depending on which interval relations are being used. Second, it presents some simplified constructions for obtaining some of these upper bounds. These are generally obtained using small-model theorems which state that whenever some interval, i.e. path of a finite Kripke structure, satisfies a given formula, then there is already a short path, resp. interval, doing so. The paper is generally well written, and is suitable as an entry point into the field of model checking for interval temporal logics.