Teacher: Francesco Spegni

Content: Il test dei modelli si è affermato come una tecnica di ragionamento logico ampiamente applicabile a tutti i tipi di sistemi: protocolli informatici, reti biologiche, sistemi complessi, ecc. Modellando il problema in questione come un sistema dinamico, riconoscendone gli stati e le transizioni, è possibile studiarne l’evoluzione nel tempo. Nel controllo probabilistico del modello, ogni partecipante viene modellato utilizzando una catena di Markov o un processo decisionale di Markov, le cui transizioni sono etichettate con probabilità che valutano la probabilità di un singolo passaggio locale. Esplorando tutti i percorsi del sistema, è possibile studiare la probabilità che vengano raggiunti stati desiderabili/indesiderabili complessi o che vengano attraversate sequenze di stati.

Dopo aver introdotto le basi teoriche del Probabilistic Model Checking, il corso mostra come descrivere un sistema utilizzando il linguaggio PRISM e mostra come applicare il model checker PRISM per valutare la probabilità di un attacco informatico o l’influenza dei parametri del modello sulle proprietà emergenti di sistemi complessi (es. sincronizzazione di oscillatori accoppiati a impulsi).