FORMAL METHODS FOR AI-BASED SYSTEMS ENGINEERING

Obiettivi formativi

Obiettivi generali: L'insegnamento è indirizzato all'acquisizione delle conoscenze logiche e di modellazione necessarie alla ingegneria dei sistemi basata su intelligenza artificiale. Obiettivi specifici: L'insegnamento consentirà agli studenti di padroneggiare un portafoglio rappresentativo di metodi formali per l'ingegneria dei sistemi basata su intelligenza artificiale, tra cui approcci alla verifica formale e di ottimizzazione del design di sistemi complessi. Conoscenza e comprensione: Alla fine del corso gli studenti avranno piena comprensione degli strumenti di modellazione e delle tecnologie proposti. Capacità di applicare conoscenza e comprensione: Gli studenti saranno in grado di utilizzare gli strumenti presentati durante il corso e di approfondirne lo studio consultando autonomamente altri testi dedicati all'argomento, inclusa la letteratura scientifica dell'area. Capacità critiche e di giudizio: Le conoscenze acquisite permetteranno agli studenti di affrontare al meglio le attività di ingegneria dei sistemi durante la loro carriera lavorativa. Capacità di comunicazione: Gli studenti verranno stimolati ad esporre ed a comunicare le proprie esperienze con i loro colleghi e con i docenti. Capacità di proseguire lo studio: Il corso tratterà soltanto alcune delle metodologie e tecnologie disponibili, ma renderà edotti gli studenti dell'ampio spettro di approcci disponibili all’ingegneria dei sistemi basata su intelligenza artificiale. Questo permetterà agli studenti di poter scegliere criticamente le metodologie e le tecnologie più opportune per ogni nuovo problema.

Canale 1
TONI MANCINI Scheda docente

Programmi - Frequenza - Esami

Programma
Strutture di Kripke, logiche temporali, il problema del model checking, complessità. Automi di Buchi, on-the-fly computation, riduzione dello spazio di ricerca, mu-calcolo, OBDD, automi ibridi. Ragionamento composizionale, model checking per il software, model checking probabilistico. Intelligenza artificiale nell'ingegneria dei sistemi, ragionatori e model checker stato dell'arte, casi di studio.
Prerequisiti
Si richiede buona conoscenza di: 1) Programmazione imperativa ed object-oriented in un qualunque linguaggio di programmazione di alto livello 2) Tecniche per il progetto di algoritmi e strutture dati 3) Matematica generale, algebra, teoria degli insiemi, calcolo delle probabilità 4) Logica proposizionale e del primo ordine 5) Progetto di basi di dati relazionali 6) Automi, calcolabilità e complessità 7) Conoscenza generale di intelligenza artificiale (anche a livello introduttivo)
Testi di riferimento
Materiale didattico reso disponibile dal docente.
Modalità insegnamento
Il modulo consiste in lezioni ed esercitazioni nelle quali verranno affrontati tutti gli argomenti in programma.
Frequenza
La frequenza delle lezioni e delle esercitazioni, sebbene non obbligatoria, è fortemente consigliata.
Modalità di esame
L'esame consiste in una prova scritta ed un progetto da svolgere sotto forma di relazione scritta e software, e da presentare in seminari multipli. La prova scritta consiste in domande ed esercizi sulle diverse parti del programma d'esame. Il progetto consiste nell'approfondimento di uno o più argomenti non visti nel corso e/o nella progettazione e sviluppo di software che permetta l'uso di metodi formali nell'ingegneria dei sistemi basata su intelligenza artificiale. Per superare con successo l'esame è necessario che il punteggio di ogni singola prova sia almeno pari a 'sufficiente'.
Bibliografia
Libro di testo consigliato: Edmund M. Clarke, Jr., Orna Grumberg, Daniel Kroening, Doron Peled and Helmut Veith. Model Checking, Second Edition. MIT Press, 2018 ISBN: 9780262038836 Altri testi suggeriti: Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (eds). Handbook of Model Checking. Springer, 2018 ISBN: 9783319105758 Christel Baier, Joost-Pieter Katoen Principles of Model Checking MIT Press, 2008. ISBN: 9780262026499
Modalità di erogazione
Il modulo consiste in lezioni ed esercitazioni nelle quali verranno affrontati tutti gli argomenti in programma.
PAOLO ZULIANI Scheda docente

Programmi - Frequenza - Esami

Programma
Sistemi dinamici discreti: modellazione e logiche temporali. Verifica di sistemi discreti via model checking. Model checking probabilistico e statistico. Sistemi ibridi (continui/discreti): modellazione e tecniche di model checking SMT.
Prerequisiti
Si richiede buona conoscenza di: 1) Programmazione imperativa ed object-oriented in un qualunque linguaggio di programmazione di alto livello 2) Tecniche per il progetto di algoritmi e strutture dati 3) Matematica generale, algebra, teoria degli insiemi, calcolo delle probabilità 4) Logica proposizionale e del primo ordine 5) Progetto di basi di dati relazionali 6) Automi, calcolabilità e complessità 7) Conoscenza generale di intelligenza artificiale (anche a livello introduttivo)
Testi di riferimento
Model Checking. E.M.Clarke, O.Grumberg, D. Kroening, D. Peled, & H. Veith. MIT Press, 2018. Principles of Model Checking. C. Baier & J.-P. Katoen. MIT Press, 2018.
Frequenza
Consigliata.
Modalità di esame
L'esame del modulo consiste in una prova scritta ed un progetto da svolgere e presentare mediante una relazione scritta ed un seminario. La prova scritta consiste in domande ed esercizi sulle diverse parti del programma d'esame. Il progetto consiste nell'approfondimento di uno o più argomenti non visti nel corso e/o nella progettazione e sviluppo di software che permetta l'uso di metodi formali nell'ingegneria dei sistemi basata su intelligenza artificiale. Per superare con successo l'esame è necessario che il punteggio di ogni singola prova sia almeno pari a 'sufficiente'.
Modalità di erogazione
Lezioni teoriche ed esercizi con software per ricerca.
  • Codice insegnamento10607006
  • Anno accademico2025/2026
  • CorsoComputer Science - Informatica
  • CurriculumCurriculum unico
  • Anno1º anno
  • Semestre2º semestre
  • SSDINF/01
  • CFU6