V&V in AI — Appunti

Settimana 3

✦
Indice← PrecedenteSuccessivo →
Capitolo 6

Capitolo 6 — Logica monadica del secondo ordine (MSO)

S1S, WS1S, teorema di Büchi, S2S, automi su alberi e linguaggi star-free.

Teoria monadica del secondo ordine con un successore - Riassunto

Fonte: raw/Monadic Second Order theory of One's Successor.md

Punti chiave

Concetti estratti

S1S debole - Riassunto

Fonte: raw/Weak S1S.md

Punti chiave

Concetti estratti

Secondo teorema di Büchi - Riassunto

Fonte: raw/Secondo teorema di Büchi.md

Punti chiave

Concetti estratti

S1S

S1S e' la teoria monadica del secondo ordine con un successore. Interpreta formule sui naturali, visti come posizioni di una parola infinita.

Elementi

Rappresentazione di parole

Una parola infinita puo essere codificata tramite insiemi di posizioni: ad esempio $X_a$ contiene le posizioni in cui compare il simbolo $a$.

Potere espressivo

Per il secondo teorema di Büchi, un omega-linguaggio e' definibile in S1S se e solo se e' omega-regolare.

Collegamenti

S1S debole

WS1S e' la variante debole di S1S in cui le variabili del secondo ordine sono limitate a insiemi finiti.

Differenza da S1S

S1S permette insiemi infiniti di posizioni; WS1S permette solo insiemi finiti. Questo rende WS1S adatta a esprimere proprieta finite o locali dentro una struttura temporale infinita.

Uso

WS1S mantiene il collegamento con automi e procedure decisionali, ed e' alla base di strumenti come MONA per ragionare su proprieta regolari.

Collegamenti

Secondo teorema di Büchi

Il secondo teorema di Büchi afferma che un omega-linguaggio e' omega-regolare se e solo se e' definibile in S1S.

Direzione automi -> logica

Dato un automa di Büchi, si costruisce una formula S1S che codifica: - stato iniziale; - appartenenza a un solo stato in ogni posizione; - rispetto della relazione di transizione; - visita infinita di almeno uno stato finale.

Direzione logica -> automi

Ogni formula S1S puo essere trasformata, tramite costruzioni effettive, in un automa di Büchi che riconosce esattamente i suoi modelli.

Importanza

Il teorema stabilisce il ponte tra logica monadica, automi su parole infinite e model checking.

Collegamenti

Chiusura per proiezione

La chiusura per proiezione dice che eliminare esistenzialmente una componente da una formula S1S preserva l'omega-regolarita del linguaggio definito.

In S1S una variabile del secondo ordine non e' un singolo valore: e' un insieme di posizioni. Se uso variabili:

$$X_1,\ldots,X_n$$

posso leggerle come una parola infinita su alfabeto $\lbrace 0,1\rbrace^n$: alla posizione $k$, il bit $i$ vale 1 se e solo se $k\in X_i$.

Proiettare via $X_i$ significa cancellare il bit $i$ da ogni posizione della parola.

Interpretazione logica

Se una formula usa piu variabili del secondo ordine per rappresentare componenti di una parola, possiamo quantificare esistenzialmente una di queste variabili:

$$ \psi(X_1,\ldots,X_{i-1},X_{i+1},\ldots,X_n) = \exists X_i\;\varphi(X_1,\ldots,X_n). $$

La parola visibile soddisfa $\psi$ se esiste almeno un modo di scegliere la componente nascosta $X_i$ che rende vera $\varphi$.

Quindi:

$$ L(\psi)=\pi_i(L(\varphi)). $$

Attenzione: la proiezione non ignora i vincoli della formula. Li soddisfa esistenzialmente scegliendo una componente nascosta adatta.

Interpretazione automata-theoretic

A livello di automi di Büchi, se:

$$ \mathcal{A}=(Q,\lbrace 0,1\rbrace^n,\Delta,q_0,F) $$

riconosce il linguaggio prima della proiezione, costruisco:

$$ \mathcal{A}'=(Q,\lbrace 0,1\rbrace^{n-1},\Delta',q_0,F) $$

dove:

$$ (p,c,q)\in\Delta' $$

se e solo se esiste una lettera completa $b\in\lbrace 0,1\rbrace^n$ con $\pi_i(b)=c$ e:

$$ (p,b,q)\in\Delta. $$

L'automa proiettato legge solo le componenti visibili e usa il nondeterminismo per indovinare la componente rimossa.

Esempio: se la formula e' $\exists Y\;\varphi(X,Y)$, l'automa su $X$ accetta una parola se esiste una traccia $Y$ tale che la parola completa $(X,Y)$ sarebbe stata accettata dall'automa per $\varphi$.

Collegamenti

Approfondimento completo settimana 3 - S1S, WS1S e secondo teorema di Büchi

Questo documento espande il Capitolo 6. Qui il punto non è imparare un nuovo automa, ma capire il ponte tra automi e logica: le stesse proprietà sulle parole infinite possono essere viste come linguaggi riconosciuti da automi di Büchi oppure come formule della logica monadica del secondo ordine con un successore.

0. Idea guida: perché passare dagli automi alla logica?

Gli automi di Büchi sono potenti, ma quando le proprietà diventano grandi è scomodo disegnarli o ragionare direttamente sui loro stati. La logica serve come linguaggio più dichiarativo:

Esempio:

"Ogni richiesta viene prima o poi seguita da una risposta."

Come automa, questa proprietà richiede stati, transizioni e una condizione di accettazione. Come formula, posso parlare direttamente delle posizioni della parola infinita: per ogni posizione in cui c'è una richiesta, esiste una posizione futura in cui c'è una risposta.

S1S è il formalismo logico che permette di parlare di:

Il risultato centrale è il secondo teorema di Büchi:

Un omega-linguaggio è omega-regolare se e solo se è definibile in S1S.

Quindi automi di Büchi e S1S hanno lo stesso potere espressivo sulle parole infinite.

1. Che cosa significa "monadica del secondo ordine"?

Spezzare il nome aiuta.

Primo ordine

Le variabili del primo ordine rappresentano singole posizioni:

$$x,y,z,\ldots$$

Se la struttura è $\mathbb{N}$, allora $x$ può essere 0, oppure 1, oppure 57, ecc.

Esempi di proprietà su posizioni:

Secondo ordine

Le variabili del secondo ordine rappresentano insiemi di posizioni:

$$X,Y,Z,\ldots$$

Esempio: $X$ può essere l'insieme delle posizioni in cui compare il simbolo $a$.

Monadico

"Monadico" significa che le variabili del secondo ordine sono insiemi di singole posizioni, non relazioni binarie o ternarie. Quindi $X$ è un predicato unario: posso scrivere $x\in X$, ma non $R(x,y)$ come relazione libera del secondo ordine.

Questo mantiene la logica abbastanza espressiva per parlare di omega-parole, ma ancora decidibile.

2. Sintassi di S1S

S1S usa:

Le formule atomiche tipiche sono:

Alcuni simboli sono ridondanti. Per esempio $<$ si può definire usando successore e quantificazione del secondo ordine, ma negli appunti viene spesso usato perché rende le formule più leggibili.

Una formula senza variabili libere si chiama enunciato. Una formula con variabili libere definisce un linguaggio parametrico rispetto a quelle variabili.

3. Semantica: parole infinite come strutture logiche

Sia $\alpha \in A^\omega$ una parola infinita su alfabeto finito $A$.

La interpretiamo come struttura:

$$\underline{\alpha} = (\omega,0,+1,<,\lbrace Q_a\rbrace_{a\in A})$$

dove:

Formalmente:

$$Q_a = \lbrace i\in\omega \mid \alpha(i)=a\rbrace$$

Esempio:

Se:

$$\alpha = a b a a b b \ldots$$

allora:

Una formula S1S definisce un linguaggio:

$$L(\varphi)=\lbrace \alpha\in A^\omega \mid \underline{\alpha}\models \varphi\rbrace$$

Quindi una formula è vera o falsa su una parola infinita, e il linguaggio della formula è l'insieme delle parole su cui è vera.

4. Versione dipendente dall'alfabeto e versione alphabet-agnostic

Negli appunti compaiono due modi di vedere S1S.

S1S su un alfabeto $A$

In $S1S_A$ ho un predicato $Q_a$ per ogni simbolo $a\in A$.

Se $A=\lbrace a,b,c\rbrace$, avrò:

$$Q_a,Q_b,Q_c$$

e posso scrivere formule come:

$$\forall x(Q_a(x)\to \exists y(x<y\land Q_b(y)))$$

che dice: ogni $a$ è seguita, prima o poi, da una $b$.

S1S generica

Per rendere la rappresentazione indipendente dall'alfabeto, posso codificare i simboli in binario.

Se l'alfabeto ha al massimo $2^n$ simboli, ogni lettera si rappresenta con $n$ bit. Una parola infinita diventa una parola su $\lbrace 0,1\rbrace^n$.

Uso variabili del secondo ordine:

$$P_1,\ldots,P_n$$

dove $P_k$ contiene le posizioni in cui il k-esimo bit vale 1.

Questa versione è più uniforme: non dipende dai nomi $a,b,c$, ma solo da insiemi di posizioni.

5. Formule S1S da saper scrivere

Qui conviene costruire un piccolo vocabolario di pattern. Sono formule da saper produrre all'orale.

P vale infinitamente spesso

$$\forall x \exists y (x<y \land y\in P)$$

Lettura: qualunque posizione x scelgo, esiste una posizione futura y in cui P vale. Quindi P non smette mai di ricomparire.

P vale solo un numero finito di volte

$$\exists x \forall y (x<y \to y\notin P)$$

Lettura: esiste un punto x dopo il quale P non compare più.

Ogni a è immediatamente seguita da b

$$\forall x(Q_a(x)\to Q_b(x+1))$$

Questa formula parla del passo successivo immediato.

Ogni a è prima o poi seguita da b

$$\forall x(Q_a(x)\to \exists y(x<y\land Q_b(y)))$$

Questa formula non impone che b sia subito dopo a. Può essere in qualunque posizione futura.

Non ci sono due a consecutive

$$\forall x(Q_a(x)\to \neg Q_a(x+1))$$

a e b si alternano

Se l'alfabeto è solo $\lbrace a,b\rbrace$, una forma semplice è:

$$\forall x((Q_a(x)\to Q_b(x+1))\land(Q_b(x)\to Q_a(x+1)))$$

Questa impone alternanza perfetta.

Da un certo punto in poi solo b

$$\exists x\forall y(x<y\to Q_b(y))$$

Questa formula definisce parole che hanno una coda infinita di sole $b$.

Infinite a e infinite b

$$(\forall x\exists y(x<y\land Q_a(y)))\land(\forall x\exists y(x<y\land Q_b(y)))$$

0 e < sono ridondanti: definirli da +1 (domanda classica)

Negli appunti viene mostrato che nella segnatura di S1S la costante $0$ e l'ordine $<$ sono definibili, quindi in linea di principio ridondanti.

Per $x = 0$, senza usare $<$:

$$\neg\exists y\,(y+1 = x)$$

(zero è l'unico punto che non è successore di nessuno).

Viceversa $+1$ si definisce da $<$ al primo ordine:

$$x+1 = y \quad\leadsto\quad x < y \land \neg\exists z\,(x < z \land z < y).$$

La direzione interessante è l'altra: definire $<$ da $+1$. Al primo ordine non si può (è un fatto da citare all'orale). Serve la quantificazione del secondo ordine:

$$x < y \quad\leadsto\quad \forall X\,\big(x+1\in X \land \forall z\,(z\in X \to z+1\in X)\ \to\ y\in X\big)$$

Lettura: ogni insieme $X$ che contiene $x+1$ ed è chiuso per successore deve contenere $y$. Il più piccolo insieme con quelle proprietà è $\{x+1, x+2, x+3,\ldots\}$: imporre $y\in X$ per tutti gli $X$ del genere forza $y$ a stare strettamente a destra di $x$.

Perché $\forall X$ e non $\exists X$? Con $\exists X$ basterebbe esibire un $X$ che contiene $y$: ma posso sempre "barare" prendendo un $X$ più grande del necessario (per esempio uno che parte da un $t < x$ ed è chiuso per successore), che finisce per contenere anche posizioni a sinistra di $x$. Il $\forall$ elimina i testimoni truccati: la condizione deve reggere anche per l'insieme minimo $\{x+1, x+2,\ldots\}$, e quello contiene solo punti a destra di $x$.

Contare modulo 2: il trucco dell'insieme alternante

Esempio svolto negli appunti: su $A = \{a,b,c\}$, il linguaggio delle ω-parole in cui tra due occorrenze consecutive di $a$ c'è un numero pari di $b$/$c$ (lo stesso linguaggio dell'automa di Büchi del Capitolo 5).

$$\forall x\forall y\Big(\big(x\in Q_a \land y\in Q_a \land x<y \land \neg\exists z(z\in Q_a \land x<z \land z<y)\big) \to$$ $$\exists X\big(x\in X \land \forall z\,(z\in X \leftrightarrow z+1\notin X) \land y\notin X\big)\Big)$$

La premessa dice "$x$ e $y$ sono due $a$ consecutive" (nessuna $a$ in mezzo). La conclusione usa un insieme $X$ alternante: la condizione $z\in X \leftrightarrow z+1\notin X$ forza $X$ a contenere esattamente una posizione sì e una no. Partendo da $x\in X$, le posizioni in $X$ sono $x, x+2, x+4,\ldots$: chiedere $y\notin X$ significa che la distanza $y - x$ è dispari, cioè il numero di posizioni strettamente comprese (le $b$/$c$) è pari.

Questo pattern — un insieme del secondo ordine usato come "contatore modulo $k$" — è esattamente ciò che separa MSO dal primo ordine: al primo ordine non si conta modulo, ed è il motivo per cui i linguaggi FO-definibili (star-free) sono una sottoclasse propria dei regolari.

6. Definire linguaggi con formule

Un linguaggio è definibile in S1S se esiste una formula che lo cattura esattamente.

Esempio:

$$L = \lbrace \alpha\in\lbrace a,b\rbrace^\omega \mid a \text{ compare infinite volte}\rbrace$$

Formula:

$$\varphi = \forall x\exists y(x<y\land Q_a(y))$$

Allora:

$$L = L(\varphi)$$

Esempio:

$$L = \lbrace \alpha\mid \text{non compaiono mai due }a\text{ consecutive}\rbrace$$

Formula:

$$\varphi = \forall x(Q_a(x)\to \neg Q_a(x+1))$$

Esempio:

$$L = \lbrace \alpha\mid \text{ogni } request \text{ è seguita da un } grant\rbrace$$

Formula:

$$\forall x(Q_{request}(x)\to \exists y(x<y\land Q_{grant}(y)))$$

Questa è una proprietà di vivacità, spesso chiamata liveness: non dice che il grant arriva subito, ma che prima o poi arriva.

7. Chiusura per proiezione

In inglese la trovi spesso come closure by projection. E' il passaggio che collega direttamente quantificazione esistenziale e operazioni sugli automi.

La proiezione è il ponte tecnico più importante tra formule e automi. Serve a formalizzare questa idea:

osservo solo alcune componenti della parola e nascondo le altre; la parola osservata è accettata se esiste almeno un modo di riempire le componenti nascoste.

In S1S le componenti nascoste sono variabili del secondo ordine.

Supponi di avere una formula:

$$\varphi(X_1,\ldots,X_i,\ldots,X_n)$$

e di costruire:

$$\psi(X_1,\ldots,X_{i-1},X_{i+1},\ldots,X_n)=\exists X_i\;\varphi(X_1,\ldots,X_n)$$

La variabile $X_i$ sparisce dalle variabili libere, perché viene quantificata esistenzialmente.

Come una tupla di insiemi diventa una parola

Una tupla di variabili del secondo ordine:

$$X_1,\ldots,X_n$$

può essere vista come una parola infinita su alfabeto:

$$\lbrace 0,1\rbrace^n.$$

Alla posizione $k$, la lettera è il vettore di bit:

$$b_k=(b_1,\ldots,b_n)$$

dove:

$$b_j=1 \iff k\in X_j.$$

Quindi:

Questo è il punto che spesso crea confusione: non stiamo scegliendo un singolo valore per $X_i$, ma un intero insieme di posizioni, cioè una sequenza infinita di bit.

Interpretazione logica

Dire $\exists X_i$ significa: esiste una scelta dell'insieme $X_i$ che rende vera la formula.

Quindi sto nascondendo la componente $i$ della parola, ma chiedo che esista almeno un modo di completarla.

Formalmente, se $\pi_i$ cancella la componente $i$ da ogni lettera, allora:

$$ L(\exists X_i\;\varphi) = \pi_i(L(\varphi)). $$

Questo significa:

$$ \beta\in L(\exists X_i\;\varphi) \iff \exists \alpha\in L(\varphi)\text{ tale che }\pi_i(\alpha)=\beta. $$

La parola $\beta$ è la parola visibile, senza la componente $X_i$. La parola $\alpha$ è un completamento possibile di $\beta$ in cui la componente nascosta è stata reinserita.

Esempio minimo

Prendi due componenti $X$ e $Y$. Una posizione contiene una coppia di bit:

$$ (x_k,y_k)\in\lbrace 0,1\rbrace\times\lbrace 0,1\rbrace. $$

Considera la formula:

$$ \varphi(X,Y)\equiv \forall z(z\in X\to z\in Y). $$

Questa formula dice: tutte le posizioni marcate da $X$ sono marcate anche da $Y$.

Ora proietto via $Y$:

$$ \psi(X)\equiv \exists Y\;\forall z(z\in X\to z\in Y). $$

La formula $\psi$ è vera per ogni possibile $X$, perché posso sempre scegliere:

$$ Y=X. $$

In termini di parole: se vedo solo la prima componente, posso sempre completare la seconda componente copiando la prima. Quindi la proiezione del linguaggio è tutto $\lbrace 0,1\rbrace^\omega$.

Esempio meno banale

Ora aggiungo un vincolo di finitezza:

$$ \varphi(X,Y)\equiv \forall z(z\in X\to z\in Y) \land \exists m\forall z(m<z\to z\notin Y). $$

La prima parte dice che $Y$ deve contenere tutte le posizioni di $X$. La seconda dice che $Y$ è finito.

Proietto via $Y$:

$$ \exists Y\;\varphi(X,Y). $$

Che proprietà resta su $X$?

Resta: $X$ è finito.

Perché:

Quindi l'esistenziale non significa "ignoro il vincolo": significa "deve esistere una componente nascosta che rende il vincolo soddisfatto".

Interpretazione automata-theoretic

Se l'automa legge simboli con più componenti, proiettare significa cancellare una componente dall'alfabeto.

Supponi che:

$$ \mathcal{A}=(Q,\lbrace 0,1\rbrace^n,\Delta,q_0,F) $$

riconosca $L(\varphi)$.

Costruisco un automa proiettato:

$$ \mathcal{A}'=(Q,\lbrace 0,1\rbrace^{n-1},\Delta',q_0,F) $$

con gli stessi stati, lo stesso stato iniziale e gli stessi finali. Cambio solo le transizioni.

Metto:

$$ (p,c,q)\in\Delta' $$

se e solo se esiste una lettera completa $b\in\lbrace 0,1\rbrace^n$ tale che:

$$ \pi_i(b)=c $$

e:

$$ (p,b,q)\in\Delta. $$

L'automa $\mathcal{A}'$ legge la parola senza la componente $i$. Quando deve fare una transizione, sceglie nondeterministicamente quale valore nascosto della componente $i$ usare.

Perché la costruzione è corretta

Dimostriamo le due inclusioni.

Da sinistra a destra.

Se una parola visibile $\beta$ è accettata da $\mathcal{A}'$, allora esiste una run accettante:

$$ q_0q_1q_2\ldots $$

Ogni transizione della run:

$$ (q_k,\beta(k),q_{k+1}) $$

esiste in $\Delta'$ perché, per definizione di $\Delta'$, esiste almeno una lettera completa $b_k$ che proietta su $\beta(k)$ e rende valida la transizione in $\Delta$.

Scegliendo uno di questi $b_k$ per ogni posizione $k$, ottengo una parola completa:

$$ \alpha=b_0b_1b_2\ldots $$

tale che:

$$ \pi_i(\alpha)=\beta. $$

La stessa run è accettante per $\mathcal{A}$ su $\alpha$. Quindi $\beta$ appartiene alla proiezione di $L(\mathcal{A})$.

Da destra a sinistra.

Se $\beta$ è la proiezione di una parola completa $\alpha$ accettata da $\mathcal{A}$, prendo una run accettante di $\mathcal{A}$ su $\alpha$.

Ogni transizione:

$$ (q_k,\alpha(k),q_{k+1})\in\Delta $$

genera, per definizione, una transizione:

$$ (q_k,\pi_i(\alpha(k)),q_{k+1})\in\Delta'. $$

Ma $\pi_i(\alpha)=\beta$, quindi la stessa run accetta $\beta$ in $\mathcal{A}'$.

Conclusione:

$$ L(\mathcal{A}')=\pi_i(L(\mathcal{A})). $$

Quindi la proiezione di un omega-linguaggio regolare è ancora omega-regolare.

Punto orale

La frase da ricordare è:

$\exists X$ in S1S corrisponde a cancellare la componente $X$ dall'alfabeto dell'automa; il nondeterminismo dell'automa proiettato indovina i valori cancellati posizione per posizione.

Attenzione: la proiezione è esistenziale. Dopo aver cancellato $X$, una parola visibile è accettata se esiste almeno un completamento di $X$ che funzionava prima della cancellazione.

8. Secondo teorema di Büchi

Il teorema dice:

$$L\subseteq A^\omega \text{ è omega-regolare} \iff L \text{ è definibile in S1S}$$

Va capito in due direzioni.

9. Direzione automa -> logica

Supponi di avere un automa di Büchi:

$$\mathcal{A}=(Q,A,\Delta,q_0,F)$$

con:

$$Q=\lbrace q_0,\ldots,q_m\rbrace$$

Voglio costruire una formula S1S che dice: "esiste una run accettante di $\mathcal{A}$ sulla parola".

Introduco una variabile del secondo ordine $Y_i$ per ogni stato $q_i$.

Interpretazione:

$$x\in Y_i \quad \text{significa: alla posizione }x\text{ la run è nello stato }q_i$$

La formula avrà forma:

$$\exists Y_0\ldots\exists Y_m \; \Phi(Y_0,\ldots,Y_m)$$

dove $\Phi$ deve imporre quattro cose.

1. Stato iniziale

Alla posizione 0 la run è in $q_0$:

$$0\in Y_0$$

2. Esattamente uno stato a ogni posizione

Almeno uno stato:

$$\forall x \bigvee_{i=0}^{m} x\in Y_i$$

Al più uno stato:

$$\forall x \bigwedge_{i\neq j}\neg(x\in Y_i\land x\in Y_j)$$

Insieme dicono che ogni posizione della run ha uno e un solo stato.

3. Rispetto delle transizioni

Per ogni posizione x, se alla posizione x sono nello stato $q_i$ e leggo il simbolo $a$, allora alla posizione $x+1$ devo essere in uno stato $q_j$ tale che $(q_i,a,q_j)\in\Delta$.

Formula schematica:

$$\forall x \bigvee_{(q_i,a,q_j)\in\Delta}(x\in Y_i \land Q_a(x)\land x+1\in Y_j)$$

Questa formula dice che ogni passo della run è giustificato da una transizione dell'automa.

4. Condizione di Büchi

Almeno uno stato finale viene visitato infinite volte:

$$\bigvee_{q_i\in F}\forall x\exists y(x<y\land y\in Y_i)$$

Lettura: esiste uno stato finale $q_i$ tale che, qualunque punto x scelga, nel futuro trovo una posizione y in cui la run è in $q_i$.

Formula completa

Metto tutto insieme:

$$\exists Y_0\ldots\exists Y_m(\Phi_{init}\land\Phi_{unique}\land\Phi_{trans}\land\Phi_{acc})$$

Questa formula è vera su una parola $\alpha$ se e solo se $\mathcal{A}$ ha una run accettante su $\alpha$.

Quindi ogni linguaggio riconosciuto da un automa di Büchi è definibile in S1S.

10. Direzione logica -> automa

Ora bisogna mostrare l'opposto: data una formula S1S, posso costruire un automa di Büchi che riconosce esattamente i suoi modelli.

L'idea della dimostrazione è induttiva:

  1. costruisco automi per formule atomiche;
  2. uso chiusure booleane per $\lor,\land,\neg$;
  3. uso proiezione per il quantificatore esistenziale del secondo ordine;
  4. traduco il resto della sintassi in una forma ridotta equivalente.

Perché funziona?

Dato che gli omega-regolari sono chiusi per unione, intersezione, complemento e proiezione, posso costruire automi lungo la struttura della formula.

Per i quantificatori universali uso la dualità:

$$ \forall X\;\theta \equiv \neg\exists X\;\neg\theta. $$

Quindi anche il quantificatore universale si gestisce con complementazione e proiezione.

Il ruolo di S1S0

Negli appunti compare $S1S_0$, una variante ridotta di S1S che usa essenzialmente:

La dimostrazione tecnica mostra che $S1S$ e $S1S_0$ hanno lo stesso potere espressivo. Questo serve perché è più comodo costruire automi per un linguaggio logico minimale e poi dire che tutto S1S può essere riscritto lì.

L'idea da ricordare è:

Non serve memorizzare ogni formula tecnica, ma devi saper spiegare perché si può ridurre tutto a variabili monadiche del secondo ordine.

11. Decidibilità e costo

Il secondo teorema di Büchi implica che S1S è decidibile.

Per decidere se un enunciato S1S è vero:

  1. trasformo la formula in un automa di Büchi;
  2. controllo se il linguaggio dell'automa è tutto/vuoto a seconda del problema;
  3. uso emptiness e complementazione degli automi.

Ma c'è un prezzo: la procedura può avere complessità non-elementare. Il problema non è solo la lunghezza della formula, ma soprattutto il numero di alternanze tra quantificatori esistenziali e universali. Ogni negazione/complementazione e ogni proiezione può far esplodere la dimensione dell'automa.

La teoria di S1S e il conto preciso del costo

Due precisazioni dagli appunti che conviene saper enunciare.

La teoria di S1S è l'insieme degli enunciati (sentenze, formule chiuse) di S1S veri nella struttura $(\omega, 0, +1, <)$. Esempi:

"S1S è decidibile" significa: c'è una procedura che, dato un enunciato, decide se appartiene alla teoria. La procedura è: formula → automa di Büchi (input-free, per una sentenza) → test di emptiness (un ciclo finale raggiungibile).

Il costo, con precisione. La membership nella teoria di S1S è non-elementare: definendo $\exp_0(n) = n$ e $\exp_{h+1}(n) = 2^{\exp_h(n)}$, per nessun $h$ fissato il problema sta in tempo $\exp_h(n)$. Il parametro che governa l'altezza della torre non è la lunghezza della formula ma il numero di alternanze $\exists/\forall$: portando la formula in forma prenessa $\exists\cdots\exists\,\forall\cdots\forall\,\exists\cdots$, ogni blocco $\forall$ si riscrive $\neg\exists\neg$, e ogni negazione è una complementazione di Büchi (esponenziale). Una torre alta quanto il numero di alternanze.

Nota pratica degli appunti: è il worst case — strumenti come MONA (per WS1S) funzionano bene su molte formule reali.

Messaggio pratico:

12. WS1S: Weak S1S

Prima di definire WS1S conviene ricordare dove siamo arrivati, perché WS1S nasce esattamente come risposta a una domanda lasciata aperta dal secondo teorema di Büchi.

Richiamo: che cosa sappiamo già

Fino a qui abbiamo costruito questa catena di equivalenze, tutte sugli omega-linguaggi (linguaggi di parole infinite):

$$L \text{ omega-regolare} \iff L \text{ riconosciuto da un NBA} \iff L \text{ definibile in S1S}$$

L'ultima equivalenza è il secondo teorema di Büchi (sezioni 8-10). In S1S le variabili del secondo ordine $X,Y,\ldots$ sono insiemi qualsiasi di posizioni: possono essere finiti (es. $\lbrace 3,7\rbrace$) oppure infiniti (es. tutte le posizioni pari).

La domanda che si è posto Büchi è: e se obbligassi le variabili insiemistiche quantificate a rappresentare solo insiemi finiti? La logica che si ottiene è WS1S, la versione debole (weak) di S1S. Storicamente Büchi lavorò proprio con WS1S, non con S1S piena.

Definizione

WS1S = S1S in cui ogni variabile del secondo ordine quantificata ($\exists X$, $\forall X$) può rappresentare solo insiemi finiti di posizioni.

C'è un punto che crea confusione e va chiarito subito, perché è la prima cosa che fa pensare "ma allora come parlo di parole infinite?":

In breve: continuo ad analizzare parole infinite, ma gli unici insiemi che la formula può evocare come testimoni interni sono finiti. Intuitivamente WS1S parla di proprietà locali / finite dentro una parola infinita.

Perché "weak" e a cosa serve

L'aggettivo "debole" si riferisce proprio a questa restrizione: non posso quantificare liberamente su tutti gli insiemi infiniti di posizioni, ma solo su insiemi finiti.

L'intuizione degli appunti: con S1S esprimo proprietà globali, per esempio "dopo ogni $a$ ci sono solo $b$"; con WS1S il taglio tipico è "dopo ogni $a$ c'è un certo numero (finito) di $b$", cioè parlo di porzioni finite di computazione.

Si potrebbe obiettare: se mi interessano proprietà locali, perché non ritaglio il pezzo finito che mi serve e lo analizzo con i metodi sulle parole finite? Perché vogliamo comunque un formalismo che viva sulle parole infinite (le computazioni dei sistemi reattivi sono infinite) e che però sappia esprimere proprietà locali al loro interno. WS1S è esattamente questo compromesso.

Direzione facile: S1S è almeno espressiva quanto WS1S

Ogni formula WS1S è anche una formula S1S, a patto di aggiungere esplicitamente il vincolo "questo insieme è finito". E la finitezza è esprimibile in S1S: un insieme è finito se e solo se è vuoto oppure ha un elemento massimo.

$$\mathrm{Fin}(X)\ \equiv\ X=\emptyset\ \lor\ \exists m\big(m\in X\land \forall y(y\in X\to y\le m)\big)$$

(Equivalentemente, nella forma degli appunti: $X=\emptyset \lor \exists x(x\in X\land \forall y(x<y\to y\notin X))$, "in $X$ c'è un elemento dopo il quale $X$ non contiene più niente".) Allora per simulare WS1S in S1S basta scrivere $\exists X(\mathrm{Fin}(X)\land\ldots)$ e $\forall X(\mathrm{Fin}(X)\to\ldots)$.

Quindi S1S $\supseteq$ WS1S. La sorpresa è che vale anche il contrario.

Il risultato forte: WS1S e S1S hanno lo stesso potere espressivo

Teorema (espressività di WS1S). Un omega-linguaggio $L\subseteq A^\omega$ è omega-regolare (equivalentemente, definibile in S1S) se e solo se è definibile in WS1S.

A prima vista è strano: come può una logica che quantifica solo su insiemi finiti catturare proprietà genuinamente infinite come "$a$ compare infinite volte"? L'idea è elegante: invece di indovinare in un colpo solo un testimone infinito, controllo infiniti testimoni finiti, uno per ogni prefisso sempre più lungo. La dimostrazione (direzione S1S $\Rightarrow$ WS1S) mette insieme tre ingredienti, due dagli automi e uno dalla logica.

Ingrediente 1 (automi): l'operatore $\overrightarrow{W}$ (chiusura vettoriale / limite)

Dato un linguaggio di parole finite $W\subseteq A^\ast$, definiamo l'omega-linguaggio

$$\overrightarrow{W}=\lbrace \alpha\in A^\omega \mid \alpha \text{ ha infiniti prefissi in } W\rbrace.$$

Negli appunti questa operazione si scrive con una freccia, $W^{\rightarrow}$, e si chiama chiusura vettoriale (o limite) di $W$. "Infiniti prefissi in $W$" significa: nella sequenza dei prefissi $\alpha(0),\ \alpha(0)\alpha(1),\ \alpha(0)\alpha(1)\alpha(2),\ \ldots$ ce ne sono infiniti che appartengono a $W$.

Il legame con gli automi è preciso:

Un omega-linguaggio è riconosciuto da un automa di Büchi deterministico (DBA) se e solo se è della forma $\overrightarrow{W}$ per qualche $W$ regolare.

L'idea della dimostrazione: prendo il DBA e lo guardo come un DFA $\mathcal{A}'$ con la stessa struttura; sia $W=L(\mathcal{A}')$ il linguaggio di parole finite che riconosce. La computazione su $\alpha$ è unica (l'automa è deterministico) ed è accettante per Büchi se e solo se tocca uno stato finale infinite volte, cioè se e solo se infiniti prefissi di $\alpha$ finiscono in uno stato finale, cioè se e solo se infiniti prefissi stanno in $W$. Quindi $L(\text{DBA})=\overrightarrow{W}$.

Ingrediente 2 (automi): il teorema di McNaughton

I DBA da soli sono troppo deboli (per esempio non riconoscono "$a$ compare solo un numero finito di volte", come visto nel confronto NBA vs DBA del capitolo 5). Servono gli automi di Müller deterministici (DMA), e qui entra il teorema di McNaughton:

Teorema (McNaughton). Un omega-linguaggio è omega-regolare se e solo se è riconosciuto da un automa di Müller deterministico (DMA). Inoltre i linguaggi riconosciuti da DMA sono esattamente le combinazioni booleane ($\cup,\cap$ e complemento) di linguaggi della forma $\overrightarrow{W}$ con $W$ regolare.

La conseguenza che useremo è:

$$L \text{ omega-regolare} \iff L=\text{combinazione booleana di } \overrightarrow{W_1},\ldots,\overrightarrow{W_k}\quad (W_i \text{ regolari}).$$

Il quadro completo delle classi, da saper disegnare:

$$\text{DBA} \subsetneq \text{NBA} \equiv \text{NMA} \equiv \text{DMA} \supsetneq \text{DBA}$$

(NBA $\equiv$ NMA si vede passando per S1S: nella formula $\exists Y_0\cdots\exists Y_m(\varphi_1\land\varphi_2\land\varphi_3)$ che codifica un automa, $\varphi_1$ e $\varphi_2$ — stato iniziale, unicità dello stato, consequenzialità — restano identiche; cambia solo $\varphi_3$, che per Müller deve dire "gli stati di un certo $P\in\mathfrak{F}$ occorrono infinitamente spesso e quelli fuori da $P$ finitamente").

Perché la caratterizzazione è difficile: $U\cdot V^\omega$ vs $U\cdot\overrightarrow{V}$

Negli appunti c'è un'analisi fine che spiega perché il passaggio da NBA a DMA non è una semplice riscrittura. Sappiamo che gli ω-regolari sono unioni finite di $U\cdot V^\omega$; per McNaughton servono invece combinazioni booleane di $\overrightarrow{W}$. Verrebbe da sperare in identità semplici tra le due forme. Non valgono, e i controesempi sono istruttivi.

Primo tentativo: $U\cdot V^\omega = U\cdot\overrightarrow{V}$ assumendo $V\cdot V = V$?

Secondo tentativo: $U\cdot\overrightarrow{V} = \overrightarrow{U\cdot V}$?

La lettura profonda (quella da dire all'orale): le due forme differiscono per l'ordine dei quantificatori.

Il pattern $\forall\exists$ è più flessibile e non si riduce in generale a $\exists\forall$. È per questo che il lemma di caratterizzazione (ogni ω-regolare è unione finita di $\overrightarrow{U}\cap\neg\overrightarrow{V}$) è davvero difficile: la prova passa per gli automi di Rabin e la costruzione di Safra, e a lezione è stata data per enunciato.

Ingrediente 3 (logica): regolare = definibile, sulle parole finite

Sulle parole finite vale l'analogo del teorema di Büchi, noto come teorema di Büchi-Elgot-Trakhtenbrot:

Un linguaggio di parole finite $W\subseteq A^\ast$ è regolare se e solo se è definibile in logica monadica del secondo ordine, cioè in S1S interpretata su parole finite.

È la stessa corrispondenza logica $\leftrightarrow$ automi usata per Büchi, ma in versione finita. Conseguenza pratica: per ogni $W$ regolare esiste una formula $\varphi(X_1,\ldots,X_n)$ che lo definisce sulle parole finite (le $X_1,\ldots,X_n$ sono le componenti binarie delle lettere, come nella codifica della sezione 4).

Come si montano i tre pezzi

Sia $L$ omega-regolare.

  1. Per McNaughton, $L$ è una combinazione booleana di linguaggi $\overrightarrow{W_i}$ con $W_i$ regolari.
  2. Le operazioni booleane sui linguaggi diventano $\lor,\land,\neg$ tra formule. Quindi basta saper scrivere un solo $\overrightarrow{W}$ in WS1S, poi combino.
  3. Per Büchi-Elgot-Trakhtenbrot, $W$ ha una formula $\varphi(X_1,\ldots,X_n)$ sulle parole finite.
  4. "Avere infiniti prefissi in $W$" si scrive così: per ogni posizione esiste un prefisso più lungo che appartiene a $W$. La formula che definisce $\overrightarrow{W}$ è

$$\forall x\,\exists y\big(x<y\ \land\ \psi(X_1,\ldots,X_n,y)\big)$$

dove $\psi(\ldots,y)$ dice "il prefisso fino alla posizione $y$ soddisfa $\varphi$", cioè "il prefisso fino a $y$ sta in $W$".

Resta un solo nodo tecnico: come trasformo $\varphi$ (che parla di una parola finita intera) in $\psi(y)$ (che parla solo del prefisso fino a $y$ di una parola infinita)? E soprattutto: perché il risultato è una formula di WS1S e non di S1S piena? Questo è il cuore della sezione 13.

13. Relativizzare una formula a un prefisso (e perché esce WS1S)

Questo punto è il vero motore della dimostrazione di S1S $\Rightarrow$ WS1S e contiene l'osservazione che spesso sfugge.

L'operazione si chiama relativizzazione: prendo una formula che ragiona su tutto $\mathbb{N}$ e la "rinchiudo" a ragionare solo sulle posizioni $<y$, cioè sul prefisso di lunghezza $y$. Voglio passare da

"$\varphi$: la parola finita soddisfa $\varphi$" (definisce $W$)

a

"$\psi(y)$: il prefisso fino a $y$ soddisfa $\varphi$" (cioè il prefisso fino a $y$ sta in $W$).

La regola

Si riscrive ogni quantificatore limitandolo alle posizioni minori di $y$. La differenza chiave è tra esistenziale e universale:

Regola mnemonica: con $\exists$ si congiunge ($\land$) il vincolo "tutto sta nel prefisso", con $\forall$ lo si mette in premessa ($\to$). È lo stesso schema che si usa ogni volta che si relativizza un quantificatore a un sotto-dominio. Esempi concreti dagli appunti:

$$\exists X(0\in X)\quad\leadsto\quad \exists X\big(\forall z(z\in X\to z<y)\land 0\in X\big)$$

$$\forall X(0\in X)\quad\leadsto\quad \forall X\big(\forall z(z\in X\to z<y)\to 0\in X\big)$$

Applicando la regola a tutti i quantificatori interni di $\varphi(X_1,\ldots,X_n)$ ottengo $\psi(X_1,\ldots,X_n,y)$: "il prefisso fino a $y$ soddisfa $\varphi$". Le variabili libere $X_1,\ldots,X_n$ (che codificano la parola infinita) restano libere e non vengono toccate; vengono relativizzati solo i quantificatori interni.

Il punto cruciale: perché $\psi$ è WS1S

Ecco l'osservazione che chiude tutto. Dopo la relativizzazione, ogni insieme $X$ quantificato dentro $\psi$ è obbligato a stare dentro $\lbrace 0,1,\ldots,y-1\rbrace$, perché abbiamo aggiunto proprio

$$\forall z(z\in X\to z<y).$$

Ma $\lbrace 0,\ldots,y-1\rbrace$ è un insieme finito! Quindi tutte le variabili del secondo ordine quantificate spaziano solo su insiemi finiti: per definizione, $\psi$ è una formula di WS1S, non di S1S piena. (Le $X_1,\ldots,X_n$ libere codificano la parola infinita e possono restare infinite: in WS1S il vincolo di finitezza è solo sulle variabili quantificate, come chiarito nella sezione 12.)

Di conseguenza anche

$$\forall x\,\exists y\big(x<y\land \psi(X_1,\ldots,X_n,y)\big)$$

è in WS1S — i quantificatori $\forall x,\exists y$ sono del primo ordine, non insiemi — e definisce esattamente $\overrightarrow{W}$: "comunque scelga una posizione $x$, esiste un prefisso più lungo (fino a $y>x$) che sta in $W$", cioè ci sono infiniti prefissi in $W$.

Questa è la "magia" annunciata nella sezione 12: una proprietà infinita come "infiniti prefissi in $W$" viene catturata da una formula che internamente evoca solo testimoni finiti, un prefisso finito alla volta. Il "per ogni $x$ esiste $y>x$" garantisce che i prefissi buoni siano infiniti, ma ogni singolo controllo è finito.

Chiusura del cerchio

Mettendo insieme con la sezione 12:

Unendo questa direzione con quella facile (sezione 12) e con il secondo teorema di Büchi (S1S = omega-regolare), si chiude tutto:

$$\boxed{\ \text{omega-regolare}\ \iff\ \text{S1S}\ \iff\ \text{WS1S}\ }$$

14. Estensioni e frammenti da ricordare

Una volta fissato il nucleo (S1S $\equiv$ WS1S $\equiv$ omega-regolare), gli appunti guardano ai bordi: cosa succede se rendo S1S più forte, e cosa succede se la indebolisco.

Estensioni che restano decidibili (e una che no)

Posso arricchire la struttura $(\omega,0,+1,<)$ con predicati o funzioni extra. Alcune aggiunte preservano la decidibilità:

Altre aggiunte rompono tutto:

Morale: c'è una frontiera sottile tra "predicato extra inoffensivo" e "potenza che fa cadere la decidibilità". È lo stesso tipo di confine che separa l'aritmetica di Presburger (solo addizione, decidibile) dall'aritmetica di Peano (addizione e moltiplicazione, indecidibile): basta poter ricostruire la moltiplicazione per perdere la decidibilità.

S2S: dalla parola all'albero

S1S parla di una sequenza lineare di posizioni: una computazione alla volta. S2S è la teoria monadica del secondo ordine con due successori: il dominio non è più la retta $\mathbb{N}$ ma l'albero binario infinito, dove ogni posizione ha un figlio sinistro e un figlio destro.

S2S è ancora decidibile (risultato profondo di Rabin) ed è il formalismo giusto quando si vuole ragionare sull'intero ventaglio delle computazioni non deterministiche, non su un singolo ramo. Qualsiasi albero a ramificazione finita si riduce a quello binario. È lo sfondo teorico delle logiche temporali ad albero (CTL/CTL*, capitolo 7).

Alberi: il dominio di S2S

Per S2S l'albero binario infinito si può vedere come l'insieme $\lbrace 0,1\rbrace^\ast$ delle stringhe finite di 0 e 1:

Un albero etichettato su un alfabeto $A$ assegna a ogni nodo un simbolo di $A$. Un linguaggio di alberi è quindi un insieme di alberi etichettati, esattamente come un linguaggio di parole è un insieme di parole.

La differenza concettuale è questa:

Automi su alberi (tree automata)

Gli automi su alberi (tree automata) sono automi finiti che leggono alberi invece di parole. Nel caso binario infinito, una forma tipica è

$$\mathcal{A}=(Q,A,\Delta,q_0,\mathcal{C})$$

dove $Q$ è finito, $q_0$ è lo stato iniziale alla radice, $\Delta\subseteq Q\times A\times Q\times Q$ dice quali stati assegnare ai due figli, e $\mathcal{C}$ è una condizione di accettazione sui rami infiniti.

Una run non è più una sequenza di stati, ma un'etichettatura dell'intero albero con stati. Se un nodo $x$ ha etichetta $a$ e stato $q$, allora i figli $x0,x1$ devono ricevere stati $q_0',q_1'$ tali che

$$ (q,a,q_0',q_1')\in\Delta. $$

Per gli alberi infiniti l'accettazione deve controllare ogni ramo infinito. Per questo si usano condizioni analoghe a quelle degli automi su parole infinite: Büchi, Muller, Rabin.

Automi di Rabin (Rabin automata)

Gli automi di Rabin (Rabin automata) usano una condizione di accettazione fatta di coppie di insiemi di stati:

$$\Omega=\lbrace (L_1,U_1),\ldots,(L_n,U_n)\rbrace.$$

L'idea di una coppia $(L_i,U_i)$ è:

Su un ramo $\pi$, se $Inf(\rho_\pi)$ è l'insieme degli stati visitati infinitamente spesso, la condizione di Rabin richiede che esista un indice $i$ tale che

$$Inf(\rho_\pi)\cap L_i=\emptyset \quad\text{e}\quad Inf(\rho_\pi)\cap U_i\neq\emptyset.$$

Per una run su un albero, questa condizione va soddisfatta lungo tutti i rami. Il punto teorico da ricordare è il teorema di Rabin:

un linguaggio di alberi infiniti è riconoscibile da un automa di Rabin se e solo se è definibile in S2S.

Quindi il ruolo di Rabin per S2S è analogo al ruolo di Büchi per S1S: collega logica e automi, ma ora sul dominio degli alberi invece che sulle parole.

WS2S: la versione debole su alberi

Come WS1S limita le variabili monadiche del secondo ordine a insiemi finiti di posizioni della parola, WS2S limita le variabili monadiche a insiemi finiti di nodi dell'albero binario.

La relazione da ricordare è:

Negli appunti compare come parallelo naturale di WS1S: stessa idea di "weak", ma sul dominio ramificato invece che sulla linea.

Il frammento del primo ordine e i linguaggi star-free

Indebolire S1S nell'altra direzione significa tenere solo i quantificatori del primo ordine (niente $\exists X,\forall X$ sugli insiemi). Si ottiene il frammento del primo ordine di $S1S_A$, cioè i linguaggi first-order definable, caratterizzato dal teorema di McNaughton-Papert:

Un linguaggio $W\subseteq A^\ast$ è star-free (esprimibile con espressioni regolari senza stella di Kleene, ma con il complemento) se e solo se è definibile al primo ordine in $S1S_A$, con l'ordine $<$ e i predicati $Q_a$.

Una espressione star-free parte da linguaggi finiti e simboli dell'alfabeto, e usa unione, concatenazione e complemento. Non usa l'operatore $^*$ di Kleene. Quindi:

Una sottigliezza importante sulla firma logica, da ricordare:

Il motivo è che $<$ non è definibile al primo ordine a partire da $+1$ (per dire "raggiungibile in un numero arbitrario di passi" servirebbe la quantificazione del secondo ordine). Quindi il primo ordine di $S1S_A(<)$ è strettamente più espressivo del primo ordine di $S1S_A(+1)$.

Caso infinito (teorema di Ladner): gli omega-linguaggi star-free coincidono con il primo ordine di $S1S_A$ sulle parole infinite, e sono un sottoinsieme proprio degli omega-regolari (strettamente meno espressivi). Questo frammento è importante perché coincide con il potere espressivo della logica temporale lineare LTL (capitolo 7): meno espressività, ma formule e algoritmi molto più maneggevoli. È anche il motivo per cui nelle applicazioni si preferiscono spesso le logiche temporali a S1S piena.

15. Errori comuni

  1. Confondere posizione e simbolo. In S1S le variabili $x,y$ sono posizioni, non lettere.
  2. Confondere $Q_a(x)$ con $x=a$. La formula $Q_a(x)$ dice che alla posizione x compare la lettera a.
  3. Pensare che "infinitamente spesso" significhi "sempre". Non è così: $a$ può comparire infinite volte anche se tra due $a$ ci sono blocchi lunghi di $b$.
  4. Dimenticare l'unicità dello stato nella traduzione automa -> S1S. Le variabili $Y_i$ devono formare una partizione delle posizioni della run.
  5. Confondere proiezione e cancellazione senza vincoli. Proiettare via $X$ non significa che la vecchia formula smette di contare: significa che deve esistere una scelta di $X$ che la soddisfa.
  6. Confondere S1S e WS1S: WS1S quantifica solo su insiemi finiti, ma sugli omega-linguaggi ha comunque lo stesso potere espressivo di S1S.
  7. Pensare che WS1S costringa tutto a essere finito. No: il vincolo "finito" vale solo per le variabili del secondo ordine quantificate. La parola infinita resta infinita (è data dai predicati $Q_a$ / dalle variabili libere). Per questo WS1S può ancora parlare di omega-linguaggi.
  8. Confondere $\overrightarrow{W}$ ("infiniti prefissi in $W$", che riguarda gli automi deterministici e i prefissi finiti) con $W^\omega$ ("concatenazione infinita di parole di $W$"). Sono operatori diversi: in generale $W^\omega \neq \overrightarrow{W}$.
  9. Dimenticare la differenza $\land$/$\to$ nella relativizzazione: con $\exists$ si congiunge il vincolo sul prefisso, con $\forall$ lo si mette in premessa. È esattamente questo vincolo "tutto sta nel prefisso $<y$" che rende finiti gli insiemi quantificati, cioè che rende la formula WS1S.

16. Esercizi svolti

Esercizio 1: formula per "P vale infinite volte"

Scrivere una formula che dice che $P$ vale infinite volte.

Soluzione:

$$\forall x\exists y(x<y\land y\in P)$$

Perché funziona: se dopo ogni posizione x riesco a trovare una posizione futura y in P, allora P non può esaurirsi. Quindi P compare infinite volte.

Esercizio 2: formula per "P vale solo un numero finito di volte"

Soluzione:

$$\exists x\forall y(x<y\to y\notin P)$$

Perché funziona: esiste una soglia x dopo la quale P non compare più.

Esercizio 3: nessuna a consecutiva

Alfabeto $A=\lbrace a,b\rbrace$.

Soluzione:

$$\forall x(Q_a(x)\to \neg Q_a(x+1))$$

Questa formula vieta il pattern $aa$ in posizioni consecutive.

Esercizio 4: ogni richiesta ha una risposta futura

Alfabeto con predicati $Q_{req}$ e $Q_{grant}$.

Soluzione:

$$\forall x(Q_{req}(x)\to \exists y(x<y\land Q_{grant}(y)))$$

Nota: questa formula non richiede che il grant corrisponda univocamente a quella request. Richiede solo che dopo ogni request esista almeno un grant futuro.

Esercizio 5: tradurre un automa di Büchi in S1S

Dato un automa con stati $q_0,q_1$ e finale $q_1$, introduci:

Formula schematica:

$$\exists Y_0\exists Y_1(\Phi_{init}\land\Phi_{unique}\land\Phi_{trans}\land\Phi_{acc})$$

dove:

17. Laboratorio pratico: formule e traduzioni complete

Caso 1: "ogni request ha un grant successivo"

Formula:

$$\forall x(Q_{req}(x)\to \exists y(x<y\land Q_{grant}(y)))$$

Lettura parola per parola:

Questa formula permette che un singolo grant risponda a più request precedenti. Se vuoi modellare una corrispondenza uno-a-uno tra request e grant, serve una formula più forte, con insiemi o vincoli aggiuntivi.

Caso 2: "ogni request ha un grant prima della prossima request"

Questa proprietà è più forte. Dice: se vedo una request in $x$, allora trovo un grant $y$ dopo $x$, e prima di quel grant non c'è una nuova request.

Formula:

$$\forall x\bigl(Q_{req}(x)\to \exists y(x<y\land Q_{grant}(y)\land \forall z((x<z\land z<y)\to \neg Q_{req}(z)))\bigr)$$

Lettura:

Questa è una tipica formula in cui bisogna fare attenzione all'ordine dei quantificatori. Il grant $y$ dipende dalla request $x$.

Caso 3: "da un certo punto in poi vale sempre safe"

Formula:

$$\exists x\forall y(x<y\to Q_{safe}(y))$$

Questa è una proprietà di stabilizzazione: può esserci un prefisso iniziale brutto, ma dopo una soglia tutto diventa safe.

Se invece vuoi dire "safe vale sempre", la formula è più semplice:

$$\forall x Q_{safe}(x)$$

Quindi:

Caso 4: "p e q si alternano esattamente"

Supponiamo un alfabeto con due simboli $p$ e $q$, codificati da $Q_p$ e $Q_q$.

Una parola alternante può iniziare con $p$ oppure con $q$. Qui imponiamo che inizi con $p$:

$$Q_p(0)$$

e poi:

$$\forall x(Q_p(x)\to Q_q(x+1))$$

$$\forall x(Q_q(x)\to Q_p(x+1))$$

Formula completa:

$$Q_p(0)\land \forall x(Q_p(x)\to Q_q(x+1))\land \forall x(Q_q(x)\to Q_p(x+1))$$

Questa formula produce parole come:

$$pqpqpq\ldots$$

Se vuoi permettere anche:

$$qpqpqp\ldots$$

devi fare una disgiunzione tra i due casi iniziali.

Caso 5: automa semplice -> formula S1S completa

Costruiamo una formula per l'NBA che accetta parole su $\lbrace a,b\rbrace$ con infinite $a$.

Automa:

Intuizione: $q_1$ significa "la posizione corrente legge $a$"; visitare $q_1$ infinite volte significa vedere infinite $a$.

Introduco insiemi:

Formula:

$$\exists Y_0\exists Y_1(\Phi_{part}\land\Phi_{init}\land\Phi_{trans}\land\Phi_{acc})$$

Partizione degli stati:

$$\Phi_{part}\equiv \forall x((x\in Y_0\lor x\in Y_1)\land \neg(x\in Y_0\land x\in Y_1))$$

Stato iniziale:

$$\Phi_{init}\equiv 0\in Y_0$$

Transizioni:

$$\Phi_{trans}\equiv \forall x\bigl((Q_a(x)\to x+1\in Y_1)\land(Q_b(x)\to x+1\in Y_0)\bigr)$$

Accettazione Büchi:

$$\Phi_{acc}\equiv \forall x\exists y(x<y\land y\in Y_1)$$

Commento importante: questa è una versione didattica. In una codifica rigorosa, bisogna allineare con precisione se lo stato è considerato prima o dopo la lettura della posizione $x$. L'idea essenziale però è questa: la run è codificata con insiemi di posizioni, le transizioni diventano vincoli locali, e Büchi diventa "visito $Y_1$ infinite volte".

Caso 6: proiezione spiegata con bit nascosto

Supponi un alfabeto a due componenti:

$$A=\lbrace 0,1\rbrace\times\lbrace 0,1\rbrace$$

Una lettera è una coppia $(x,y)$. Immagina di avere un linguaggio che parla di entrambe le componenti:

"la seconda componente vale 1 infinite volte".

In S1S scrivo:

$$ \varphi(X,Y)\equiv \forall z\exists t(z<t\land t\in Y). $$

Ora proietto via la seconda componente:

$$ \exists Y\;\varphi(X,Y). $$

Vuol dire che osservo solo la prima componente $X$ e mi chiedo:

esiste una scelta della seconda componente che rende vera la proprietà?

La risposta è sì per qualunque $X$: basta scegliere $Y=\mathbb{N}$. Quindi la proiezione è l'intero linguaggio $\lbrace 0,1\rbrace^\omega$ sulla prima componente.

Questo esempio mostra perché la proiezione è esistenziale: la componente nascosta viene scelta nel modo più favorevole.

Un esempio più informativo è:

$$ \theta(X,Y)\equiv \forall z(z\in X\to z\in Y) \land \exists m\forall z(m<z\to z\notin Y). $$

Qui $Y$ deve contenere $X$ ma deve essere finito. Dopo la proiezione:

$$ \exists Y\;\theta(X,Y) $$

resta la proprietà "X è finito".

In automi, il nondeterminismo indovina i valori della componente nascosta posizione per posizione. Se esiste una sequenza nascosta che porta a una run accettante, la parola proiettata viene accettata.

Caso 7: WS1S e prefissi finiti

In WS1S le variabili insiemistiche quantificate rappresentano insiemi finiti. Questo sembra più debole, ma sugli omega-linguaggi si recupera S1S usando un'idea di relativizzazione.

Esempio: voglio parlare di una proprietà entro un prefisso finito delimitato da una posizione $z$.

Un quantificatore:

$$\exists x\;\psi(x)$$

diventa:

$$\exists x(x\le z\land \psi(x))$$

Un quantificatore universale:

$$\forall x\;\psi(x)$$

diventa:

$$\forall x(x\le z\to \psi(x))$$

L'idea è: invece di far variare tutto su $\omega$, restringo temporaneamente la formula a un pezzo finito. Poi uso argomenti di automi e periodicità per collegare il comportamento finito al comportamento infinito.

Caso 8: da $W$ regolare a $\overrightarrow{W}$ in WS1S, esempio completo

Rendiamo concreto il meccanismo della sezione 13 con numeri. Alfabeto $A=\lbrace a,b\rbrace$. Riprendiamo il linguaggio del Caso 5: "$\alpha$ ha infinite $a$".

Passo 1 — scelgo $W$. Osservazione chiave: un prefisso $\alpha(0)\cdots\alpha(n-1)$ termina con $a$ esattamente quando $\alpha(n-1)=a$. Quindi i prefissi che terminano con $a$ sono infiniti se e solo se $\alpha$ ha infinite $a$. Prendo allora il linguaggio di parole finite

$$W=\lbrace w\in A^\ast \mid w \text{ termina con } a\rbrace = A^\ast\cdot a,$$

che è regolare, e affermo che "infinite $a$" $=\overrightarrow{W}$.

Passo 2 — formula $\varphi$ per $W$ (parole finite). "L'ultima posizione porta $a$". L'ultima posizione è quella senza successore dentro la parola:

$$\varphi \equiv \exists x\big(Q_a(x)\land \neg\exists w(x<w)\big).$$

Passo 3 — relativizzo al prefisso fino a $y$ (regola della sezione 13: "nessun successore" diventa "nessun successore $<y$"):

$$\psi(y)\equiv \exists x\big(x<y\land Q_a(x)\land \neg\exists w(x<w\land w<y)\big).$$

A parole: tra le posizioni $<y$ ce n'è una con $a$ che è l'ultima del prefisso (non ha posizioni intermedie tra sé e $y$). Cioè la posizione immediatamente prima di $y$ porta $a$. Si vede bene che equivale a $\exists x(x+1=y\land Q_a(x))$.

Passo 4 — la formula di $\overrightarrow{W}$:

$$\forall x\,\exists y\big(x<y\land \psi(y)\big).$$

Sviluppata: $\forall x\,\exists y\big(x<y\land \exists w(w+1=y\land Q_a(w))\big)$, cioè "comunque scelga $x$, più avanti c'è un prefisso che termina con $a$" = infinite $a$. Esattamente il linguaggio del Caso 5, ma ottenuto per via logica.

Perché è WS1S. Qui $\psi$ usa solo quantificatori del primo ordine, quindi è banalmente WS1S. In generale $\varphi$ può usare insiemi quantificati: la relativizzazione li costringe dentro $\lbrace 0,\ldots,y-1\rbrace$, cioè li rende finiti, ed è proprio questo che garantisce che la formula stia in WS1S (sezione 13). Le combinazioni booleane di più $\overrightarrow{W_i}$ (per McNaughton) si scrivono con $\lor,\land,\neg$, e si ottiene qualunque omega-linguaggio omega-regolare.

18. Domande da orale

  1. Che cosa significa "monadica del secondo ordine"?
  2. Qual è la differenza tra variabili del primo ordine e del secondo ordine?
  3. Come si rappresenta una parola infinita come struttura logica?
  4. Che cosa sono i predicati $Q_a$?
  5. Scrivi una formula S1S per "a compare infinite volte".
  6. Scrivi una formula S1S per "dopo ogni request arriva un grant".
  7. Spiega il lemma di chiusura per proiezione in termini logici e in termini di automi.
  8. Enuncia il secondo teorema di Büchi.
  9. Spiega la direzione automa -> logica.
  10. Spiega la direzione logica -> automa.
  11. Che cos'è WS1S? In WS1S che cosa è obbligato a essere finito, e che cosa no?
  12. Perché S1S è decidibile ma costosa? (parametro: numero di alternanze di quantificatori)
  13. Definisci $\overrightarrow{W}$ e collega l'operatore agli automi di Büchi deterministici.
  14. Enuncia il teorema di McNaughton e spiega perché serve nella dimostrazione di S1S $\equiv$ WS1S.
  15. Spiega la relativizzazione a un prefisso e perché produce una formula di WS1S (e non di S1S piena).
  16. Perché WS1S, pur quantificando solo su insiemi finiti, ha lo stesso potere espressivo di S1S sugli omega-linguaggi?
  17. Qual è la differenza tra S1S e S2S? Fai un esempio di estensione di S1S che resta decidibile e una che diventa indecidibile.

19. Quiz interattivo

Quiz Capitolo 6 - S1S e WS1S

1. In S1S, cosa rappresenta una variabile del secondo ordine X?




2. Quale formula esprime che P vale infinitamente spesso?




3. Che cosa afferma il secondo teorema di Büchi?




4. A livello di automi, cosa corrisponde a esistenzializzare una variabile del secondo ordine?




5. Qual è la differenza semantica principale tra S1S e WS1S?




20. Mini-scaletta di ripasso

  1. Spiega perché S1S è utile dopo gli automi di Büchi.
  2. Distingui variabili di primo ordine e secondo ordine.
  3. Spiega come una omega-parola diventa una struttura logica.
  4. Scrivi le formule per "P vale infinite volte" e "P vale solo un numero finito di volte".
  5. Spiega proiezione come $\exists X$ e come nondeterminismo.
  6. Enuncia il secondo teorema di Büchi.
  7. Racconta automa -> logica con gli insiemi $Y_i$.
  8. Racconta logica -> automa usando chiusure booleane e proiezione.
  9. Spiega WS1S e perché ha lo stesso potere espressivo di S1S sugli omega-linguaggi.
  10. Ricostruisci la catena del risultato WS1S $\equiv$ S1S: $\overrightarrow{W}$ e DBA $\to$ McNaughton (omega-regolare = combinazione booleana di $\overrightarrow{W}$) $\to$ Büchi-Elgot-Trakhtenbrot ($\varphi$ per $W$ regolare) $\to$ relativizzazione al prefisso ($\Rightarrow$ insiemi finiti $\Rightarrow$ WS1S).
  11. Cita un'estensione decidibile e una indecidibile di S1S, e spiega cos'è S2S.

Esercizi (piano di studio)

Esercizi e domande — settimana 3

Obiettivo della settimana: padroneggiare automi su parole infinite e il ponte logica-automi.

Esercizi scritti essenziali

  1. NBA base. Costruisci un NBA su $\lbrace a,b\rbrace$ che accetta le parole con infinitamente molte $a$: $$L=\lbrace \alpha\in\lbrace a,b\rbrace^\omega \mid a \text{ occorre infinite volte}\rbrace$$

  2. Numero finito di occorrenze di a. Costruisci un NBA per: $$L=\lbrace \alpha\in\lbrace a,b\rbrace^\omega \mid a \text{ occorre finitamente molte volte}\rbrace$$ Spiega perche il nondeterminismo e' naturale qui.

  3. Limite dei DBA. Argomenta perche il linguaggio "solo un numero finito di $a$" non e' riconoscibile da un DBA. Non serve una prova topologica completa: basta una spiegazione orale convincente basata sull'impossibilita di sapere deterministicamente l'ultima $a$.

  4. Espressioni omega-regolari. Scrivi un'espressione omega-regolare per:

  5. infinitamente molte $a$;
  6. finitamente molte $a$;

  7. parole in cui ogni blocco tra due $a$ consecutive contiene un numero pari di simboli diversi da $a$.

  8. Equivalenza espressione -> automa. Prendi $(b^*a)^\omega$ e costruisci un NBA che la riconosce. Indica perche gli stati finali vengono visitati infinite volte.

  9. GNBA -> NBA. Dato un GNBA con insiemi di accettazione $F_1,F_2,F_3$, descrivi la costruzione dell'NBA equivalente con contatore di obblighi. Poi applicala a un esempio piccolo.

  10. Chiusura per intersezione. Costruisci il prodotto di due NBA per riconoscere: "infinitamente molte $a$" e "infinitamente molte $b$".

  11. Muller automata. Dai un automa di Muller deterministico molto semplice che distingue le parole in cui il set degli stati visitati infinitamente spesso appartiene a una famiglia $\mathcal{F}$. Spiega perche il complemento e' facile per Muller.

  12. S1S: infinitamente spesso. Scrivi una formula S1S per dire che il predicato $P$ vale in infinite posizioni: $$\forall x\exists y(x<y \land y\in P)$$ Poi riscrivila spiegando il ruolo delle variabili di primo e secondo ordine.

  13. S1S: alternanza. Scrivi una formula S1S per parole su $\lbrace a,b\rbrace$ in cui non compaiono mai due $a$ consecutive.

  14. Chiusura per proiezione. Spiega con un esempio cosa significa proiettare via una componente dell'alfabeto. Traduci l'idea in una frase sugli automi di Büchi.

  15. Secondo teorema di Büchi. Scrivi una dimostrazione-scheletro delle due direzioni:

  16. automa di Büchi -> formula S1S;
  17. formula S1S -> automa di Büchi.

Domande orali secche

  1. Perche per i sistemi reattivi servono parole infinite?
  2. Definizione formale di NBA e condizione di accettazione.
  3. Differenza tra NBA, DBA, GNBA e Muller automata.
  4. Che cosa dice il secondo teorema di Büchi?
  5. Differenza tra S1S e WS1S.

Controllo

Hai superato la settimana se sai costruire gli automi per "infinite occorrenze di a" e "solo un numero finito di a", e se sai raccontare il ponte S1S-Büchi senza perderti nei dettagli tecnici.

Indice← PrecedenteSuccessivo →