51. Model checking well-behaved fragments of HS: The (almost) final picture
- Author
-
Molinari, A., Montanari, A., Peron, A., Pietro SALA, Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala, Delgrande J.,Baral C.,Wolter F., Alberto, Molinari, Angelo, Montanari, Peron, Adriano, and Pietro, Sala
- Subjects
Computational Complexity ,Temporal logic Interval temporal logic ,Knowledge representation ,System verifications ,Model checker ,Point-based ,Model checking algorithm ,Model Checking, Interval Temporal Logics, Computational Complexity ,Model checking problem ,Model checking Interval Temporal Logic Computational Complexity ,Model Checking ,Interval Temporal Logics - Abstract
Model checking is one of the most powerful and widespread tools for system verification with applications in many areas of computer science and artificial intelligence. The large majority of model checkers deal with properties expressed in point-based temporal logics, such as LTL and CTL. However, there exist relevant properties of systems which are inherently interval-based. Model checking algorithms for interval temporal logics (ITLs) have recently been proposed to check interval properties of computations. As the model checking problem for full Halpern and Shoham's ITL (HS for short) turns out to be decidable, but computationally heavy, research has focused on its well-behaved fragments. In this paper, we provide an almost final picture of the computational complexity of model checking for HS fragments with modalities for (a subset of) Allen's relations meets, met by, starts, and ends.