In the last years, model checking with interval temporal logics is emergingas a viable alternative to model checking with standard point-based temporallogics, such as LTL, CTL, CTL*, and the like. The behavior of the system ismodeled by means of (finite) Kripke structures, as usual. However, whiletemporal logics which are interpreted "point-wise" describe how the systemevolves state-by-state, and predicate properties of system states, those whichare interpreted "interval-wise" express properties of computation stretches,spanning a sequence of states. A proposition letter is assumed to hold over acomputation stretch (interval) if and only if it holds over each componentstate (homogeneity assumption). A natural question arises: is there anyadvantage in replacing points by intervals as the primary temporal entities, oris it just a matter of taste? In this paper, we study the expressiveness of Halpern and Shoham's intervaltemporal logic (HS) in model checking, in comparison with those of LTL, CTL,and CTL*. To this end, we consider three semantic variants of HS: thestate-based one, introduced by Montanari et al., that allows time to branchboth in the past and in the future, the computation-tree-based one, that allowstime to branch in the future only, and the trace-based variant, that disallowstime to branch. These variants are compared among themselves and to theaforementioned standard logics, getting a complete picture. In particular, weshow that HS with trace-based semantics is equivalent to LTL (but at leastexponentially more succinct), HS with computation-tree-based semantics isequivalent to finitary CTL*, and HS with state-based semantics is incomparablewith all of them (LTL, CTL, and CTL*).
展开▼
