Section outline
-
Fissato un modello formale di un sistema, reale o da realizzare, vogliamo stabilire se il modello soddisfa certi requisiti. Le tecniche di model-checking si basano sull'impiego di logiche modali e temporali per esprimere le proprietà che vogliamo studiare, e su algoritmi che decidono se il modello del sistema in esame le soddisfa o no. Studiamo alcuni linguaggi logici e i relativi algoritmi di decisione.
-
Raccomando di leggere questo breve articolo introduttivo, sorvolando in prima lettura sui dettagli dell'esempio nella sezione 3, e tenendo conto che nella descrizione degli operatori di logica temporale ci sono alcuni errori (nel corso delle lezioni e negli appunti pubblicati sul sito verranno date le definizioni formali precise).
-
Riferimenti a materiale di consultazione
-
Da leggere: paragrafo 1 (Introduction), introduzione alla sezione 3 (Systems and Properties), sezione 3.1 (Transition Systems), sezione 3.2 (Properties and Temporal Logic).
-
Glynn Winskel
Per i teoremi di punto fisso, si veda la sezione 1.5.
-
Clarke, Emerson, Sifakis
Turing Lecture
-
-
-
Attenzione: il contenuto è provvisorio; ci sono ripetizioni e contenuti in ordine diverso rispetto alla lezione. I file saranno aggiornati il prima possibile.
-
-
-
di HA Priestley, tratto da R. Backhouse et al. (Eds.): Algebraic and Coalgebraic Methods . . . , LNCS 2297, pp. 21–78, 2002. Springer-Verlag.
-
-
Kaltura Video Resource
15:30-17:30, aula U4-02
Il livello della registrazione audio è molto basso; provate a regolare al massimo il volume di uscita.
-
Kaltura Video Resource
15:30-17:30, aula U4-02
Il livello della registrazione audio è molto basso; provate a regolare al massimo il volume di uscita.
-