Document

Logiche temporali
Torniamo all’esempio
dell’ascensore
Nell’esempio dell’ascensore, visto nella lezione
precedente, supponiamo di voler verificare le
seguenti proprietà:
Prima o poi ogni richiesta deve venire soddisfatta
L’ascensore non attraversa mai un piano nel quale
ci sia una richiesta pendente senza soddisfare tale
richiesta
Tino Cortesi
Tecniche di Analisi di Programmi
2
Proprietà comportamentali
Queste proprietà hanno a che fare con il
comportamento dinamico del sistema.
Possono essere formalzzate usando una notazione del
tipo “la posizione al tempo t deve garantire che…”
Possiamo usare la seguente notazione
H(t) è la posizione della cabina al tempo t
app(n,t) è una richiesta pendente al piano n al
tempo t
serv(n,t) è il servizio al piano n al tempo t
Tino Cortesi
Tecniche di Analisi di Programmi
3
Formalizzazione (1)
Prima o poi ogni richiesta deve venire soddisfatta
per ogni t, per ogni n:
(se app(n,t) allora $t’>t: serv(n,t’))
Tino Cortesi
Tecniche di Analisi di Programmi
4
Formalizzazione (2)
L’ascensore non attraversa mai un piano nel quale ci sia
una richiesta pendente senza soddisfare tale richiesta
Per ogni t, per ogni t’>t, per ogni n:
se app(n,t) & H(t’) !=n & $ttrav: t  ttrav  t’ & H(ttrav)=n
allora $tserv: t  tserv  t’ & serv(n, tserv)
Tino Cortesi
Tecniche di Analisi di Programmi
5
Logiche temporali
Logiche che permettono di esprimere proprietà legate
al tempo
Pnueli (1977) suggerisce di utilizzarle per la specifica
di sistemi dinamici
Operatori che indicano “sempre”, “finché”,…
Tino Cortesi
Tecniche di Analisi di Programmi
6
Logiche temporali
Linear Time
Branching Time
Ogni stato ha un unico successore
Sequenze infinite (words)
Linear Temporal Logic (LTL)
Tino Cortesi
Tecniche di Analisi di Programmi
Ogni stato ha diversi successori
Alberi infiniti
Computation Tree Logic (CTL)
7
CTL*
CTL* serve per formalizzare proprietà degli stati che
riguardano le esecuzioni di un sistema
Una esecuzione è una sequenza di stati. Ad ogni
stato sono associate le proposizioni atomiche che
sono vere in quello stato
Ci sono poi le costanti true e false, e i connettivi logici
di congiunzione, disgiunzione, implicazione e
negazione.
Parliamo di formule proposizionali quando ci riferiamo
a formule in cui compaiono solo proposizioni
atomiche e connettivi logici
Tino Cortesi
Tecniche di Analisi di Programmi
8
Combinatori temporali
Permettono di parlare di sequenze di stati
appartenenti ad una stessa esecuzione
X Se p è una proprietà dello stato corrente, Xp dice
che il prossimo stato soddisferà p.
Per esempio (p v Xp) dice che p è soddisfatta o nello
stato corrente o nel prossimo stato (o in entrambi)
F Fp dice che uno stato futuro soddisferà p
ovvero “ci sarà un tempo in cui p varrà (almeno una
volta)”
G Gp dice che tutti gli stati futuri soddisfano p
ovvero “p varrà sempre”
Gli operatori possono essere innestati. Ad esempio
GFp dice che p sarà vera infinite volte nell’esecuzione
considerata
Tino Cortesi
Tecniche di Analisi di Programmi
9
Combinatori temporali
U pUq dice che a un certo punto q sarà verificata, e
nel frattempo vale p.
Esempio: G(alert -> (alarm U halt)) si legge: “ se
sono in uno stato di allerta, l’allarme rimane attivato
finché viene raggiunto lo stato di halt”
F è un caso speciale di U, infatti Fp è equivalente a
true U p
Osservate che gli operatori introdotti finora (X,F,G,U)
ci permettono di parlare di proprietà di una singola
esecuzione
Tino Cortesi
Tecniche di Analisi di Programmi
10
Path Quantifiers
A La formula Ap dice che tutte le esecuzioni che
partono dallo stato corrente soddisfano la proprietà p
Attenzione a non confondere A con G:
Ap dice che tutte le esecuzioni che in questo
momento sono possibili soddisfano p
Gp dice che p vale in ogni passo di una esecuzione
che si considera
E La formula Ep dice che dallo stato corrente esiste
un’esecuzione che soddisfa p
Tino Cortesi
Tecniche di Analisi di Programmi
11
Combinazioni di A E F G
EFg dice che seguendo una qualche esecuzione è
possibile raggiungere uno stato che soddisfa g
Tino Cortesi
Tecniche di Analisi di Programmi
12
Combinazioni di A E F G
AFg dice che seguendo ogni esecuzione si raggiunge
prima o poi uno stato che soddisfa g (g è inevitabile!)
Tino Cortesi
Tecniche di Analisi di Programmi
13
Combinazioni di A E F G
EGg dice che esiste un’esecuzione nella quale g è
sempre soddisfatta
Tino Cortesi
Tecniche di Analisi di Programmi
14
Combinazioni di A E F G
AGg dice che in ogni esecuzione g è sempre
soddisfatta
Tino Cortesi
Tecniche di Analisi di Programmi
15
Combinazioni di A E F G
AGFg
in ogni esecuzione (A) ad ogni istante di
tempo (G) si incontrerà necessariamente prima o poi
(F) uno stato che soddisfa g
AGEFg
in ogni esecuzione (A) ad ogni istante di
tempo è possibile raggiungere g
Quindi AGEFg può essere verificata anche se esiste
un’esecuzione in cui g non è verificata.
Osserva inoltre che Ag è equivalente a -E-g
Tino Cortesi
Tecniche di Analisi di Programmi
16
Esempio
Un sistema di controllo del traffico: vogliamo
garantire che non ci siano collisioni e che il traffico
scorra…
S
E
N
Tino Cortesi
Tecniche di Analisi di Programmi
17
Specifica in CTL*
Safety (nothing bad happens)
AG  (E_Go  (N_Go  S_Go));
Liveness (something good happens)
AG ( N_Go  N_Sense  AF N_Go);
AG ( S_Go  S_Sense  AF S_Go);
AG ( E_Go  E_Sense  AF E_Go);
Fairness constraints
AF (N_Go  N_Sense);
AF (S_Go  S_Sense);
AF (E_Go  E_Sense);
Tino Cortesi
Tecniche di Analisi di Programmi
AF=in ogni cammio prima o poi
AG=in ogni cammino sempre
18
Semantica di CTL*
Vogliamo definire cosa significa, dato un automa A,
che una formula g di CTL* è vera al tempo i di una
esecuzione s di A (che non parte necessariamente
dallo stato iniziale)
Questo si indica con A,s,i |= g
La definizione di |= è data per induzione sulla
struttura della formula g
Tino Cortesi
Tecniche di Analisi di Programmi
19
Semantica di CTL*
A,s,i |= p
A,s,i |= x
A,s,i |= x  y
A,s,i |= x  y
A,s,i |= X x
A,s,i |= F x
A,s,i |= G x
A,s,i |= x U y
Tino Cortesi
se p l(s(i)) cioè se p è vera nello
stato i-esimo della sequenza s
se non è vero che A,s,i |= x
se A,s,i |= x e A,s,i |= y
se A,s,i |= p oppure A,s,i |= y
if i<|s| e A,s,i+1 |= x
if $j, (|s| ≥ j ≥ 0): A,s,j |= x
if j, (|s| ≥ j ≥ 0): A,s,j |= x
if $j, (|s| ≥ j ≥ 0): A,s,j |= y e
k t.c. j > k ≥ 0: A,s,k |= x
Tecniche di Analisi di Programmi
20
Semantica di CTL* (ctd.)
A,s,i |= E x
A,s,i |= A x
se $ s’: s(0)…s(i) = s’(0)… s’(i)
e A,s’,i |= x
se  s’: s(0)…s(i) = s’(0)… s’(i)
vale A,s’,i |= x
Possiamo ora definere formalmente cosa significa
che un automa soddisfa la formula x
A |= x
Tino Cortesi
se e solo se
per ogni esecuzione s di A: A,s,0 |= x
Tecniche di Analisi di Programmi
21
CTL*, LTL, CTL
Il tempo è discreto (né continuo né denso!)
LTL è un frammento di CTL* dove mancano i
quantificatori A ed E
In altre parole LTL parla di cammini senza
preoccuparsi di come sono organizzato in un albero
CTL è il frammento di CTL* dove si richiede che ogni
combinatore temporale sia nello scope di un path
quantifier: i combinatori che si possono utilizzare
sono quindi EX, AX, E_U_, A_U_, ecc.
Tino Cortesi
Tecniche di Analisi di Programmi
22
Model Checking CTL
La componente fondamentale dell’algoritmo di model
checking per CTL è una procedura di marcatura che
opera su un automa, e che, a partire da una formula
x di CTL, marca, per ogni stato q dell’automa e per
ogni sottoformula y di x se y è soddisfatta nello stato
q.
Parliamo di marcatura, perché il valore di y in q,
denotato con q.y è calcolato e poi memorizzato.
Quando la marcatura di x è completa, è immediato
verificare se A |= x guardando al valore di q0.x nello
stato iniziale q0.
Tino Cortesi
Tecniche di Analisi di Programmi
23
Risultati di complessità
Il problema di soddisfacibilità di LTL è PSPACE-completo.
LTL Model Checking ha complessità PSPACE-completa
Il problema di soddisfacibilità di CTL è EXPTIME-completo.
CTL Model Checking ha complessità polinomiale
Il problema di soddisfacibilità di CTL* è 2EXPTIME-completo.
CTL* Model Checking ha complessità PSPACE-completa
Tino Cortesi
Tecniche di Analisi di Programmi
24
Rappresentare gli stati
Rappresentare gli stati mediante formule booleane
2m stati possono essere codificati con m variabili
proposizionali
Stati – congiunzione di proposizioni (o di negazioni d
proposizioni)
Insieme di stati – disgiunzione di formule che codificano
stati
Esempio: m = 2, S={s1,s2,s3,s4}
Variabili proposizionali {a, b}
S={00, 01, 10, 11}={ab, a b, ab, ab}
{s1,s2}={00, 01}=(ab)(ab)
Tino Cortesi
Tecniche di Analisi di Programmi
25
Rappresentazione di funzioni
booleane
Una funzione booleana può essere rappresentata
come albero binario
Ogni nodo interno è etichettato con una variabile
booleana
Ogni nodo interno ha un successore etichettato con 1
e uno etichettato con 0
I nodi terminali sono etichettati con 1 o 0
Tino Cortesi
Tecniche di Analisi di Programmi
26
x y
z
g
y
1
0
0 0
0 0
0 0
1 1
0 1
0 1
0 1
1 0
1 0
0 1
0
1 0
1 0
0
1 1
0 0
1 1
1 1
z
z
0
x
x
1
1
0
1
1
0
1
x
1
0
0
1
x
1
0
1
0
0
1
g = (y  (x  z))  (y  (x  z))
Tino Cortesi
Tecniche di Analisi di Programmi
27
OBDD
Tre regole di riduzione:
Condivisione degli stessi nodi terminali. (R1)
Test ridondanti (R2)
Condivisione degli stessi nodi non terminali (R3)
Tino Cortesi
Tecniche di Analisi di Programmi
28
Ordered Binary Decision
Diagram (OBDD)
0
0
a1
1
b1
1
a2
b1
a2
0
1
1 0
b2 b2
b2 b2
0 1 0 1 0 1 0 1
1 0 0 1 0 0 0 0
0
a2
1
a2
0 1
0 1
b2 b2 b2 b2
0 1 0 1 0 1 0 1
0 0 0 0 1 0 0 1
(a1  b1)  (a2  b2)
Tino Cortesi
Tecniche di Analisi di Programmi
29
Reduced Ordered BDD
0
0
a2
0
1
b2
b2
0 1 0 1
1 0 0 1
b1
a1
1
b1
1
0
a2
0
1
a2
1
0
1
0
b2
b2
b2
b2
0 1 0 1 0 1 0 1
0 0 0 0 1 0 0 1
(a1  b1)  (a2  b2)
Tino Cortesi
Tecniche di Analisi di Programmi
30
Reduced Ordered BDD
0
0
a2
0
1
b2
b2
0 1 0 1
1 0 0 1
b1
a1
1
1
0
b1
0
1
a2
1
0
b2
b2
0 1 0 1
1 0 0 1
(a1  b1)  (a2  b2)
Tino Cortesi
Tecniche di Analisi di Programmi
31
Reduced Ordered BDD
0
0
a2
0
1
b2
b2
0 1 0 1
1 0 0 1
Tino Cortesi
b1
a1
1
1
1
0
b1
0
(a1  b1)  (a2  b2)
Tecniche di Analisi di Programmi
32
Reduced Ordered BDD
0
0
a2
0
1
b2
b2
0 11
1
Tino Cortesi
b1
a1
1
b1
1
1
0
0
0
(a1  b1)  (a2  b2)
Tecniche di Analisi di Programmi
33
Reduced BDD
Binary Decision Tree
y
y
z
z
z
x
0
1
x
1
x
0
1
x
x
0
0
1
0
1
g = (y  (x  z))  (y  (x  z))
Tino Cortesi
Tecniche di Analisi di Programmi
34
Ordered Binary Decision
Diagrams
Dato un oridinamento fissato delle variabili, ogni
funzione bolleana ha esattamente un BDD ridotto.
Gli OBDD sono oggetti canonici
Per testare se due formule booleane sono equivalenti
è sufficiente verificare che il loro OBDD siano identici.
Questo è un risultato fondamentale per garantire
l’efficienza del model checking
Tino Cortesi
Tecniche di Analisi di Programmi
35
Reduced OBDDs
x1 < y1 < x2 < y2
x1 < x2 < y1 < y2
x1
x1
(x1 = y1  x2 = y2)
y1
x2
y2
1
Tino Cortesi
x2
x2
y1
y1
y1
y2
y2
y2
1
0
Tecniche di Analisi di Programmi
y1
y1
0
36
Genealogia
Floyd/Hoare
late 60s
Büchi, 60
Logics of
Programs
w-automata
S1S
Pnueli
late 70’s
Aristotle 300’s BCE
Kripke 59
Temporal/
Modal Logics
Tarski 50’s
Park, 60’s
Clarke/Emerson
Early 80’s
m-Calculus
Kurshan Vardi/Wolper
mid 80’s
CTL Model
ATV
LTL Model
Checking
Checking
Bryant, mid 80’s
QBF
BDD
Symbolic
Model Checking late 80’s
Tino Cortesi
Tecniche di Analisi di Programmi
37