Appunti di Verifica e Validazione in AI: capitoli del corso, guide rapide, glossario, dimostrazioni e mappe per ripassare automi, logiche temporali, model checking, sintesi e planning.
Logica proposizionale, QBF, logica del primo ordine, tableaux, giochi di Ehrenfeucht-Fraisse e formule di Hintikka.
Open Notes →DFA, NFA, epsilon-mosse, espressioni regolari, proprieta di chiusura e teorema di Myhill-Nerode.
Open Notes →Algoritmo L* di Angluin, MAT, membership query, equivalence query e matrici di Hankel.
Open Notes →Modellazione di sistemi reattivi, Fair Transition System, Simple Programming Language, fairness debole e forte.
Open Notes →Omega-linguaggi, automi di Buchi, GNBA, automi di Muller, chiusure e decidibilita.
Open Notes →S1S, WS1S, secondo teorema di Buchi, automi su alberi e connessione tra logica e automi.
Open Notes →LTL, CTL, CTL*, semantiche sui cammini e incomparabilita espressiva.
Open Notes →Tableau LTL, behavior graph, P-SAT, P-VALID, model checking CTL e punti fissi.
Open Notes →State explosion, partial-order reduction, OBDD, symbolic model checking e bounded model checking con SAT.
Open Notes →Church's problem, giochi di Muller e parita, Buchi-Landweber, LAR e strategie di Mealy.
Open Notes →Weak, strong e strong-cyclic planning tramite model checking simbolico, preimmagini e linguaggio AR.
Open Notes →Mappa sintetica degli argomenti principali, con collegamenti ai capitoli e risposte brevi per orientare il ripasso.
Open Notes →Definizioni corte da usare come lingua comune nelle lezioni e nelle risposte orali.
Open Notes →Definizioni, prove essenziali, usi e criteri di scelta per confrontare le famiglie di automi del corso.
Open Notes →Dimostrazioni complete delle chiusure presenti negli appunti, organizzate come riferimento di studio.
Open Notes →Versioni estese dei passaggi dimostrativi degli appunti, pensate come supporto per studio e ripasso.
Open Notes →