[INdAM-GNCS] Logica e Automi per il Model-Checking Intervallare

La verifica automatica o semi-automatica delle proprieta di un sistema hardware o software è diventato un problema classico che spazia dalla formalizzazione (logica) delle proprietà, la rappresentazione del sistema che si vuole verificare, la scelta o il progetto di un algoritmo efficiente per la verifica, e lo studio delle caratteristiche del problema stesso (ad esempio, la sua complessita). I sistemi (reattivi), normalmente rappresentati come grafi di transizione, sono stati oggetto di numerosissime ricerche sul model-checking; questo si deve al fatto che proprietà di interesse possono essere rappresentate in logiche temporali come LTL, CTL, e CTL , e queste ultime si interpretano in maniera naturale su grafi di transizione (si vedano, tra gli altri, i lavori di Clarke, Emerson, Pnueli, e Sistla). Uno dei limiti piu rilevanti della formalizzazione classica del problema del model-checking, però, è proprio l'uso di logiche temporali basate su punti. Infatti, la formalizzazione del problema in termini di punti temporali rende difficile, quando non impossibile, esprimere proprieta che coinvolgono durata, raggiungimento di un obbiettivo, o aggregazione temporale. Tra le proposte recenti che mirano al superamento di questi limiti (intrinsechi) del problema del model-checking e della sua formalizzazione, una posizione di rilievo e certamente quella occupata dai lavori di Montanari, Murano, ed altri, basati essenzialmente sull'uso della logica temporale ad intervalli inizialmente proposta da Halpern e Shoham (e conosciuta come HS) e dalla ri-definizione della sua semantica per renderla compatibile con i sistemi reattivi.

In questo progetto ci proponiamo di affrontare il problema del model-checking di proprieta intervallari da due punti di vista diversi e tra loro complementari. Vogliamo, da un lato, proseguire l'approccio di Montanari nella direzione di esplorare sia frammenti della logica HS al fine di ottenere algoritmi di model-checking piu efficienti, sia semantiche diverse per HS stessa che permettano esprimere propriea diverse. Parallelamente però, ci proponiamo di definire il problema del model-checking di proprieta intervallari in una maniera distinta ed ortogonale basata non su gra di transizione ma su modelli astratti che rappresentano l'informazione contenuta in basi di dati temporali o storicizzate.

Contrariamente allo schema precedentemente descritto, una logica come HS con la sua semantica standard (intervallare) si adatta perfettamente a questa definizione, ed il problema si sposta dal lato della rappresentazione del modello. Scopo di questo progetto e anche un ragionato confronto tra questi due approcci che hanno in comune il linguaggio logico (HS) ma sposano semantiche diverse e risolvono problemi diversi: idealmente, si vorrebbe denire un approccio sucientemente generale del quale i due modelli sopra descritti diventassero casi particolari.

p.p1 {margin: 0.0px 0.0px 0.0px 0.0px; font: 12.0px Helvetica} span.s1 {font: 8.0px Helvetica}