Model checking - Riassunto

Fonte: raw/Model Checking.md

Punti chiave

• Il model checking verifica automaticamente se un modello soddisfa una specifica temporale.
• Model checking LTL: usa un approccio automata-theoretic; per verificare una proprieta si controlla l'assenza di computazioni che soddisfano la negazione.
• Model checking CTL: valuta formule sugli stati di un modello di Kripke tramite labeling e punti fissi.
• LTL e' piu adatta a vincoli globali sui cammini; CTL e' piu adatta a proprieta di ramificazione e possibilita.
• La complessita del model checking LTL e' piu alta; CTL e' tipicamente polinomiale nella dimensione del modello e della formula.

Concetti estratti

• Model checking
• Grafo dei comportamenti
• Modello di Kripke

Model checking

Il model checking verifica automaticamente se un modello formale soddisfa una specifica.

Idea centrale

Dato un modello $M$ e una formula $\varphi$, il problema e' stabilire se: $$M \models \varphi$$

Nel caso LTL, spesso si controlla se esiste una computazione del sistema che soddisfa $\neg\varphi$. Nel caso CTL, si etichettano gli stati che soddisfano sottoformule fino alla formula completa.

Vantaggi

• verifica esaustiva sui comportamenti del modello;
• generazione di controesempi;
• forte integrazione con logiche temporali.

Limite principale

Il problema dello state explosion: lo spazio degli stati puo crescere esponenzialmente con il numero di componenti concorrenti.

Collegamenti

• Logica temporale lineare (LTL)
• Logica ad albero computazionale (CTL)
• Model checking simbolico
• Model checking limitato

Grafo dei comportamenti

Un grafo dei comportamenti e' una struttura usata nel model checking LTL. Si ottiene combinando il grafo delle computazioni del programma con il tableau della formula LTL.

I nodi sono coppie $(s,A)$, dove $s$ e' uno stato del programma e $A$ e' un atomo del tableau compatibile con quello stato.

Uso

Il grafo permette di cercare sottografi adeguati: sottografi che rappresentano computazioni fair e realizzanti, cioe' computazioni che soddisfano le eventualita richieste dalla formula.

Collegamenti

• Model checking
• Logica temporale lineare (LTL)

Modello di Kripke

Un modello di Kripke e' una struttura a stati usata nel model checking temporale.

Componenti

Tipicamente contiene: - un insieme di stati; - una relazione di transizione; - uno o piu stati iniziali; - una funzione di labeling che associa proposizioni vere a ciascuno stato.

Uso

Le formule CTL e LTL vengono valutate sui cammini generati dalla relazione di transizione.

Collegamenti

• Model checking
• Logica ad albero computazionale (CTL)
• Logica temporale lineare (LTL)

Approfondimento completo settimana 4 - Procedure decisionali e model checking

Questo capitolo spiega come si passa dalle logiche temporali alla verifica automatica. L'idea centrale e' sempre la stessa:

$$\text{sistema} + \text{specifica} \quad \Rightarrow \quad \text{algoritmo che risponde vero/falso e, se falso, produce un controesempio}.$$

La difficolta' e' che i sistemi reattivi non terminano: generano computazioni infinite. Per questo non basta controllare un output finale. Bisogna ragionare su tutti i cammini possibili, su proprieta' che parlano di "sempre", "prima o poi", "finche" e "esiste un futuro".

Il capitolo usa due tecniche principali:

• per LTL, si cerca un controesempio costruendo un tableau/automaton per la negazione della formula e combinandolo con il sistema;
• per CTL, si etichettano gli stati del modello con le sottoformule vere, usando preimmagini e punti fissi.

La differenza nasce dalla semantica: LTL parla di cammini lineari infiniti, CTL parla di stati dentro un albero di computazioni ramificate.

1. Il problema di model checking

Dato un modello $M$ e una formula temporale $\varphi$, il problema di model checking e':

$$M \models \varphi?$$

La formula descrive una proprieta' richiesta. Il modello descrive tutti i comportamenti possibili del sistema. La risposta e' vera se ogni comportamento rilevante del modello soddisfa la specifica.

Perche e' utile

Il model checking e' diverso da una simulazione:

• una simulazione visita alcuni comportamenti scelti;
• il model checking visita implicitamente tutti i comportamenti del modello;
• se la proprieta' fallisce, l'algoritmo puo' restituire una computazione che mostra l'errore.

Il controesempio e' fondamentale perche' rende il fallimento leggibile: non dice solo "la formula e' falsa", ma mostra una traccia che viola la specifica.

Perche non e' banale

Il sistema puo' avere molti stati, e i comportamenti possono essere infiniti. Anche un modello finito genera infiniti cammini, perche' puo' contenere cicli.

Quindi il punto tecnico e':

trasformare una domanda su infiniti cammini in una domanda finita su grafi, automi, tableau o punti fissi.

Questa trasformazione e' cio' che rende decidibile e automatizzabile il model checking.

2. Modelli di Kripke

Il modello standard per interpretare LTL e CTL e' la struttura di Kripke:

$$K=(S,S_0,R,L).$$

Dove:

• $S$ e' l'insieme finito degli stati;
• $S_0\subseteq S$ e' l'insieme degli stati iniziali;
• $R\subseteq S\times S$ e' la relazione di transizione;
• $L:S\to 2^{AP}$ assegna a ogni stato le proposizioni atomiche vere in quello stato.

La funzione $L$ e' necessaria per collegare il modello alla formula. Se una formula contiene la proposizione $p$, allora $p$ e' vera nello stato $s$ quando:

$$p\in L(s).$$

Perche si usa una relazione totale

Spesso si assume che ogni stato abbia almeno un successore. Questa scelta non e' un dettaglio tecnico casuale: LTL e CTL sono logiche per computazioni infinite. Se un cammino terminasse, formule come $X\varphi$, $G\varphi$ o $F\varphi$ diventerebbero ambigue.

Per evitare questo problema, uno stato terminale viene spesso completato con un self-loop. Questo rappresenta l'idling: il sistema resta nello stesso stato per sempre.

Cammini

Un cammino e' una sequenza infinita:

$$\pi=s_0s_1s_2\ldots$$

tale che:

$$R(s_i,s_{i+1}) \quad \text{per ogni } i\ge 0.$$

La traccia osservabile del cammino e':

$$L(s_0),L(s_1),L(s_2),\ldots$$

Le formule temporali non leggono direttamente gli stati interni, ma le proposizioni vere lungo questa traccia.

3. Richiamo: LTL e CTL hanno semantiche diverse

LTL e CTL usano operatori simili, ma parlano di oggetti diversi.

LTL

Una formula LTL viene valutata su un singolo cammino infinito:

$$\pi,i\models \varphi.$$

Gli operatori principali sono:

• $X\varphi$: $\varphi$ vale nel prossimo stato del cammino;
• $F\varphi$: prima o poi $\varphi$ vale;
• $G\varphi$: $\varphi$ vale sempre;
• $\varphi U \psi$: $\varphi$ vale fino al momento in cui vale $\psi$.

Quando diciamo che un modello soddisfa una formula LTL, intendiamo di solito:

$$K\models \varphi$$

se tutti i cammini iniziali di $K$ soddisfano $\varphi$.

Quindi LTL e' lineare: guarda ogni computazione come una parola infinita.

CTL

Una formula CTL viene valutata sugli stati:

$$K,s\models \varphi.$$

Gli operatori temporali sono combinati con quantificatori di cammino:

• $A$: per tutti i cammini;
• $E$: esiste un cammino.

Esempi:

• $EF\ goal$: esiste un cammino che prima o poi raggiunge goal;
• $AF\ goal$: tutti i cammini prima o poi raggiungono goal;
• $EG\ safe$: esiste un cammino che resta sempre safe;
• $AG\ safe$: tutti i cammini restano sempre safe.

CTL e' branching-time: ragiona sull'albero delle possibilita' che partono da uno stato.

Perche questa differenza cambia gli algoritmi

LTL richiede di controllare cammini infiniti. Per questo si usano automi, tableau e ricerca di cicli accettanti.

CTL valuta formule stato per stato. Per questo si possono calcolare insiemi di stati che soddisfano ogni sottoformula.

La differenza algoritmica deriva direttamente dalla differenza semantica.

4. Perche nel model checking LTL si controlla la negazione

Supponiamo di voler verificare:

$$K\models \varphi.$$

Questo significa:

ogni cammino iniziale del sistema soddisfa $\varphi$.

La negazione e':

esiste un cammino iniziale del sistema che soddisfa $\neg\varphi$.

Quindi:

$$K\models \varphi \quad \Longleftrightarrow \quad \text{non esiste un cammino di }K\text{ che soddisfa }\neg\varphi.$$

Questa forma e' utile perche' un controesempio e' esattamente un cammino che soddisfa $\neg\varphi$. L'algoritmo non deve dimostrare direttamente una proprieta' universale: cerca un oggetto esistenziale. Se lo trova, la proprieta' fallisce. Se non lo trova, la proprieta' e' valida sul modello.

Questa e' la ragione teorica dietro la frase:

per verificare $\varphi$, cerco una computazione che soddisfi $\neg\varphi$.

5. Tableau LTL: perche serve

Una formula LTL parla di un cammino infinito, ma un algoritmo deve lavorare con strutture finite. Il tableau risolve questo problema.

L'idea e':

1. scomporre la formula nelle sue sottoformule;
2. descrivere cosa puo' essere vero in una singola posizione del cammino;
3. collegare queste descrizioni tramite vincoli di "prossimo stato";
4. cercare un ciclo che realizza tutte le eventualita'.

Il tableau e' quindi un grafo finito che rappresenta tutte le possibili evoluzioni coerenti con la formula.

6. Chiusura della formula

Per costruire il tableau si parte dalla closure della formula, cioe' dall'insieme finito delle sottoformule necessarie per valutarla.

Se la formula contiene:

$$G(p\to Fq)$$

la closure contiene, tra le altre:

• $G(p\to Fq)$;
• $p\to Fq$;
• $p$;
• $Fq$;
• $q$;
• le negazioni rilevanti.

La closure e' finita perche' la formula e' finita. Questo e' importante: trasforma il problema temporale in un problema combinatorio su un insieme finito di pezzi.

7. Atomi del tableau

Un atomo rappresenta una descrizione completa e coerente di una singola posizione del cammino rispetto alla closure.

In pratica, per ogni sottoformula rilevante l'atomo decide se essa vale oppure no, rispettando le regole logiche.

Un atomo non puo' contenere contraddizioni:

• non puo' contenere sia $\varphi$ sia $\neg\varphi$;
• contiene $\varphi\land\psi$ se e solo se contiene $\varphi$ e $\psi$;
• contiene $\varphi\lor\psi$ se contiene almeno una tra $\varphi$ e $\psi$;
• tratta le formule temporali in modo coerente con la loro espansione.

Perche gli atomi sono utili

LTL valuta una formula in una posizione del cammino. Un atomo e' una possibile "fotografia logica" di quella posizione.

Invece di ragionare direttamente su tutte le parole infinite, il tableau ragiona su sequenze infinite di atomi. Ogni sequenza di atomi rappresenta una possibile evoluzione temporale della verita' delle sottoformule.

8. Regole temporali: next e until

Gli operatori temporali creano vincoli tra posizioni successive.

Next

Se in un atomo $A$ compare $X\varphi$, allora nel prossimo atomo $B$ deve comparire $\varphi$:

$$X\varphi\in A \quad \Rightarrow \quad \varphi\in B.$$

Questo e' il caso piu' semplice: $X$ parla direttamente dello stato successivo.

Until

L'operatore until e' piu' delicato. La formula:

$$\varphi U \psi$$

significa che $\psi$ deve diventare vera in qualche posizione futura e, prima di quel momento, deve valere $\varphi$.

La sua espansione ricorsiva e':

$$\varphi U \psi \equiv \psi \lor (\varphi\land X(\varphi U \psi)).$$

Questa equivalenza spiega perche l'until genera una promessa:

• se $\psi$ vale ora, l'obbligo e' realizzato;
• se $\psi$ non vale ora, allora deve valere $\varphi$ ora e l'obbligo deve continuare nel prossimo stato.

Senza un controllo globale, il tableau potrebbe rimandare l'obbligo per sempre. Per questo servono le condizioni di fulfilling.

9. Promesse e cammini fulfilling

Una formula eventuale, come $Fq$ o $\varphi U \psi$, promette che qualcosa succedera' prima o poi.

Ricorda che:

$$Fq \equiv true\ U\ q.$$

Quindi anche $Fq$ e' una promessa: q deve comparire in una posizione futura.

Un cammino infinito nel tableau e' fulfilling se ogni promessa che resta attiva viene prima o poi realizzata.

Perche non basta un ciclo qualsiasi

Considera:

$$Fq.$$

Un tableau potrebbe avere un ciclo in cui l'obbligo $Fq$ viene mantenuto per sempre, ma $q$ non compare mai. Quel ciclo e' localmente coerente, perche' ogni passo dice "q arrivera' dopo", ma globalmente e' sbagliato.

Il vincolo fulfilling elimina proprio questi falsi cammini.

Questa e' una delle idee piu' importanti del capitolo: la correttezza temporale non e' solo locale. Bisogna garantire che le eventualita' vengano davvero realizzate.

10. SCC, terminal SCC e MCSCS

Il tableau e' finito. Ogni cammino infinito in un grafo finito prima o poi ripete stati e resta dentro una componente fortemente connessa.

Una SCC e' un insieme di nodi in cui ogni nodo e' raggiungibile da ogni altro nodo dell'insieme.

Per controllare la soddisfacibilita' LTL si cercano componenti che possano sostenere un cammino infinito fulfilling.

Negli appunti compaiono:

• terminal SCC: componente fortemente connessa senza uscite rilevanti;
• MCSCS: componente fortemente connessa massimale usata per rappresentare una parte ciclica del tableau;
• componente fulfilling: componente in cui ogni promessa attiva puo' essere realizzata.

Perche le SCC decidono il problema

Una computazione infinita in un grafo finito ha sempre una parte prefisso e una parte ciclica:

$$\text{prefisso finito} + \text{ciclo ripetuto/in SCC}.$$

Quindi, invece di cercare direttamente una parola infinita, basta cercare:

1. un nodo iniziale coerente con la formula;
2. un cammino finito verso una SCC;
3. una SCC che realizza le promesse.

Se questa struttura esiste, la formula e' soddisfacibile. Se non esiste, non c'e' nessun cammino infinito che soddisfa la formula.

11. Esempio: perche $G p \land F\neg p$ e' insoddisfacibile

La formula:

$$G p \land F\neg p$$

richiede due cose:

• $G p$: p deve valere in ogni posizione;
• $F\neg p$: prima o poi deve esistere una posizione in cui p e' falso.

La prima richiesta impedisce la seconda. Nel tableau, ogni atomo raggiungibile che rispetta $G p$ deve contenere $p$. Ma la promessa $F\neg p$ richiede prima o poi un atomo con $\neg p$.

Non esiste una SCC fulfilling: o mantieni sempre $p$, e allora non realizzi $F\neg p$, oppure realizzi $\neg p$, ma violi $G p$.

Questo esempio mostra bene perche' le promesse non possono essere ignorate.

12. Dal tableau al model checking LTL

Il tableau da solo decide se una formula e' soddisfacibile in astratto. Nel model checking, pero', non vogliamo sapere se $\neg\varphi$ e' soddisfacibile in generale. Vogliamo sapere se e' soddisfacibile da una computazione concreta del sistema.

Per questo si costruisce il behavior graph, che combina:

• il grafo delle computazioni del programma;
• il tableau della formula;
• la compatibilita' tra stati del programma e atomi logici.

Questo e' un prodotto tra modello e formula.

13. P-SAT e P-VALID

Gli appunti distinguono due problemi.

P-SAT

$P$-SAT chiede se esiste una computazione del programma $P$ che soddisfa una formula $\varphi$.

In forma intuitiva:

$$P\models_{sat}\varphi \quad \text{se esiste una run di }P\text{ che soddisfa }\varphi.$$

E' una domanda esistenziale.

P-VALID

$P$-VALID chiede se tutte le computazioni del programma $P$ soddisfano $\varphi$.

In forma intuitiva:

$$P\models \varphi \quad \text{se ogni run di }P\text{ soddisfa }\varphi.$$

E' una domanda universale.

Collegamento tra P-SAT e P-VALID

Il collegamento e':

$$P\models \varphi \quad \Longleftrightarrow \quad \text{non esiste una run di }P\text{ che soddisfa }\neg\varphi.$$

Quindi:

$$P\text{-VALID}(\varphi) \quad \Longleftrightarrow \quad \neg P\text{-SAT}(\neg\varphi).$$

Questo spiega perche' l'algoritmo cerca spesso la negazione: trovare una run che soddisfa $\neg\varphi$ significa trovare un controesempio alla validita' di $\varphi$.

14. Behavior graph

Il behavior graph sincronizza il sistema con la formula.

Un nodo ha forma:

$$ (s,A) $$

dove:

• $s$ e' uno stato del programma o della struttura di Kripke;
• $A$ e' un atomo del tableau;
• $A$ deve essere compatibile con le proposizioni vere in $s$.

La compatibilita' significa:

$$p\in A \quad \Longleftrightarrow \quad p\in L(s)$$

per le proposizioni atomiche osservabili.

Un arco:

$$ (s,A)\to(s',A') $$

esiste quando:

• $R(s,s')$ e' una transizione del sistema;
• $A\to A'$ e' un arco del tableau;
• le condizioni di next e until sono rispettate.

Perche il prodotto funziona

Il sistema dice quali stati possono seguire quali altri stati. Il tableau dice quali configurazioni logiche possono seguire quali altre configurazioni logiche.

Il behavior graph tiene solo le coppie in cui queste due evoluzioni sono compatibili.

Quindi un cammino infinito nel behavior graph corrisponde a:

1. una computazione reale del sistema;
2. una valutazione coerente della formula lungo quella computazione.

Se il cammino e' fulfilling per la formula $\neg\varphi$, allora e' un controesempio reale a $\varphi$.

Mini-prodotto tracciato nodo per nodo

Esempio piccolo ma completo, da saper rifare. Programma $P$: due stati che si alternano per sempre,

s0 (p vera)  <-->  s1 (p falsa)

Formula da testare su $P$: $\psi = Gp$. Chiusura: $\Phi_\psi = \{Gp, \neg Gp, p, \neg p, XGp, \neg XGp\}$. Gli atomi rilevanti (insiemi massimali consistenti, con la regola $Gp \approx p\land XGp$):

• $A_1 = \{Gp,\ p,\ XGp\}$ — "$p$ vale e varra' per sempre";
• $A_2 = \{\neg Gp,\ p,\ \neg XGp\}$ — "$p$ vale ora ma prima o poi cadra'" (da $\neg Gp \approx \neg p \lor X\neg Gp$, con $p$ vera resta $X\neg Gp$);
• $A_3 = \{\neg Gp,\ \neg p,\ \neg XGp\}$ — "$p$ e' gia' falsa".

Costruzione dei nodi (compatibilita' atomo–stato sulle lettere):

• $s_0$ ha $p$ vera $\Rightarrow$ compatibile con $A_1$ e $A_2$: nodi $(s_0, A_1)$, $(s_0, A_2)$;
• $s_1$ ha $p$ falsa $\Rightarrow$ compatibile solo con $A_3$: nodo $(s_1, A_3)$.

Costruzione degli archi (serve sia $R(s,s')$ sia la coerenza dei next: $X\chi\in A \iff \chi\in A'$):

• $(s_0, A_1)\to(s_1, A_3)$? $R(s_0,s_1)$ ✓, ma $XGp\in A_1$ richiede $Gp\in A_3$ — falso. Nessun arco: $(s_0,A_1)$ e' terminale;
• $(s_0, A_2)\to(s_1, A_3)$? $R$ ✓, $\neg XGp\in A_2$ e $\neg Gp\in A_3$ ✓. Arco;
• $(s_1, A_3)\to(s_0, A_2)$? $R$ ✓, $\neg XGp\in A_3$ e $\neg Gp\in A_2$ ✓. Arco. (Verso $(s_0,A_1)$ no: servirebbe $Gp\in A_1$ ✓ ma $\neg XGp\in A_3$ lo vieta.)

Risultato: $(s_0,A_1)$ — l'unico nodo in cui $Gp$ e' vera — non ha successori e viene potato. Resta il ciclo $(s_0,A_2)\leftrightarrow(s_1,A_3)$. Quindi nessuna computazione di $P$ soddisfa $Gp$ (ovvio: $P$ passa per $s_1$ dove $p$ e' falsa). Il ciclo superstite e' invece un MSCS per $\neg Gp$: la formula promette $\neg p$ (perche' $\neg Gp = F\neg p$) e il nodo $(s_1, A_3)$ contiene $\neg p$ $\Rightarrow$ fulfilling. Conclusione: P-SAT$(\neg Gp)$ = si', quindi $Gp$ non e' P-valida — con $(s_0 s_1)^\omega$ come controesempio.

Il pattern del prodotto e' tutto qui: lettere $\to$ compatibilita' dei nodi, formule $X$ $\to$ compatibilita' degli archi, promesse $\to$ analisi dei cicli.

15. Adequate subgraphs

Un adequate subgraph e' un sottografo del behavior graph che garantisce l'esistenza di una computazione infinita valida per il controllo che stiamo facendo.

Deve soddisfare, in sostanza:

• raggiungibilita' da uno stato iniziale;
• compatibilita' con le transizioni del programma;
• assenza di blocchi che impediscano la computazione infinita;
• realizzazione delle promesse temporali;
• eventuale rispetto delle condizioni di fairness, se il programma le prevede.

Se esiste un adequate subgraph per $\neg\varphi$, allora esiste una computazione del programma che viola $\varphi$.

Se non esiste nessun adequate subgraph per $\neg\varphi$, allora tutte le computazioni del programma soddisfano $\varphi$.

Perche non basta la raggiungibilita'

Un nodo del behavior graph potrebbe essere raggiungibile ma non dare origine a un cammino infinito fulfilling. Il model checking LTL non cerca solo un prefisso finito: cerca una computazione infinita.

Per questo il controllo passa da:

esiste un nodo raggiungibile?

a:

esiste una regione ciclica raggiungibile che realizza tutti gli obblighi?

Questa e' la stessa idea dell'emptiness check per automi di Buchi: serve un ciclo accettante raggiungibile, non un singolo stato accettante isolato.

Le definizioni precise (quelle da dare all'orale)

Dato il behavior graph $\mathcal{B}(P,\varphi)$ e un sottografo fortemente connesso $S$:

• $\tau$ e' enabled su un nodo $(s, A)$ se e' enabled sullo stato $s$ del programma (l'atomo non c'entra);
• $\tau$ e' taken in $S$ se esiste un $\tau$-arco tra due nodi di $S$;
• $S$ e' just se ogni $\tau\in\mathcal{J}$ e' taken in $S$ oppure disabled su qualche nodo di $S$;
• $S$ e' compassionate se ogni $\tau\in\mathcal{C}$ e' taken in $S$ oppure disabled su tutti i nodi di $S$;
• $S$ e' fair se e' just e compassionate;
• $S$ e' fulfilling se ogni formula promising di $\Phi_\varphi$ e' fulfilled da un atomo $A$ con $(s,A)\in S$ per qualche $s$;
• $S$ e' adequate se e' fair e fulfilling.

Proposizione. $P$ ha una computazione che soddisfa $\varphi$ se e solo se $\mathcal{B}(P,\varphi)$ contiene un sottografo fortemente connesso adequate.

Perche' i MSCS non bastano: l'asimmetria della compassion

Per $S'\subseteq S$ sottografi fortemente connessi:

• $S'$ just $\implies$ $S$ just, e $S'$ fulfilling $\implies$ $S$ fulfilling: sono condizioni esistenziali ("c'e' un nodo/arco con la proprieta'"), preservate passando a sottografi piu' grandi;
• $S'$ compassionate $\not\implies$ $S$ compassionate: la condizione "disabled su tutti i nodi" e' universale e puo' rompersi aggiungendo nodi.

Controesempio degli appunti: $\tau_2\in\mathcal{C}$ enabled su $s_2$ e disabled su $s_1$. Il sottografo $S' = \{(s_1, A_3)\}$ e' compassionate ($\tau_2$ disabled ovunque); il sovragrafo $S = \{(s_1,A_3),(s_2,A_4)\}$ non lo e' ($\tau_2$ enabled su un nodo ma mai taken). Quindi puo' esistere un sottografo adequate dentro un MSCS non adequate: limitarsi ai massimali non basta. Regola operativa: se un MSCS fallisce justice o fulfillingness, si scarta (sono condizioni monotone); se fallisce solo la compassion, bisogna scendere nei sottografi.

L'algoritmo ADEQUATE-SUB

Notazione: $EN(\tau, S)$ = insieme dei nodi di $S$ su cui $\tau$ e' enabled.

function adequate-sub(S: SCS) returns SCS
  if S non fulfilling   then return ∅          -- fallimento definitivo
  if S non just         then return ∅          -- fallimento definitivo
  if S compassionate    then return S          -- successo
  -- S fulfilling e just ma non compassionate:
  sia T = { τ ∈ C non taken in S }             -- EN(T,S) ≠ ∅
  U := S − EN(T, S)                            -- togli i nodi "colpevoli"
  decomponi U in MSCS U1, ..., Uk
  for i = 1..k:
     V := adequate-sub(Ui)
     if V ≠ ∅ then return V
  return ∅

L'idea: i nodi in cui una transizione compassionate e' enabled ma mai taken non possono stare in un ciclo fair; li rimuovo, ri-decompongo in MSCS e ricontrollo ricorsivamente.

L'esempio LOOP+ (riassunto operativo)

Sistema LOOP+ con $\mathcal{J} = \{\tau_1,\tau_2\}$, $\mathcal{C} = \{\tau_3\}$ ($\tau_3$ porta da $s_1$ a $s_3$), formula $\psi: \Diamond\Box(x\neq 3)$. MSCS candidato: $S = \{(s_0,A_7),(s_1,A_7),(s_2,A_7)\}$.

• fulfilling: $\psi$ promette $\Box(x\neq 3)$, e $\Box(x\neq 3)\in A_7$ ✓
• just: $\tau_1, \tau_2$ sono taken in $S$ ✓
• non compassionate: $\tau_3$ non e' taken in $S$ ma e' enabled su $(s_1, A_7)$ ✗

ADEQUATE-SUB rimuove $(s_1,A_7)$: resta $U = \{(s_0,A_7),(s_2,A_7)\}$, dove $\tau_3$ non e' enabled da nessuna parte. $U$ e' fortemente connesso, fulfilling e fair $\Rightarrow$ adequate: LOOP+ ha una computazione $(s_0 s_2)^\omega$ che soddisfa $\Diamond\Box(x\neq 3)$. Nota il contrasto con LOOP (senza $\tau_3$): li' il behavior graph per la stessa $\psi$ non aveva sottografi adequate — i cicli su $A_5/A_4$ erano fair ma non fulfilling ($\psi$ promette $\Box(x\neq 3)$ che non sta in nessuno dei due atomi), quelli su $A_7$ fulfilling ma non just rispetto a $\tau$ — quindi LOOP soddisfa la negazione $\Box\Diamond(x=3)$.

16. Algoritmo LTL model checking

Per verificare:

$$P\models\varphi$$

si procede cosi':

1. si costruisce la negazione $\neg\varphi$;
2. si costruisce il tableau di $\neg\varphi$;
3. si costruisce il behavior graph combinando programma e tableau;
4. si cercano adequate subgraphs, cioe' SCC raggiungibili e fulfilling;
5. se una SCC adeguata esiste, la proprieta' e' falsa e la SCC produce un controesempio;
6. se non esiste, la proprieta' e' vera per tutte le computazioni del programma.

Complessita' intuitiva

La parte costosa e' la formula LTL: il tableau puo' essere esponenziale nella dimensione della formula. Questo e' coerente con il fatto che LTL model checking ha complessita' piu' alta rispetto a CTL.

Pero' nella dimensione del sistema, una volta fissata la formula, il controllo e' simile a una visita di grafo/prodotto con ricerca di SCC.

17. Model checking CTL

CTL ha un algoritmo diverso perche' le formule CTL sono formule di stato.

La domanda:

$$K,s\models \varphi$$

si risolve calcolando l'insieme:

$$Sat(\varphi)=\{s\in S \mid K,s\models\varphi\}.$$

Poi il modello soddisfa $\varphi$ se:

$$S_0\subseteq Sat(\varphi).$$

18. Algoritmo di labeling

Questo algoritmo e' spesso chiamato anche CTL labeling algorithm, perche' etichetta progressivamente ogni stato con le sottoformule CTL che risultano vere in quello stato.

L'algoritmo CTL lavora bottom-up sulle sottoformule.

Per ogni sottoformula $\psi$, calcola gli stati in cui $\psi$ e' vera. Alla fine controlla la formula completa.

Per le proposizioni atomiche:

$$Sat(p)=\{s\in S \mid p\in L(s)\}.$$

Per i booleani:

$$Sat(\neg\psi)=S\setminus Sat(\psi).$$

$$Sat(\psi_1\land\psi_2)=Sat(\psi_1)\cap Sat(\psi_2).$$

Il punto interessante sono gli operatori temporali.

19. Predecessori

Per CTL serve spesso calcolare da quali stati si puo' andare in un insieme target $X$.

La preimmagine esistenziale e':

$$Pre_E(X)=\{s\in S \mid \exists s'.\ R(s,s')\land s'\in X\}.$$

La preimmagine universale e':

$$Pre_A(X)=\{s\in S \mid \forall s'.\ R(s,s')\Rightarrow s'\in X\}.$$

Queste definizioni spiegano gli operatori next:

$$Sat(EX\varphi)=Pre_E(Sat(\varphi)).$$

$$Sat(AX\varphi)=Pre_A(Sat(\varphi)).$$

20. EF come minimo punto fisso

$EF\varphi$ significa:

esiste un cammino lungo cui prima o poi si raggiunge uno stato che soddisfa $\varphi$.

Si calcola partendo dagli stati che gia' soddisfano $\varphi$ e andando all'indietro:

$$Z_0=Sat(\varphi).$$

$$Z_{i+1}=Z_i\cup Pre_E(Z_i).$$

Quando $Z_{i+1}=Z_i$, abbiamo trovato tutti gli stati da cui esiste un cammino verso $\varphi$.

Questo e' un minimo punto fisso perche' si parte dal minimo insieme necessario e si aggiungono stati finche' non cambia piu' nulla.

21. AF come minimo punto fisso universale

$AF\varphi$ significa:

su tutti i cammini, prima o poi si raggiunge $\varphi$.

Si parte ancora da:

$$Z_0=Sat(\varphi).$$

Poi si aggiungono gli stati da cui tutti i successori sono gia' in $Z_i$:

$$Z_{i+1}=Z_i\cup Pre_A(Z_i).$$

La differenza con EF e' il quantificatore:

• EF usa "esiste un successore buono";
• AF usa "tutti i successori sono buoni".

Questo rispecchia esattamente la differenza tra possibilita' e garanzia.

22. EG come massimo punto fisso

$EG\varphi$ significa:

esiste un cammino infinito lungo cui $\varphi$ resta sempre vera.

Qui non cerchiamo un target da raggiungere. Cerchiamo una regione in cui si puo' restare per sempre.

Si parte da tutti gli stati che soddisfano $\varphi$:

$$Z_0=Sat(\varphi).$$

Poi si eliminano gli stati che non hanno un successore dentro la regione:

$$Z_{i+1}=Sat(\varphi)\cap Pre_E(Z_i).$$

Quando il punto fisso si stabilizza, $Z$ contiene gli stati da cui esiste almeno un cammino infinito che rimane sempre in $\varphi$.

E' un massimo punto fisso perche' si parte da una regione grande e si rimuovono gli stati che non possono sostenere il comportamento infinito.

23. AG come duale di EF

$AG\varphi$ significa:

su tutti i cammini, $\varphi$ vale sempre.

Si puo' calcolare direttamente, ma spesso e' piu' chiaro usare la dualita':

$$AG\varphi \equiv \neg EF\neg\varphi.$$

Perche funziona?

Dire che $\varphi$ vale sempre su tutti i cammini equivale a dire che non esiste un cammino che prima o poi raggiunge uno stato in cui $\varphi$ e' falsa.

Quindi:

1. calcolo gli stati da cui e' possibile raggiungere $\neg\varphi$;
2. prendo il complemento.

24. EU come minimo punto fisso

$E(\varphi U \psi)$ significa:

esiste un cammino in cui $\psi$ viene raggiunta e, prima di quel momento, $\varphi$ resta vera.

Si calcola con:

$$Z_0=Sat(\psi).$$

$$Z_{i+1}=Z_i\cup(Sat(\varphi)\cap Pre_E(Z_i)).$$

La formula aggiunge stati che:

• soddisfano $\varphi$ ora;
• hanno almeno un successore gia' buono.

Il punto fisso finale e' l'insieme degli stati da cui esiste un cammino che realizza l'until.

25. AU come garanzia universale

$A(\varphi U \psi)$ significa:

su tutti i cammini, $\psi$ deve arrivare, e prima del suo arrivo deve valere $\varphi$.

La forma diretta usa una preimmagine universale:

$$Z_0=Sat(\psi).$$

$$Z_{i+1}=Z_i\cup(Sat(\varphi)\cap Pre_A(Z_i)).$$

Anche qui la differenza con EU e' il quantificatore:

• EU richiede almeno una scelta che porta avanti l'obiettivo;
• AU richiede che tutte le scelte possibili portino avanti l'obiettivo.

Gli algoritmi espliciti degli appunti: CheckEU e CheckAU

Oltre alla vista "a punti fissi sugli insiemi", gli appunti danno le procedure ricorsive di marcatura (stile Clarke-Emerson), che e' utile saper scrivere.

Per $E(\gamma\,U\,\delta)$: si parte dagli stati che soddisfano $\delta$ e si propaga all'indietro lungo i predecessori che soddisfano $\gamma$.

procedure CheckEU(M, w, γ, δ):        -- chiamata su ogni w con δ ∈ V(w)
  V(w) := V(w) ∪ {E(γ U δ)}           -- marca w
  for ogni v tale che R(v, w):        -- predecessori di w
     if E(γ U δ) ∉ V(v) and γ ∈ V(v):
        CheckEU(M, v, γ, δ)

Ogni stato viene marcato al piu' una volta e ogni arco visitato un numero costante di volte: tempo lineare in $|S| + |R|$ per sottoformula.

Per $A(\gamma\,U\,\delta)$ la propagazione all'indietro non basta marcare un predecessore appena lo si tocca: bisogna verificare che tutti i suoi successori siano gia' buoni. La procedura degli appunti esplora in avanti con marcatura:

function CheckAU(M, w, γ, δ) returns Bool:
  if marked(w):                        -- gia' visitato
     return (A(γ U δ) ∈ V(w))
  mark(w)
  if δ ∈ V(w):
     V(w) := V(w) ∪ {A(γ U δ)}; return True
  if γ ∉ V(w): return False
  for ogni v tale che R(w, v):         -- tutti i successori
     if not CheckAU(M, v, γ, δ): return False
  V(w) := V(w) ∪ {A(γ U δ)}; return True

Se un solo successore fallisce, $A(\gamma U \delta)$ e' falsa in $w$; serve inoltre attenzione ai cicli (uno stato gia' in visita senza marca positiva non puo' garantire l'arrivo di $\delta$: e' il caso del cammino che gira per sempre dentro $\gamma$). Il quadro complessivo dell'algoritmo di labeling: si elaborano le sottoformule in ordine crescente di lunghezza (come nel caso modale), e alla fine si controlla se $s_0\in[\varphi]$. Complessita' totale: $O(|\varphi|\cdot(|S|+|R|))$ — lineare sia nella formula sia nel modello, il grande vantaggio pratico di CTL.

26. Esempio CTL: calcolo di EF

Supponi di avere tre stati:

$$s_0\to s_1,\quad s_1\to s_2,\quad s_2\to s_2.$$

e supponi che $goal$ valga solo in $s_2$.

Calcoliamo $EF\ goal$.

Passo iniziale:

$$Z_0=\{s_2\}.$$

Predecessori esistenziali:

$$Pre_E(Z_0)=\{s_1,s_2\}.$$

Quindi:

$$Z_1=\{s_1,s_2\}.$$

Altro passo:

$$Pre_E(Z_1)=\{s_0,s_1,s_2\}.$$

Quindi:

$$Z_2=\{s_0,s_1,s_2\}.$$

Il punto fisso e' raggiunto. Tutti gli stati soddisfano $EF\ goal$.

Il motivo e' semplice: da ogni stato esiste un cammino che arriva a $goal$.

27. Esempio CTL: differenza tra EF e AF

Aggiungi da $s_0$ un secondo ramo verso uno stato morto $s_3$, con self-loop, in cui $goal$ non vale:

$$s_0\to s_1,\quad s_0\to s_3,\quad s_3\to s_3.$$

Allora:

• $s_0\models EF\ goal$, perche' esiste il ramo verso $s_1,s_2$;
• $s_0\not\models AF\ goal$, perche' esiste anche il ramo verso $s_3$ che non raggiunge mai goal.

Questo e' il punto concettuale di CTL: distingue possibilita' e inevitabilita'.

28. Esempio CTL: EG

$EG\ safe$ chiede se esiste un cammino infinito che resta sempre safe.

Se una SCC contiene solo stati safe e ha almeno un ciclo interno, allora gli stati che possono entrare in quella SCC possono soddisfare $EG\ safe$.

Il calcolo a massimo punto fisso rimuove progressivamente gli stati safe che non riescono a restare dentro una regione safe.

Per questo EG e' legato all'idea di regione chiusa: non basta che safe valga adesso, deve essere possibile mantenerlo per sempre.

29. Perche CTL e' spesso piu efficiente di LTL

Nel model checking CTL, ogni sottoformula produce un insieme di stati. Gli operatori temporali si calcolano con visite di grafo o punti fissi.

In termini intuitivi:

$$\text{costo CTL} \approx |formula|\cdot |modello|.$$

Nel model checking LTL, invece, bisogna costruire una struttura per la negazione della formula e combinarla con il sistema. La parte formula puo' crescere esponenzialmente.

Quindi:

• CTL e' piu' locale e algoritmicamente diretto;
• LTL e' spesso piu' naturale per specifiche lineari di fairness e liveness;
• la scelta della logica influenza direttamente la forma dell'algoritmo.

30. Differenza tra soddisfacibilita' e model checking

La soddisfacibilita' chiede:

esiste un modello o un cammino che soddisfa la formula?

Il model checking chiede:

il modello dato soddisfa la formula?

Per LTL:

• soddisfacibilita': cerco un cammino astratto che soddisfi $\varphi$;
• model checking: cerco un cammino del sistema che soddisfi $\neg\varphi$.

Per CTL:

• soddisfacibilita': esiste una struttura di Kripke con uno stato che soddisfa la formula?
• model checking: nella struttura data, quali stati soddisfano la formula?

Non confondere questi problemi: usano strumenti simili, ma rispondono a domande diverse.

31. Errori tipici

Confondere $F$ con $EF$

$F\varphi$ e' LTL: parla di un singolo cammino.

$EF\varphi$ e' CTL: parla di uno stato e dice che esiste almeno un cammino verso $\varphi$.

Confondere $G$ con $AG$

$G\varphi$ e' LTL: lungo il cammino corrente, $\varphi$ vale sempre.

$AG\varphi$ e' CTL: da questo stato, su tutti i cammini, $\varphi$ vale sempre.

Pensare che un ciclo basti sempre

Nel tableau LTL non basta un ciclo. Serve un ciclo fulfilling, cioe' un ciclo che realizza le eventualita'.

Pensare che EF implichi AF

EF dice "posso arrivare". AF dice "devo arrivare qualunque cosa succeda".

Sono proprieta' molto diverse nei sistemi non deterministici.

32. Mappa operativa del capitolo

Se devi ricostruire il capitolo all'orale, segui questa sequenza:

1. Un sistema reattivo genera computazioni infinite.
2. Una struttura di Kripke modella stati, transizioni e proposizioni vere.
3. LTL valuta formule su cammini; CTL valuta formule su stati con quantificatori di cammino.
4. Per verificare una formula LTL, cerco un controesempio per la negazione.
5. Il tableau LTL trasforma la formula in un grafo finito di atomi.
6. Le formule until/eventually generano promesse che devono essere fulfilling.
7. Il behavior graph combina sistema e tableau.
8. Un adequate subgraph raggiungibile per $\neg\varphi$ e' un controesempio.
9. CTL si calcola invece con labeling di stati.
10. EX/AX usano preimmagini, EF/AF/EU/AU usano minimi punti fissi, EG/AG usano massimi punti fissi o dualita'.

33. Mini-esercizi guidati

Esercizio 1

Formula:

$$G(req\to F grant).$$

Spiegazione: ogni richiesta deve essere prima o poi seguita da una concessione.

Per falsificarla serve una computazione in cui:

• a un certo punto vale $req$;
• da quel punto in poi $grant$ non arriva mai.

Quindi il controesempio ha forma:

$$\text{prefisso fino a req} + \text{ciclo senza grant}.$$

Questo spiega perche' nel model checking LTL si cercano cicli.

Esercizio 2

Formula CTL:

$$AG(request\to AF grant).$$

Spiegazione: in ogni stato raggiungibile, se c'e' una richiesta, allora su tutti i cammini futuri prima o poi arrivera' grant.

Questa e' piu' forte della versione esistenziale:

$$AG(request\to EF grant).$$

La seconda dice solo che grant resta possibile; la prima dice che grant e' garantito.

Esercizio 3

Formula:

$$EG\ safe.$$

Metodo:

1. prendi tutti gli stati safe;
2. elimina quelli che non hanno successori safe;
3. ripeti fino al punto fisso.

Gli stati rimasti sono quelli da cui esiste un cammino infinito sempre safe.

34. Riassunto finale

Il capitolo 8 e' il punto in cui la teoria diventa algoritmo.

Per LTL, la domanda universale "tutte le computazioni soddisfano $\varphi$" si trasforma nella ricerca esistenziale di un controesempio per $\neg\varphi$. Tableau, behavior graph e adequate subgraphs servono a rendere finita questa ricerca su cammini infiniti.

Per CTL, la semantica di stato permette un algoritmo piu' diretto: si calcolano insiemi di stati con labeling e punti fissi. Gli operatori esistenziali usano preimmagini esistenziali; quelli universali usano preimmagini universali o duali.

La regola mentale da tenere e':

LTL cerca cicli accettanti nel prodotto sistema-formula; CTL propaga insiemi di stati fino a un punto fisso.