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

摘要: Abstract Model checking (MC) for Halpern and Shoham's interval temporal logic HS has been recently shown to be decidable. An intriguing open question is its exact complexity full : it at least EXPSPACE-hard, the only known upper bound, which exploits an abstract representation of Kripke structure paths (descriptor), non-elementary. In this paper, we provide a uniform framework MC meaningful fragments it, with specific type descriptor each fragment. Then, devise general alternating algorithm, parameterized by descriptor's type, polynomially bounded number alternations whose running time length minimal representatives descriptors (certificates). We analyze give tight bounds on certificates. For two types descriptor, obtain exponential lower bounds; other ones, non-elementary bounds.