Title: Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison,
Abstract: In the last 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, CTL*, 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 paper, we study the expressiveness of Halpern and Shoham's interval
temporal logic (HS) in model checking, in comparison with those of LTL, CTL,
and CTL*. To this end, we consider three semantic variants of HS: the
state-based one, introduced by Montanari et al., 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 CTL*, and HS with state-based semantics is incomparable
with all of them (LTL, CTL, and CTL*).