MVS - 08 - Model Checking Esplicito
Lecture Info
Date:
1 Reachability Analysis
Una volta che abbiamo ristretto la CTL, arriviamo al cuore del model checking. Il model checking infatti si basa sull'utilizzo di un certo algoritmo per verificare una proprietà su un dato sistema. In particolare noi andremo a studiare il model checking esplicito, caratterizzato dal fatto che l'algoritmo che effettua la verifica controlla la formula \(\phi\) su tutti gli stati raggiungibili dall'automa.
Esplicito = considero "uno per uno" tutti gli stati raggiungibili dallo stato iniziale.
Il cuore del model checking esplicito è dunque la reachability analysis, che esplora tutti i possibili cammini di esecuzione e che dunque enumera tutti gli stati raggiungibili. Il risultato della reachability analysis è una rappresentazione in memoria RAM (che è direttamente indirizzabile) di tutti gli stati e della funzione di transizione dell'automa. La funzione di transizione deve essere percorribile in avanti e in indietro. Nasce dunque un problema di come strutturiamo i dati.
Tralasciamo, per adesso, la rappresentazione degli stati in RAM. In generale per ogni stato devo avere la lista dei successori e dei predecessori.
\[\begin{array}{c | c | c} \textbf{S} & \text{successori} & \text{predecessori} \end{array}\]
Nell'esempio della cabina lo stato era una quintupla:
\[\begin{array}{c | c | c | c | c} \text{cabina} & p_0 & p_1 & p_2 & \text{controller} \end{array}\]
Dalle caratteristiche dei valori valori dello stato, devo essere in grado di calcolare l'indirizzo in cui è stato memorizzato lo stato. In questo modo durante la reachability analysis siamo in grado di verificare se abbiamo già incontrato uno stato. Come conseguenza di ciò notiamo che il costo di stress della RAM è molto elevato.
2 Model Checking Algorithm
L'algoritmo di model checking è una procedura di marking che va avanti e indietro nel grafo costruito dalla reachability analysis e si basa su un approccio analogo a quello della programmazione dinamica.
Consideriamo la formula
\[E F (P \lor Q)\]
La verifica consiste nel decorare una copia del grafo di transizione dell'automa, in cui ad ogni stato associo una zona di memoria in cui descrivo se ogni sottoformula \(\psi\) della formula di partenza \(\phi\) è vera o falsa in quel particolare stato.
Andiamo adesso a discutere come funziona l'algoritmo di verifica per le varie formule della CTL:
2.1 Case 1: \(\phi = P\)
Nel primo caso dobbiamo soddisfare la proposizione atomica \(P\)
for all q in Q do
if P in l(q)
do.phi = true
else
do.phi = false
done
2.2 Case 2: \(\phi = \neg \psi\)
do marking(psi);
for all q in Q: do
q.phi := not(q.psi)
done
2.3 Case 3: \(\phi = \psi_1 \land \psi_2\)
do marking(psi_1);
do marking(psi_2);
for all q in Q do
q.phi := and(q.psi_1, q.psi_2)
done
2.4 Case 4: \(\phi = EX \psi\)
do marking(psi)
for all q in Q do
q.phi := false;
done
for all (q, q') in T do
if q'.psi = true
q.phi := true
done
2.5 Case 5: \(\phi = EF \psi\)
Consideriamo la formula \(EF \psi\) e supponiamo di aver markato il grafo di transizione rispetto alla sotto-formula \(\psi\). Per valutare la verità di questa formula devo partire da uno stato con \(\psi\) vero e poi tornare indietro utilizzando la funzione di transizione inversa. In ciascun stato raggiungibile in questo modo la formula sarà vera. Ad un certo punto mi fermo, in quanto non riuscirò a raggiungere nessun stato nuovo all'insieme degli stati raggiunti tornando indietro.
L'algoritmo per gestire la formula \(EF \psi\) è così decritto
do marking(psi)
X, Y := empty
// initalization
for all q in Q:
q.phi := false
if q.psi = true:
X = X U {q}
while X != Y do:
Y := X
for all q in X:
segna q come visitato
for all q' in Q:
if ((q', q) in T and q' not visited):
X := X U {q'}
end
end
done
for x in X do:
x.phi = true
done
2.6 Case 6: \(\phi = E \psi_1 U \psi_2\)
do marking(psi_1)
do marking(psi_2)
for all q in Q do
q.phi := false
done
L := {};
for all q in Q do
if q.psi_2 = true
L := L + {q}
done
while L nonempty {
draw q from L;
L := L - { q };
q.phi := true
for all (q', q) in T {
if q'.seenbefore = false then do {
q'.seenbefore = true;
if q'.psi_1 = true then
L := L + { q' };
}
}
}
2.7 Case 7: \(\phi = A \psi_1 U \psi_2\)
do marking (psi_1);
do marking (psi_2);
L := {}
for all q in Q do
q.nb := degree(q);
q.phi := false;
done
for all q in Q do
if q.psi2 = true
L := L + { q };
done
while L nonempty {
draw q from L;
L := L - { q };
q.phi := true;
for all (q', q) in T {
q'.nb := q'.nb - 1;
if (q'.nb = 0) and (q'.psi1 = true) and (q'.phi = false)
L := L + { q' };
}
}