Approcci al model-checking:
automata theoretic approach,
symbolic model checking
Contenuto della lezione
LTL model-checking: automata-theoretic
approach
Symbolic model-checking
LTL model-checking (LMC)
AP: proposizioni atomiche
K: struttura di Kripke su AP
ϕ: formula LTL su AP
Def. K è un modello di ϕ se ϕ è soddisfatta su ogni traccia di K
Model-checking: K è un modello della formula ϕ?
K è un modello di ϕ
se e solo se L(K) ⊆ L(ϕ)
se e solo se L(K) ∩ L(ϕ) = ∅
se e solo se L(K) ∩ L(¬ ϕ) = ∅
Se costruiamo un automa di Büchi che accetta tutte le ωparole su AP che soddisfano ϕ abbiamo soluzione a LTL
model-checking (automata-theoretic approach)
si sfrutta chiusura rispetto all'intersezione e decidibilità del
vuoto degli automi di Büchi
Automata-theoretic approach
Proviamo i seguenti risultati:
Teorema 1. La classe degli automi di Büchi è chiusa
rispetto all'intersezione. L'automa che accetta il linguaggio
intersezione si può effettivamente costruire e ha taglia
proporzionale al prodotto della taglia degli automi di
partenza.
Teorema 2. Il problema del vuoto per gli automi di Büchi è
decidibile in tempo lineare nella taglia dell'automa.
Teorema 3. Data una formula LTL è possibile costruire un
automa di Büchi che accetta esattamente tutti i suoi modelli.
Chiusura rispetto a intersezione
Automi di Büchi: Ai = (Σ, Qi, Q_ini, δi, Q_fini), i=1,2
Sia A = (Σ, Q, Q_in, δ ,Q_fin) dove:
Q = Q1 x Q2 x {0,1,2}, Q_in = Q_in1 x Q_in2 x {1}
Q_fin = Q1 x Q2 x {0}
δ contiene regole del tipo (q1, q2, i ) –a
(q1’, q2’, i') t.c.:
q1 –a q1’ ∈ δ1 , q2 –a q2' ∈δ2 e
i' = i +1 mod 3 se i = 0 oppure qi ∈ Q_fin
i' = i, altrimenti
A simula ogni Ai nella componente i del suo stato
la terza componente diventa infinite volte 0 sse gli stati finali di
entrambi A1 e A2 vengono visitati infinite volte
se ad es. l'automa Aj da un certo punto non visita più uno
stato finale, allora la terza componente rimane bloccata su i
Decidere il vuoto per gli automi di Büchi
Algoritmo 1 ---componenti fortemente connesse:
computa componenti fortemente connesse del grafo di
transizione ---tempo O(|Q|+|δ|)
denota come finali le componenti che contengono uno stato
finale ---contestualmente a step precedente
risolvi raggiungibilità con insieme target gli stati delle
componenti fortemente connesse finali ---tempo O(|Q|+|δ|)
output risultato raggiungibilità
Si può verificare che Algoritmo 1 da una risposta affermativa
sse l'automa di Büchi in input accetta un linguaggio non vuoto
Nested depth-first search
Idea: eseguire due DFS interfogliate
una esterna per visitare tutti gli stati finali raggiungibili
una interna per individuare cicli su stati finali
Algoritmo 2 ---nested DFS:
non appena terminata la visita DFS esterna da tutti i
successori di s, se s è finale parte la DFS interna da s
nella DFS interna, vengono esplorati tutti gli stati
raggiungibili da s non ancora visitati nella DFS interna
(la DFS interna è fatta a pezzi, e si interfoglia con quella
esterna)
nessun ciclo su s? continua la DFS esterna
Nested depth-first search
Generazione del controesempio: concatena gli stack DFS
stack U usato per la DFS esterna = cammino da s0 ∈ I a s
(dal bottom al top)
stack V usato per la DFS interna = ciclo da s a s (dal bottom
al top)
Tempo di esecuzione O(|Q|+|δ|)
Si può verificare che Algoritmo 2 dà una risposta affermativa
sse l'automa di Büchi in input accetta un linguaggio non vuoto
Inoltre, in caso di risposta affermativa viene generato un
cammino da uno stato iniziale a uno stato di accettazione
seguito da un ciclo su questo stato
se automa di Büchi esprime negazione specifica, output è
controesempio
Pseudo-codice nested DFS
set of states R := ∅; //stati visitati DFS est.
stack of states U := ε;
// stack DFS est.
set of states T := ∅; //stati visitati DFS int.
stack of states V := ε;
//stack DFS int.
boolean cycle_found := false;
while (Q_in \ R != ∅ ∧ !cycle_found) do
let s ∈ Q_in\ R; // explore reachable cycles
reachable_cycle(s); // outer DFS
od
if !cycle_found then return (”yes”)
else return (”no”, reverse(V.U))
fi
procedure reachable_cycle (state s)
push(s,U); R := R ∪ {s };
repeat
s := top(U);
if Post(s) \ R != ∅ then
let s ∈ Post(s) \ R;
push(s, U);
R := R ∪ {s };
else
pop(U); // DFS est. finita per s
if s è finale then
cycle_found := cycle_check(s); fi
fi
until ((U = ε) ∨ cycle_found)
endproc
Pseudo-codice nested DFS: cycle_check
if Post(s') \ T ! = ∅ then
/* esegue DFS interna */
procedure boolean cycle_check(state s)
boolean cycle_found := false;
push(s, V );
// V è uno stack
T := T ∪ {s };
repeat
s' := top(V );
if s ∈ Post(s') then
cycle_found := true;
push(s, V );
else
// stati già visitati in DFS interna
// non vengono rivisitati
let s'' ∈ Post(s') \ T ;
push(s'', V );
T := T ∪ {s'' };
else
pop(V );
fi
fi
until ((V = ε) ∨ cycle_found)
return cycle_found
endproc
Correttezza nested DFS
Supponiamo che un ciclo su stato finale s non viene scoperto
Stati visitati nella DFS interna non sono rivisitati
possibile errore: non rivisitiamo stato cruciale per ciclo
Supponiamo che l’algoritmo:
(1) da s scopre s’ nella DFS interna, ma (2) s’ è già stato visitato e
(3) c’è un ciclo c su s che passa da s’
Da (2), esiste stato finale s’’ da cui raggiungiamo s’ nella DFS interna
(e quindi tutto il ciclo c, ed in particolare s, è già visitato)
Due casi:
s’’ scoperto da s in DFS esterna, allora esiste ciclo su s’’ che
dovrebbe essere scoperto prima e terminare l’algoritmo (assurdo)
altrimenti, DFS esterna avrebbe dovuto scoprire s da s’’ tramite s’ e
quindi s’ non potrebbe essere stato già visitato quando viene
scoperto in DFS interna da s (assurdo)
Algoritmo 1 vs Algoritmo 2
per applicazioni in model-checking è preferibile
utilizzare la nested DFS
principali vantaggi:
ha un'implementazione on-the-fly (richiede meno
spazio)
consente di generare un controesempio
facilmente
stessa complessità asintotica
Automa di Büchi generalizzato (GBA)
A = (Σ, Q, Q_in, δ ,F) dove:
Σ, Q, Q_in, δ come in automa di Büchi
F={F1,..,Fk} famiglia di insiemi di stati finali, Fi ⊆ Q per ogni i
accettazione alla Büchi generalizzata:
data un'ω-esecuzione
r=(q0,a1,q1) (q1,a2,q2) … (qi-1,ai,qi)......
per ogni Fh ∈ F: qi ∈ F per un numero infinito di indici i
utile per costruire automa equivalente a formula LTL
Esercizio: provare che dato un automa di Büchi generalizzato
A come sopra, esiste un automa di Büchi B tale che L(A)=L(B)
e |B|=O(k |A|)
Chiusura e insiemi elementari
Sia ϕ una formula LTL, l'insieme closure(ϕ) è l'insieme di tutte
e sole le sottoformule ψ di ϕ e della loro negazione ￢ψ
(dove ψ e ￢￢ψ sono identificate)
B ⊆ closure(ϕ) è elementare se
B è logically consistent: per ogni ϕ1 ∧ϕ2, ψ ∈ closure(ϕ)
ϕ1 ∧ϕ2 ∈ B ⇔ ϕ1 ∈ B e ϕ2 ∈ B
ψ ∈ B ⇒ ￢ψ ∉B
true ∈ closure(ϕ) ⇒ true ∈ B
B è locally consistent: per ogni ϕ1 U ϕ2 ∈ closure(ϕ)
ϕ2 ∈ B ⇒ ϕ1 U ϕ2 ∈ B
ϕ1 U ϕ2 ∈ B and ϕ2 ∉ B ⇒ ϕ1 ∈ B
B è massimale: per ogni ψ ∈ closure(ϕ)
ψ ∉ B ⇒ ￢ψ ∈ B
GBA equivalente a LTL formula
Per una LTL-formula ϕ, sia Gϕ = (2AP, Q, Q_in, δ, F) dove
Q = tutti gli insiemi elementari B ⊆ closure(ϕ)
Q_in = {B ∈ Q | ϕ ∈ B }
F = { {B ∈ Q | ϕ1 U ϕ2 ∉ B or ϕ2 ∈ B} | ϕ1 U ϕ2 ∈ closure(ϕ)}
La relazione di transizione δ : Q × 2AP → 2Q è data da:
Se A ≠ B ∩ AP, allora δ(B,A) = ∅
δ(B, B ∩ AP) è l'insieme B' di tutti gli insiemi elementari di
formule che soddisfano:
(i) Per ogni ○ψ ∈ closure(ϕ): ○ψ ∈ B ⇔ ψ ∈ B', and
(ii) For every ϕ1 U ϕ2 ∈ closure(ϕ):
ϕ1 U ϕ2 ∈ B ⇔ ϕ2 ∈ B ∨ (ϕ1 ∈ B ∧ ϕ1 U ϕ2 ∈ B')
\
Automi di Büchi più espressivi di LTL
AP={p}
Sia L il linguaggio di tutte le sequenze sull'alfabeto 2{p} tali che
{p} sia il simbolo ad ogni posizione pari:
L = {A1A2A3…. / A2i={p} per ogni i ≥0}
Non esiste alcuna formula LTL ϕ su AP tale che L(ϕ) = L
Tuttavia esiste un automa di Büchi B tale che L(B) = L
(Esercizio)
Complessità LTL model checking
Gli stati di Gϕ sono insiemi elementari di formule in closure(ϕ)
ogni iniseme B può essere rappresentato con un vettore di
bit, con un bit in corrispondenza di ogni sottoformula ψ di ϕ
Il numero di stati di Gϕ è al più 2|subf(ϕ)|
dove subf(ϕ) è l'insieme di tutte le sottoformule di ϕ
siccome |subf(ϕ)| ≤ 2・|ϕ|, il numero di stati di Gϕ è 2O(|ϕ|)
Il numero di insiemi di accettazione di Gϕ è O(|ϕ|)
Il numero di stati nell'automa di Büchi equivalente Aϕ è 2O(|ϕ|)
O(|ϕ|)
2O(|ϕ|) O(|ϕ|) = 2O(|ϕ| log |ϕ|)
Complessità LTL model checking
Dato che
è possibile costruire in tempo lineare un automa AK che
accetta L(K) (tracce di una struttura di Kripke K) di taglia
O(|K|)
è possibile costruire un automa A che accetta L(K)∩L(Aϕ)
in tempo O(|K| |Aϕ|) e tale che |A|=O(|K| |Aϕ|)
|Aϕ|=2O(|ϕ| log |ϕ|)
èpossibile testare il vuoto di un automa di Büchi B in tempo
O(|B|) e spazio logaritmico (NLOGSPACE)
LTL model-checking può essere risolto in tempo |K| 2O(|ϕ| log |ϕ|)
e spazio polinomiale (PSPACE)
Inoltre, si può verificare che il problema è anche PSPACEhard, dunque LTL model-checking è PSPACE-complete
Contenuto della lezione
LTL model-checking: automata-theoretic
approach
Symbolic model-checking
Explicit-State MC e Symbolic MC
Explicit-State MC: gli algoritmi di verifica esplorano gli stati
individualmente
model-checker SPIN si basa su esplorazione esplicita degli
stati di automi di Büchi costruiti on-the-fly
la performance ottenuta con una serie di ottimizzazioni
(partial order reduction, state compression, etc.)
Symbolic MC: gli algoritmi di verifica esplorano gli stati in
insiemi rappresentati simbolicamente (formula logica)
L'insieme di successori di un insieme di stati è calcolato
dalla rappresentazione dell'insieme e la rappresentazione
delle transizioni
Algoritmo simbolico per raggiungibilità
A = (Σ, Q, Q_in, δ ) macchina a stati finiti
T: insieme target
algoritmo manipola insiemi di stati (forward reachability):
Inizializzazione: Q0 = Q_in
Passo: Qi+1 = Qi ∪ { q’ | ∃ q ∈ Qi, (q, a, q') ∈ δ}
Terminazione:
Se Qi ∩ T ≠ ∅, termina con risposta positiva
Se Qi+1 == Qi termina con risposta negativa
(cattura visita breadth-first seach)
si può ottenenere un altro algoritmo (backward reachability)
partendo dal target T e visitando gli stati a ritroso fino a
raggiungere stato iniziale oppure completata esplorazione
stati raggiungibili
Insiemi di stati come formule booleane
per implementare efficientemente algoritmi simbolici occorre
una struttura dati efficiente per
rappresentare in maniera compatta insiemi di stati
facilitare le tipiche operazioni su insiemi (unione,
intersezione, test uguaglianza, test vuoto, etc.)
Insiemi di stati possono essere rappresentati come formule
booleane
stati sono rappresentati da vettori binari (corrispondenti a
valutazioni delle variabili)
uno stato appartiene ad un insieme rappresentato da
formula ϕ se corrisponde a valutazione soddisfacente ϕ
Visita simbolica con formule
R0(X) = Qin(X)
Ri+1(X) = Ri(X) ∨ ∃ Z. ( Ri (Z) ∧ T(Z,X) )
dove:
X,Z sono vettori binari,
Rj con j≥0, e sono Qin sono predicati sui vettori
(insiemi) e
T è una relazione binaria su vettori (relazione di
transizione)
Rappresentazione compatta di formule
formula ϕ = (x1 ∧ x2) ∨ (¬ x1 ∧ x3)
una formula può essere vista come una funzione booleana e
quindi definita attraverso una tavola di verità:
x1
x2
x3
ϕ
F
F
F
F
F
F
T
T
F
T
F
F
F
T
T
T
T
F
F
F
T
F
T
F
T
T
F
T
T
T
T
T
ridondante:
formula vera se
entrambi x1 e x2 veri
oppure x1 falso e x3
vero
utilizziamo un albero di
decisione binario
Albero di decisione binario
x1
T
F
x2
x2
T
F
x3
F
T
x3
x3
x3
T
F
T
F
T
F
T
F
T
T
F
F
T
F
T
F
corrisponde alla tavola
di verità
ogni livello (eccetto
foglie) corrisponde ad
una variabile
archi uscenti etichettate
con valore variabile
valutazioni
corrispondono a
cammini dalla radice
alle foglie
valore foglie = valore
formula
Diagramma di decisione binario
possiamo compattare
ridondanze
ad es., non servono
tutte le foglie
basta solo un
rappresentante per T
e uno per F
x1
T
F
x2
x2
T
F
x3 x3
T
F
T
T T
x3
F T
F
T
T
F
x3
FF T
F
T
F
T
x3
F
F
F
T T
TF
F
F
Diagramma di decisione binario
nodo x3 più a sinistra
collegato a foglia T
indipendentemente dal
valore assegnato
stesso per secondo
nodo stesso livello
x1
T
F
x2
T
x2
F
x3
x3
T
possiamo rimuoverli e
collegare archi da x2
direttamente alle foglie
F
F
T
T
x3
F T
F
x3
T
F
T
T
F
Diagramma di decisione binario
x1
i sottografi radicati in x3
coincidono
F
T
x2
possiamo accorparli in
un unico sottografo
x2
F
T
x3
T
TT
F
T
F
F
x3
x3
T
F
T
F
F
Diagramma di decisione binario
archi uscenti da nodo x2
più a destra entrano
nello stesso nodo
possiamo rimuovere
questo nodo
non sono possibili altre
semplificazioni
x1
F
T
x2
x2
x3
F
T
T
x3
T
T
diagramma finale ha
solo 5 nodi contro i 15
di quello iniziale
F
T
F
F
T
F
Diagramma di decisione binario (BDD)
BDD: grafo aciclico direzionato (DAG) t.c.
nodi pozzo (foglie) sono etichettati con T (true) e F (false)
gli altri nodi (nodi interni) con variabili booleane
esiste un unico nodo sorgente (radice)
ogni nodo interno ha due archi uscenti:
uno etichettato con T (T-arco) e l'altro con F (F-arco)
su ogni cammino dalla radice alle foglie, le variabili sono
incontrate sempre nello stesso ordine (ordinamento delle
variabili fissato per ogni BDD)
Nota: cammini di un BDD corrispondono a funzioni di
assegnamento delle variabili
Notazione
Sia V = < v1, v2 , … vn > una sequenza ordinata di variabili
Una tupla (vn,C,D) denota un BDD B su < v1, v2 , … vn > t.c. :
la radice di B è etichettata con vn
C è il BDD su < v1, v2 , … vn-1 > la cui radice è collegata alla
radice di B con un F-arco
D è il BDD su < v1, v2 , … vn-1 > la cui radice è collegata
alla radice di B con un T-arco
Nota che C e D non sono necessariamente disgiunti (in un
BDD minimale hanno sicuramente in comune almeno le foglie)
dim(B)=n
fB denota una formula corrispondente a B
Definizione induttiva dei BDD
Sia V = < v1, v2 , … vn > una sequenza ordinata di variabili
Un BDD è :
un nodo singolo F (rappresenta la formula false)
un nodo singolo T (rappresenta la formula true)
se B and C sono due BDD sulla sequenza < v1, v2 , … vi-1 >
allora il DAG D=(vi, B, C) è un BDD su < v1, v2 , … vi > e
rappresenta la formula:
(¬ vi ∧ fB) ∨ ( vi ∧ fC)
BDD minimali: riduzione e canonicità
Fissato l'ordine delle variabili, per ogni funzione booleana
esiste un unico BDD minimale corrispondente e si può
ottenere applicando le seguenti regole:
rimpiazzare foglie con unico rappresentante per T e per F
iterativamente a partire dalle foglie (fino a saturazione):
Xm
Y1
accorpamento sottografi identici
X1
Xm Y1
u
T
Yn
u
F T
u
T
v
F
v
Yn
X1
w
F
w
eliminazione nodi interni superflui
u
T
u'
v
T
w
F
F
u
T
u'
w
F
AND di BDD
Dati due BDD B and C, il BDD D=B⊗C per fB ∧ fC si
ottiene ricorsivamente:
se dim(B) = dim(C)=0, allora dim(D)=0 e D è il singolo
nodo T se e solo se C e D sono entrambi T
se dim(B) = dim(C)>0, B = (vi , lB, rB) e C = (vi , lC, rC)
allora D=(vi, lB ⊗ lC, rB ⊗ rC)
se dim(B) > dim(C) e B = (vi , lB, rB) allora
D=(vi, lB ⊗ C, rB ⊗ C)
Nota che B⊗C è in genere non minimale anche se B e C
sono non minimali
OR di BDD
Dati due BDD B and C, il BDD D=B⊕C per fB ∨ fC si
ottiene ricorsivamente:
se dim(B) = dim(C)=0, allora dim(D)=0 e D è il singolo
nodo F se e solo se C e D sono entrambi F
se dim(B) = dim(C)>0, B = (vi , lB, rB) e C = (vi , lC, rC)
allora D=(vi, lB ⊕ lC, rB ⊕ rC)
se dim(B) > dim(C) e B = (vi , lB, rB) allora
D=(vi, lB ⊕ C, rB ⊕ C)
Nota che B ⊕ C è in genere non minimale anche se B e C
sono non minimali
NOT e Complessità AND e OR
Per calcolare, il BDD per la negazione di una formula
basta scambiare le etichette delle foglie (T diventa F e
F diventa T)
richiede tempo costante
Utilizzando programmazione dinamica, AND e OR di
BDD possono essere fatti risolvendo O(|B|.|C|)
sottoproblemi
per ogni nodo u in B e v in C, (u,v) è risolto una volta
si mantengono i risultati per ogni coppia (r,s)
Quindi, l'algoritmo richiede tempo O(|B|.|C|) e il BDD
ottenuto ha taglia O(|B|.|C|).
Restrizione di una variabile a un valore
Per una formula f con n variabili,
f↓(x=b) è la formula con n-1 variabili ottenuta da f
assegnando x con b
Dato un BDD per f, calcola il BDD per f↓(x=b) come segue:
visita BDD per f
redireziona ogni arco che punta a un nodo v etichettato x
al nodo u tale che (v,u) è un b-arco
x
b
y
¬b
y
Quantificazione
Si consideri una formula f.
Quantificazione esistenziale:
∃ v.f = f↓(v=F) ∨ f↓(v=T)
dato un BDD per f, possiamo calcolare un BDD for ∃ v.f in
tempo O(n^2)
Quantificazione universale (duale):
∀ v.f = f↓(v=F) ∧ f↓(v=T)
dato un BDD per f, possiamo calcolare un BDD for ∀ v.f in
tempo O(n^2)
AndExists
nell'algoritmo simbolico che risolve la reachability occorre
calcolare
∃ Z. ( Ri (Z) ∧ T(Z,X) )
possiamo combinare gli algoritmo per il calcolo dell'AND e
della quantificazione esistenziale così che i BDD da
memorizzare hanno solo |X| variabili (invece di 2|X| variabili)
T è la relazione di transizione data, è costante
si devono calcolare BDD che rappresentano insiemi di
stati raggiungibili
Model-checking con BDD
Reachability( X, Q_in(X), T(X,X’), F(X)){
// X – vars; Q_in, T(X,X’) e F sono BDD
R:=0; R’= Q_in;
do {
R = R’;
R’ = R ∨ ∃ Z. ( R(Z) ∧ T(Z,X) ) ;
} while (R≠R’ or R∧F ≠ ∅);
if (R∧F = ∅)
return “unreachable”
else
return “reachable”;
}
Modifichiamo reachability
ReachableSet( X, Q_in(X), T(X,X’)){
// X – vars; Q_in e T(X,X’) sono BDD
R:=0;
R’= ∃ Z.(Q_in(Z) ∧ T(Z,X) ) ;
// stati iniziali compaiono in R solo se possono essere
// raggiunti nuovamente
do {
R = R’;
R’ = R ∨
} while (R≠R’);
return R;
}
∃ Z. ( R(Z) ∧ T(Z,X) ) ;
Model-checking con BDD
Buchi( X, Gin(X), T(X,X’), F(X)){
// X – vars; Gin , T(X,X’) e F sono BDD
F' = F ∧ ReachableSet(X, Q_in(X), T(X,X’);
do {
F = F’;
F’ = F ∧ ReachableSet(X,F(X),T(X,X’);
} while (F≠F’);
if (F = ∅)
return “unsatisfied”
else
return “satisfied”;
}
Implementazione di BDD
Alcuni BDD packages disponibili:
CuDD --- Fabio Somenzi, Colarado Univ.
VIS --- Colorado, Berkeley
Numerose euristiche implementate in pratica:
Forward/Backward
Ordinamento delle variabili
Supporto diretto per domini finiti (MDD)
Partizionamento delle transizioni/ della rete
Scelta frontiere
Ordinamento delle variabili
aspetto cruciale per la prestazione di algoritmi che usano BDD
influenza sensibilmente la taglia dei BDD
scegliendo il giusto ordinamento, taglia BDD può essere
esponenzialmente più succinto
Es. (x1∨ y1) ∧ …. ∧(xn ∨ yn)
BDD esponenziale in n se ordinamento <x1,….,xn,y1,….,yn>
lineare se ordinamento <x1, y1,….,xn,yn>
non sempre è possibile avere BDD di taglia trattabile
(esistono formule per le quali la taglia del BDD è
esponenziale nel numero di variabili indipendentemente
dall'ordinamento)
Osservazioni
Il model-checkig simbolico con BDD ha avuto molto successo
nella verifica dell'hardware
BDD non sono ampiamente usati nella verifica del software
difficili da combinare con partial-order reduction (insieme
all'astrazione principale artefice dei successi in software
verification)
difficile modellare l'allocazione dinamica della memoria
in software verification approccio simbolico fa uso di
esecuzioni simboliche e vincoli (constraints)
Model checker simbolico: nuSMV