Model checking simbolico e limitato - Riassunto

Fonte: raw/Symbolic MC and Bounded MC.md

Punti chiave

• Lo state explosion problem rende impraticabile l'esplorazione esplicita di sistemi con moltissimi stati.
• Il model checking simbolico rappresenta insiemi di stati e transizioni tramite formule booleane invece di enumerarli.
• Gli OBDD rappresentano funzioni booleane come DAG ridotti e ordinati; sono centrali per CTL simbolico e calcolo di punti fissi.
• Il BMC cerca controesempi fino a un bound $k$ traducendo il problema in SAT.
• BMC e' molto efficace come bug finder, ma per dimostrare correttezza completa puo richiedere bound difficili da calcolare.

Concetti estratti

• Model checking simbolico
• Diagrammi di decisione binaria ordinati (OBDD)
• Model checking limitato

Model checking simbolico

Il model checking simbolico rappresenta insiemi di stati e transizioni tramite formule o strutture simboliche, invece di enumerare ogni stato esplicitamente.

Motivazione

Serve ad affrontare lo state explosion problem, tipico dei sistemi con molte componenti concorrenti.

Tecniche

• OBDD per rappresentare funzioni booleane;
• calcolo simbolico di preimmagini;
• punti fissi per CTL;
• metodi basati su SAT, come model checking limitato.

Collegamenti

• Model checking
• Diagrammi di decisione binaria ordinati (OBDD)
• Model checking limitato

Diagrammi di decisione binaria ordinati

Gli OBDD sono grafi aciclici diretti usati per rappresentare funzioni booleane in modo compatto.

Idea

Si parte da un decision tree e si riducono ridondanze: - si fondono sottografi isomorfi; - si eliminano test inutili; - si usa un ordine fisso delle variabili.

Canonicita

Per una funzione booleana e un ordine fissato delle variabili, l'OBDD ridotto e' canonico. Questo rende efficiente il controllo di equivalenza tra funzioni.

Operazioni

Negazione, congiunzione, disgiunzione, restrict e quantificazione esistenziale possono essere implementate direttamente sugli OBDD.

Ruolo nel model checking

Gli OBDD rappresentano insiemi di stati, relazioni di transizione e risultati di punti fissi nel model checking simbolico.

Collegamenti

• Model checking simbolico
• Model checking limitato

Model checking limitato

Il Bounded Model Checking (BMC), o model checking limitato, cerca controesempi a una proprieta fino a una profondita fissata $k$.

Invece di esplorare tutto lo spazio degli stati, il sistema viene srotolato per $k$ passi e il problema viene codificato come formula proposizionale:

$$\llbracket M \rrbracket_k \land \llbracket \neg\varphi \rrbracket_k$$

Se la formula e' soddisfacibile, esiste una traccia di lunghezza limitata che viola la proprieta.

Lasso e LTL

Poiche LTL parla di cammini infiniti, BMC usa spesso cammini finiti con loopback, cioe' cammini a forma di lasso che rappresentano parole infinite ultimamente periodiche.

Punto forte e limite

BMC e' molto efficace per trovare bug; per dimostrare assenza di bug puo richiedere bound completi costosi da calcolare.

Collegamenti

• Model checking simbolico
• Logica temporale lineare (LTL)
• Diagrammi di decisione binaria ordinati (OBDD)

Approfondimento completo settimana 5 - Model checking simbolico, OBDD e BMC

Questa e' la versione estesa e autocontenuta del capitolo, riscritta passo passo. Ogni formula viene prima motivata, poi enunciata, poi riletta in parole. Gli esempi sono svolti riga per riga. Nessun passaggio e' dato per scontato: se una sezione usa un concetto, quel concetto e' stato introdotto prima (o richiamato nella sezione 0).

Di cosa parla davvero questo capitolo

Il capitolo 8 ha consegnato algoritmi di model checking concettualmente chiari: dato un modello $K$ e una formula temporale $\varphi$, sappiamo decidere se $K\models\varphi$ visitando stati e transizioni. Il problema e' che nei sistemi reali gli stati sono troppi per essere visitati uno a uno. Negli appunti viene dato anche un numero: i model checker espliciti arrivavano a circa $10^6$ stati, mentre le tecniche di questo capitolo permettono di verificare sistemi con oltre $10^{20}$ stati.

Il capitolo presenta tre risposte al problema, e conviene capire subito che non sono varianti della stessa idea:

• Symbolic model checking con OBDD: non si elencano piu' gli stati; un intero insieme di stati diventa una formula booleana, e le formule booleane vengono manipolate con una struttura dati efficiente (gli OBDD). Serve soprattutto per dimostrare proprieta' su tutto il modello.
• Bounded model checking (BMC) con SAT: si rinuncia (inizialmente) a dimostrare; si cerca un controesempio di lunghezza al massimo $k$, traducendo la ricerca in un problema SAT. Serve soprattutto per trovare bug.
• Partial-order reduction: si attacca la causa specifica di esplosione dovuta alla concorrenza, evitando di esplorare interleaving equivalenti.

Il percorso del capitolo e' lungo, quindi ecco la mappa:

1. Parte I: perche' gli stati esplodono e perche' serve cambiare rappresentazione.
2. Parte II: come si rappresentano stati, insiemi di stati e transizioni con formule booleane.
3. Parte III: la teoria dei punti fissi, cioe' il motore matematico che permette di calcolare CTL su queste rappresentazioni.
4. Parte IV: gli OBDD, la struttura dati che rende tutto questo eseguibile.
5. Parte V: l'algoritmo CHECK, cioe' CTL simbolico completo.
6. Parte VI: partial-order reduction.
7. Parte VII: BMC, con l'encoding SAT completo (unrolling, lasso, bounded semantics) e uno sguardo a nuXmv.
8. Parte VIII: confronto fra le tecniche, errori tipici, esercizi e mappa per l'orale.

0. Richiami minimi (per non dare nulla per scontato)

Struttura di Kripke. Un modello $K=(S,S_0,R,L)$ dove $S$ e' l'insieme finito degli stati, $S_0\subseteq S$ gli stati iniziali, $R\subseteq S\times S$ la relazione di transizione (totale: ogni stato ha almeno un successore) e $L$ assegna a ogni stato le lettere proposizionali vere in esso.

Operatori CTL. Ogni operatore temporale e' preceduto da un quantificatore di cammino: $E$ = "esiste un cammino", $A$ = "per tutti i cammini". Letture in parole:

SAT. Data una formula proposizionale, il problema SAT chiede se esiste un assegnamento di verita' alle variabili che la rende vera. I SAT solver moderni risolvono in pratica istanze con milioni di variabili; e' questa efficienza che il BMC sfrutta.

QBF. Le formule booleane quantificate ($\exists x.\,f$, $\forall x.\,f$) non aggiungono potere espressivo rispetto alle formule proposizionali (ogni quantificatore si puo' eliminare), ma permettono di scrivere formule molto piu' succinte. Questo capitolo usa i quantificatori booleani di continuo, e nella sezione 36 vedremo che eliminarli su OBDD costa solo due restrict e un apply.

Parte I — Il problema: lo state explosion

1. Lo state explosion problem

Nel model checking esplicito il modello e' un grafo $K=(S,S_0,R,L)$ e gli algoritmi visitano stati e archi. Una visita costa almeno tempo proporzionale al numero di stati. Quindi tutto funziona finche' $S$ e' piccolo. Il punto critico e' che $S$ non cresce "un po' alla volta" con la taglia del sistema: cresce esponenzialmente. Questo fenomeno si chiama state explosion problem.

2. Perche' i numeri esplodono: variabili e concorrenza

Ci sono due sorgenti distinte di esplosione, e conviene saperle separare.

Prima sorgente: le variabili. Uno stato di un sistema e' una fotografia dei valori di tutte le sue variabili. Con $n$ variabili booleane le fotografie possibili sono tutte le combinazioni di valori, cioe':

$$2^n$$

Per fissare le idee:

• 10 variabili: $2^{10}=1024$ stati;
• 20 variabili: $2^{20}\approx 10^6$ stati (il limite pratico del model checking esplicito);
• 40 variabili: $2^{40}\approx 10^{12}$ stati, fuori portata per qualunque visita esplicita.

Notare che 40 variabili booleane sono pochissime: bastano 5 interi a 8 bit.

Seconda sorgente: la concorrenza. Se il sistema e' il prodotto di componenti, $\mathcal{M}=\mathcal{M}_1\times\cdots\times\mathcal{M}_n$, il numero di stati globali e' il prodotto dei numeri di stati locali, quindi di nuovo esponenziale in $n$. In piu', processi concorrenti generano interleaving: se il processo 1 fa l'azione $a$ e il processo 2 fa l'azione $b$, e le due azioni sono indipendenti, il sistema globale contiene sia l'esecuzione $a;b$ sia l'esecuzione $b;a$ — due cammini distinti che spesso, dal punto di vista della proprieta' da verificare, sono indistinguibili. Con molti processi le permutazioni possibili diventano moltissime, e il grafo esplicito le contiene tutte.

3. La svolta: cambiare rappresentazione, non algoritmo di visita

Se il grafo ha $10^{12}$ nodi, sostituire DFS con BFS o ottimizzare le strutture dati non serve a nulla: anche solo toccare ogni nodo una volta e' troppo. L'unica via d'uscita e' non costruire affatto il grafo esplicito.

L'idea del model checking simbolico e':

non elencare gli stati uno per uno; rappresentare interi insiemi di stati con una sola formula booleana, e fare i calcoli direttamente sulle formule.

Perche' questo possa funzionare servono tre ingredienti, che sono esattamente il contenuto delle prossime tre parti:

1. un modo per scrivere stati, insiemi e transizioni come formule (Parte II);
2. un modo per esprimere gli operatori CTL come calcoli su insiemi, cioe' i punti fissi (Parte III);
3. una struttura dati che renda efficienti le operazioni sulle formule, cioe' gli OBDD (Parte IV).

Parte II — Stati e transizioni come formule booleane

4. Uno stato = un assegnamento booleano

Fissiamo un vettore di variabili booleane:

$$\bar{x}=x_1,\ldots,x_n.$$

Ogni assegnamento di valori a $\bar{x}$ rappresenta uno stato. Se gli stati sono $2^m$ per qualche $m$, bastano $m$ variabili: ogni stato riceve un codice binario.

Esempio concreto con due variabili $x_1,x_2$ (quindi fino a 4 stati):

Da qui in avanti "stato" e "assegnamento alle variabili $\bar{x}$" sono la stessa cosa.

5. Un insieme di stati = una formula booleana

Un insieme di stati $A\subseteq S$ viene rappresentato da una formula $A(\bar{x})$ tale che:

uno stato appartiene ad $A$ se e solo se il suo assegnamento rende vera la formula $A(\bar{x})$.

In altre parole, la formula e' la funzione caratteristica dell'insieme: vale 1 esattamente sugli elementi dell'insieme.

Esempio, con il codice della sezione 4. La formula:

$$x_1\land\neg x_2$$

e' vera solo per l'assegnamento $x_1=1,x_2=0$: rappresenta l'insieme $\{s_{10}\}$, un singolo stato. Invece la formula:

$$x_1$$

e' vera per due assegnamenti ($s_{10}$ e $s_{11}$): rappresenta un insieme di due stati. Con $n$ variabili, la formula $x_1$ (una sola lettera!) rappresenta $2^{n-1}$ stati.

Questo e' il motivo per cui la rappresentazione simbolica puo' essere compatta: la taglia della formula non dipende dal numero di stati dell'insieme, ma dalla regolarita' dell'insieme. Un insieme enorme ma regolare ha una formula piccola. Le operazioni insiemistiche diventano connettivi:

• unione $\cup$ $\to$ disgiunzione $\lor$;
• intersezione $\cap$ $\to$ congiunzione $\land$;
• complemento $\to$ negazione $\neg$;
• inclusione $A\subseteq B$ $\to$ validita' di $A\to B$;
• uguaglianza di insiemi $\to$ equivalenza logica delle formule.

L'ultima riga e' importante: per sapere se due insiemi sono uguali bisogna saper decidere l'equivalenza di due formule booleane. Tenere a mente questo punto: e' la ragione per cui la canonicita' degli OBDD (sezione 32) sara' preziosa.

6. La relazione di transizione: $R(\bar{x},\bar{x}')$ e le variabili primate

Una transizione collega due stati: quello di partenza e quello di arrivo. Per parlarne in una sola formula servono due copie delle variabili:

• $\bar{x}=x_1,\ldots,x_n$ per lo stato corrente;
• $\bar{x}'=x_1',\ldots,x_n'$ per lo stato successivo.

La relazione di transizione diventa una formula su entrambe le copie:

$$R(\bar{x},\bar{x}').$$

Come leggerla: la coppia di stati $(s,s')$ e' una transizione del sistema se e solo se l'assegnamento che descrive $s$ sulle variabili $\bar{x}$ e l'assegnamento che descrive $s'$ sulle variabili $\bar{x}'$ rendono vera $R$.

Perche' servono le variabili primate? Se usassimo le stesse variabili per prima e dopo, non potremmo dire "il valore cambia". La formula:

$$x'\leftrightarrow\neg x$$

dice: "il prossimo valore di $x$ e' l'opposto del valore attuale". Senza la copia primata questa frase non e' nemmeno scrivibile.

Esempio completo (dagli appunti). Sistema con due variabili $x_1,x_2$ e tre transizioni, che descriviamo arco per arco:

1. dallo stato $11$ allo stato $10$;
2. dallo stato $10$ allo stato $11$;
3. dallo stato $10$ a se stesso.

Ogni arco diventa una congiunzione che fissa tutte le variabili correnti (stato di partenza) e tutte le primate (stato di arrivo):

• arco 1: $x_1\land x_2\land x_1'\land\neg x_2'$;
• arco 2: $x_1\land\neg x_2\land x_1'\land x_2'$;
• arco 3: $x_1\land\neg x_2\land x_1'\land\neg x_2'$.

La relazione completa e' la disgiunzione degli archi:

$$R(\bar{x},\bar{x}')= (x_1\land x_2\land x_1'\land\neg x_2')\lor (x_1\land\neg x_2\land x_1'\land x_2')\lor (x_1\land\neg x_2\land x_1'\land\neg x_2').$$

Come leggerla: "la coppia $(s,s')$ e' una transizione se e' l'arco 1, oppure l'arco 2, oppure l'arco 3". Questa costruzione arco-per-arco funziona per qualunque struttura di Kripke; nei casi reali, pero', non si elencano gli archi (sarebbero troppi): si scrive direttamente una formula compatta, come $x'\leftrightarrow\neg x$ sopra, o come le formule TRANS di SMV che vedremo nella sezione 47.

7. Etichettatura e stati iniziali

Restano da codificare gli altri due ingredienti della struttura di Kripke.

Stati iniziali: una formula $I(\bar{x})$, vera esattamente sugli assegnamenti che codificano stati iniziali.

Etichettatura $L$: invece di dire, stato per stato, quali lettere sono vere, si rovescia il punto di vista: per ogni lettera proposizionale $p$ si da' l'insieme degli stati in cui $p$ e' vera,

$$S_p=\{s : p\in L(s)\},$$

e questo insieme, come ogni insieme di stati, e' una formula $p(\bar{x})$. Il rovesciamento e' naturale nel mondo simbolico: "la lettera $p$" e "l'insieme degli stati dove vale $p$" diventano lo stesso oggetto.

8. La domanda di safety diventa una domanda di soddisfacibilita'

Supponiamo di avere (lo costruiremo nella sezione 43) l'insieme $Reach$ degli stati raggiungibili dagli iniziali, come formula $Reach(\bar{x})$, e l'insieme $Bad$ degli stati vietati, come formula $Bad(\bar{x})$.

La proprieta' di safety "nessuno stato bad e' mai raggiunto" equivale a:

$$Reach\cap Bad=\emptyset,$$

cioe', passando alle formule: la congiunzione

$$Reach(\bar{x})\land Bad(\bar{x})$$

deve essere insoddisfacibile.

Come leggerla: se esiste un assegnamento che rende vera la congiunzione, quell'assegnamento e' uno stato raggiungibile e vietato insieme — la safety e' violata, e l'assegnamento stesso e' l'inizio del controesempio. Se nessun assegnamento la rende vera, i due insiemi sono disgiunti e la safety vale.

Questo e' un primo assaggio del tema del capitolo: le domande sul sistema diventano domande logiche sulle formule.

9. Post-immagine e preimmagini: muoversi senza enumerare

Gli algoritmi devono "camminare" sul grafo senza vederlo. I tre movimenti fondamentali sono questi.

Post-immagine (un passo in avanti). Dato un insieme $X$, vogliamo gli stati raggiungibili da $X$ con una transizione:

$$Post(X)(\bar{x}')=\exists\bar{x}.\ X(\bar{x})\land R(\bar{x},\bar{x}').$$

Come leggerla: "lo stato $\bar{x}'$ e' nella post-immagine se esiste uno stato $\bar{x}$ che sta in $X$ e da cui parte una transizione verso $\bar{x}'$". Il quantificatore esistenziale dice esattamente "esiste un predecessore in $X$"; notare che il risultato e' una formula sulle variabili primate (lo stato di arrivo).

Preimmagine esistenziale (un passo all'indietro, versione "esiste"). Dato un insieme target $T$, vogliamo gli stati da cui si puo' entrare in $T$ in un passo:

$$Pre_E(T)(\bar{x})=\exists\bar{x}'.\ R(\bar{x},\bar{x}')\land T(\bar{x}').$$

Come leggerla: "lo stato $\bar{x}$ sta nella preimmagine se esiste un suo successore $\bar{x}'$ che sta in $T$". E' la versione simbolica dell'operatore $EX$: infatti $Pre_E(T)$ e' esattamente l'insieme degli stati che soddisfano $EX\,T$.

Preimmagine universale (un passo all'indietro, versione "per tutti"). Stati i cui successori stanno tutti in $T$:

$$Pre_A(T)(\bar{x})=\forall\bar{x}'.\ R(\bar{x},\bar{x}')\to T(\bar{x}').$$

Come leggerla: "comunque si scelga un successore $\bar{x}'$ di $\bar{x}$, quel successore sta in $T$". E' la versione simbolica di $AX$.

Micro-esempio svolto. Una variabile, transizione che la inverte: $R(x,x')\equiv(x'\leftrightarrow\neg x)$. Calcoliamo $Pre_E(T)$ per $T(x')=x'$ (il target e' "lo stato in cui $x$ vale 1"):

$$Pre_E(T)(x)=\exists x'.\ (x'\leftrightarrow\neg x)\land x'.$$

Eliminiamo il quantificatore distinguendo i due valori possibili di $x'$:

• con $x'=0$: $(0\leftrightarrow\neg x)\land 0=0$ (la congiunzione con 0 e' falsa);
• con $x'=1$: $(1\leftrightarrow\neg x)\land 1=\neg x$ (la doppia implicazione con 1 lascia $\neg x$).

La disgiunzione dei due casi e' $0\lor\neg x=\neg x$. Quindi:

$$Pre_E(x')=\neg x.$$

Verifica di buon senso: il sistema inverte $x$ a ogni passo; per arrivare in uno stato con $x=1$ bisogna partire da $x=0$. Torna.

Perche' la preimmagine e' centrale. Quasi tutti gli algoritmi che vedremo ragionano all'indietro: si parte dal target e si aggiungono, strato dopo strato, gli stati che possono arrivarci. L'operazione che produce ogni nuovo strato e' la preimmagine. La struttura "ripeti finche' non cambia nulla" e' un punto fisso, ed e' l'argomento della prossima parte.

Parte III — La teoria dei punti fissi (il motore del CTL simbolico)

10. Perche' servono i punti fissi: $EF$ calcolato a mano

Prima la pratica, poi la teoria. Vogliamo gli stati che soddisfano $EF\,goal$: "esiste un cammino che prima o poi raggiunge $goal$". Ragioniamo:

• gli stati in cui $goal$ vale adesso sicuramente soddisfano $EF\,goal$;
• gli stati con un successore che soddisfa $EF\,goal$ lo soddisfano anche loro (basta fare un passo e poi seguire il cammino del successore);
• nessun altro stato lo soddisfa.

Questo suggerisce il calcolo iterativo:

$$Z_0=Goal,\qquad Z_{i+1}=Z_i\cup Pre_E(Z_i).$$

Come leggerlo: $Z_i$ contiene gli stati da cui si raggiunge $goal$ in al piu' $i$ passi. A ogni iterazione aggiungiamo gli stati che arrivano in $Z_i$ con un passo in piu'. Poiche' gli stati sono finiti e $Z_i$ puo' solo crescere, prima o poi $Z_{i+1}=Z_i$: aggiungere un passo non scopre piu' nulla. Quell'insieme stabile e' la risposta.

L'insieme a cui ci si ferma ha una proprieta' precisa: applicargli ancora l'operazione non lo cambia. Si chiama punto fisso. La teoria che segue risponde a tre domande che l'esempio lascia aperte:

1. il punto a cui ci si ferma e' unico? E' quello giusto?
2. perche' la procedura termina sempre?
3. funziona per tutti gli operatori CTL o solo per $EF$?

11. Il reticolo $Powerset(S)$

L'ambiente in cui si svolge tutto e' l'insieme dei sottoinsiemi di $S$, ordinato per inclusione. $Powerset(S)$ con l'ordine $\subseteq$ e' un reticolo: ogni famiglia di insiemi ha un'unione (estremo superiore) e un'intersezione (estremo inferiore). In particolare ha:

• un elemento minimo: $\emptyset$, che simbolicamente e' la formula $false$ (nessuno stato la soddisfa);
• un elemento massimo: $S$, che simbolicamente e' la formula $true$ (tutti gli stati la soddisfano).

Nel resto della parte III "insieme di stati", "predicato" e "formula" sono sinonimi: un predicato e' identificato dall'insieme degli stati in cui e' vero.

12. Predicate transformer

Un predicate transformer e' una funzione che trasforma insiemi di stati in insiemi di stati:

$$\tau:\ Powerset(S)\to Powerset(S).$$

Esempio concreto, che e' anche il protagonista del capitolo: fissata una formula $f_1$,

$$\tau(Z)=f_1\land EX\,Z$$

prende un insieme $Z$ e restituisce "gli stati in cui vale $f_1$ e che hanno almeno un successore dentro $Z$". E' una funzione legittima da insiemi a insiemi: dato l'input $Z$, l'output e' determinato.

Un insieme $Z$ tale che:

$$\tau(Z)=Z$$

si chiama punto fisso di $\tau$: applicare la trasformazione non lo muove. In generale $\tau$ puo' avere molti punti fissi; quelli che ci interessano sono il piu' piccolo (least fixpoint, scritto $\mu Z.\tau(Z)$) e il piu' grande (greatest fixpoint, scritto $\nu Z.\tau(Z)$).

13. Monotonia (con dimostrazione completa)

Definizione. $\tau$ e' monotona se conserva le inclusioni:

$$P\subseteq Q\ \implies\ \tau(P)\subseteq\tau(Q).$$

Come leggerla: se allargo l'input, l'output puo' solo allargarsi (o restare uguale), mai restringersi.

Tutti i predicate transformer che useremo per CTL sono monotoni. Vediamo la dimostrazione per il caso principale, che e' anche un modello di come si scrivono queste prove all'orale.

Lemma (monotonia di $\tau(Z)=f_1\land EX\,Z$). Siano $P_1\subseteq P_2$. Allora $\tau(P_1)\subseteq\tau(P_2)$.

Dimostrazione. Per dimostrare un'inclusione tra insiemi si prende un elemento generico del primo e si mostra che sta nel secondo. Sia $s\in\tau(P_1)$, cioe' $s$ soddisfa $f_1\land EX\,P_1$. Spacchettiamo cosa significa:

1. $s\models f_1$ (primo congiunto);
2. $s$ ha almeno un successore in $P_1$: esiste $s'$ con $R(s,s')$ e $s'\in P_1$ (secondo congiunto, per la semantica di $EX$).

Per ipotesi $P_1\subseteq P_2$, quindi quel medesimo successore $s'$ sta anche in $P_2$. Allora $s$ soddisfa $f_1$ e ha un successore in $P_2$, cioe' $s\in f_1\land EX\,P_2=\tau(P_2)$. $\square$

La struttura e' sempre questa: spacchettare l'appartenenza a $\tau(P_1)$, usare $P_1\subseteq P_2$ sul testimone, rimpacchettare.

14. Continuita', e perche' nel caso finito e' gratuita

Servono altre due nozioni, che enunciamo e subito ridimensioniamo (nel nostro caso finito si ottengono gratis).

Definizione. $\tau$ e' ∪-continua se per ogni catena crescente $P_1\subseteq P_2\subseteq P_3\subseteq\cdots$ vale $\tau\left(\bigcup_i P_i\right)=\bigcup_i\tau(P_i)$ (la trasformazione "commuta" con l'unione della catena). Dualmente, e' ∩-continua se per ogni catena decrescente commuta con l'intersezione.

Lemma 1. Se $\tau$ e' monotona e $S$ e' finito, allora $\tau$ e' sia ∪-continua sia ∩-continua.

Perche' e' vero. Con $S$ finito, una catena crescente di sottoinsiemi non puo' crescere per sempre: da un certo indice $m$ in poi e' costante, e l'unione dell'intera catena e' semplicemente $P_m$. Allora:

$$\tau\Big(\bigcup_i P_i\Big)=\tau(P_m).$$

D'altra parte, per monotonia, anche la catena delle immagini $\tau(P_1)\subseteq\tau(P_2)\subseteq\cdots$ e' crescente e da $m$ in poi vale $\tau(P_m)$; quindi la sua unione e' $\tau(P_m)$. I due lati coincidono. L'argomento per ∩ e' identico, rovesciando le inclusioni. $\square$

Morale: in fixpoint theory generale (insiemi infiniti) la continuita' e' un'ipotesi delicata; per noi, che lavoriamo su una struttura di Kripke finita, e' una conseguenza automatica della monotonia.

Notazione per le iterazioni. Scriviamo $\tau^i(Z)$ per "applica $\tau$ $i$ volte a $Z$":

$$\tau^0(Z)=Z,\qquad \tau^{i+1}(Z)=\tau(\tau^i(Z)).$$

15. Il teorema di Tarski, letto con calma

Teorema (Tarski). Ogni predicate transformer monotono $\tau$ ha un minimo punto fisso e un massimo punto fisso, e valgono le caratterizzazioni:

$$\mu Z.\tau(Z)=\bigcap\{Z : \tau(Z)\subseteq Z\}, \qquad \nu Z.\tau(Z)=\bigcup\{Z : Z\subseteq\tau(Z)\}.$$

Come leggerle. Un insieme con $\tau(Z)\subseteq Z$ si chiama pre-punto fisso: e' un insieme "chiuso" rispetto a $\tau$ (applicare $\tau$ non porta fuori). Il teorema dice: il minimo punto fisso e' l'intersezione di tutti gli insiemi chiusi — cioe' e' contenuto in ognuno di essi, ed e' quindi il piu' piccolo possibile. Dualmente, un insieme con $Z\subseteq\tau(Z)$ e' un post-punto fisso ("auto-sostenuto": ogni suo elemento e' giustificato da $\tau$), e il massimo punto fisso e' l'unione di tutti gli insiemi auto-sostenuti.

Per noi le due conseguenze operative sono:

• se trovo un punto fisso e dimostro che e' contenuto in ogni pre-punto fisso, quello e' $\mu$;
• se trovo un punto fisso e dimostro che contiene ogni post-punto fisso, quello e' $\nu$.

Inoltre, con la continuita' (che nel finito abbiamo gratis dal Lemma 1), i punti fissi si calcolano per iterazione:

$$\mu Z.\tau(Z)=\bigcup_i\tau^i(false), \qquad \nu Z.\tau(Z)=\bigcap_i\tau^i(true).$$

Come leggerle: il minimo punto fisso si raggiunge partendo dal basso (insieme vuoto) e applicando $\tau$ ripetutamente; il massimo partendo dall'alto (tutti gli stati) e applicando $\tau$ ripetutamente.

16. I lemmi del caso finito: catene, stabilizzazione, convergenza

I tre lemmi seguenti trasformano le formule astratte di Tarski in un algoritmo con garanzia di terminazione.

Lemma 2 (le iterazioni formano catene). Se $\tau$ e' monotona, allora per ogni $i$:

$$\tau^i(false)\subseteq\tau^{i+1}(false) \qquad\text{e}\qquad \tau^{i+1}(true)\subseteq\tau^i(true).$$

Perche' e' vero. Induzione su $i$. Base: $\tau^0(false)=\emptyset$ e' contenuto in qualunque cosa, in particolare in $\tau^1(false)$. Passo: se $\tau^i(false)\subseteq\tau^{i+1}(false)$, applichiamo $\tau$ a entrambi i lati; la monotonia conserva l'inclusione, e otteniamo $\tau^{i+1}(false)\subseteq\tau^{i+2}(false)$. Per la catena da $true$ l'argomento e' speculare ($\tau^1(true)\subseteq S=\tau^0(true)$ per la base). $\square$

Come leggerlo: partendo dal vuoto si costruisce una successione di insiemi che puo' solo crescere; partendo dal tutto, una che puo' solo calare.

Lemma 3 (le catene si stabilizzano). Se $\tau$ e' monotona e $S$ e' finito, esiste un indice $i_0$ tale che $\tau^j(false)=\tau^{i_0}(false)$ per ogni $j\ge i_0$ (e dualmente esiste $j_0$ per la catena da $true$).

Perche' e' vero. Una catena crescente di sottoinsiemi di un insieme con $|S|$ elementi puo' crescere strettamente al massimo $|S|$ volte (ogni crescita stretta aggiunge almeno un elemento). Quindi a un certo punto due iterate consecutive coincidono: $\tau^{i_0}(false)=\tau^{i_0+1}(false)$. Da li' in poi non si muove piu' nulla: applicare $\tau$ a insiemi uguali da' insiemi uguali. $\square$

Lemma 4 (a cosa convergono le catene). Sotto le stesse ipotesi:

$$\mu Z.\tau(Z)=\tau^{i_0}(false), \qquad \nu Z.\tau(Z)=\tau^{j_0}(true),$$

e in entrambi i casi servono al piu' $|S|$ iterazioni.

Perche' e' vero (caso $\mu$; il caso $\nu$ e' duale). Due cose da verificare.

Primo: il limite e' un punto fisso. Per definizione di $i_0$: $\tau(\tau^{i_0}(false))=\tau^{i_0+1}(false)=\tau^{i_0}(false)$.

Secondo: e' il minimo. Sia $Z$ un punto fisso qualunque di $\tau$. Mostriamo per induzione che ogni iterata sta dentro $Z$: $\tau^0(false)=\emptyset\subseteq Z$; e se $\tau^i(false)\subseteq Z$, per monotonia $\tau^{i+1}(false)\subseteq\tau(Z)=Z$ (qui si usa che $Z$ e' punto fisso). In particolare $\tau^{i_0}(false)\subseteq Z$. Quindi il limite e' contenuto in ogni punto fisso: e' il minimo. $\square$

Questo risponde alle tre domande della sezione 10: il punto raggiunto e' unico e ben caratterizzato (e' $\mu$ o $\nu$), la terminazione e' garantita in al piu' $|S|$ passi, e tutto vale per qualunque $\tau$ monotona.

17. Gli algoritmi lfp e gfp, riga per riga

I due lemmi si traducono in due cicli while speculari:

function lfp(τ): predicate          function gfp(τ): predicate
  Q := false                          Q := true
  Q' := τ(false)                      Q' := τ(true)
  while Q ≠ Q':                       while Q ≠ Q':
     Q := Q'                             Q := Q'
     Q' := τ(Q')                         Q' := τ(Q')
  return Q                            return Q

Commento riga per riga di lfp (per gfp cambia solo il punto di partenza):

• Q := false; Q' := τ(false) — inizializza la coppia con le prime due iterate, $\tau^0(false)$ e $\tau^1(false)$;
• while Q ≠ Q' — all'inizio della $i$-esima iterazione del ciclo vale $Q=\tau^{i-1}(false)$ e $Q'=\tau^i(false)$: il ciclo confronta due iterate consecutive e continua finche' sono diverse;
• Q := Q'; Q' := τ(Q') — fa scorrere la finestra: la coppia $(\tau^{i-1},\tau^i)$ diventa $(\tau^i,\tau^{i+1})$;
• return Q — all'uscita $Q=Q'$, cioe' $Q=\tau(Q)$: abbiamo trovato un punto fisso, e per il Lemma 4 e' proprio $\mu Z.\tau(Z)$.

L'invariante del ciclo, utile da citare all'orale, e':

$$Q'=\tau(Q)\ \ \land\ \ Q'\subseteq\mu Z.\tau(Z),$$

cioe' la seconda variabile e' sempre l'immagine della prima, e non si "scavalca" mai il minimo punto fisso (lo si raggiunge da sotto). Il numero di iterazioni e' al massimo $|S|$ per il Lemma 3.

Il punto pratico: $\tau$ e' fatta di operazioni booleane ($\land$, $\lor$) e di $EX$ (= preimmagine esistenziale); il test Q ≠ Q' e' un confronto di uguaglianza tra insiemi. Tutte queste operazioni si eseguono direttamente sulle formule/OBDD: l'algoritmo non tocca mai un singolo stato.

18. CTL come punti fissi: le sei equazioni

Ecco le caratterizzazioni, ognuna con la sua lettura.

Le letture, una per una:

• $EF f_1$: "raggiungo $f_1$" vale se $f_1$ vale ora, oppure se ho un successore da cui raggiungo $f_1$. L'equazione $Z=f_1\lor EX\,Z$ e' esattamente questa frase; il $\mu$ dice di prendere la soluzione minima, cioe' solo gli stati che hanno una giustificazione concreta in un numero finito di passi.
• $AF f_1$: uguale, ma il passo e' "tutti i miei successori raggiungeranno $f_1$": $AX$ al posto di $EX$.
• $EG f_1$: "posso restare in $f_1$ per sempre" vale se $f_1$ vale ora e ho un successore da cui posso restare in $f_1$ per sempre. Il $\nu$ dice di prendere la soluzione massima: si parte ottimisti (tutti gli stati candidati) e si scartano via via gli stati che non riescono a mantenere la promessa.
• $AG f_1$: uguale con $AX$: tutti i successori devono restare nella regione.
• $E[f_1 U f_2]$: "o $f_2$ vale gia' adesso, oppure $f_1$ vale adesso e ho un successore da cui l'until e' soddisfatto". Minimo punto fisso perche' l'until esige che $f_2$ arrivi davvero, in un numero finito di passi.
• $A[f_1 U f_2]$: uguale con $AX$.

19. La regola mnemonica: chi decide tra $\mu$ e $\nu$

A decidere il tipo di punto fisso e' il quantificatore temporale (quello sul tempo, non quello sui cammini):

• $F$ ("prima o poi") e' esistenziale sul tempo $\to$ $\mu$: si parte dal basso e si aggiungono testimoni, perche' la proprieta' richiede un evento che accade davvero;
• $G$ ("per sempre") e' universale sul tempo $\to$ $\nu$: si parte dall'alto e si eliminano i colpevoli, perche' la proprieta' richiede di non sbagliare mai;
• $U$ contiene un "prima o poi $f_2$" $\to$ sempre $\mu$.

Il quantificatore di cammino ($E$/$A$) decide invece solo se nel corpo compare $EX$ oppure $AX$.

20. $EG\,f_1$ e' davvero il massimo punto fisso (i lemmi degli appunti)

Negli appunti questa parte e' sviluppata come catena di lemmi (a–d) per $\tau(Z)=f_1\land EX\,Z$. Diamoli con le idee delle prove: e' materiale da orale.

Lemma a (monotonia). Gia' dimostrato per intero nella sezione 13.

Lemma b (struttura del limite). Sia $\tau^{i_0}(true)$ il limite della catena decrescente $true\supseteq\tau(true)\supseteq\tau^2(true)\supseteq \cdots$. Allora ogni $s\in\tau^{i_0}(true)$ soddisfa $f_1$ e ha almeno un successore ancora dentro $\tau^{i_0}(true)$.

Perche': il limite e' un punto fisso (Lemma 4), quindi $\tau^{i_0}(true)=\tau(\tau^{i_0}(true))=f_1\land EX\,\tau^{i_0}(true)$: l'appartenenza al limite dice letteralmente "soddisfo $f_1$ e ho un successore nel limite".

Lemma c ($EG\,f_1$ e' un punto fisso di $\tau$). Doppia inclusione.

• Se $s\models EG\,f_1$, esiste un cammino infinito da $s$ con $f_1$ sempre vera. Allora $s\models f_1$ (primo stato del cammino) e il secondo stato del cammino soddisfa a sua volta $EG\,f_1$ (il cammino prosegue da li'). Quindi $s\in f_1\land EX\,(EG\,f_1)=\tau(EG\,f_1)$.
• Viceversa, se $s\in\tau(EG\,f_1)$: $s\models f_1$ e ha un successore $s'$ con $s'\models EG\,f_1$; incollando $s$ davanti al cammino di $s'$ si ottiene un cammino infinito da $s$ sempre in $f_1$, cioe' $s\models EG\,f_1$. $\square$

Lemma d ($EG\,f_1$ e' il massimo punto fisso). Per Tarski basta mostrare che ogni post-punto fisso e' contenuto in $EG\,f_1$. Sia $Z\subseteq\tau(Z)$ e sia $s_0\in Z$. Allora $s_0\in\tau(Z)$, quindi $s_0\models f_1$ ed esiste un successore $s_1\in Z$. Ripetendo lo stesso argomento su $s_1$, poi su $s_2$, eccetera, si costruisce un cammino infinito $s_0\to s_1\to s_2\to\cdots$ che non esce mai da $Z$, e lungo il quale $f_1$ vale sempre. Quindi $s_0\models EG\,f_1$. Questo vale per ogni post-punto fisso; siccome $EG\,f_1$ stesso e' un punto fisso (Lemma c), e' il massimo. $\square$

21. $E[f_1\,U\,f_2]$ e' davvero il minimo punto fisso

Lemma e. $E[f_1\,U\,f_2]$ e' il minimo punto fisso di $\tau(Z)=f_2\lor(f_1\land EX\,Z)$.

Idea della prova. Che sia un punto fisso si vede come nel Lemma c (spacchettando la semantica dell'until: o $f_2$ vale subito, o $f_1$ vale ora e l'until prosegue da un successore). Che sia il minimo: sia $Z$ un punto fisso qualunque e sia $s\models E[f_1\,U\,f_2]$; allora esiste un cammino da $s$ con $f_2$ vera in una posizione $j$ e $f_1$ vera nelle posizioni precedenti. Si mostra che $s\in Z$ per induzione su $j$, partendo dal fondo: lo stato alla posizione $j$ soddisfa $f_2$, quindi sta in $\tau(Z)=Z$; lo stato alla posizione $j-1$ soddisfa $f_1$ e ha un successore in $Z$, quindi sta in $\tau(Z)=Z$; e cosi' via risalendo fino a $s$. Quindi $E[f_1\,U\,f_2]\subseteq Z$ per ogni punto fisso $Z$: e' il minimo. $\square$

22. Esempio svolto 1: $EG\,p$ che converge a $\emptyset$

Il modello. Cinque stati in catena, con un cappio finale:

$$s_0\to s_1\to s_2\to s_3\to s_4,\qquad s_4\to s_4.$$

La proposizione $p$ e' vera in $\{s_1,s_2,s_3\}$ (falsa in $s_0$ e $s_4$).

Cosa ci aspettiamo, prima di calcolare. Ogni cammino, da qualunque stato, finisce inevitabilmente nel cappio su $s_4$, dove $p$ e' falsa. Quindi nessuno stato ha un cammino con $p$ vera per sempre: deve venire $EG\,p=\emptyset$.

Il calcolo. $\tau(Z)=p\land EX\,Z$, massimo punto fisso: si parte da $true=\{s_0,s_1,s_2,s_3,s_4\}$. Ad ogni passo servono due ingredienti: l'insieme dove vale $p$ (sempre $\{s_1,s_2,s_3\}$) e $EX\,Z$ = "chi ha un successore in $Z$".

Iterazione 1. $EX(S)$ = chi ha un successore in $S$ = tutti (la relazione e' totale). Quindi:

$$\tau(true)=\{s_1,s_2,s_3\}\cap S=\{s_1,s_2,s_3\}.$$

Iterazione 2. $EX\{s_1,s_2,s_3\}$ = chi ha un successore tra $s_1,s_2,s_3$ = $\{s_0,s_1,s_2\}$ (perche' $s_0\to s_1$, $s_1\to s_2$, $s_2\to s_3$; invece $s_3\to s_4$ e $s_4\to s_4$ escono dall'insieme). Quindi:

$$\tau^2(true)=\{s_1,s_2,s_3\}\cap\{s_0,s_1,s_2\}=\{s_1,s_2\}.$$

Iterazione 3. $EX\{s_1,s_2\}=\{s_0,s_1\}$. Quindi:

$$\tau^3(true)=\{s_1,s_2,s_3\}\cap\{s_0,s_1\}=\{s_1\}.$$

Iterazione 4. $EX\{s_1\}=\{s_0\}$. Quindi:

$$\tau^4(true)=\{s_1,s_2,s_3\}\cap\{s_0\}=\emptyset.$$

Iterazione 5. $\tau(\emptyset)=\emptyset$: punto fisso raggiunto.

Risultato: $EG\,p=\emptyset$, come previsto. Si vede bene il movimento del massimo punto fisso: a ogni giro vengono erosi gli stati che non possono mantenere la promessa (prima $s_0$ e $s_4$ dove $p$ e' falsa, poi $s_3$ che e' costretto a entrare in $s_4$, poi $s_2$, poi $s_1$).

23. Esempio svolto 2: $E[p\,U\,q]$

Il modello. Quattro stati:

$$s_0\to s_1\to s_2\to s_3,\qquad s_3\to s_2,$$

con $p$ vera in $\{s_0,s_1\}$ e $q$ vera in $\{s_2\}$.

Cosa ci aspettiamo. Da $s_0$: cammino $s_0 s_1 s_2$, con $p$ vera in $s_0,s_1$ e poi $q$ in $s_2$: l'until e' soddisfatto. Da $s_1$: idem, piu' corto. $s_2$: $q$ vale subito, soddisfatto banalmente. $s_3$: $q$ non vale e nemmeno $p$, quindi no. Risultato atteso: $\{s_0,s_1,s_2\}$.

Il calcolo. $\tau(Z)=q\lor(p\land EX\,Z)$, minimo punto fisso: si parte da $false=\emptyset$. Ricordare: $\lor=\cup$, $\land=\cap$.

Iterazione 1. $EX\,\emptyset=\emptyset$ (nessuno ha successori nel vuoto):

$$\tau(false)=\{s_2\}\cup(\{s_0,s_1\}\cap\emptyset)=\{s_2\}.$$

Sono gli stati dove l'until e' soddisfatto "a costo zero": $q$ vale gia'.

Iterazione 2. $EX\{s_2\}$ = chi ha un successore in $\{s_2\}$ = $\{s_1,s_3\}$ (perche' $s_1\to s_2$ e $s_3\to s_2$):

$$\tau^2(false)=\{s_2\}\cup(\{s_0,s_1\}\cap\{s_1,s_3\}) =\{s_2\}\cup\{s_1\}=\{s_1,s_2\}.$$

Nota come $s_3$ viene scartato dall'intersezione con $p$: ha un successore buono ma non soddisfa $p$ adesso, quindi l'until non vale.

Iterazione 3. $EX\{s_1,s_2\}$ = chi ha un successore in $\{s_1,s_2\}$ = $\{s_0,s_1,s_3\}$ ($s_0\to s_1$, $s_1\to s_2$, $s_3\to s_2$):

$$\tau^3(false)=\{s_2\}\cup(\{s_0,s_1\}\cap\{s_0,s_1,s_3\}) =\{s_2\}\cup\{s_0,s_1\}=\{s_0,s_1,s_2\}.$$

Iterazione 4. $EX\{s_0,s_1,s_2\}=\{s_0,s_1,s_3\}$ (come prima: $s_2\to s_3$ esce dall'insieme):

$$\tau^4(false)=\{s_2\}\cup(\{s_0,s_1\}\cap\{s_0,s_1,s_3\})=\{s_0,s_1,s_2\} =\tau^3(false)\ \Rightarrow\ \text{stop}.$$

Risultato: $E[p\,U\,q]=\{s_0,s_1,s_2\}$, come previsto. Qui il movimento e' quello del minimo punto fisso: si propaga all'indietro la bonta', prima gli stati dove $q$ vale gia', poi chi li raggiunge in un passo restando in $p$, poi in due passi, eccetera.

24. $\mu$ e $\nu$: i due movimenti, in sintesi

• $\mu$ (minimo): parto da $\emptyset$, aggiungo a ogni giro gli stati che hanno appena acquisito una giustificazione concreta. Adatto a proprieta' che chiedono che qualcosa accada ($F$, $U$): nulla entra nell'insieme senza un testimone finito.
• $\nu$ (massimo): parto da $S$, tolgo a ogni giro gli stati che si scoprono incapaci di mantenere la promessa. Adatto a proprieta' che chiedono che qualcosa non si rompa mai ($G$): si resta nell'insieme finche' si riesce a sopravvivere un altro passo.

Tutto il calcolo, in entrambi i casi, usa solo: $\cup$, $\cap$, e $EX$ (preimmagine esistenziale). Resta da capire come eseguire queste operazioni su formule booleane in modo efficiente. Entrano in scena gli OBDD.

Parte IV — OBDD: la struttura dati per le funzioni booleane

25. Il punto di partenza: alberi di decisione

L'esempio guida degli appunti e' il comparatore a due bit:

$$f(a_1,a_2,b_1,b_2)=(a_1\leftrightarrow b_1)\land(a_2\leftrightarrow b_2).$$

Come leggerla: $f$ vale 1 quando la coppia $a_1a_2$ e la coppia $b_1b_2$ sono uguali bit a bit.

Una funzione booleana si puo' sempre rappresentare con un albero di decisione: ogni nodo interno $v$ e' etichettato da una variabile $var(v)$ e ha due figli, $low(v)$ (da seguire quando la variabile vale 0) e $high(v)$ (quando vale 1); le foglie sono etichettate 0 o 1. Per valutare la funzione su un assegnamento si parte dalla radice, a ogni nodo si guarda il valore della variabile testata e si scende nel figlio corrispondente: la foglia raggiunta e' il valore della funzione.

Il problema: l'albero completo su $n$ variabili ha $2^n$ foglie. Per il comparatore a due bit (4 variabili) sono 16 foglie e 31 nodi totali. Quindi l'albero di decisione, da solo, non risolve nulla: e' grande quanto la tabella di verita'. Pero' e' pieno di ridondanza: interi sottoalberi sono identici tra loro, e molti test non cambiano il risultato. L'idea degli OBDD e' spremere via tutta questa ridondanza.

26. La funzione calcolata da un nodo

Diamo la definizione formale, perche' tutto il resto ci si appoggia. Ogni nodo $v$ di un diagramma di decisione definisce una funzione booleana $f_v$:

1. se $v$ e' una foglia con etichetta 1, allora $f_v=1$ (costante vero); se ha etichetta 0, allora $f_v=0$;
2. se $v$ e' un nodo interno con $var(v)=x_i$, allora:

$$f_v=(\neg x_i\land f_{low(v)})\lor(x_i\land f_{high(v)}).$$

Come leggerla: "se $x_i=0$ il valore e' quello del ramo low; se $x_i=1$ e' quello del ramo high". I due casi sono esclusivi, e la formula li incolla in una disgiunzione.

27. L'espansione di Shannon

La definizione appena data e' un caso particolare di un'identita' generale. Per qualunque funzione booleana $f$ e qualunque variabile $x$:

$$f=(\neg x\land f|_{x=0})\lor(x\land f|_{x=1})$$

dove $f|_{x=b}$ e' la funzione $f$ con $x$ fissata al valore $b$. Questa e' l'espansione di Shannon.

Perche' e' vera: dato un assegnamento qualunque, $x$ vale 0 oppure 1. Se vale 0, il secondo disgiunto e' falso e il primo si riduce a $f|_{x=0}$, che su quell'assegnamento coincide con $f$. Se vale 1, simmetricamente. In entrambi i casi i due lati coincidono. $\square$

Perche' ci interessa: dice che ogni funzione si puo' scomporre in due funzioni piu' semplici (una variabile in meno), distinguendo i casi sulla prossima variabile. Un BDD e' esattamente la forma a grafo di questa ricorsione, con i sottoproblemi uguali condivisi invece che duplicati. Anche l'algoritmo APPLY (sezione 34) e la quantificazione (sezione 36) sono applicazioni dirette di Shannon.

28. Da BDD a OBDD: l'ordine delle variabili

Un BDD (binary decision diagram) e' un DAG — non piu' un albero: i sottografi possono essere condivisi — con nodi interni etichettati da variabili e foglie 0/1, come sopra.

Un OBDD (ordered BDD) e' un BDD in cui e' fissato un ordine totale sulle variabili, ad esempio $x_1<x_2<\cdots<x_n$, e lungo ogni cammino dalla radice alle foglie le variabili compaiono solo in quell'ordine (non necessariamente tutte, ma mai in ordine diverso e mai ripetute).

Due fatti vanno ricordati subito (sono i due "important points" degli appunti):

1. l'ordine influenza la taglia dell'OBDD, anche in modo drammatico (sezione 31);
2. per confrontare due funzioni tramite i loro OBDD bisogna usare lo stesso ordine in entrambi: la forma canonica e' canonica a parita' di ordine.

29. Le tre regole di riduzione

Per passare dall'albero (o da un BDD qualunque) alla forma compatta si applicano ripetutamente, finche' possibile, tre regole. Per ognuna diamo la regola e il motivo per cui non cambia la funzione rappresentata.

Regola 1: rimuovi i terminali duplicati. Se ci sono piu' foglie con la stessa etichetta (es. tante foglie 0), se ne tiene una sola e tutti gli archi entranti nelle altre vengono ridiretti su quella.

Perche' e' corretta: il valore di un cammino dipende dall'etichetta della foglia raggiunta, non da quale foglia fisicamente sia. Dopo la regola, ogni OBDD ha al massimo due foglie: una 0 e una 1.

Regola 2: rimuovi i nodi interni duplicati. Se due nodi interni distinti $u$ e $v$ testano la stessa variabile ($var(u)=var(v)$) e hanno gli stessi figli ($low(u)=low(v)$ e $high(u)=high(v)$), se ne elimina uno e gli archi entranti vengono ridiretti sull'altro.

Perche' e' corretta: per la definizione della sezione 26, $f_u$ e $f_v$ sono determinate da (variabile, figlio low, figlio high); se questi tre dati coincidono, $f_u=f_v$: i due nodi rappresentano la stessa funzione e uno e' superfluo.

Regola 3: rimuovi i test ridondanti. Se un nodo interno $v$ ha $low(v)=high(v)$, il nodo si elimina e gli archi entranti vengono ridiretti direttamente sul figlio (unico).

Perche' e' corretta: per Shannon, $f_v=(\neg x\land f_w)\lor(x\land f_w)=f_w$ dove $w$ e' il figlio comune: il valore della variabile testata non influenza il risultato, quindi il test non serve.

Un OBDD su cui nessuna regola e' piu' applicabile si dice ridotto (ROBDD). Quando si dice "OBDD" in questo capitolo si intende quasi sempre la forma ridotta.

30. L'esempio completo: da 31 nodi a 8

Per il comparatore a due bit, con l'ordine interleaved $a_1<b_1<a_2<b_2$ (le variabili da confrontare stanno vicine), l'albero da 31 nodi si riduce a un OBDD con 8 nodi. Vale la pena descriverlo esplicitamente, livello per livello:

• radice $a_1$;
• due nodi $b_1$ (uno per ramo di $a_1$): quello raggiunto con $a_1=0$ manda $b_1=0$ avanti e $b_1=1$ alla foglia 0; quello raggiunto con $a_1=1$ fa il viceversa. In altre parole: se $a_1\ne b_1$ la funzione e' gia' decisa (vale 0), altrimenti il confronto continua;
• un solo nodo $a_2$: i due rami "sopravvissuti" ($a_1=b_1=0$ e $a_1=b_1=1$) confluiscono qui, perche' da questo punto in poi la funzione e' la stessa ($a_2\leftrightarrow b_2$) — questa e' la condivisione tipica del DAG, impossibile in un albero;
• due nodi $b_2$, simmetrici ai $b_1$;
• le due foglie 0 e 1.

Totale: $1+2+1+2+2=8$ nodi. Ogni cammino verso la foglia 1 legge una coppia uguale ($a_1=b_1$), poi un'altra coppia uguale ($a_2=b_2$): esattamente la semantica del comparatore.

31. Quanto conta l'ordine: da lineare a esponenziale

Con l'ordine "sbagliato" $a_1<a_2<b_1<b_2$ (prima tutte le $a$, poi tutte le $b$) lo stesso comparatore richiede 11 nodi invece di 8. Sembra poco, ma il fenomeno scala malissimo. Per il comparatore a $n$ bit:

• ordine interleaved $a_1<b_1<a_2<b_2<\cdots$: $3n+2$ nodi (lineare in $n$);
• ordine separato $a_1<\cdots<a_n<b_1<\cdots<b_n$: $3\cdot 2^n-1$ nodi (esponenziale in $n$).

Perche' succede: con l'ordine separato, dopo aver letto tutte le $a_i$ l'OBDD deve ricordare l'intera sequenza letta (per poterla confrontare con le $b_i$ che arrivano dopo): servono $2^n$ rami distinti, uno per ogni valore possibile della prima meta'. Con l'ordine interleaved, invece, ogni confronto $a_i$ vs $b_i$ si chiude subito e la memoria necessaria e' costante ("finora uguali" oppure "gia' deciso 0").

La regola pratica: tenere vicine nell'ordine le variabili che interagiscono nella formula. Due avvertenze importanti:

• trovare l'ordine ottimo (e perfino verificare che un ordine sia ottimo) e' un problema NP-completo: nella pratica si usano euristiche e riordinamento dinamico;
• esistono funzioni intrinsecamente difficili, che hanno OBDD esponenziale per qualunque ordine (esempio classico: il bit centrale della moltiplicazione binaria). Gli OBDD garantiscono canonicita', non compattezza.

32. Canonicita': cosa garantisce e a cosa serve

Teorema (canonicita'). Fissato l'ordine delle variabili, l'OBDD ridotto di una funzione booleana e' unico (a meno di isomorfismo). Quindi due formule definiscono la stessa funzione se e solo se i loro OBDD ridotti, costruiti con lo stesso ordine, sono lo stesso grafo.

Le conseguenze pratiche sono enormi:

• test di equivalenza: "le due formule sono equivalenti?" non richiede piu' un ragionamento logico (che in generale costa quanto SAT/validita'): basta confrontare i due grafi. Nelle implementazioni reali, dove tutti gli OBDD vivono in una tabella condivisa (unique table) che impedisce fisicamente i duplicati, il confronto e' addirittura un confronto di puntatori: stessa radice = stessa funzione, in tempo costante;
• test di soddisfacibilita' e validita': $f$ e' insoddisfacibile se e solo se il suo OBDD ridotto e' la sola foglia 0; e' valida se e solo se e' la sola foglia 1;
• test di terminazione dei punti fissi: gli algoritmi lfp/gfp devono controllare a ogni giro se $Z_{i+1}=Z_i$, cioe' se due insiemi (due funzioni booleane) coincidono. Con OBDD canonici questo test, ripetuto migliaia di volte, e' immediato. Questa e' la ragione profonda per cui gli OBDD e il model checking simbolico stanno cosi' bene insieme.

33. RESTRICT: fissare una variabile

Definizione. Data $f$ e un valore $b\in\{0,1\}$, la funzione ristretta $f|_{x_i\leftarrow b}$ e' definita da:

$$f|_{x_i\leftarrow b}(x_1,\ldots,x_n)=f(x_1,\ldots,x_{i-1},b,x_{i+1}, \ldots,x_n).$$

Come leggerla: e' la funzione $f$ in cui l'argomento $x_i$ non e' piu' libero ma inchiodato al valore $b$. E' esattamente l'oggetto che compare nell'espansione di Shannon.

Come si calcola sull'OBDD (regola generale): per ogni nodo $v$ che ha un puntatore verso un nodo $w$ con $var(w)=x_i$, si ridirige quel puntatore su $low(w)$ se $b=0$, su $high(w)$ se $b=1$. In parole: i test su $x_i$ vengono scavalcati, seguendo d'ufficio il ramo corrispondente a $b$.

Esempio svolto (dagli appunti): comparatore a due bit, OBDD a 8 nodi della sezione 30, restrizione $b_1\leftarrow 0$. Scavalchiamo i due nodi $b_1$ seguendo il loro ramo low:

• il nodo $b_1$ di sinistra (raggiunto con $a_1=0$) ha $low$ = il nodo $a_2$: la radice $a_1$ ora punta, per $a_1=0$, direttamente ad $a_2$;
• il nodo $b_1$ di destra (raggiunto con $a_1=1$) ha $low$ = la foglia 0 (perche' $a_1=1\ne 0=b_1$): la radice ora punta, per $a_1=1$, direttamente alla foglia 0.

Risultato: radice $a_1$, un nodo $a_2$, due nodi $b_2$, due foglie — 6 nodi, che rappresentano la funzione $\neg a_1\land(a_2\leftrightarrow b_2)$. Verifica di buon senso: se $b_1=0$, il comparatore puo' accettare solo se $a_1=0$, e resta da confrontare il secondo bit. Torna.

Avvertenza: il grafo prodotto dalla regola puo' non essere ridotto; in generale dopo un restrict bisogna ripassare le regole di riduzione (nel nostro esempio non serviva).

34. APPLY: combinare due OBDD con un connettivo

Le operazioni binarie sulle funzioni booleane sono $2^4=16$ (per ognuna delle 4 righe della tabella di verita' su due argomenti si sceglie 0 o 1): congiunzione, disgiunzione, implicazione, xor, eccetera. L'algoritmo APPLY le calcola tutte con lo stesso schema: dato un connettivo $*$ e gli OBDD di $f$ e $f'$, produce l'OBDD di $f*f'$.

L'idea e' ancora Shannon: per calcolare $f*f'$ distinguo i casi sulla prossima variabile dell'ordine, e su ciascun caso il problema si riduce a combinare funzioni piu' semplici, perche' il connettivo commuta con la distinzione di casi:

$$f*f'=\big(\neg x\land(f|_{x\leftarrow 0}*f'|_{x\leftarrow 0})\big) \lor\big(x\land(f|_{x\leftarrow 1}*f'|_{x\leftarrow 1})\big).$$

Siano $v,v'$ le radici dei due OBDD, $x=var(v)$, $x'=var(v')$. I casi:

1. $v$ e $v'$ entrambi foglie: il risultato e' la costante $value(v)*value(v')$ (es. per $\land$: $1*1=1$, altrimenti 0).
2. $x=x'$ (stessa variabile in testa): si crea un nodo per $x$ il cui ramo low e' APPLY sui due rami low, e il ramo high e' APPLY sui due rami high. (Le restrizioni di $f$ rispetto a $x$ sono esattamente i suoi figli.)
3. $x<x'$ nell'ordine: la variabile $x$ non compare in testa a $f'$, e per via dell'ordinamento non compare affatto in $f'$ (sotto $v'$ possono esserci solo variabili maggiori di $x'$, quindi maggiori di $x$). Allora $f'|_{x\leftarrow 0}=f'|_{x\leftarrow 1}=f'$: si crea il nodo per $x$ con ramo low = APPLY su ($low(v)$, $f'$ intero) e ramo high = APPLY su ($high(v)$, $f'$ intero).
4. $x'<x$: simmetrico al caso 3.

Alla fine si riduce il risultato con le tre regole.

Il punto della complessita'. Applicata ciecamente, la ricorsione raddoppia i sottoproblemi a ogni livello: rischio esponenziale. Ma ogni sottoproblema e' identificato da una coppia di nodi (un sottografo di $f$, uno di $f'$), e di coppie distinte ce ne sono al massimo $|f|\cdot|f'|$ (prodotto delle taglie dei due OBDD). Con una cache (hash table) che memorizza i sottoproblemi gia' risolti — da consultare prima di risolverne uno "nuovo" — ogni coppia si risolve una sola volta, e il costo totale e' $O(|f|\cdot|f'|)$: polinomiale, non esponenziale. Questa memoizzazione e' essenziale, non un'ottimizzazione facoltativa.

35. La negazione

La negazione e' un caso speciale, piu' semplice: l'OBDD di $\neg f$ si ottiene da quello di $f$ scambiando le etichette delle foglie (0 diventa 1 e viceversa).

Perche': ogni assegnamento segue nel grafo lo stesso cammino di prima; deve solo arrivare al risultato opposto. Le implementazioni reali usano i complemented edges per farlo in tempo costante senza nemmeno copiare il grafo.

36. Quantificare su OBDD: il ritorno di QBF

I quantificatori booleani si riducono a restrict piu' un connettivo:

$$\exists x.\,f=f|_{x\leftarrow 0}\lor f|_{x\leftarrow 1}, \qquad \forall x.\,f=f|_{x\leftarrow 0}\land f|_{x\leftarrow 1}.$$

Perche' (caso $\exists$): "esiste un valore di $x$ che rende vera $f$" significa esattamente "$f$ e' vera con $x=0$ oppure con $x=1$": i valori possibili sono solo due, e il quantificatore e' la disgiunzione dei due casi. Il $\forall$ e' la congiunzione, per lo stesso motivo.

Operativamente: due restrict e un APPLY. Per quantificare un vettore di variabili ($\exists\bar{x}'$) si elimina una variabile alla volta. Questo conferma quanto richiamato nella sezione 0: QBF non aggiunge potere espressivo (ogni quantificatore si elimina), ma la versione quantificata e' piu' succinta — e sugli OBDD l'eliminazione e' meccanica.

37. Renaming e relational product

Renaming. Nel model checking simbolico si lavora con $\bar{x}$ (correnti) e $\bar{x}'$ (next). La preimmagine $Pre_E(T)$ produce una formula su $\bar{x}$ a partire da una $T$ su $\bar{x}'$; ma il $T$ che abbiamo in mano di solito e' scritto su $\bar{x}$. Serve quindi rinominare $\bar{x}$ in $\bar{x}'$ (o viceversa) prima/dopo l'operazione. Il renaming non cambia l'insieme rappresentato, solo il nome delle variabili; sugli OBDD e' una sostituzione di etichette (facile quando le variabili primate sono adiacenti alle originali nell'ordine — un altro motivo per usare ordini interleaved $x_1<x_1'<x_2<x_2'<\cdots$).

Relational product. La preimmagine esistenziale:

$$Pre_E(T)(\bar{x})=\exists\bar{x}'.\ R(\bar{x},\bar{x}')\land T(\bar{x}')$$

combina in un colpo solo una congiunzione (APPLY) e una quantificazione di un intero vettore (catena di restrict+APPLY). Questa combinazione si chiama relational product ed e' l'operazione singola piu' importante — e piu' costosa — del symbolic model checking: il prodotto intermedio $R\land T$ puo' crescere molto prima che le quantificazioni lo sgonfino. Le implementazioni serie la calcolano come primitiva unica (quantificando "al volo" durante la congiunzione) e ne controllano il costo con: buoni ordini di variabili, partizionamento della relazione $R$ (congiunzioni/disgiunzioni di pezzi piccoli invece di un blocco monolitico), scelta dell'ordine di eliminazione delle variabili, caching.

Parte V — Tutto insieme: CTL simbolico

38. L'algoritmo CHECK: la struttura

Ora abbiamo tutti i pezzi: insiemi = OBDD, operazioni booleane = APPLY, $EX$ = relational product, punti fissi = cicli lfp/gfp con test di uguaglianza canonico. L'algoritmo CHECK li assembla.

CHECK prende una formula CTL $\varphi$ (e la struttura di Kripke, codificata come OBDD per $I$, $R$ e per ogni lettera $p$) e restituisce l'OBDD dell'insieme degli stati dove $\varphi$ e' vera. E' definito per induzione sulla struttura della formula:

• $\varphi=p$ (lettera proposizionale): si restituisce l'OBDD di $S_p$, che fa parte della codifica del modello;
• $\varphi=\neg f_1$: negazione (scambio foglie) di $CHECK(f_1)$;
• $\varphi=f_1\land f_2$: $APPLY(\land,CHECK(f_1),CHECK(f_2))$, e analogamente per gli altri connettivi booleani;
• $\varphi=EX f_1$: $CheckEX(CHECK(f_1))$;
• $\varphi=E[f_1\,U\,f_2]$: $CheckEU(CHECK(f_1),CHECK(f_2))$;
• $\varphi=EG f_1$: $CheckEG(CHECK(f_1))$.

Perche' bastano $EX$, $EU$, $EG$: sono un insieme adeguato di modalita'. Tutte le altre si riducono a queste tramite equivalenze, ognuna con la sua giustificazione semantica:

• $EF f_1\equiv E[true\,U\,f_1]$ — "prima o poi $f_1$" e' un until con condizione di attesa banale (aspettare non costa nulla);
• $AX f_1\equiv\neg EX\neg f_1$ — "tutti i successori soddisfano $f_1$" equivale a "non esiste un successore che la viola";
• $AG f_1\equiv\neg EF\neg f_1$ — "su ogni cammino sempre $f_1$" equivale a "non esiste un cammino che raggiunge una violazione";
• $AF f_1\equiv\neg EG\neg f_1$ — "su ogni cammino prima o poi $f_1$" fallisce esattamente se esiste un cammino che resta per sempre in $\neg f_1$;
• $A[f_1\,U\,f_2]$ si riduce con una formula piu' articolata (oppure si calcola direttamente col suo punto fisso, usando $Pre_A$ al posto di $Pre_E$).

A ogni passo dell'induzione l'algoritmo manipola solo OBDD: mai un singolo stato. Vediamo le tre procedure.

39. CheckEX

$$CheckEX(f_1(\bar{x}))=\exists\bar{x}'.\ R(\bar{x},\bar{x}')\land f_1(\bar{x}').$$

Come leggerla, pezzo per pezzo: $f_1(\bar{x}')$ e' l'OBDD di $f_1$ rinominato sulle variabili next (renaming); $R(\bar{x},\bar{x}')\land\cdot$ e' un APPLY; $\exists\bar{x}'$ e' la catena di quantificazioni restrict+APPLY. Cioe': CheckEX e' il relational product della sezione 37. La formula risultante e' su $\bar{x}$ e rappresenta "gli stati con almeno un successore in $f_1$" — esattamente la semantica di $EX$.

Esempio svolto. Una variabile, $R(x,x')=(x'\leftrightarrow\neg x)$ (il sistema che inverte $x$). Calcoliamo $CHECK(EX\,x)$:

$$\exists x'.\ (x'\leftrightarrow\neg x)\land x'.$$

E' lo stesso calcolo della sezione 9, svolto la' passo per passo: restringendo $x'\leftarrow 0$ si ottiene $0$, restringendo $x'\leftarrow 1$ si ottiene $\neg x$, la disgiunzione e' $\neg x$. Quindi:

$$CHECK(EX\,x)=\neg x:$$

dagli stati con $x=0$ (e solo da quelli) il prossimo stato puo' avere $x$ vero. L'intero calcolo e' avvenuto su formule.

40. CheckEU

$CheckEU(f_1,f_2)$ calcola $E[f_1\,U\,f_2]$ instanziando l'algoritmo lfp sul predicate transformer $\tau(Z)=f_2\lor(f_1\land EX\,Z)$ (sezioni 18 e 21):

$$Z_0=false,\qquad Z_{i+1}=f_2\lor\big(f_1\land CheckEX(Z_i)\big),$$

fermandosi quando $Z_{i+1}=Z_i$.

La corrispondenza tra il calcolo insiemistico e le operazioni OBDD e' uno a uno: $\lor$ e $\land$ sono APPLY, $EX$ e' il relational product, e il test di arresto $Z_{i+1}=Z_i$ e' il confronto canonico (puntatori). L'esempio della sezione 23 e' un'esecuzione di CheckEU, scritta con gli insiemi al posto degli OBDD.

41. CheckEG

$CheckEG(f_1)$ calcola $EG\,f_1$ instanziando gfp su $\tau(Z)=f_1\land EX\,Z$ (sezioni 18 e 20):

$$Z_0=f_1,\qquad Z_{i+1}=f_1\land CheckEX(Z_i),$$

fermandosi quando $Z_{i+1}=Z_i$. (Partire da $f_1$ o da $true$ e' equivalente: la prima iterazione da $true$ produce comunque $f_1\land EX\,true=f_1$.)

L'esempio della sezione 22 e' un'esecuzione di CheckEG. La lettura operativa del massimo punto fisso: a ogni giro sopravvivono solo gli stati di $f_1$ con almeno un successore ancora sopravvissuto — l'analogo simbolico della ricerca di un ciclo (una SCC) tutto dentro la regione $f_1$.

42. Raggiungibilita' e safety, simbolicamente

Con gli stessi ingredienti si calcola l'insieme degli stati raggiungibili, stavolta in avanti con la post-immagine:

$$Z_0=I,\qquad Z_{i+1}=Z_i\lor Post(Z_i),$$

fino a $Z_{i+1}=Z_i$. Perche' funziona: $Z_i$ e' l'insieme degli stati raggiungibili in al piu' $i$ passi (induzione immediata), la catena e' crescente, il modello e' finito, quindi si stabilizza, e il limite e' $Reach$.

A quel punto la safety "mai $Bad$" si decide come nella sezione 8: $Reach\land Bad$ insoddisfacibile (OBDD = foglia 0) significa proprieta' verificata; altrimenti ogni assegnamento che la soddisfa e' uno stato bad raggiungibile, e una traccia di errore si ricostruisce a ritroso intersecando, livello per livello, i $Z_i$ con le preimmagini dello stato bad trovato.

Parte VI — Partial-order reduction

43. L'idea: non esplorare interleaving equivalenti

La partial-order reduction (POR) e' la terza arma contro lo state explosion, e attacca specificamente l'esplosione da concorrenza (sezione 2). Si usa nel model checking esplicito (tipicamente in strumenti come SPIN), spesso in combinazione con le tecniche simboliche nel panorama generale.

Due azioni $a$ e $b$ di processi diversi si dicono indipendenti quando:

• eseguire $a$ non abilita ne' disabilita $b$, e viceversa (non interferiscono sul controllo);
• da uno stesso stato, eseguire $a;b$ oppure $b;a$ porta allo stesso stato finale (commutano sui dati).

Se inoltre la proprieta' da verificare non osserva l'ordine relativo di $a$ e $b$ (non distingue gli stati intermedi), allora i due interleaving $a;b$ e $b;a$ sono indistinguibili ai fini della verifica, ed esplorarli entrambi e' lavoro sprecato.

Esempio. Il processo 1 incrementa la variabile locale $x$, il processo 2 incrementa la variabile locale $y$. Variabili diverse, nessuna interferenza: $inc_x;inc_y$ e $inc_y;inc_x$ portano allo stesso stato. Se la proprieta' riguarda solo lo stato finale (es. "entrambi terminano"), basta esplorare un rappresentante delle due sequenze. Con $n$ processi che fanno $k$ passi indipendenti l'una, gli interleaving sono un numero combinatorio gigantesco, ma le classi di equivalenza possono essere pochissime: la POR esplora un rappresentante per classe, riducendo il grafo anche di ordini di grandezza.

Il punto delicato: la riduzione e' corretta solo rispetto a proprieta' che davvero non osservano l'ordine scartato. Se la formula temporale distingue gli stati intermedi (es. parla di $x$ e di $y$ in momenti precisi), certe permutazioni non si possono potare. Gli algoritmi reali (ample sets e simili) calcolano, stato per stato, un sottoinsieme di azioni sufficiente a preservare la verita' della proprieta'.

Parte VII — Bounded Model Checking

44. Cambio di prospettiva: da dimostrare a cercare bug

Il model checking LTL chiede $\mathcal{M},s\models\psi$. Come visto nel capitolo 8, conviene lavorare sulla negazione: $\psi$ e' violata se e solo se esiste un cammino che soddisfa $\varphi:=\neg\psi$, cioe' se il problema esistenziale $\mathcal{M},s\models E\varphi$ ha risposta si' (in termini di automi: se $\mathcal{M}\times\mathcal{A}_{\neg\psi}$ ha linguaggio non vuoto — ma il BMC questo prodotto non lo costruira' mai esplicitamente).

Il bounded model checking affronta il problema esistenziale cosi':

1. si parte con $k=0$;
2. si chiede: "esiste un'esecuzione di $\mathcal{M}$ di lunghezza $k$ che soddisfa $\varphi$?" — e si codifica questa domanda come istanza SAT, da dare a un SAT solver;
3. se il solver risponde SAT, abbiamo trovato un controesempio a $\psi$ (e l'assegnamento del solver e' la traccia, leggibile stato per stato); se risponde UNSAT, si incrementa $k$ e si riprova.

Il guadagno di efficienza sta tutto nel punto 2: i SAT solver moderni sono straordinariamente ottimizzati, e cercare una traccia di lunghezza bounded e' un problema che si scrive in modo naturale come formula proposizionale.

45. Sistemi di transizione simbolici

L'encoding parte dalla stessa idea della Parte II, che qui rivediamo nella notazione usata per il BMC. Data $\mathcal{M}=(S,I,T,L)$ esplicita, la sua codifica booleana e':

• $\bar{s}$: un vettore di variabili booleane di stato; uno stato e' un assegnamento a tutte le variabili di $\bar{s}$ (con $n$ variabili, $2^n$ stati possibili);
• $f_I(\bar{s})$: un assegnamento $m$ soddisfa $f_I$ se e solo se $m$ e' uno stato iniziale;
• $f_T(\bar{s},\bar{s}')$: la coppia di assegnamenti $(m,m')$ soddisfa $f_T$ se e solo se $(m,m')$ e' una transizione;
• $f_p(\bar{s})$ per ogni etichetta $p$: $m$ soddisfa $f_p$ se e solo se $p$ e' vera nello stato $m$.

Un cammino (o traccia) e' una successione infinita di assegnamenti $\pi=m_0,m_1,m_2,\ldots$ tale che $m_0$ soddisfa $I$ e ogni coppia consecutiva $(m_i,m_{i+1})$ soddisfa $T$.

46. SMV: scrivere il modello direttamente come formule

Nella pratica nessuno scrive $f_I$ e $f_T$ a mano arco per arco: si usano linguaggi di modellazione simbolici. SMV (e il suo erede nuXmv) e' l'esempio del corso: un file SMV e' la rappresentazione simbolica di una struttura di Kripke. Tre parole chiave:

• VAR: dichiara le variabili di stato;
• INIT: una formula booleana sulle variabili di stato = gli stati iniziali;
• TRANS: una formula booleana su variabili correnti e next(...) = la relazione di transizione.

Esempio 1: il flip-flop.

MODULE main
VAR
    s0 : boolean;
INIT
    !s0;
TRANS
    next(s0) <-> !s0;

Lettura riga per riga: una sola variabile booleana s0, quindi due stati; si parte dallo stato con s0 falso (INIT !s0); a ogni passo il prossimo valore di s0 e' l'opposto di quello attuale (TRANS). E' esattamente il sistema "inverti $x$" usato negli esempi delle sezioni 9 e 39, scritto in sintassi concreta.

Esempio 2: il contatore modulo 4.

MODULE main
VAR
    s0 : boolean;
    s1 : boolean;
INIT
    !s0 & !s1;
TRANS
    (next(s0) <-> !s0)
  & (next(s1) <-> ((s0 & !s1) | (!s0 & s1)));

Qui gli stati sono 4 e servono due variabili: s0 e' il bit meno significativo, s1 il piu' significativo. INIT fissa il valore 00. La prima riga di TRANS dice che il bit basso si inverte a ogni passo (come in ogni incremento binario); la seconda dice che il bit alto al passo successivo vale "s0 xor s1" (riporto dell'incremento). Il sistema cicla:

$$00\to 01\to 10\to 11\to 00\to\cdots$$

cioe' conta modulo 4. Da notare: la transizione e' data come formula su variabili correnti e next, mai come elenco di archi.

47. Unrolling: la formula $[\![M]\!]_k$

Primo ingrediente dell'encoding SAT: una formula i cui modelli sono tutti e soli i cammini di lunghezza $k$ del sistema. Si introducono $k+1$ copie delle variabili di stato, $\bar{s}_0,\bar{s}_1,\ldots,\bar{s}_k$ (la copia $\bar{s}_i$ rappresenta lo stato al tempo $i$), e si scrive:

$$[\![M]\!]_k\ :=\ I(\bar{s}_0)\ \land\ \bigwedge_{i=0}^{k-1}T(\bar{s}_i,\bar{s}_{i+1}).$$

Come leggerla: "l'assegnamento alla copia 0 e' uno stato iniziale, e ogni coppia di copie consecutive e' una transizione". Un assegnamento che soddisfa questa formula assegna valori a tutte le copie, cioe' descrive una sequenza di $k+1$ stati che parte bene e si muove legalmente: un prefisso di esecuzione di lunghezza $k$. Questa costruzione si chiama unrolling (srotolamento) della relazione di transizione.

48. Il problema dei cammini infiniti e la soluzione del lasso

C'e' un ostacolo concettuale: le formule LTL sono definite su cammini infiniti, ma il BMC maneggia prefissi finiti. Come si decide, su un oggetto finito, una proprieta' che parla dell'infinito?

L'osservazione cruciale: un prefisso finito puo' rappresentare un cammino infinito se contiene un loop-back, cioe' una transizione dall'ultimo stato a uno stato gia' visitato.

Definizione ((k,l)-loop). Un cammino $\pi$ e' un $(k,l)$-loop, con $l\le k$, se $T(\pi(k),\pi(l))$ vale e:

$$\pi=u\cdot v^\omega,\qquad u=\pi(0)\cdots\pi(l-1),\quad v=\pi(l)\cdots\pi(k).$$

Come leggerla: il cammino e' fatto di un prefisso $u$ (gli stati prima del punto di rientro) seguito dal ciclo $v$ ripetuto per sempre. La forma grafica e' quella di un lasso. Diciamo che $\pi$ e' un $k$-loop se e' un $(k,l)$-loop per qualche $l\le k$.

Perche' basta: e' lo stesso argomento degli automi di Buchi: in un sistema a stati finiti, ogni cammino infinito prima o poi ripete uno stato, quindi se esiste un controesempio infinito ne esiste uno ultimamente periodico, cioe' a forma di lasso. Cercare lassi non fa perdere controesempi (pur di far crescere $k$ abbastanza).

Il BMC quindi distingue due casi per ogni traccia bounded:

• la traccia ha un loop-back: rappresenta un vero cammino infinito, e si puo' valutare $\varphi$ con la semantica LTL standard;
• la traccia non ha loop-back: e' solo un prefisso finito, e serve una semantica apposita e prudente (la bounded semantics, sezione 51).

49. Codificare il loop: ${}_lL_k$, $L_k$ e $succ$

Anche "la traccia ha un loop-back" deve diventare una formula booleana.

$${}_lL_k\ :=\ T(\bar{s}_k,\bar{s}_l)$$

Come leggerla: "dall'ultimo stato (copia $k$) c'e' una transizione che rientra nella copia $l$": la traccia e' un $(k,l)$-loop.

$$L_k\ :=\ \bigvee_{l=0}^{k}\ {}_lL_k$$

Come leggerla: "esiste un punto di rientro": la traccia e' un $k$-loop per qualche $l$. Il quantificatore "esiste $l$" diventa una disgiunzione finita, perche' i candidati sono solo $k+1$.

Per dare la semantica dentro un $(k,l)$-loop serve sapere chi e' il "prossimo" di ogni posizione:

$$succ(i)=\begin{cases}i+1 & \text{se } i<k\\ l & \text{se } i=k\end{cases}$$

cioe' si avanza normalmente lungo il prefisso, e dall'ultima posizione si rientra nel punto $l$ del ciclo.

50. Encoding di $\varphi$ nel caso con loop

Per una traccia che e' un $(k,l)$-loop, la formula LTL si traduce ricorsivamente in una formula booleana ${}_l[\![\varphi]\!]_k^i$ ("$\varphi$ vale alla posizione $i$"):

• ${}_l[\![p]\!]_k^i:=p(\bar{s}_i)$ — il caso base, e il piu' importante: "la lettera $p$ vale al tempo $i$" diventa la formula booleana di $p$ valutata sulla copia $i$-esima delle variabili;
• ${}_l[\![\neg p]\!]_k^i:=\neg p(\bar{s}_i)$;
• congiunzioni e disgiunzioni si traducono per induzione sui due argomenti;
• ${}_l[\![X\varphi]\!]_k^i:={}_l[\![\varphi]\!]_k^{succ(i)}$ — "next" salta alla posizione successiva, che grazie a $succ$ esiste sempre (da $k$ si rientra in $l$);
• ${}_l[\![G\varphi]\!]_k^i:=\bigwedge_{j=\min(i,l)}^{k} {}_l[\![\varphi]\!]_k^j$ — "per sempre" diventa una congiunzione su tutte le posizioni che il cammino visitera' da $i$ in poi: quelle del ciclo e quelle del suffisso del prefisso (l'indice parte da $\min(i,l)$ proprio per coprire l'intero ciclo);
• ${}_l[\![F\varphi]\!]_k^i:=\bigvee_{j=\min(i,l)}^{k} {}_l[\![\varphi]\!]_k^j$ — "prima o poi" e' la disgiunzione sulle stesse posizioni;
• $\varphi\,U\,\psi$ segue la semantica: esiste una posizione futura (eventualmente raggiunta rientrando nel ciclo) dove vale $\psi$, e $\varphi$ vale in tutte le posizioni attraversate prima.

Il punto da capire e' uno solo: su un lasso le posizioni "future" sono un insieme finito e noto (prefisso + ciclo), quindi ogni quantificazione temporale diventa una congiunzione o disgiunzione finita. La semantica LTL standard si applica per intero: nessuna approssimazione.

51. Bounded semantics nel caso senza loop: le tre trappole

Se la traccia non ha loop-back, e' solo un prefisso: del futuro oltre $k$ non sappiamo nulla. La bounded semantics $\pi\models_k^i\varphi$ e' definita per essere prudente: dichiara vera una formula solo se il prefisso basta a garantirla, comunque continui il cammino.

• proposizioni e connettivi booleani: come sempre ($p$ vale se sta nell'etichetta dello stato $i$; induzione per $\lor$ e $\land$);
• trappola 1 — Next: $\pi\models_k^i X\varphi$ se e solo se $i<k$ e $\pi\models_k^{i+1}\varphi$. La condizione $i<k$ non e' pignoleria: serve a garantire che la posizione $i+1$ esista nel prefisso; all'ultima posizione, $X\varphi$ e' falsa perche' non possiamo verificarla;
• trappola 2 — Globally: $\pi\models_k^i G\varphi$ e' sempre falsa. Sembra brutale, ma e' inevitabile: "per sempre" parla di infinite posizioni, e un prefisso finito non puo' certificarle tutte. Nessun prefisso senza loop dimostra un $G$;
• trappola 3 — Eventually: $\pi\models_k^i F\varphi$ richiede un testimone entro il bound: esiste $j$ con $i\le j\le k$ e $\pi\models_k^j\varphi$. "Prima o poi, ma entro $k$";
• Until: $\pi\models_k^i\varphi\,U\,\psi$ se esiste $j$ con $i\le j\le k$ tale che $\psi$ vale in $j$ e $\varphi$ vale in tutte le posizioni $n$ con $i\le n<j$ — come la semantica standard, ma col testimone confinato nel prefisso.

La proprieta' che giustifica tutto (la conservativita'): se $\varphi$ e' vera su un prefisso sotto bounded semantics, allora e' vera, sotto semantica standard, su ogni estensione infinita di quel prefisso. Quindi un controesempio trovato con la bounded semantics e' un controesempio vero: niente falsi allarmi.

In forma di encoding (con la convenzione che oltre il bound tutto e' falso):

$$[\![\varphi]\!]_k^{k+1}:=\bot,\qquad [\![X\varphi]\!]_k^i:=[\![\varphi]\!]_k^{i+1},\qquad [\![F\varphi]\!]_k^i:=\bigvee_{j=i}^{k}[\![\varphi]\!]_k^j,$$

$$[\![\varphi\,U\,\psi]\!]_k^i:=\bigvee_{j=i}^{k}\Big([\![\psi]\!]_k^j\land \bigwedge_{n=i}^{j-1}[\![\varphi]\!]_k^n\Big),$$

e $G\varphi$ risulta falso automaticamente (la sua espansione arriva sempre a toccare la posizione $k+1$, dove vale $\bot$).

52. La formula complessiva e il teorema di soundness

Mettendo insieme i pezzi, la formula che il BMC consegna al SAT solver all'iterazione $k$ e':

$$[\![M,\varphi]\!]_k\ :=\ [\![M]\!]_k\ \land\ \Big(\big(\neg L_k\land[\![\varphi]\!]_k^0\big)\ \lor\ \bigvee_{l=0}^{k}\big({}_lL_k\land{}_l[\![\varphi]\!]_k^0\big)\Big).$$

Come leggerla, da sinistra a destra: "la sequenza di assegnamenti e' una vera esecuzione lunga $k$ ($[\![M]\!]_k$), e: o non c'e' alcun loop-back ($\neg L_k$) e allora $\varphi$ vale alla posizione 0 secondo la bounded semantics, oppure c'e' un rientro in $l$ (${}_lL_k$) e allora $\varphi$ vale alla posizione 0 secondo la semantica standard sul lasso".

Teorema (soundness). $[\![M,\varphi]\!]_k$ e' soddisfacibile se e solo se $\mathcal{M}\models_k E\varphi$, cioe' se esiste una traccia bounded da $k$ passi che soddisfa $\varphi$.

Conseguenze operative: se il solver dice SAT, l'assegnamento trovato contiene i valori di tutte le copie $\bar{s}_0,\ldots,\bar{s}_k$, cioe' il controesempio leggibile stato per stato. Se dice UNSAT, sappiamo che non esiste un controesempio di lunghezza $\le k$ — e nient'altro: potrebbe esisterne uno piu' lungo.

53. Completezza: cosa succede se il bug non c'e'

Qui sta il limite strutturale del BMC. L'algoritmo e':

1. $k:=0$;
2. chiama il SAT solver su $[\![M,\varphi]\!]_k$;
3. se SAT: stop, controesempio trovato; altrimenti $k:=k+1$ e torna al punto 2.

Se il sistema soddisfa la proprieta' (cioe' il controesempio non esiste), questo ciclo non termina mai da solo: ogni UNSAT dice solo "non a questa lunghezza". Per fermarsi legittimamente bisogna sapere a priori un bound $k^*$ con la garanzia:

se esiste un controesempio, ne esiste uno di lunghezza al massimo $k^*$.

Bound del genere esistono — il diametro del grafo degli stati per raggiungibilita', il recurrence diameter (il piu' lungo cammino senza stati ripetuti) per le proprieta' generali, il completeness threshold — ma calcolarli e' molto costoso, spesso quanto il problema originale. Per questo nella pratica:

il BMC si usa come bug finder, non come prover: SAT = bug trovato (con traccia); una serie di UNSAT per $k$ piccoli = "nessun bug corto", che aumenta la fiducia ma non e' una dimostrazione di correttezza.

54. BMC incrementale

Un dettaglio pratico importante: passando da $k$ a $k+1$ la formula cambia pochissimo — si aggiunge una copia di variabili $\bar{s}_{k+1}$, un congiunto $T(\bar{s}_k,\bar{s}_{k+1})$, e si aggiorna la parte sulla violazione. I SAT solver moderni supportano l'incremental solving: riusano tra una chiamata e l'altra le clausole apprese e lo stato interno, invece di ripartire da zero. Il ciclo del BMC e' fatto apposta per sfruttarlo.

55. Uno sguardo a nuXmv

nuXmv e' il model checker simbolico che chiude il capitolo: erede di NuSMV, analizza sistemi a stati finiti e infiniti:

• per il caso finito offre sia il motore BDD-based (i punti fissi della Parte V) sia un motore SAT-based moderno (il BMC della Parte VII): le due meta' del capitolo convivono nello stesso strumento;
• per il caso infinito usa tecniche SMT, tramite l'integrazione con MathSAT5.

Il linguaggio di modellazione e' quello visto nella sezione 46 (VAR, INIT, TRANS, piu' le IVAR per gli input controllati dall'ambiente e lo stile alternativo ASSIGN init(v)/next(v)). Le proprieta' si dichiarano nel file, ad esempio per LTL:

LTLSPEC G !(bad);

con la sintassi $X,F,G,U,R$. E' il punto in cui tutta la teoria del capitolo (encoding booleano, unrolling, loopback) diventa un comando concreto da eseguire.

Parte VIII — Quadro finale

56. OBDD contro SAT/BMC: quando usare cosa

Le due tecniche simboliche non sono in competizione: rispondono a domande diverse.

Symbolic model checking con OBDD. Punti forti: dimostra proprieta' su tutto il modello (punti fissi = quantificazione su tutti i cammini); rappresenta insiemi enormi in modo compatto quando l'ordine e' buono; e' la tecnica naturale per CTL e per la raggiungibilita' completa. Limiti: la taglia degli OBDD dipende criticamente dall'ordine delle variabili (e trovare quello ottimo e' NP-completo); alcune funzioni sono grandi per qualunque ordine; il relational product puo' esplodere nei passaggi intermedi.

SAT-based BMC. Punti forti: eccellente nel trovare controesempi, anche profondi, sfruttando SAT solver modernissimi; non costruisce mai l'insieme degli stati raggiungibili; la formula cresce in modo controllato con $k$. Limiti: UNSAT a bound basso non dimostra nulla; la completezza richiede bound (diametri) costosi da calcolare; le proprieta' di liveness richiedono la macchineria dei lassi.

Regola di scelta: per dimostrare una proprieta' su tutto il modello, OBDD/punti fissi; per cercare rapidamente un bug, BMC; se l'esplosione nasce da molte interleaving indipendenti, la POR riduce il grafo prima o durante l'esplorazione. Nella pratica industriale le tecniche si combinano.

57. Collegamento con i capitoli 8 e 10

Indietro (capitolo 8). Il capitolo 9 non cambia la teoria logica: cambia la rappresentazione. Dove il capitolo 8 scriveva $Sat(\varphi)\subseteq S$ come insieme esplicito, ora c'e' la formula $CHECK(\varphi)(\bar{x})$; dove calcolava $Pre(X)$ visitando archi, ora c'e' $\exists\bar{x}'.R(\bar{x},\bar{x}')\land X(\bar{x}')$. Gli algoritmi sono gli stessi, tradotti in operazioni su formule.

Avanti (capitolo 10). La sintesi e' piu' difficile del model checking: non verifica un sistema dato, deve costruirlo. Le idee di questo capitolo ricompaiono identiche: rappresentare insiemi di posizioni, calcolare regioni vincenti con punti fissi, evitare enumerazioni esplicite.

58. Errori tipici

• Pensare che "simbolico" significhi "approssimato". No: il model checking simbolico e' esatto. Cambia la rappresentazione degli insiemi, non la semantica della logica.
• Confondere OBDD e SAT. Un OBDD rappresenta una funzione booleana come DAG canonico (e rende facili equivalenza e quantificazione); un SAT solver cerca un assegnamento che soddisfa una formula. Strumenti diversi, usati da tecniche diverse (punti fissi vs BMC).
• Credere che BMC dimostri correttezza. UNSAT al bound $k$ esclude solo i controesempi di lunghezza $\le k$. Per una dimostrazione serve un completeness threshold (costoso) o un'altra tecnica.
• Dimenticare le variabili primate. Senza $\bar{x}'$ non si puo' nemmeno scrivere "il valore cambia": la relazione di transizione vive su due copie delle variabili.
• Scambiare $Pre_E$ e $Pre_A$. "Esiste un successore buono" ($EX$) e "tutti i successori sono buoni" ($AX$) sono proprieta' opposte: scambiarle ribalta il significato delle formule CTL.
• Dimenticare che la canonicita' e' relativa all'ordine. Due OBDD si confrontano solo se costruiti con lo stesso ordine di variabili.
• Nel BMC, dimenticare il caso senza loop. $G\varphi$ su un prefisso senza loop-back e' sempre falso: un prefisso finito non certifica un "per sempre".

59. Mini-esercizi svolti

Esercizio 1 (preimmagine). $R(x,x')=(x'\leftrightarrow\neg x)$. Calcolare $Pre_E(x')$.

Svolgimento: $\exists x'.(x'\leftrightarrow\neg x)\land x'$. Caso $x'=0$: $(0\leftrightarrow\neg x)\land 0=0$. Caso $x'=1$: $(1\leftrightarrow\neg x)\land 1=\neg x$. Disgiunzione: $\neg x$. Risultato: $Pre_E(x')=\neg x$ (per finire in $x=1$ col sistema che inverte, bisogna partire da $x=0$).

Esercizio 2 (punto fisso EF). Dato $Goal(\bar{x})$, scrivere il calcolo simbolico di $EF\,goal$ e spiegarlo.

Svolgimento: $Z_0=Goal$, $Z_{i+1}=Z_i\lor Pre_E(Z_i)$, stop quando $Z_{i+1}=Z_i$. A ogni iterazione si aggiungono gli stati che raggiungono in un passo una regione gia' buona; $Z_i$ = "raggiungo $goal$ in $\le i$ passi"; la catena cresce, il modello e' finito, quindi si stabilizza sul minimo punto fisso, che e' $EF\,goal$.

Esercizio 3 (riduzione OBDD). Ridurre l'OBDD di $f=(x\land y)\lor(x\land\neg y)$ con ordine $x<y$.

Svolgimento: algebricamente $f=x\land(y\lor\neg y)=x$. Sul grafo: il nodo $y$ raggiunto con $x=1$ ha entrambi i figli sulla foglia... attenzione, va costruito: con $x=0$ entrambi i rami portano a 0; con $x=1$, $y=0$ da' 1 e $y=1$ da' 1, quindi il nodo $y$ ha $low=high=1$ e cade per la regola 3 (test ridondante). Resta il solo test su $x$: $x=0\to 0$, $x=1\to 1$. Risultato: l'OBDD ridotto e' il singolo nodo $x$ con le due foglie.

Esercizio 4 (BMC safety, $k=2$). Scrivere l'encoding per cercare una violazione di $G\,\neg bad$ entro 2 passi.

Svolgimento: la negazione della proprieta' e' $F\,bad$; su un prefisso la bounded semantics richiede un testimone entro il bound, quindi:

$$I(\bar{s}_0)\land T(\bar{s}_0,\bar{s}_1)\land T(\bar{s}_1,\bar{s}_2) \land\big(bad(\bar{s}_0)\lor bad(\bar{s}_1)\lor bad(\bar{s}_2)\big).$$

Se SAT: l'assegnamento e' una traccia di al piu' 2 passi che tocca uno stato bad (per una violazione di safety non serve il lasso: il prefisso basta, per conservativita'). Se UNSAT: nessuna violazione entro 2 passi — il che non prova che $bad$ sia irraggiungibile in assoluto.

60. Mappa per l'orale

Sequenza con cui ricostruire il capitolo a voce:

1. Problema: state explosion ($2^n$ con $n$ variabili; prodotto e interleaving con la concorrenza); esplicito $\approx 10^6$ stati, serve cambiare rappresentazione.
2. Mondo simbolico: stato = assegnamento a $\bar{x}$; insieme di stati = formula (funzione caratteristica); transizione = $R(\bar{x},\bar{x}')$ con variabili primate; operazioni insiemistiche = connettivi.
3. Movimenti: $Post$, $Pre_E$, $Pre_A$ con i quantificatori booleani; $Pre_E=EX$, $Pre_A=AX$.
4. Punti fissi: reticolo $Powerset(S)$, predicate transformer, monotonia (saperne dimostrare una!), Tarski ($\mu$ = intersezione dei pre-punti fissi, $\nu$ = unione dei post-punti fissi), i 4 lemmi del caso finito, algoritmi lfp/gfp con invariante e bound $|S|$.
5. CTL come punti fissi: le sei equazioni; regola mnemonica (F da' $\mu$, G da' $\nu$, U sempre $\mu$); saper tracciare $EG\,p$ e $E[p\,U\,q]$ sugli esempi.
6. OBDD: decision tree (comparatore), funzione di un nodo, Shannon, le tre regole di riduzione, ordine (3n+2 vs $3\cdot 2^n-1$; NP-completezza), canonicita' e sue conseguenze.
7. Operazioni: restrict (regola dei puntatori), apply (4 casi + memoizzazione $O(|f||f'|)$), negazione (scambio foglie), quantificazione ($\exists x f=f|_0\lor f|_1$), relational product.
8. CHECK: induttivo; bastano EX/EU/EG (dualita'); CheckEX = relational product; CheckEU = lfp; CheckEG = gfp.
9. POR: azioni indipendenti, un rappresentante per classe di interleaving, cautela con proprieta' che osservano l'ordine.
10. BMC: riduzione a $E\varphi$ con $\varphi=\neg\psi$; unrolling $[\![M]\!]_k$; lasso/(k,l)-loop e $succ$; bounded semantics (X con $i<k$, G sempre falso, F entro il bound); formula complessiva; soundness; completezza via recurrence diameter (costoso) $\Rightarrow$ bug finder; incrementale; nuXmv.
11. Confronto finale: OBDD per dimostrare, BMC per cercare bug, POR per la concorrenza.

61. Riassunto finale

Il capitolo 9 rende eseguibili su sistemi reali gli algoritmi del capitolo 8.

Il model checking simbolico non enumera stati: codifica insiemi di stati e transizioni come funzioni booleane, esegue le operazioni insiemistiche come operazioni logiche, e calcola gli operatori CTL come punti fissi di predicate transformer monotoni — con la garanzia di Tarski sull'esistenza e con convergenza in al piu' $|S|$ iterazioni. Gli OBDD sono la struttura dati che rende tutto questo efficiente: canonici (equivalenza in tempo costante, test di arresto dei punti fissi immediato), spesso compatti con un buon ordine delle variabili, e dotati di tutte le operazioni necessarie (restrict, apply, quantificazione, relational product).

Il BMC segue la strada opposta: non costruisce l'insieme degli stati raggiungibili, ma cerca un controesempio di lunghezza $\le k$ traducendo unrolling + violazione in una formula SAT; i cammini infiniti sono catturati dai lassi, i prefissi senza loop da una semantica prudente. E' eccellente per trovare bug; per dimostrare correttezza servirebbe un bound di completezza costoso.

La regola mentale conclusiva:

OBDD e punti fissi servono a ragionare globalmente su insiemi di stati; BMC e SAT servono a cercare rapidamente tracce di errore entro un limite; la POR toglie di mezzo la ridondanza creata dalla concorrenza.