Résumé | 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 modelled 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). The most well-known interval temporal logic is Halpern and Shoham's modal logic of time intervals HS, which features one modality for each possible ordering relation between a pair of intervals, apart from equality. In the seminar, we provide an overview of the main results on model checking with HS and its fragments under the homogeneity assumption. In particular, we show that the problem turns out to be non-elementarily decidable and EXPSPACE-hard for full HS, but it is often computationally much better for its fragments. Then, we briefly compare the expressiveness of HS in model checking with that of LTL, CTL, CTL*. We conclude by discussing a recent generalization of the proposed MC framework that allows one to use regular expressions to define the behavior of proposition letters over intervals in terms of the component states. |