Docente

• Prof. Angelo Montanari

Indirizzo e-mail
angelo.montanari@uniud.it

Crediti

9 CFU

Finalità

Il corso vuole presentare in modo sistematico metodi, formalismi e algoritmi proposti in ambito informatico per la specifica formale e la verifica automatica di sistemi reattivi complessi. Ampio spazio verrà dedicato alla teoria degli automi operanti su oggetti infiniti (parole e alberi) e alle logiche temporali (LTL, CTL, CTL*, mu-calculus). Particolare attenzione verrà riservata ai risultati relativi all'equivalenza espressiva tra classi di automi e sistemi logici. Verrà, inoltre, illustrato il possibile utilizzo della teoria logica dei giochi nella verifica formale. Dal punto di vista algoritmico, con riferimento ai modelli computazionali e ai formalismi di specifica presi in considerazione, verranno studiati in dettaglio gli algoritmi per la verifica della consistenza delle specifiche e della correttezza dei modelli. Un ruolo centrale verrà assegnato agli algoritmi di model checking, che consentono di validare il comportamento di un sistema hardware o software, descritto formalmente attraverso un modello matematico appropriato (ad esempio, un automa), rispetto alle proprietà attese del sistema, specificate mediante formule logiche (ad esempio, formule di CTL). In particolare, verranno presentate le soluzioni proposte per migliorare le prestazioni degli algoritmi di model checking (model checking simbolico, OBDD, partial order reduction). Verranno, inoltre, presi in esame alcuni esempi significativi di model checker. Nell'ultima parte del corso verranno introdotti alcuni temi di carattere più avanzato, quali, ad esempio, lo studio dei sistemi aperti e la verifica di sistemi a stati infiniti.

Programma

Parte 1 - Introduzione ai sistemi reattivi.
Sistemi reattivi e real-time; sistemi di transizione equi; un semplice linguaggio di programmazione (SPL): sintassi e semantica, moduli; specifiche logiche e loro proprietà; l’uso della logica temporale per la specifica, la verifica e la validazione di programmi.

Parte 2 - Automi su oggetti infiniti
Automi su parole infinite: notazione, automi di Büchi, congruenze e complementazione, il calcolo sequenziale, determinismo e teorema di McNaughton; automi di Rabin e di Muller, elementi di teoria dei giochi; il teorema di McNaughton e Papert; omega-linguaggi star-free e logica temporale. Automi su alberi infiniti: notazione, automi su alberi, automi su alberi finiti, automi non deterministici di Büchi e di Rabin su alberi infiniti e loro relazioni, problema del vuoto e alberi regolari, complementazione e determinatezza dei giochi, teoria monadica degli alberi e risultati di decidibilità.

Parte 3 - Logiche modali e temporali
Introduzione, classificazione delle logiche temporali, le logiche temporali lineari, le logiche temporali ramificate, LTL, CTL, CTL* e mu-calculus, un ambiente per la modellazione della concorrenza: modelli astratti e concreti di concorrenza, concorrenza e logica temporale, espressività, decidibilità e complessità delle logiche temporali, algoritmi di satisfiability checking e di model checking.

Parte 4 - Verifica e validazione di sistemi reattivi
Algoritmi di satisfiability checking e di model checking per la verifica di programmi a stati finiti: soddisfacibilità e validità di una formula temporale, soddisfacibilità e validità di una formula temporale rispetto ad un programma a stati finiti, esempi, il problema della verifica di sistemi a stati infiniti (cenni).

Parte 5 – Model checking
Introduzione al model checking, model checking per LTL e CTL, massimi e minimi punti fissi di operatori monotoni, teorema di Tarski sulle approssimazioni, diagrammi di decisione binari ordinati (OBDD), model checking simbolico, automi alternanti e model checking, tecniche di partial order reduction, model checking per il mu-calculus (giochi di parità), esempi significativi di model checker.

Bibliografia

A. Montanari, Linguaggi formali, automi e logiche, Note al Corso, 2011.
Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer, 1992.
W. Thomas. Automata on Infinite Objects, in Handbook of Theoretical Computer Science - Vol. B (capitolo 4), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.
W. Thomas. Languages, Automata, and Logic, in Handbook of Formal Languages, Vol. III, G. Rozenberg and A. Salomaa (eds.), Springer, pp. 389-455, 1997.
D. Perrin, J.-E. Pin, Infinite Words. Automata, Semigroups, and Games, Pure and Applied Mathematics Vol. 141, Elsevier, 2004.
E. A. Emerson. Temporal and Modal Logic, in Handbook of Theoretical Computer Science Vol. B (capitolo 16), J. van Leeuwen (ed.), Elsevier Science Publisher, 1990.
Z. Manna, A. Pnueli. Temporal verification of Reactive Systems: Safety, Springer, 1995.
E. M. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, 2000.

Modalità d'esame

Homework e approfondimento