Which Fragments of the Interval Temporal Logic HS are Tractable in Model Checking

Since the 80s, model checking (MC) has been applied to the automatic verification of hardware/software systems. Point-based temporal logics, such as LTL, CTL, CTL⁎, and the like, are commonly used in MC as the specification language; however, there are some inherently interval-based properties of computations, e.g., temporal aggregations and durations, that cannot be properly dealt with by these logics, as they model a state-by-state evolution of systems.