Complexity of ITL model checking: some well-behaved fragments of the interval logic HS

Abstract

Model checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics, while little work has been done in the interval temporal logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS over finite Kripke structures (under the homogeneity assumption) and an EXPSPACE model checking procedure for two meaningful fragments of it have been proposed. In this paper, we show that more efficient model checking procedures can be developed for some expressive enough fragments of HS.

References in corpus (1)

• Checking Interval Properties of Computations

Cited by in corpus (5)

• On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions
• Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
• Model Checking for Fragments of Halpern and Shoham's Interval Temporal Logic Based on Track Representatives
• Model Checking the Logic of Allen's Relations Meets and Started-by is $P^{N}P$-Complete
• Model checking: the interval way