Constraining Cycle Alternations in Model Checking for Interval Temporal Logic

Model checking is one of the most successful techniques in system verification. While a variety of methods and tools exist to check properties expressed in point-based temporal logics, like LTL and CTL, model checking for interval temporal logic has entered the research agenda only very recently. In previous work, we devised a non-elementary model checking procedure for Halpern and Shoham's modal logic of time intervals, interpreted over finite Kripke structures, and an EXPSPACE algorithm for two meaningful fragments of it. In this paper, we show that the latter algorithm can be suitably tailored in order to check a subset of the computations of a system, that satisfy a given bound on the number of cycle alternations, by making use of a polynomial (instead of exponential) working space. We also prove that such a revised algorithm turns out to be complete for Kripke structures whose strongly connected components are simple cycles.