Logiche classiche - Riassunto

Punti chiave

• Fondamenti della logica: sintassi, semantica e vocabolario della logica proposizionale e della logica del primo ordine.
• Soddisfacibilita e validita: una formula e' soddisfacibile se e' vera in almeno un'interpretazione; e' valida se e' vera in tutte.
• Riduzioni: molti problemi logici si riducono l'uno all'altro, ad esempio equivalenza e validita.

Argomenti centrali

• Espressivita vs decidibilita: aumentando l'espressivita del linguaggio spesso aumenta anche il costo computazionale, fino all'indecidibilita.
• Base per i formalismi avanzati: LTL, CTL, S1S e altri linguaggi di specifica poggiano sui concetti della logica classica.

Rilevanza per V&V in AI

La logica fornisce il linguaggio matematico con cui formalizzare proprieta, requisiti e vincoli dei sistemi da verificare.

Logica proposizionale

La logica proposizionale usa variabili booleane e connettivi per costruire formule vere o false rispetto a un'interpretazione.

Sintassi

Le formule si costruiscono da proposizioni atomiche tramite: $$ \neg,\land,\lor,\rightarrow,\leftrightarrow$$

Semantica

Un'interpretazione assegna vero o falso a ogni proposizione. Una formula e' soddisfatta se valuta a vero sotto quell'assegnamento.

Problemi principali

• Model checking: valutare una formula su una struttura data.
• SAT: decidere se esiste un'interpretazione che rende vera la formula.
• Validita: decidere se la formula e' vera in tutte le interpretazioni.

Forme normali

• NNF: negazioni solo davanti agli atomi.
• CNF: congiunzione di clausole.

Rilevanza

SAT e le formule booleane sono alla base di BMC, QBF e molte tecniche simboliche.

Collegamenti

• Formule booleane quantificate (QBF)
• Algoritmo dei tableaux
• Model checking limitato

Formule booleane quantificate

Le QBF estendono la logica proposizionale con quantificatori su variabili booleane.

Sintassi e semantica

Si possono scrivere formule come: $$\exists p\;\varphi \quad\text{e}\quad \forall p\;\varphi$$

• $\exists p\;\varphi$ e' vera se almeno una scelta di valore per $p$ rende vera $\varphi$.
• $\forall p\;\varphi$ e' vera se entrambe le scelte di valore per $p$ rendono vera $\varphi$.

Complessita

La verita di una QBF completamente quantificata e' PSPACE-completa, piu difficile del SAT proposizionale.

Uso

Le QBF permettono di rappresentare in modo succinto problemi di gioco, reachability e verifica con alternanza di scelte esistenziali e universali.

Collegamenti

• Logica proposizionale
• Model checking simbolico

Logica del primo ordine

La logica del primo ordine estende la logica proposizionale introducendo variabili su oggetti, predicati, funzioni e quantificatori.

Elementi

• variabili individuali come $x,y,z$;
• predicati e relazioni;
• quantificatori $\forall$ ed $\exists$;
• connettivi booleani.

Espressivita e decidibilita

La logica del primo ordine e' molto espressiva, ma il ragionamento generale su di essa e' indecidibile. Per questo la verifica formale usa spesso frammenti decidibili o logiche specializzate come LTL, CTL e S1S.

Giochi e formule di Hintikka

I giochi di Ehrenfeucht-Fraisse e le formule di Hintikka permettono di studiare quali strutture sono distinguibili da formule di una certa profondita.

Uso in V&V

FOL fornisce il linguaggio per esprimere invarianti, relazioni tra stati e proprieta strutturali, ma in pratica va controllata la trattabilita del frammento scelto.

Collegamenti

• Logica proposizionale
• Formule booleane quantificate (QBF)
• Giochi di Ehrenfeucht-Fraïssé
• Formule di Hintikka

Algoritmo dei tableaux

L'algoritmo dei tableaux e' una procedura per decidere la soddisfacibilita di formule logiche decomponendole in sottoformule.

Idea

Invece di indovinare direttamente un modello, si scompone la formula fino a ottenere rami fatti di letterali. Un ramo aperto rappresenta un possibile modello; un ramo chiuso contiene una contraddizione.

Regole principali

• Congiunzioni: entrambi i congiunti devono stare nello stesso ramo.
• Disgiunzioni: il ramo si divide in alternative.
• Contraddizione: un ramo con $p$ e $\neg p$ viene chiuso.

LTL

Nel caso LTL, il tableau deve gestire anche obblighi temporali, ad esempio eventualita che devono essere realizzate lungo un cammino infinito.

Collegamenti

• Logica proposizionale
• Logica temporale lineare (LTL)

Giochi di Ehrenfeucht-Fraisse

I giochi di Ehrenfeucht-Fraisse forniscono una caratterizzazione ludica dell'equivalenza logica tra strutture.

Meccanica

Il gioco si svolge tra Spoiler e Duplicator su due strutture. A ogni turno Spoiler sceglie un elemento in una struttura e Duplicator risponde scegliendo un elemento nell'altra.

Duplicator vince dopo $n$ round se gli elementi scelti preservano le relazioni rilevanti, cioe' formano un isomorfismo parziale.

Significato logico

Due strutture sono indistinguibili da formule del primo ordine di profondita quantificazionale $n$ se e solo se Duplicator ha una strategia vincente nel gioco di $n$ round.

Uso

Questi giochi servono a mostrare limiti espressivi della logica: se Duplicator puo sempre vincere, nessuna formula del frammento considerato distingue le due strutture.

Collegamenti

• Logica del primo ordine
• Formule di Hintikka

Formule di Hintikka

Le formule di Hintikka descrivono completamente cio' che una struttura soddisfa fino a una certa profondita quantificazionale.

Idea

Per ogni livello $n$, la formula di Hintikka rappresenta la classe di equivalenza logica della struttura rispetto alle formule di profondita al massimo $n$.

Relazione con EF games

Due strutture soddisfano la stessa formula di Hintikka di livello $n$ se e solo se Duplicator ha una strategia vincente nel gioco di Ehrenfeucht-Fraisse di $n$ round.

Importanza

Sono uno strumento teorico per studiare espressivita, equivalenza e limiti della logica del primo ordine.

Collegamenti

• Logica del primo ordine
• Giochi di Ehrenfeucht-Fraïssé

Approfondimento Completo Settimana 1 - Logica, Formule e Ragionamento Automatico

Questo documento costituisce un'espansione dettagliata e teorica (passo per passo) degli argomenti introduttivi della prima settimana di V&V. Sostituisce il riassunto precedente con una trattazione approfondita necessaria per la comprensione rigorosa dei concetti formali su cui si basano il model checking e le altre tecniche di verifica.

1. Logica Proposizionale: Fondamenti e Definizioni Formali

La logica proposizionale è il linguaggio matematico più semplice per ragionare sulla verità e falsità di affermazioni elementari. Nonostante la sua semplicità, i problemi algoritmici associati (come il SAT) sono fondamentali nell'informatica teorica e nella verifica dei sistemi.

1.1 Sintassi

La sintassi definisce quali sequenze di simboli sono "formule ben formate" (WFF, Well-Formed Formulas). Partiamo da un insieme infinito numerabile di variabili proposizionali (o atomi): $\mathcal{P} = \{p_1, p_2, q, r, \dots\}$. A queste uniamo i connettivi logici classici e le parentesi.

L'insieme delle formule proposizionali $\mathcal{F}$ è definito induttivamente (o ricorsivamente) come segue: 1. Caso base: Ogni variabile proposizionale $p \in \mathcal{P}$ è una formula ($p \in \mathcal{F}$). Anche le costanti speciali $\top$ (Vero) e $\bot$ (Falso) sono in $\mathcal{F}$. 2. Passo induttivo: Se $\varphi$ e $\psi$ sono formule in $\mathcal{F}$, allora lo sono anche: - $\neg \varphi$ (Negazione, "non $\varphi$") - $(\varphi \land \psi)$ (Congiunzione, "$\varphi$ e $\psi$") - $(\varphi \lor \psi)$ (Disgiunzione, "$\varphi$ o $\psi$") - $(\varphi \rightarrow \psi)$ (Implicazione, "se $\varphi$ allora $\psi$") - $(\varphi \leftrightarrow \psi)$ (Doppia implicazione, "$\varphi$ se e solo se $\psi$") 3. Chiusura: Nient'altro è una formula.

Nota teorica: L'uso delle parentesi è cruciale per evitare ambiguità sintattiche. Nella pratica, adottiamo regole di precedenza (ad esempio $\neg$ lega più forte di $\land$ e $\lor$, che a loro volta legano più di $\rightarrow$) per omettere parentesi superflue.

1.2 Semantica

La semantica attribuisce un significato (un valore di verità) alle formule sintatticamente corrette. Nella logica classica, il principio di bivalenza stabilisce che ogni proposizione è o vera o falsa.

Un'interpretazione (o assegnamento, o modello) è una funzione $\mathcal{I}: \mathcal{P} \rightarrow \{0, 1\}$ (dove $1$ sta per Vero e $0$ per Falso) che mappa ogni atomo a un valore di verità. Data un'interpretazione $\mathcal{I}$, il valore di verità di una formula complessa $\varphi$ sotto $\mathcal{I}$, denotato con $\mathcal{I} \models \varphi$ (letto "$\mathcal{I}$ modella $\varphi$" o "$\varphi$ è vera in $\mathcal{I}$"), si calcola in modo ricorsivo strutturale: - $\mathcal{I} \models p$ se e solo se $\mathcal{I}(p) = 1$ (per $p \in \mathcal{P}$). - $\mathcal{I} \models \neg \varphi$ se e solo se $\mathcal{I} \not\models \varphi$. - $\mathcal{I} \models \varphi \land \psi$ se e solo se $\mathcal{I} \models \varphi$ e $\mathcal{I} \models \psi$. - $\mathcal{I} \models \varphi \lor \psi$ se e solo se $\mathcal{I} \models \varphi$ oppure $\mathcal{I} \models \psi$. - $\mathcal{I} \models \varphi \rightarrow \psi$ se e solo se $\mathcal{I} \not\models \varphi$ oppure $\mathcal{I} \models \psi$. (Nota: l'implicazione materiale è falsa solo quando la premessa è vera e la conseguenza è falsa). - $\mathcal{I} \models \varphi \leftrightarrow \psi$ se e solo se $\mathcal{I} \models \varphi \rightarrow \psi$ e $\mathcal{I} \models \psi \rightarrow \varphi$.

1.3 Soddisfacibilità, Validità ed Equivalenza Logica

Dalla semantica derivano le definizioni dei principali problemi decisionali della logica:

1. Soddisfacibilità (SAT): Una formula $\varphi$ è soddisfacibile se esiste almeno un'interpretazione $\mathcal{I}$ tale che $\mathcal{I} \models \varphi$. Questa $\mathcal{I}$ è chiamata un modello per $\varphi$. Se non esiste, $\varphi$ è detta insoddisfacibile (o contraddizione).
2. Validità (Tautologia): Una formula $\varphi$ è valida se per ogni interpretazione $\mathcal{I}$ si ha $\mathcal{I} \models \varphi$. La validità è indicata scrivendo semplicemente $\models \varphi$.
3. Equivalenza logica: Due formule $\varphi$ e $\psi$ sono logicamente equivalenti, scritto $\varphi \equiv \psi$, se per ogni interpretazione $\mathcal{I}$, $\mathcal{I} \models \varphi$ se e solo se $\mathcal{I} \models \psi$. Questo significa che le loro tavole di verità sono identiche.

Teorema fondamentale (Relazione Validità-Insoddisfacibilità): Una formula $\varphi$ è valida se e solo se la sua negazione $\neg \varphi$ è insoddisfacibile. Dimostrazione passo-passo: - Supponiamo che $\varphi$ sia valida. Ciò significa che ogni interpretazione rende $\varphi$ vera. Di conseguenza, nessuna interpretazione può rendere falsa $\varphi$. Per definizione della semantica della negazione, nessuna interpretazione può rendere vera $\neg \varphi$. Dunque $\neg \varphi$ è insoddisfacibile. - Viceversa, supponiamo $\neg \varphi$ sia insoddisfacibile. Nessuna interpretazione rende vera $\neg \varphi$. Pertanto, ogni interpretazione deve rendere falsa $\neg \varphi$, il che significa che ogni interpretazione rende vera $\varphi$. Quindi $\varphi$ è valida.

Questa relazione è il pilastro del ragionamento automatico (come nei risolutori SAT): per dimostrare che un sistema è corretto (una proprietà $\varphi$ è sempre valida), il solver tenta di trovare un controesempio, ossia un modello per $\neg \varphi$. Se fallisce, il sistema è sicuro.

2. Forme Normali e Trasformazioni

Lavorare con la sintassi completa della logica proposizionale è scomodo per gli algoritmi. Spesso occorre normalizzare le formule.

2.1 Negation Normal Form (NNF)

Una formula è in NNF se l'operatore di negazione $\neg$ viene applicato esclusivamente alle variabili proposizionali (atomi) e non compaiono gli operatori $\rightarrow$ e $\leftrightarrow$. In NNF si usano solo $\land, \lor$ e $\neg$ (solo sugli atomi). Esempio: $\neg p \lor (q \land \neg r)$ è in NNF. $\neg(p \lor q)$ non lo è.

Algoritmo per la conversione in NNF: 1. Eliminare le doppie implicazioni: sostituire $\varphi \leftrightarrow \psi$ con $(\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$. 2. Eliminare le implicazioni: sostituire $\varphi \rightarrow \psi$ con $\neg \varphi \lor \psi$. 3. Spingere le negazioni verso l'interno usando le leggi di De Morgan: - $\neg(\varphi \land \psi) \equiv \neg\varphi \lor \neg\psi$ - $\neg(\varphi \lor \psi) \equiv \neg\varphi \land \neg\psi$ 4. Eliminare le doppie negazioni: $\neg\neg\varphi \equiv \varphi$.

Esempio passo-passo: Convertire $\neg(p \rightarrow (q \land \neg r))$ in NNF. - Passo 2 (elimino implicazione): $\neg(\neg p \lor (q \land \neg r))$ - Passo 3 (De Morgan sul $\lor$): $\neg\neg p \land \neg(q \land \neg r)$ - Passo 4 (doppia negazione): $p \land \neg(q \land \neg r)$ - Passo 3 (De Morgan sul $\land$): $p \land (\neg q \lor \neg\neg r)$ - Passo 4 (doppia negazione): $p \land (\neg q \lor r)$. (Forma finale in NNF).

2.2 Conjunctive Normal Form (CNF) e Disjunctive Normal Form (DNF)

• Un letterale è un atomo ($p$) o la negazione di un atomo ($\neg p$).
• Una formula è in CNF se è una congiunzione di disgiunzioni di letterali. (Un "AND di OR"). Le disgiunzioni di letterali sono chiamate clausole. Esempio: $(p \lor \neg q) \land (\neg r \lor s \lor t)$. Molti SAT solver (es. basati sull'algoritmo DPLL/CDCL) accettano input solo in CNF.
• Una formula è in DNF se è una disgiunzione di congiunzioni di letterali. (Un "OR di AND"). Esempio: $(p \land \neg q) \lor (\neg r \land s \land t)$.

Per convertire in CNF, dopo aver ottenuto la NNF, si applica ripetutamente la proprietà distributiva dell'OR rispetto all'AND: - $\varphi \lor (\psi \land \chi) \equiv (\varphi \lor \psi) \land (\varphi \lor \chi)$. Attenzione: Questa distribuzione può portare a un'esplosione esponenziale delle dimensioni della formula. In applicazioni reali (es. in SAT solving) si usa la Trasformazione di Tseitin, che introduce variabili ausiliarie per convertire una formula in CNF in tempo e spazio lineari, preservando la soddisfacibilità.

3. Algoritmo dei Tableaux Semantici

L'algoritmo dei tableaux è un metodo di deduzione che verifica la soddisfacibilità di una formula cercando di costruire sistematicamente un modello per essa. Funziona decomponendo la formula originaria secondo regole semantiche.

3.1 Funzionamento del Tableau

Il tableau assume la forma di un albero. La radice dell'albero è la formula da verificare. Si procede applicando regole di espansione ai nodi, decomponendo le formule in base al loro connettivo principale. Le regole si dividono in due tipi (assumendo la formula sia già ridotta usando $\neg, \land, \lor$):

• Regole $\alpha$ (espansione lineare o and-rule): Decompongono congiunzioni. Se un ramo contiene $\varphi \land \psi$, il ramo viene esteso inserendo sia $\varphi$ che $\psi$ uno sotto l'altro (poiché entrambi devono essere veri per rendere vera la congiunzione).
• Regole $\beta$ (espansione ramificata o or-rule): Decompongono disgiunzioni. Se un ramo contiene $\varphi \lor \psi$, il ramo si biforca in due nuovi sotto-rami: uno contenente $\varphi$ e l'altro contenente $\psi$. Questo rappresenta un punto di scelta non deterministica (almeno uno dei due deve essere vero).

Per usare il tableau con tutti i connettivi senza convertirli, esistono regole anche per le negazioni: - $\neg(\varphi \land \psi)$ diventa una regola $\beta$ biforcando in $\neg\varphi$ e $\neg\psi$ (per De Morgan). - $\neg(\varphi \lor \psi)$ diventa una regola $\alpha$ aggiungendo $\neg\varphi$ e $\neg\psi$ sullo stesso ramo. - $\neg\neg\varphi$ viene semplicemente semplificato in $\varphi$.

3.2 Rami Aperti, Rami Chiusi e Conclusione

• Ramo chiuso: Un ramo in cui compaiono simultaneamente una formula $\varphi$ e la sua negazione esatta $\neg\varphi$ (o comunemente un atomo $p$ e $\neg p$). Si contrassegna con una "X". Questo significa che il percorso ha portato a una contraddizione: non è possibile trovare un modello seguendo quelle scelte.
• Ramo aperto: Un ramo in cui sono state decomposte tutte le formule complesse e non sono state trovate contraddizioni (contiene solo letterali compatibili).

Teoremi di completezza e correttezza: - Una formula $\varphi$ è insoddisfacibile se e solo se esiste un tableau per $\varphi$ in cui tutti i rami si chiudono. (Il tableau diventa una dimostrazione di contraddizione). - Una formula $\varphi$ è soddisfacibile se e solo se il suo tableau completamente sviluppato presenta almeno un ramo aperto. I letterali su quel ramo aperto definiscono l'assegnamento (modello) che soddisfa la formula.

3.3 Esempio Guidato Passo-Passo

Vogliamo dimostrare la validità del Modus Tollens: $((p \rightarrow q) \land \neg q) \rightarrow \neg p$. Per verificare se è valida, ne cerchiamo un controesempio testando l'insoddisfacibilità della sua negazione: Formula da testare: $\neg [((p \rightarrow q) \land \neg q) \rightarrow \neg p]$

Passo 1: Regola $\alpha$ sull'implicazione negata. L'implicazione negata $\neg(A \rightarrow B)$ equivale ad $A \land \neg B$. Il ramo si espande con: 1. $((p \rightarrow q) \land \neg q)$ 2. $\neg\neg p$

Passo 2: Semplificazione e regola $\alpha$ sulla congiunzione (riga 1). Riga 2 si semplifica in $p$. Riga 1 si decompone mettendo sullo stesso ramo: 3. $(p \rightarrow q)$ 4. $\neg q$ A questo punto il nostro ramo lineare contiene: $\{p, (p \rightarrow q), \neg q\}$.

Passo 3: Regola $\beta$ sull'implicazione (riga 3). L'implicazione $(p \rightarrow q)$ equivale a $\neg p \lor q$. Pertanto, la regola $\beta$ fa biforcare il ramo corrente in due: - Ramo Sinistro: aggiungiamo $\neg p$. Ora questo ramo contiene $\{p, \neg q, \neg p\}$. È presente sia $p$ che $\neg p$. Il ramo si chiude (X). - Ramo Destro: aggiungiamo $q$. Ora questo ramo contiene $\{p, \neg q, q\}$. È presente sia $q$ che $\neg q$. Il ramo si chiude (X).

Conclusione: Poiché tutti i rami si sono chiusi, la formula in input $\neg [((p \rightarrow q) \land \neg q) \rightarrow \neg p]$ è insoddisfacibile. Di conseguenza, la formula originale è logicamente valida (una tautologia).

4. Formule Booleane Quantificate (QBF)

Mentre la logica proposizionale lavora solo su variabili libere implicitamente quantificate a un livello base, le QBF (Quantified Boolean Formulas) estendono il linguaggio introducendo i quantificatori universali ($\forall$) ed esistenziali ($\exists$) che agiscono su variabili booleane.

4.1 Sintassi e Semantica Intuitiva

Una QBF ha la forma tipica: $Q_1 x_1 \dots Q_n x_n \ \varphi$, dove $Q_i \in \{\exists, \forall\}$ e $\varphi$ è una formula proposizionale senza quantificatori. Tutte le variabili in $\varphi$ devono essere quantificate (si parla di QBF chiuse o formule fully-quantified). Poiché non ci sono variabili libere, il valore di verità di una QBF chiusa non dipende da un'interpretazione, è assolutamente Vero o Falso.

• $\exists x \ \varphi(x)$ si interpreta come "esiste un valore booleano per $x$ tale per cui $\varphi(x)$ sia vera". Matematicamente, equivale a $\varphi(0) \lor \varphi(1)$.
• $\forall x \ \varphi(x)$ si interpreta come "per ogni valore booleano assegnato ad $x$, $\varphi(x)$ è vera". Equivale a $\varphi(0) \land \varphi(1)$.

Nota sulla complessità: Valutare la verità di una QBF chiusa (il problema TQBF - True Quantified Boolean Formula) è un problema PSPACE-completo. È computazionalmente più "difficile" del problema SAT (che è "solo" NP-completo). SAT si può vedere come un caso particolare di QBF in cui tutti i quantificatori sono esistenziali ($\exists x_1 \exists x_2 \dots \varphi$).

4.2 La prospettiva della Teoria dei Giochi

L'intuizione più profonda per le QBF, vitale per la verifica formale, è concepirle come un gioco a due giocatori. Supponiamo di avere la QBF: $\forall x \ \exists y \ \forall z \ \varphi(x, y, z)$.

• Il giocatore Universale (la natura o l'ambiente non deterministico) sceglie i valori per le variabili quantificate universalmente ($x, z$). Questo giocatore vince se riesce a rendere falsa la matrice proposizionale $\varphi$.
• Il giocatore Esistenziale (il controllore o il risolutore) sceglie i valori per le variabili esistenziali ($y$). Questo giocatore vince se riesce a rendere vera $\varphi$.
• L'ordine dei quantificatori definisce la sequenza dei turni, che implica chi ha informazioni su quali scelte precedentemente effettuate.

Esempio: Confrontiamo $\forall x \exists y \ (x \leftrightarrow y)$ e $\exists y \forall x \ (x \leftrightarrow y)$. 1. $\forall x \exists y \ (x \leftrightarrow y)$: Inizia l'ambiente scegliendo $x$. Poi, conoscendo $x$, il controllore sceglie $y$. Il controllore può semplicemente copiare il valore di $x$ in $y$. La formula originale sarà vera ($1 \leftrightarrow 1$ o $0 \leftrightarrow 0$). Il controllore ha una strategia vincente. La QBF è Vera. 2. $\exists y \forall x \ (x \leftrightarrow y)$: Il controllore deve scegliere un valore per $y$ per primo, al buio. Se sceglie $y=1$, l'ambiente al turno dopo (vedendo $y$) sceglie maliziosamente $x=0$, falsificando la formula ($0 \leftrightarrow 1$ è falso). Se il controllore sceglie $y=0$, l'ambiente sceglie $x=1$, vincendo ancora. Il controllore non ha una strategia vincente. La QBF è Falsa.

Questo paradigma a "mosse alternate" è esattamente il meccanismo su cui si basa il Bounded Model Checking e la pianificazione nei giochi a somma zero (parità) e la sintesi dei controllori.

5. Logica del Primo Ordine (FOL)

La logica del primo ordine, o calcolo dei predicati, permette una formalizzazione molto più ricca della realtà superando i limiti della logica proposizionale "piatta". Permette di parlare di entità, loro proprietà relazionali, e di fare affermazioni universali o esistenziali su elementi di un dominio infinito.

5.1 Elementi Sintattici

La FOL si basa su un "vocabolario" o "segnatura" che comprende: - Variabili individuali: $x, y, z, \dots$ - Simboli di costante: $c_1, c_2, \dots$ (oggetti specifici). - Simboli di funzione: $f, g, h \dots$ (con una certa arità o numero di argomenti, es. il successore di un numero). - Simboli di predicato (o relazione): $P, Q, R, \dots$ (anch'essi con un'arità definita). - Connettivi logici e i quantificatori $\forall$ e $\exists$.

Un termine è un'espressione che si riferisce a un oggetto (es. costanti, variabili, e l'applicazione di funzioni a termini, come $f(x)$). Una formula atomica è ottenuta applicando un predicato a termini (es. $P(x, f(y))$). L'uguaglianza ($x = y$) è solitamente inclusa come predicato speciale standard binario con semantica fissa.

5.2 Semantica della FOL (Strutture Relazionali)

Per stabilire se una formula FOL è vera, non basta più la tavola di verità. Abbiamo bisogno di una Struttura (o Modello) $\mathcal{M} = (D, \mathcal{I})$ formata da: - Un insieme non vuoto $D$, il dominio di discorso (l'universo degli oggetti). - Una funzione di interpretazione $\mathcal{I}$ che assegna significato ai simboli: - Ad ogni costante $c$, $\mathcal{I}$ associa un elemento $c^\mathcal{M} \in D$. - Ad ogni funzione $n$-aria $f$, $\mathcal{I}$ associa una vera funzione matematica $f^\mathcal{M} : D^n \rightarrow D$. - Ad ogni predicato $n$-ario $P$, $\mathcal{I}$ associa una relazione $P^\mathcal{M} \subseteq D^n$.

Inoltre serve un assegnamento $\mu$ che associa ogni variabile $x$ a un elemento del dominio $d \in D$.

La verità di $\forall x \ \varphi(x)$ nella struttura $\mathcal{M}$ significa che per qualunque elemento $d$ del dominio che decidiamo di assegnare alla variabile $x$, la formula $\varphi$ risulta vera.

Espressività e Indecidibilità: Il grande pregio della FOL è l'infinita potenza descrittiva, il poter parlare di grafi infiniti, aritmetica, ecc. Il prezzo da pagare è l'indecidibilità del problema della validità e della soddisfacibilità (Teorema di Church-Turing). Non esiste nessun algoritmo generale garantito a terminare che possa dirci in tempo finito se una generica formula FOL è valida. Per l'uso in V&V, ci si affida a frammenti decidibili o logiche che sono astrazioni specifiche (es. LTL per percorsi discreti), per cui esistono algoritmi ad-hoc.

6. Giochi di Ehrenfeucht-Fraïssé e Formule di Hintikka

Questi due concetti formano un ponte tra la teoria dei giochi e la teoria dei modelli, e vengono impiegati per studiare l'espressività e i limiti della logica del primo ordine.

6.1 Profondità Quantificazionale (Quantifier Rank)

La profondità quantificazionale ($qr$) di una formula FOL indica il livello massimo di annidamento dei quantificatori: - Formule proposizionali atomiche: $qr = 0$. - $qr(\neg\varphi) = qr(\varphi)$. - $qr(\varphi \lor \psi) = \max(qr(\varphi), qr(\psi))$. - $qr(\exists x \ \varphi) = qr(\forall x \ \varphi) = qr(\varphi) + 1$.

L'interesse si pone nell'analizzare se due diverse strutture matematiche (es. due grafi, o due stringhe di transizione di uno stato) non possano essere distinte da nessuna formula FOL che abbia al massimo un certo $qr = n$.

6.2 Il Gioco di Ehrenfeucht-Fraïssé (EF Games)

È un gioco matematico che serve a dimostrare formalmente che due strutture $\mathcal{A}$ e $\mathcal{B}$ sono elementarmente equivalenti fino a profondità $n$. Il gioco $G_n(\mathcal{A}, \mathcal{B})$ si svolge tra due giocatori per $n$ turni (round): - Spoiler (Sfidante): Tenta di dimostrare che le due strutture sono diverse. In ogni turno, sceglie una struttura (ad esempio $\mathcal{A}$) e seleziona un elemento dal suo dominio. - Duplicator (Difensore): Tenta di dimostrare che le due strutture sono simili. Deve rispondere scegliendo un elemento dall'altra struttura ($\mathcal{B}$).

Dopo $n$ turni, sono state selezionate due sequenze di elementi: $a_1, \dots, a_n \in \mathcal{A}$ e $b_1, \dots, b_n \in \mathcal{B}$. Il Duplicator vince la partita se la mappatura $a_i \mapsto b_i$ costituisce un isomorfismo parziale; in pratica, se qualsiasi relazione o uguaglianza valga per le selezioni in $\mathcal{A}$, deve valere identicamente per le selezioni in $\mathcal{B}$, e viceversa.

Teorema di Ehrenfeucht-Fraïssé: Le strutture $\mathcal{A}$ e $\mathcal{B}$ soddisfano esattamente le stesse formule FOL di profondità quantificazionale $n$ (scritto $\mathcal{A} \equiv_n \mathcal{B}$) se e solo se il Duplicator ha una strategia vincente nel gioco a $n$ round $G_n(\mathcal{A}, \mathcal{B})$.

Utilizzo pratico: Nella verifica, se riesco a trovare una strategia vincente per Duplicator, dimostro matematicamente un limite dell'espressività della mia logica: il linguaggio non ha formule "abbastanza complesse" per distinguere uno stato di errore (struttura $\mathcal{A}$) da uno stato sicuro (struttura $\mathcal{B}$).

6.3 Formule di Hintikka

Le formule di Hintikka sono il corrispettivo sintattico (le formule stesse) dell'equivalenza semantica dimostrata dai giochi EF. Data una struttura finita $\mathcal{A}$ e un livello $n$, esiste un'unica (a meno di equivalenza logica) formula $\tau_{\mathcal{A}}^n$, detta Formula di Hintikka per $\mathcal{A}$ al livello $n$, che "descrive tutto il possibile descrivibile" di quella struttura usando esattamente profondità $n$.

Il teorema si completa con questa equivalenza trina: 1. Duplicator ha una strategia vincente nel gioco EF a $n$ round su $\mathcal{A}$ e $\mathcal{B}$. 2. $\mathcal{A}$ e $\mathcal{B}$ non sono distinguibili da alcuna formula di profondità $n$ ($\mathcal{A} \equiv_n \mathcal{B}$). 3. $\mathcal{B} \models \tau_{\mathcal{A}}^n$ (e viceversa).

Le Formule di Hintikka sono lunghe e complesse e difficilmente costruite a mano, ma forniscono la base per algoritmi di minimizzazione degli automi e per decisioni di equivalenza comportamentale.

7. Model checking, SAT e validita': non confonderli

Negli appunti la logica proposizionale viene usata subito per distinguere tre problemi che sembrano simili ma hanno input diversi.

Model checking proposizionale

Il model checking proposizionale ha come input:

• una formula $\varphi$;
• una struttura/interpretazione $S$.

La domanda e':

$$S\models \varphi?$$

Qui la struttura e' gia' data. Non bisogna cercarla. L'algoritmo valuta la formula ricorsivamente sull'albero sintattico:

• se la formula e' un atomo, guarda il valore assegnato da $S$;
• se e' una congiunzione, valuta entrambe le parti;
• se e' una disgiunzione, valuta almeno una parte;
• se e' una negazione, inverte il risultato.

Per questo il problema e' concettualmente piu' semplice di SAT: non c'e' scelta di modello, c'e' solo valutazione.

SAT

SAT ha come input solo:

$$\varphi.$$

La domanda e':

esiste almeno una interpretazione $S$ tale che $S\models\varphi$?

Quindi SAT deve cercare una struttura. Se la formula contiene $n$ variabili, in brute force ci sono:

$$2^n$$

assegnamenti possibili.

Questo spiega perche' SAT e' piu' difficile del semplice model checking proposizionale.

Validita'

La validita' chiede:

tutte le interpretazioni soddisfano $\varphi$?

Formalmente:

$$\models\varphi.$$

Quindi:

• SAT cerca un modello;
• validita' cerca assenza di controesempi;
• model checking controlla un modello specifico.

Questa distinzione ritorna in tutto il corso:

• in LTL, la soddisfacibilita' cerca un cammino/modello;
• nel model checking, si controllano le computazioni di un programma;
• in BMC, si cerca un controesempio finito tramite SAT;
• nella sintesi, si cerca una strategia/controller.

8. Riduzioni tra problemi logici

Un passaggio degli appunti che vale la pena rendere esplicito e':

$$\varphi \text{ valida}\quad\Longleftrightarrow\quad \neg\varphi \text{ insoddisfacibile}.$$

Questo non e' solo un fatto teorico: e' il modo standard con cui si usano i solver.

Se voglio dimostrare una proprieta' $\varphi$, cerco un modello di $\neg\varphi$.

• se esiste, ho trovato un controesempio;
• se non esiste, $\varphi$ e' valida.

Anche l'equivalenza logica si riduce alla validita':

$$\varphi\equiv\psi \quad\Longleftrightarrow\quad \models(\varphi\leftrightarrow\psi).$$

E si puo' ridurre a SAT cercando un assegnamento che distingue le due formule:

$$\varphi\not\equiv\psi \quad\Longleftrightarrow\quad (\varphi\land\neg\psi)\lor(\neg\varphi\land\psi) \text{ e' soddisfacibile}.$$

Questa formula e' la differenza simmetrica dei modelli: e' vera esattamente quando una delle due formule e' vera e l'altra e' falsa.

La riduzione inversa: dalla validità all'equivalenza

Negli appunti viene osservato che la riduzione funziona anche nell'altro verso: il problema della validità si riduce al problema dell'equivalenza.

Data una formula $\varphi$ di cui voglio testare la validità, costruisco due formule da confrontare:

• $\varphi_1 = \varphi$;
• $\varphi_2 = \top$ (una formula sempre vera, per esempio $p \lor \neg p$).

Allora:

$$\varphi \text{ valida} \quad\Longleftrightarrow\quad \varphi \equiv \top.$$

Il motivo è immediato: $\varphi \equiv \top$ significa che in ogni struttura $\varphi$ ha lo stesso valore di $\top$, cioè è vera ovunque. Quindi un oracolo per l'equivalenza risolve anche la validità. Le due riduzioni insieme dicono che validità ed equivalenza sono inter-riducibili: dal punto di vista della calcolabilità sono lo stesso problema.

9. Perche' servono le forme normali

Le forme normali non cambiano il significato della logica. Servono agli algoritmi.

Un algoritmo e' piu' semplice se riceve formule con una struttura regolare. Per esempio, un SAT solver lavora bene con formule in CNF:

$$C_1\land C_2\land\cdots\land C_m,$$

dove ogni $C_i$ e' una clausola, cioe' una disgiunzione di letterali.

Eliminare implicazione e doppia implicazione

Gli operatori $\to$ e $\leftrightarrow$ non aumentano il potere espressivo.

Si eliminano con:

$$\varphi\to\psi \equiv \neg\varphi\lor\psi.$$

E:

$$\varphi\leftrightarrow\psi \equiv (\varphi\land\psi)\lor(\neg\varphi\land\neg\psi).$$

Attenzione: eliminare $\leftrightarrow$ duplicando sottoformule puo' aumentare la dimensione della formula. Questo e' il primo punto in cui si vede il tema dello state/formula explosion.

NNF

La NNF, negation normal form, porta le negazioni solo davanti agli atomi.

Esempio:

$$\neg(p\lor(q\land r))$$

diventa:

$$\neg p\land(\neg q\lor\neg r).$$

Perche' funziona? Perche' le leggi di De Morgan preservano la verita' in ogni interpretazione.

CNF: equivalenza vs equisoddisfacibilita'

Qui c'e' un punto importante.

Una trasformazione puo' essere:

• equivalente, se preserva gli stessi modelli sulle stesse variabili;
• equisoddisfacibile, se preserva solo l'esistenza di almeno un modello.

La trasformazione di Tseitin introduce variabili ausiliarie. Per questo non preserva necessariamente gli stessi modelli sulle variabili nuove, ma preserva SAT:

$$\varphi \text{ soddisfacibile} \quad\Longleftrightarrow\quad Tseitin(\varphi) \text{ soddisfacibile}.$$

Per SAT basta. Se invece sto ragionando sull'equivalenza logica esatta, devo essere piu' prudente.

DNF e tableaux

Una formula in DNF rende SAT facile: basta controllare se almeno un termine e' coerente, cioe' non contiene insieme $p$ e $\neg p$.

Il problema e' che trasformare in DNF puo' essere esponenziale.

Il tableau puo' essere visto come una costruzione ad albero che esplora implicitamente una DNF: le ramificazioni rappresentano alternative, i rami lineari rappresentano congiunzioni. Non serve materializzare tutta la DNF come formula piatta.

10. QBF: variabili libere, legate e ordine dei quantificatori

In QBF bisogna distinguere:

• occorrenze libere;
• occorrenze legate.

In:

$$\neg p\lor \exists p\,(p\land q)$$

la prima occorrenza di $p$ e' libera, mentre la seconda e' legata dal quantificatore $\exists p$.

Se sostituisco la variabile libera $p$ con $\alpha$, ottengo:

$$\neg \alpha\lor \exists p\,(p\land q).$$

Non devo sostituire anche il $p$ dentro $\exists p$, perche' quello e' locale al quantificatore.

Renaming

Il nome di una variabile legata non e' importante, purche' non catturi variabili libere.

Per esempio:

$$\exists p\,\varphi$$

e' equivalente a:

$$\exists q\,\varphi[p/q]$$

se $q$ non compare libera in $\varphi$.

Questo dettaglio diventa importante nelle traduzioni logica-automi: spesso si rinominano variabili per evitare collisioni.

Ordine dei quantificatori

L'ordine cambia il significato.

Con:

$$\forall x\exists y\,(x\leftrightarrow y)$$

$y$ puo' dipendere da $x$. L'esistenziale vede la scelta dell'universale e puo' copiarla.

Con:

$$\exists y\forall x\,(x\leftrightarrow y)$$

$y$ viene scelto prima. Non puo' adattarsi a $x$. La formula e' falsa.

Questo e' il primo esempio di strategia nel corso: una QBF vera non dice solo che esistono valori, ma che il giocatore esistenziale ha una strategia coerente con l'ordine dell'informazione.

11. Hintikka ed Ehrenfeucht-Fraisse: cosa devi davvero capire

La parte su Hintikka e EF games e' facile da sottovalutare, ma serve per capire i limiti espressivi delle logiche.

La domanda tipica e':

con formule di profondita' quantificazionale al massimo $n$, riesco a distinguere due strutture?

Se no, le due strutture sono $n$-equivalenti.

Formula di Hintikka a livello 0

A livello 0 non posso usare quantificatori. Posso solo descrivere fatti atomici sulle variabili gia' assegnate.

La formula di Hintikka di livello 0 contiene:

• tutti gli atomi veri;
• la negazione di tutti gli atomi falsi.

Quindi e' la descrizione atomica completa della struttura espansa con le variabili gia' interpretate.

Passo induttivo

A livello $n+1$, la formula deve descrivere cosa succede se aggiungo una nuova variabile e la interpreto con un elemento del dominio.

Per questo compaiono congiunzioni di formule del livello precedente, precedute da quantificatori. L'idea e':

tutte le mosse possibili del gioco a un round vengono codificate con formule di livello inferiore.

Questo spiega il legame con EF games.

Perche' i giochi sono piu' maneggevoli

Le formule di Hintikka crescono enormemente. Negli appunti viene sottolineato che la dimensione puo' crescere come una torre di esponenziali.

Il gioco EF e' spesso piu' leggibile:

• Spoiler prova a distinguere le strutture;
• Duplicator prova a mantenere un isomorfismo parziale;
• se Duplicator sopravvive $n$ round, nessuna formula FO di quantifier rank $n$ distingue le due strutture.

Esempio su parole

Una parola finita come abbb puo' essere vista come struttura:

• dominio: posizioni $\{0,1,2,3\}$;
• ordine $<$ sulle posizioni;
• predicato $A(x)$ per le posizioni con lettera a;
• predicato $B(x)$ per le posizioni con lettera b.

Con un solo quantificatore posso dire:

esiste una posizione con a; esiste una posizione con b.

Ma non posso ancora distinguere bene tutte le configurazioni d'ordine.

Aumentando il numero di round/quantificatori, Spoiler puo' chiedere piu' posizioni e provare a distinguere lunghezze, ordine e distribuzione delle etichette.

Le partizioni indotte sulle parole, livello per livello

Negli appunti questo viene mostrato concretamente: poiché due strutture con la stessa formula di Hintikka di livello $n$ sono $n$-equivalenti, ogni livello $n$ partiziona l'universo delle parole in classi di equivalenza, e le classi diventano più fini al crescere di $n$.

A livello $n = 1$ (un solo quantificatore, nessun annidamento) posso solo dire "esiste una posizione con $a$", "esiste una posizione con $b$", "ogni posizione è $a$ o $b$". Le classi sono quattro:

Nota che a questo livello non posso usare l'ordine: per confrontare due posizioni con $<$ servono due variabili quantificate insieme, quindi $ab$ e $ba$ stanno nella stessa classe.

A livello $n = 2$ (due quantificatori annidati) la partizione si raffina: posso parlare di coppie di posizioni, del loro ordine e delle loro etichette. Per esempio:

• separo $a$ da $aa$: in $aa$ vale $\exists x \exists y\,(x < y \land A(x) \land A(y))$, in $a$ no;
• separo $ab$ da $aabbb$ (numero di $a$ maggiore di 1) e $aabb$ da $abbb$ (numero di $b$);
• non separo $aa$ da $aaa$: con due sole variabili non posso "contare" fino a tre posizioni distinte. Duplicator sopravvive 2 round nel gioco EF tra $aa$ e $aaa$.

La regola generale: con quantifier rank $n$ si riesce a contare al massimo "fino a $n$", e ogni incremento di $n$ spacca alcune classi in classi più fini. Vale anche il viceversa in negativo: se due parole hanno la stessa Hintikka di livello 3, ce l'hanno anche ai livelli 2, 1, 0 (le formule di livello inferiore sono implicate da quelle di livello superiore).

Come si usa per dimostrare non definibilita'

Per dimostrare che una proprieta' $P$ non e' definibile in FO, la strategia e':

per ogni $n$, trovare due strutture $\mathcal{A}_n$ e $\mathcal{B}_n$ tali che una soddisfa $P$, l'altra no, ma Duplicator vince il gioco EF a $n$ round.

Allora nessuna formula FO di profondita' $n$ distingue quelle due strutture. Se questo accade per ogni $n$, nessuna formula FO definisce $P$.

Questo schema ritorna indirettamente quando il corso parla di linguaggi first-order definable, star-free e limiti espressivi.

12. Il quadro del corso: verificare = controllare un'inclusione di linguaggi

Gli appunti aprono con un esempio che vale la pena tenere a mente per tutto il corso, perché anticipa esattamente la pipeline del model checking (Capitolo 8).

Immagina una macchina del caffè modellata come macchina a stati finiti $S$: inserisci monete (5¢, 10¢), ottieni un caffè, oppure premi reset. Ogni esecuzione del sistema è una sequenza di eventi, e l'insieme di tutte le esecuzioni possibili è un linguaggio:

$$Lang(S) = \{\,10\text{¢ } reset \text{ } 5\text{¢}\ldots,\; 5\text{¢ } 5\text{¢ } 10\text{¢}\ldots,\;\ldots\,\}$$

Una specifica è una formula logica $\varphi$ che descrive le esecuzioni "buone", per esempio:

$$\varphi = \text{"}(10\text{¢} \lor 5\text{¢}) \text{ UNTIL } (coffee \lor reset \lor kick)\text{"}$$

La domanda "tutte le esecuzioni del modello soddisfano la specifica?" diventa un'inclusione tra linguaggi:

$$Lang(S) \subseteq Lang(\varphi).$$

Il trucco fondamentale è riscrivere l'inclusione come un problema di vuotezza:

$$Lang(S) \subseteq Lang(\varphi) \quad\Longleftrightarrow\quad Lang(S) \cap Lang(\neg\varphi) = \emptyset.$$

La procedura quindi è:

1. compilare la specifica negata $\neg\varphi$ in un automa (per l'esempio: $\neg\varphi$ = "per sempre solo monete, senza mai caffè/reset/kick");
2. costruire il prodotto tra il modello e l'automa di $\neg\varphi$;
3. controllare la vuotezza del prodotto: se è vuoto, nessuna esecuzione viola la specifica.

Questo spiega perché la logica è centrale nel corso: è il linguaggio di alto livello in cui scriviamo le proprietà, e tutte le tecniche che vedremo (automi, S1S, LTL, tableau, OBDD) servono a compilare la logica in oggetti a basso livello su cui la vuotezza si decide algoritmicamente. Nota anche il problema di fondo: i sistemi reattivi hanno esecuzioni infinite, e non si può testare passo passo qualcosa di infinito in tempo finito — serviranno automi su parole infinite (Capitolo 5).

13. Riduzioni, complessità, espressività e succintezza

Prima di studiare le singole logiche, gli appunti fissano il vocabolario con cui le confronteremo per tutto il corso.

Riduzioni

Una riduzione da un problema $P$ a un problema $Q$ (intuitivamente: "$P$ è più facile di $Q$") è un algoritmo $F$ che risolve $P$ usando un oracolo che restituisce soluzioni di $Q$.

Il caso particolare più usato è la riduzione many-to-one: una funzione $F$ che trasforma le istanze in modo che

$$\forall x,\quad P(x) \iff Q(F(x)).$$

Per risolvere $P$ su $x$, calcolo $F(x)$ e chiedo all'oracolo se $Q(F(x))$. Esempi già visti: validità $\to$ insoddisfacibilità ($F(\varphi) = \neg\varphi$), equivalenza $\to$ validità ($F(\varphi_1,\varphi_2) = \varphi_1 \leftrightarrow \varphi_2$).

Complessità

Un algoritmo $Alg$ è limitato in TEMPO/SPAZIO da una funzione $f:\mathbb{N}\to\mathbb{N}$ se $Alg(input)$ usa al più $f(|input|)$ unità di tempo/spazio. Da qui le classi di complessità usate nel corso: P, NP, PSPACE, EXP. Ricorda i punti fissi del capitolo: EVAL è P-completo, SAT è NP-completo, TQBF è PSPACE-completo.

Espressività

Quali proprietà si possono esprimere in una data logica? Questa logica è più o meno espressiva di quest'altra?

Più una logica è espressiva, più proprietà posso formalizzare — ma il prezzo è la decidibilità o la complessità: l'espressività si paga sempre. Questo trade-off torna ovunque: FOL è più espressiva della proposizionale ma indecidibile; S1S è decidibile ma con complessità non elementare; LTL e CTL sono frammenti che barattano espressività per algoritmi efficienti.

Succintezza

Due logiche possono esprimere le stesse proprietà ma con costi diversi: la stessa proprietà può richiedere 10 simboli in una e un milione nell'altra.

L'analogia degli appunti: Python e Assembly calcolano le stesse funzioni, ma Python è molto più succinto (lo stesso programma richiede molti meno simboli), mentre Assembly è molto più efficiente da eseguire. Allo stesso modo una logica più succinta tende ad avere algoritmi più costosi: la succintezza si paga in complessità.

Definibilità tra logiche

Ultimo problema del quadro: date due logiche $L_1$ e $L_2$ e una formula $\varphi_1 \in L_1$, posso riscriverla come $\varphi_2 \in L_2$ equivalente in ogni struttura?

Il caso interessante è quando $L_2$ è un frammento di $L_1$: meno espressivo, ma con miglior comportamento computazionale. Se la mia proprietà è definibile nel frammento, conviene usare il frammento. È esattamente quello che faremo con star-free $\subseteq$ regolari, LTL vs S1S, CTL vs CTL*.

14. Due esempi che preparano il resto del corso

Gli appunti introducono due esempi di formalizzazione che sembrano digressioni ma anticipano due capitoli interi. Vale la pena capirli ora.

14.1 Il lemma di Kőnig in logica (anteprima di MSO)

Il lemma di Kőnig dice:

ogni albero infinito a ramificazione finita ha un cammino infinito.

Per formalizzarlo serve parlare di alberi, antenati e insiemi: gli appunti usano la relazione $A(x,y)$ = "$x$ è antenato di $y$" e variabili di sorte diversa (sorted logic: ogni variabile spazia su un universo di tipo diverso, come ordini e istanti di tempo nell'esempio "ogni ordine verrà processato in un istante futuro" con $t < t'$).

I pezzi della formalizzazione:

• "essere un albero": se $y$ e $z$ sono entrambi antenati di $x$ ($A(y,x) \land A(z,x)$), allora sono confrontabili tra loro ($A(y,z) \lor A(z,y)$) — gli antenati di un nodo formano una catena, non ci sono "rombi";
• "ramificazione finita": per ogni nodo, l'insieme dei figli è finito, espresso con un quantificatore su insiemi finiti ($\exists Y_{finite}$);
• "cammino infinito": esiste un insieme infinito di nodi ($\exists Z_{infinite}$) totalmente ordinato da $A$ — una catena infinita (attenzione: una catena è un sottoinsieme di un cammino, i suoi elementi devono solo essere a due a due confrontabili).

Il punto importante è la differenza tra i due tipi di variabili:

• variabili del primo ordine ($x, y, z$): interpretate da singoli elementi;
• variabili del secondo ordine ($Y_{finite}$, $Z_{infinite}$): interpretate da insiemi (finiti o infiniti) di elementi.

Quantificare su insiemi è ciò che la logica monadica del secondo ordine (MSO) aggiunge alla FOL: è la logica S1S del Capitolo 6. Questo esempio mostra perché serve: proprietà come "esiste un cammino infinito" non sono esprimibili restando al primo ordine.

14.2 Raggiungibilità di un circuito con SAT (anteprima di BMC)

Considera un dispositivo il cui stato interno è codificato da $k$ bit. Lo descriviamo con tre formule proposizionali:

• $\varphi_{init}(\bar p)$: descrive l'insieme degli stati iniziali. Con $\bar p = p_1,\ldots,p_k$, lo stato $1011$ si scrive $p_1 \land \neg p_2 \land p_3 \land p_4$; una formula generica può descrivere molti stati iniziali insieme;
• $\varphi_{target}(\bar p)$: descrive gli stati obiettivo;
• $\varphi_{step}(\bar p, \bar p\,')$: descrive la relazione di transizione, usando due copie delle variabili — $\bar p$ per lo stato corrente, $\bar p\,'$ per il successivo.

Problema: il dispositivo ammette un'esecuzione dallo stato iniziale a quello obiettivo?

Osservazione chiave sulla lunghezza: con $k$ bit ci sono al più $2^k$ configurazioni, quindi se un cammino esiste, ne esiste uno di lunghezza al più $n = 2^k$. Possiamo anzi assumere lunghezza esattamente $n$: basta che $\varphi_{step}$ ammetta anche il passo "non fare nulla" ($\bar p = \bar p\,'$), così i cammini corti si allungano con passi vuoti senza cambiare la raggiungibilità.

La soluzione è una formula con $n$ tuple di variabili $\bar p^{(1)},\ldots,\bar p^{(n)}$ (una per ogni istante):

$$\varphi_{reach} = \varphi_{init}(\bar p^{(1)}) \land \varphi_{target}(\bar p^{(n)}) \land \bigwedge_{i=1}^{n-1} \varphi_{step}(\bar p^{(i)}, \bar p^{(i+1)})$$

ed è soddisfacibile se e solo se esiste un'esecuzione dallo stato iniziale al target: un modello di $\varphi_{reach}$ è esattamente un cammino, letto assegnamento per assegnamento.

Questo schema — srotolare la relazione di transizione per $n$ passi e chiedere a un SAT solver se esiste un cammino — è esattamente il Bounded Model Checking del Capitolo 9, dove l'unica differenza è che il bound viene tenuto piccolo e incrementato, invece di essere fissato a $2^k$.

15. QBF: un esempio valutato con la semantica ricorsiva

Oltre alla lettura "a gioco" della sezione 10, conviene saper valutare una QBF applicando meccanicamente la semantica, come negli appunti.

Formula da controllare, partendo dalla struttura vuota $S = \emptyset$:

$$S \models \forall p\,\exists q\,\big((p \lor \neg q) \land (\neg p \lor q)\big)?$$

Passo 1 — il $\forall p$. Per la semantica, $S \models \forall p\,\psi$ vale se $\psi$ vale per entrambe le espansioni di $S$:

• $S_1 = [p := tt] \models \exists q\,(p \lor \neg q) \land (\neg p \lor q)$, e
• $S_2 = [p := ff] \models \exists q\,(p \lor \neg q) \land (\neg p \lor q)$.

Passo 2 — il $\exists q$ dentro $S_1$. Per la semantica dell'esistenziale basta che una delle due espansioni funzioni:

• $S_1' = [p := tt,\, q := tt] \models (p \lor \neg q) \land (\neg p \lor q)$? Con $p$ vero il primo congiunto è vero; il secondo, $\neg p \lor q$, richiede $q$ vero — ed è il nostro caso. Sì.
• (non serve nemmeno provare $S_1'' = [p := tt,\, q := ff]$.)

Passo 3 — il $\exists q$ dentro $S_2$. Simmetrico: con $p$ falso il secondo congiunto è vero, e il primo, $p \lor \neg q$, richiede $q$ falso. Quindi $S_2' = [p := ff,\, q := ff]$ funziona. Sì.

Entrambi i rami del $\forall$ hanno successo: la formula è vera. Nota che la valutazione ha trovato la strategia del giocatore esistenziale della sezione 10: "copia il valore di $p$".

L'algoritmo di model checking per QBF

La procedura usata sopra è esattamente l'estensione ricorsiva del ModelCheck proposizionale:

• $\varphi = \exists p\,\varphi'$: ritorna $ModelCheck(\varphi', S[p := tt])$ or $ModelCheck(\varphi', S[p := ff])$;
• $\varphi = \forall p\,\varphi'$: ritorna $ModelCheck(\varphi', S[p := tt])$ and $ModelCheck(\varphi', S[p := ff])$.

Ogni quantificatore raddoppia le chiamate: con $n$ quantificatori annidati il tempo è $O(2^n)$, ma lo spazio è polinomiale (la ricorsione è profonda quanto la formula, e ogni livello memorizza solo un'espansione di $S$). È il motivo intuitivo per cui TQBF sta in PSPACE — e ne è anzi il problema completo.

16. Quiz Interattivo per l'Autovalutazione