Logiche temporali

Tino Cortesi Tecniche di Analisi di Programmi 2

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 soddisfattaL’ascensore non attraversa mai un piano nel quale ci sia una richiesta pendente senza soddisfare tale richiesta


Proprietà comportamentaliQueste 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 tapp(n,t) è una richiesta pendente al piano n al tempo tserv(n,t) è il servizio al piano n al tempo t


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’))


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)


Logiche temporaliLogiche che permettono di esprimere proprietà legate al tempoPnueli (1977) suggerisce di utilizzarle per la specifica di sistemi dinamiciOperatori che indicano “sempre”, “finché”,…


Logiche temporali

Linear TimeOgni stato ha un unico successore

Sequenze infinite (words)

Linear Temporal Logic (LTL)

Branching TimeOgni stato ha diversi successori

Alberi infiniti

Computation Tree Logic (CTL)


CTL*CTL* serve per formalizzare proprietà degli stati che riguardano le esecuzioni di un sistemaUna esecuzione è una sequenza di stati. Ad ogni stato sono associate le proposizioni atomiche che sono vere in quello statoCi 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


Combinatori temporaliPermettono di parlare di sequenze di stati appartenenti ad una stessa esecuzioneX 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à povvero “ci sarà un tempo in cui p varrà (almeno una volta)” G Gp dice che tutti gli stati futuri soddisfano povvero “p varrà sempre”Gli operatori possono essere innestati. Ad esempio GFp dice che p sarà vera infinite volte nell’esecuzione considerata


Combinatori temporaliU 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 pOsservate che gli operatori introdotti finora (X,F,G,U) ci permettono di parlare di proprietà di una singola esecuzione


Path QuantifiersA La formula Ap dice che tutte le esecuzioni che partono dallo stato corrente soddisfano la proprietà pAttenzione a non confondere A con G:

Ap dice che tutte le esecuzioni che in questo momento sono possibili soddisfano pGp 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


Combinazioni di A E F GEFg dice che seguendo una qualche esecuzione è possibile raggiungere uno stato che soddisfa g


Combinazioni di A E F GAFg dice che seguendo ogni esecuzione si raggiunge prima o poi uno stato che soddisfa g (g è inevitabile!)


Combinazioni di A E F GEGg dice che esiste un’esecuzione nella quale g è sempre soddisfatta


Combinazioni di A E F GAGg dice che in ogni esecuzione g è sempre soddisfatta


Combinazioni di A E F GAGFg in ogni esecuzione (A) ad ogni istante di tempo (G) si incontrerà necessariamente prima o poi (F) uno stato che soddisfa gAGEFg in ogni esecuzione (A) ad ogni istante di tempo è possibile raggiungere gQuindi AGEFg può essere verificata anche se esiste un’esecuzione in cui g non è verificata.

Osserva inoltre che Ag è equivalente a -E-g


EsempioUn sistema di controllo del traffico: vogliamo garantire che non ci siano collisioni e che il traffico scorra…

E

S

N


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); AF=in ogni cammio prima o

poiAG=in ogni cammino sempre


Semantica di CTL*Vogliamo definire cosa significa, dato un automa A, che una formula g di CTL* è vera al tempo i di una esecuzione di A (che non parte necessariamente dallo stato iniziale)Questo si indica con A,,i |= gLa definizione di |= è data per induzione sulla struttura della formula g


Semantica di CTL*A,,i |= p se p l((i)) cioè se p è vera nello stato i-esimo della sequenza A,,i |= se non è vero che A,,i |= A,,i |= se A,,i |= e A,,i |= A,,i |= se A,,i |= p oppure A,,i |= A,,i |= X if i<|| e A,,i+1 |= A,,i |= F if j, (|| ≥ j ≥ 0): A,,j |= A,,i |= G if j, (|| ≥ j ≥ 0): A,,j |= A,,i |= U if j, (|| ≥ j ≥ 0): A,,j |= e

k t.c. j > k ≥ 0: A,,k |=


CTL*, LTL, CTLIl tempo è discreto (né continuo né denso!)LTL è un frammento di CTL* dove mancano i quantificatori A ed EIn altre parole LTL parla di cammini senza preoccuparsi di come sono organizzato in un alberoCTL è 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.


Model Checking CTLLa 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 di CTL, marca, per ogni stato q dell’automa e per ogni sottoformula di se è soddisfatta nello stato q.Parliamo di marcatura, perché il valore di in q, denotato con q. è calcolato e poi memorizzato.Quando la marcatura di è completa, è immediato verificare se A |= guardando al valore di q0.nello stato iniziale q0.


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


Rappresentare gli statiRappresentare gli stati mediante formule booleane

2m stati possono essere codificati con m variabili proposizionaliStati – 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}={ab, a b, ab, ab}

{s1,s2}={00, 01}=(ab)(ab)


Rappresentazione di funzioni booleane

Una funzione booleana può essere rappresentata come albero binarioOgni nodo interno è etichettato con una variabile booleanaOgni nodo interno ha un successore etichettato con 1 e uno etichettato con 0I nodi terminali sono etichettati con 1 o 0


0 0 0 0

0 0 1 1

0 1 0 1

0 1 1 0

1 0 0 1

1 0 1 0

1 1 0 0

1 1 1 1

x y z g y

z

x x

z

x x

0 1 1 0 1 0 0 1

g = (y (x z)) (y (x z))

0

0

0 0 0 0

1

1 1

1 1

0

11


OBDDTre regole di riduzione:

Condivisione degli stessi nodi terminali. (R1)Test ridondanti (R2)Condivisione degli stessi nodi non terminali (R3)


Ordered Binary Decision Diagram (OBDD)

(a1 b1) (a2 b2)

a1

b1 b1

a2 a2

b2 b2 b2

a2 a2

b2 b2b2b2 b2

00 110000

0

0

0 0

0

0 0

0 0 0 0

1

1

11

1

11

1 1 1 100 001001

0 0 0 01 1 1 1


(a1 b1) (a2 b2)

a1

b1 b1

a2

b2 b2

a2 a2

b2 b2b2 b2

00 110000

0

0

0

0

0 0

0 0 0 0

1

1

11

1

1

1 1 1 101001

0 01 1

Reduced Ordered BDD


(a1 b1) (a2 b2)

a1

b1 b1

a2

b2 b2

a2

b2 b2

00 11

0

0

0

0

0

0 0

1

1

1

1

1

1 101001

0 01 1

Reduced Ordered BDD


(a1 b1) (a2 b2)

a1

b1 b1

a2

b2 b2

0

0

0

0

1

11

1

010010 01 1

Reduced Ordered BDD


(a1 b1) (a2 b2)

a1

b1 b1

a2

b2 b2

0

0

0

1

1

1

010 01

1

0

1

Reduced Ordered BDD


y

z

x

0

Reduced BDD

y

z

x x

z

x x

0 1 1 0 1 0 0 1

Binary Decision Tree

g = (y (x z)) (y (x z))

1


Ordered Binary Decision Diagrams

Dato un oridinamento fissato delle variabili, ogni funzione bolleana ha esattamente un BDD ridotto. Gli OBDD sono oggetti canoniciPer 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


Reduced OBDDs

x1

y1

x2

y2y2

1 0

y1

x1 < y1 < x2 < y2 x1 < x2 < y1 < y2

x1

x2 x2

y1 y1 y1y1

y2y2

1 0

(x1 = y1 x2 = y2)


Genealogia

Logics ofPrograms

Temporal/Modal Logics

CTL ModelChecking

SymbolicModel Checking

-automataS1S

LTL ModelChecking

ATV

Tarski

-Calculus

QBF BDD

Floyd/Hoarelate 60s

Aristotle 300’s BCEKripke 59

Pnuelilate 70’s Clarke/Emerson

Early 80’s

Büchi, 60

Kurshan Vardi/Wolpermid 80’s

50’s

Park, 60’s

Bryant, mid 80’s

late 80’s

Logiche temporali

Documents

Transcript of Logiche temporali