Programma del corso dell'a.a. 2019/2020 e materiale di riferimento
Prerequisiti
Il corso presuppone la conoscenza dei concetti fondamentali
alla base della sintassi e semantica della
logica proposizionale (o booleana), quali è
possibile acquisire
dal Cap. 2 delle dispense MC14.
Argomenti del corso
- Logica dei predicati
([MC14])
Sintassi e semantica.
Proprietà della logica dei predicati.
Teorie del primo ordine.
- Deduzione automatica
([MC14])
Il metodo dei tableaux per la logica proposizionale.
Algoritmo di unificazione.
Il metodo di risoluzione.
Raffinamenti della risoluzione: risoluzione lineare, risoluzione
con clausole unitarie.
Risoluzione SLD e programmazione logica.
- Cenni sul linguaggio Prolog
(Qualunque testo di introduzione al Prolog, ad esempio
[Bra88],
[CM93],
[CLMM97],
[FL88].
Per chi è interessato, i
testi seguenti contengono materiale più avanzato sul
linguaggio Prolog:
[NM95],
[Sho94].)
Il compilatore utilizzato è SWI-Prolog
[SWI].
- Metodi formali per la verifica di sistemi
-
Model
checking con LTL (logica temporale lineare).
([Pel] capitoli 1-6,
[MC09],
[Kat: cap. 1 (escluso 1.4) e cap. 2]
Modellazione di un sistema (sistemi di transizioni).
Linguaggi di specifica formale: logica temporale lineare.
Tableaux per la logica temporale lineare.
Automi su parole infinite, automi di Büchi.
Traduzione di formule LTL in automi.
Verifica di proprietà di un sistema rappresentate da formule
LTL.
Il tool per la verifica formale di sistemi software
SPIN.
-
Modellazione e verifica di sistemi con
proprietà temporali
([Kat: cap. 3 (introduzione, 3.1, 3.2 e
3.5); cap. 4 (4.1, 4.2 e 4.9)],
[Tutorial1],
[Tutorial2.)
Automi temporizzati (Timed Automata, TA).
Linguaggi di
specifica formale: Computational Tree Logic (CTL).
Il tool di modellazione e verifica
UPPAAL. Consultare la
Guida al linguaggio.
- Automi temporizzati di gioco (Timed Game Automata) e
applicazioni
alla pianificazione automatica
([Tiga],
[Timelines],
[ECAI 2010],
[Time 2015],
[Plan2Tiga]).
- Timed Gamed Automata (TGA) e
UPPAAL
TIGA
- Introduzione alla pianificazione temporale basata su timeline
- Verifica e validazione di piani mediante l'uso di TGA
- Esecuzione e controllabilità dei
piani.
- Rappresentazione di un piano mediante reti di TGA e verifica
di controllabilità dinamica.
Materiale di riferimento
-
[MC14]
M. Cialdea Mayer.
Logica (dispense)
-
[Bra88]
I. Bratko.
Programmare in Prolog per l'Intelligenza Artificiale.
Masson - Addison Wesley, 1988.
-
[CM93]
W. F. Clocksin and C. S. Mellish.
Programmare in Prolog.
Franco Angeli, 1993.
(Il testo originale, in inglese, è disponibile
online)
-
[CLMM97]
L. Console, E. Lamma, P. Mello, M. Milano.
Programmazione Logica
e Prolog.
UTET Libreria, 1997.
-
[FL88]
F. Furlan e G.A. Lanzarone.
Prolog. Linguaggio e metodologia di programmazione logica.
Franco Angeli, 1988. Il libro è fuori stampa, ma si può
scaricare la
versione pdf.
-
[NM95]
U. Nilsson and J. Maluszynski.
Logic, Programming and Prolog.
John Wiley & Sons, 1995.
-
[Sho94]
Y. Shoham.
Artificial Intelligence techniques in Prolog.Morgan Kaufmann, 1994.
-
[SWI]
SWI-Prolog: un compilatore Prolog (Free Software).
Ambienti e strumenti di programmazione:
Program development tools
SWI prolog editor (segnalato da uno studente, non testato dal docente)
Per chi lavora in ambiente
emacs o
Xemacs:
Prolog mode per Emacs (per sistemi Linux Debian o Ubuntu,
istallare il pacchetto prolog-el)
-
[Pel]
D. A. Peled.
Software Reliability Methods.
Springer, 2001.
Gli argomenti dei
capitoli 5 e 6 di questo testo sono trattati anche nelle dispense
MC09.
Questo testo è utile soprattutto per l'introduzione ai metodi
formali e la modellazione di sistemi (capitoli 1 e 4). Si noti che i
capitoli 2 e 3 dello stesso testo riguardano concetti di base trattati
in altra parte del corso.
-
[Kat]
J.-P. Katoen.
Concepts, Algorithms and Tools for Model Checking (Lecture
Notes of the Course
"Mechanised Validation of Parallel Systems", Friedrich-Alexander
Universität Erlangen-Nürnberg).
-
[MC09]
M. Cialdea Mayer.
Logica temporale e verifica di proprietà dei programmi (dispense).
-
[Tutorial1]
Gerd Behrmann, Alexandre David, and Kim G. Larsen.
A Tutorial on Uppaal 4.0.
-
[Tutorial2]
F. Vaandrager.
A First Introduction to Uppaal.
-
[Tiga]
G. Behrmann et al.
UPPAAL Tiga User-manual.
-
[Timelines]
M. Cialdea Mayer, A. Orlandini, A. Umbrico.
Planning and execution with flexible timelines: a formal account.
Acta Informatica, 53 (6):649–680, 2016.
- [ECAI 2010]
A. Cesta, A. Finzi, S. Fratini, A. Orlandini, E. Tronci.
Analyzing Flexible Timeline-based Plans.
Proceedings of the 19th European Conference on Artificial
Intelligence (ECAI 2010), pp. 471-476. IOS Press.
- [Time 2015]
M. Cialdea Mayer, A. Orlandini.
An executable semantics of flexible plans in terms of
Timed Game Automata.
Proceedings of the 22nd International Symposium on Temporal
Representation and Reasoning (TIME 2015), pages 160-169, IEEE 2015.