ESERCIZI Model Checking
Esercizio 1
Si consideri l'algoritmo di model checking descritto in [LD].Una parte di tale algoritmo corrisponde al controllo della verita' o falsita'di sottoformule della forma EG(f) supponendo di sapere se f e' vera o falsa (ovviamente rispetto ai nodi del grafo).Tale controllo, per un dato nodo s, corrisponde a verificare che
esiste un cammino infinito in M' a partire da s se e solo se (cioe' <==>) esiste un cammino da s ad un elemento di un SCC massimale.
Il verso "se" (<==)e' abbastanza immediato.Dimostrare - con sufficiente precisione - il verso "solo se" (==>).
Esercizio 2
Esercizio XX
Possibile soluzione.