On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions

TL;DR

This paper analyzes the complexity of model checking for maximal fragments of the interval temporal logic HS with regular expressions, establishing an asymptotically optimal complexity bound.

Contribution

It provides the first complexity classification of model checking for these HS fragments under the expressive regular expression semantics.

Findings

Model checking for these fragments is AEXP_pol-complete.

Complexity bounds are asymptotically optimal.

Results extend understanding of interval temporal logic MC complexity.

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.