|Abstract||Model checking is a powerful method widely explored in formal verification.
Given a model of a system, e.g., a Kripke structure, and a formula specifying
its expected behaviour, one can verify whether the system meets the behaviour
by checking the formula against the model.
Classically, system behaviour is expressed by a formula of a temporal logic,
such as LTL and the like. These logics are ``point-wise'' interpreted, as
they describe how the system evolves state-by-state.
However, there are relevant properties, such as those constraining the temporal
relations between pairs of temporally extended events or involving temporal
aggregations, which are inherently ``interval-based'', and thus asking for
an interval temporal logic.
In this paper, we give a formalization of the model checking problem in an
interval logic setting. First, we provide an interpretation of formulas of
Halpern and Shoham's interval temporal logic HS over finite Kripke structures,
which allows one to check interval properties of computations. Then, we prove that
the model checking problem for HS against finite Kripke structures is decidable by
a suitable small model theorem, and we provide a lower bound to its computational