Model checking is a successful technique widely usedin formal verification. Given a model of a system and aformula specifying a desired property of it, one can verifywhether the system satisfies the property by checking theformula against the model. Distinctive features of modelchecking are: (i) it is a fully automatic process, (ii) it exaustivelychecks all the possible behaviours of the system,and (iii) it produces a counterexample, in case the propertyis violated. Systems are usually modeled as (finite) Kripkestructures, that is, state-transition systems, and their propertiesare specified by formulas of point-based temporal logics,such as LTL, CTL, and the like. These logics allowone to express requirements on computation states and theirrelationships; however, they are not well suited to specifyconditions on computation stretches, which come into playwhen dealing with, for instance, actions with duration, accomplishments,and temporal aggregations. To overcomethe limitations of point-based logics, one can resort to intervaltemporal logics (ITLs), that assume time intervals,instead of time points, as their primitive entities. The mostwell-known ITL is Halpern and Shoham’s modal logic oftime intervals HS [4], which features one modality for eachpossible ordering relation between a pair of intervals, apartfrom equality. The satisfiability problem for HS has beenstudied in [4], and it turns out to be highly undecidable forall relevant (classes of) linear orders. The same holds formost fragments of it [2]; luckily, some meaningful exceptionsexist, including the logic of temporal neighbourhoodand the temporal logic of sub-intervals.
['Angelo Montanari']
Interval Temporal Logics Model Checking