Complexity analysis of a unifying algorithm for model checking interval temporal logic

Abstract The model checking (MC) problem for Halpern and Shoham's interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable. An intriguing open question is the exact complexity of the problem for full HS : it is at least EXPSPACE-hard, and the only known upper bound, which has been obtained by exploiting an abstract representation of Kripke structure paths, called descriptor, is non-elementary. In this paper, we generalize the approach by providing a uniform framework for model checking full HS and meaningful fragments of it, where a specific type of descriptor is defined for each fragment. Then, we devise a general MC alternating algorithm, parameterized by the type of descriptor, which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze the complexity of the algorithm and give, by means of non-trivial arguments, tight bounds on the length of certificates. For two types of descriptor, we obtain exponential upper and lower bounds, which lead to an elementary MC algorithm for the corresponding HS fragments. For the other types of descriptor, we provide non-elementary lower bounds. This last result negatively answers an open question about the possibility of giving an elementary upper bound on the size of the descriptors for full HS .