Model checking well-behaved fragments of HS: the (almost) final picture

Abstract

Model checking is one of the most powerful and widespread
\ntools for system verification with applications in many areas
\nof computer science and artificial intelligence. The large majority
\nof model checkers deal with properties expressed in
\npoint-based temporal logics, such as LTL and CTL. However,
\nthere exist relevant properties of systems which are inherently
\ninterval-based. Model checking algorithms for interval
\ntemporal logics (ITLs) have recently been proposed to check
\ninterval properties of computations. As the model checking
\nproblem for full Halpern and Shoham’s ITL (HS for short)
\nturns out to be decidable, but computationally heavy, research
\nhas focused on its well-behaved fragments. In this paper, we
\nprovide an almost final picture of the computational complexity
\nof model checking for HS fragments with modalities for
\n(a subset of) Allen’s relations meets, met by, starts, and ends