Title: On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions,
Abstract: In this paper, we investigate the model checking (MC) problem for Halpern and
Shoham's interval temporal logic HS. In the last years, interval temporal logic
MC has received an increasing attention as a viable alternative to the
traditional (point-based) temporal logic MC, which can be recovered as a
special case. Most results have been obtained under the homogeneity assumption,
that constrains a proposition letter to hold over an interval if and only if it
holds over each component state. Recently, Lomuscio and Michaliszyn proposed a
way to relax such an assumption by exploiting regular expressions to define the
behaviour of proposition letters over intervals in terms of their component
states. When homogeneity is assumed, the exact complexity of MC is a difficult
open question for full HS and for its two syntactically maximal fragments
AA'BB'E' and AA'EB'E'. In this paper, we provide an asymptotically optimal
bound to the complexity of these two fragments under the more expressive
semantic variant based on regular expressions by showing that their MC problem
is AEXP_pol-complete, where AEXP_pol denotes the complexity class of problems
decided by exponential-time bounded alternating Turing Machines making a
polynomially bounded number of alternations.