Model Checking: il Metodo Intervallare

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.

I metodi formali sono metodologie strutturate che supportano lo sviluppo di sistemi critici allo scopo di dimostrare la loro correttezza con rigore matematico, fornendo tecniche e strumenti di verifica efficaci, e riducendo il tempo del processo di verifica, aumentando contemporaneamente il grado di copertura. Il model checking (MC) è una famiglia di metodi formali che sono stati accettati dal mondo dell’industria e stanno diventando parte integrante di standard. Nel MC, alcune proprietà di un sistema di transizione vengono espresse mediante linguaggi di specifica e, successivamente, queste sono verificate su un modello del sistema stesso (di solito una struttura di Kripke), tramite l’enumerazione completa degli stati raggiungibili. Tale tecnica è automatica ed ogni volta che è violata una proprietà desiderata, viene fornito un controesempio che illustra un comportamento che falsifica la proprietà: ciò è utile per il debugging. Le più famose tecniche di MC furono sviluppate negli anni 80 considerando le famose logiche temporali LTL e CTL, che sono basate su punti. Tuttavia, esistono alcune proprietà che potremmo voler verificare che hanno inerentemente una semantica intervallare e quindi non possono essere espresse da logiche puntuali, per esempio: “la proposizione p deve valere in almeno un dato numero medio di stati del sistema, in un settore di computazione specifico”. Le logiche temporali intervallari entrano in gioco in questi casi, permettendoci di ragionare su aspetti temporali in modo diverso: esse adottano gli intervalli, invece dei punti, come loro entità primitive. Questa caratteristica dà loro l’abilità di esprimere proprietà intervallari, come azioni con durata e aggregazioni temporali, che non possono essere trattate nelle logiche puntuali. La logica modale degli intervalli temporali di Halpern e Shoham (HS) è una delle più famose logiche intervallari: essa ha una modalità per ognuna delle 13 relazioni di ordinamento fra coppie di intervalli, eccetto l’uguaglianza. In questa tesi viene considerato il problema del MC basato su HS, come linguaggio di specifica delle proprietà, il quale ha ricevuto poca attenzione in letteratura. L’idea è quella di valutare formule di HS su strutture di Kripke finite, per riuscire a verificare la correttezza di un sistema rispetto a proprietà intervallari. A questo scopo, ognuno dei percorsi finiti di una struttura di Kripke (i quali possono essere presenti in quantità infinita) è interpretato come un intervallo, e le proprietà atomiche che valgono su quest’ultimo sono definite sulla base di quelle degli stati che lo costituiscono, inizialmente secondo il principio di omogeneità: esso prevede che una proprietà atomica valga su un intervallo se e solo se vale su tutti i suoi sottointervalli. Dimostriamo che il MC per HS su strutture di Kripke finite è decidibile (la sua complessità ha un upper bound non-elementare); poi mostriamo che è EXPSPACE-hard. Poiché il problema non ammette procedure di decisione polinomiali, consideriamo anche frammenti di HS, i quali hanno complessità migliori—da EXPSPACE, giù fino a livelli bassi della gerarchia polinomiale—pur tuttavia mantenendo l’abilità di esprimere proprietà intervallari significative. Presentiamo svariati algoritmi di MC, costruiti ad-hoc per gli specifici frammenti considerati, e fondati su concetti e tecniche diversi fra loro. Studiamo poi il potere espressivo di HS in confronto a quello delle logiche puntuali LTL, CTL e CTL∗, sempre sotto l’ipotesi di omogeneità, la quale viene poi rilassata mostrando quali sono le implicazioni sul MC per HS ed i suoi frammenti, e sull’espressività della logica stessa. Infine, consideriamo una possibile alternativa alle strutture di Kripke: studiamo un modello di sistemi più espressivo, che ci permette di descrivere gli stessi in termini delle loro proprietà intervallari. Ciò apre la strada a un MC intervallare più generale.