Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTLa, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted “point-wise” describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted “interval-wise” express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this article, we study the expressiveness of Halpern and Shoham’s interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTLa. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al. in l30, 34r, that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTLa, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTLa).