Model Checking: the Interval Way

Formal methods are structured methodologies that support the development of critical systems, with the aim of establishing system correctness with mathematical rigor, providing effective verification techniques and tools, and reducing verification time while simultaneously increasing coverage. Model checking (MC) is a family of formal methods that have been accepted by industry and are becoming integral part of standards. In MC, some properties of a transition system are expressed in suitable specification languages and then verified over a model of the system itself (usually a Kripke structure) through exhaustive enumeration of the reachable states. This technique is fully automatic and every time the design violates a desired property, a counterexample is produced, which illustrates a behavior falsifying such a property: this is extremely useful for debugging. The most famous MC techniques were developed from the late 80s, bearing in mind the well-known “point-based” temporal logics LTL and CTL. However, while the expressiveness of such logics is beyond doubt, there are some properties we may want to check that are inherently “interval-based” and thus cannot be expressed by point-based temporal logics, e.g., “the proposition p has to hold in at least an average number of system states in a given computation sector”. Here interval temporal logics (ITLs) come into play, providing an alternative setting for reasoning about time. Such logics deal with intervals, instead of points, as their primitive entities: this feature gives them the ability of expressing temporal properties, such as actions with duration, accomplishments, and temporal aggregations, which cannot be dealt with in standard point-based logics. The Halpern and Shoham’s modal logic of time intervals (HS, for short) is one of the most famous ITLs: it features one modality for each of the 13 possible ordering relations between pairs of intervals, apart from equality. In this thesis we focus our attention on MC based on HS, in the role of property specification language, for which a little work has been done if compared to MC for point-based temporal logics. The idea is to evaluate HS formulas on finite Kripke structures, making it possible to check the correctness of the behavior of systems with respect to meaningful interval properties. To this end, we interpret each one of the (possibly infinitely many) finite paths of a Kripke structure as an interval, and we define its atomic properties on the basis of the properties of the states composing it, at first assuming the homogeneity principle: the latter enforces an atomic property to hold over an interval if and only if it holds over all its subintervals. We prove that MC for HS interpreted over finite Kripke structures is a decidable problem (whose computational complexity has a nonelementary upper bound), and then we show it to be EXPSPACE-hard. Since the problem provably admits no polynomial-time decision procedure, we also focus on HS fragments, which feature considerably better complexities—from EXPSPACE, down to low levels of the polynomial hierarchy—yet retaining the ability to capture meaningful interval properties of state transition systems. Several MC algorithms are presented, tailored to the specific fragments being considered, and founded on concepts and techniques different from each other. Moreover, we study the expressive power of HS in MC, in comparison with that of the standard point-based logics LTL, CTL and CTL∗, still under the homogeneity principle, which is then relaxed showing how this impacts on the complexity of MC for HS and its fragments, and on the expressiveness of the logic. Finally, we consider a possible replacement of Kripke structures by a more expressive model, which allows us to directly describe systems in terms of their interval-based behavior and properties, thus paving the way for a more general interval-based MC.