Dimostrazioni formali complete

Come usare questa pagina

Questa pagina raccoglie le dimostrazioni degli appunti che piu facilmente possono diventare domande orali. L'obiettivo non e' riassumere l'idea, ma avere una versione studiabile in cui i passaggi "immediati" sono esplicitati.

Le fonti locali usate sono soprattutto:

• raw/Automi a stati finiti su parole finite.md
• raw/Myhill-Nerode Theorem.md
• raw/Automi a stati finiti su parole infinite.md
• raw/Secondo teorema di Büchi.md
• raw/Linear Temporal Logic.md
• raw/Model Checking.md
• raw/notes.pdf
• raw/Riassunti si o.pdf (controllo visivo: PDF manoscritto senza testo estraibile)
• expansions/week01_finite_automata_deepening.md
• expansions/week03_infinite_automata_deepening.md
• expansions/week03_mso_s1s_deepening.md

Indice delle dimostrazioni

• 1. Subset construction: ogni NFA ha un DFA equivalente
• 2. Vuotezza dei DFA: small model property
• 3. Infinitudine dei DFA
• 4. Teorema di Myhill-Nerode
• 5. Da automi di Büchi a espressioni omega-regolari, e viceversa
• 6. Intersezione di automi di Büchi e GNBA
• 7. Emptiness degli automi di Büchi
• 8. Complementazione Büchi tramite congruenza e saturazione
• 9. Caratterizzazione dei DBA e non-chiusura per complemento
• 10. Secondo teorema di Büchi: direzione automa -> S1S
• 11. Secondo teorema di Büchi: direzione S1S -> automa
• 12. Behavior graph LTL: componente adeguata implica soddisfacibilita' sul programma
• 13. Traduzioni LTL: forme da saper giustificare
• 14. Da epsilon-NFA a NFA
• 15. Teorema automi finiti - espressioni regolari
• 16. Chiusura booleana dei linguaggi regolari finiti
• 17. Chiusure base degli omega-regolari: $V^\omega$ e $V\cdot L$
• 18. Parole ultimamente periodiche
• 19. Decidibilita' per automi di Büchi
• 20. Tableau LTL: soddisfacibilita' tramite fulfilling MSCS
• 21. CTL tramite punti fissi: $EG$ ed $EU$
• 22. Chiusura di DBA per unione e intersezione
• 23. Automi di Muller: da Büchi, complemento e operazioni booleane
• 24. NMA e S1S: formalizzare la condizione di Muller
• 25. Giochi di raggiungibilita': attractor e strategie posizionali
• 26. Weak Muller games come weak parity games
• 27. Da Muller a parity con LAR

1. Subset construction: ogni NFA ha un DFA equivalente

Enunciato

Per ogni NFA

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

con $\Delta:Q\times\Sigma\to 2^Q$, esiste un DFA $\mathcal{D}$ tale che:

$$ L(\mathcal{D})=L(\mathcal{N}). $$

Costruzione

Costruiamo:

$$ \mathcal{D}=(2^Q,\Sigma,\delta^D,\{q_0\},F^D) $$

dove:

$$ \delta^D(S,a)=\bigcup_{q\in S}\Delta(q,a) $$

e:

$$ F^D=\{S\subseteq Q\mid S\cap F\neq\emptyset\}. $$

Uno stato del DFA non rappresenta un singolo stato dell'NFA, ma l'insieme di tutti gli stati in cui l'NFA potrebbe trovarsi dopo aver letto un certo prefisso.

Invariante da dimostrare

Per ogni parola $w\in\Sigma^\ast$:

$$ \hat{\delta}^{D}(\{q_0\},w) = \{q\in Q\mid q_0\xrightarrow[\mathcal{N}]{w}q\}. $$

Il lato sinistro e' lo stato raggiunto dal DFA. Il lato destro e' l'insieme degli stati raggiungibili dall'NFA leggendo $w$.

Dimostrazione per induzione su $|w|$

Base: $w=\varepsilon$.

Per definizione dell'estensione della transizione del DFA:

$$ \hat{\delta}^{D}(\{q_0\},\varepsilon)=\{q_0\}. $$

Nell'NFA, leggendo la parola vuota da $q_0$, l'unico stato raggiungibile senza consumare simboli e' $q_0$. Quindi:

$$ \{q\in Q\mid q_0\xrightarrow[\mathcal{N}]{\varepsilon}q\}=\{q_0\}. $$

I due insiemi coincidono.

Passo induttivo.

Supponiamo vera la tesi per una parola $w$. Dimostriamola per $wa$, con $a\in\Sigma$.

Per definizione di transizione estesa nel DFA:

$$ \hat{\delta}^{D}(\{q_0\},wa) = \delta^{D}(\hat{\delta}^{D}(\{q_0\},w),a). $$

Per ipotesi induttiva:

$$ \hat{\delta}^{D}(\{q_0\},w) = R_w $$

dove:

$$ R_w=\{q\in Q\mid q_0\xrightarrow[\mathcal{N}]{w}q\}. $$

Quindi:

$$ \hat{\delta}^{D}(\{q_0\},wa) = \delta^{D}(R_w,a) = \bigcup_{q\in R_w}\Delta(q,a). $$

Ora guardiamo il significato del lato destro. Uno stato $r$ appartiene a $\bigcup_{q\in R_w}\Delta(q,a)$ se e solo se esiste uno stato $q\in R_w$ tale che $r\in\Delta(q,a)$. Ma $q\in R_w$ significa che l'NFA puo arrivare da $q_0$ a $q$ leggendo $w$, e $r\in\Delta(q,a)$ significa che puo poi andare da $q$ a $r$ leggendo $a$.

Dunque:

$$ r\in\bigcup_{q\in R_w}\Delta(q,a) \iff q_0\xrightarrow[\mathcal{N}]{wa}r. $$

Quindi:

$$ \hat{\delta}^{D}(\{q_0\},wa) = \{r\in Q\mid q_0\xrightarrow[\mathcal{N}]{wa}r\}. $$

L'invariante e' dimostrato.

Uguaglianza dei linguaggi

Una parola $w$ e' accettata da $\mathcal{D}$ se e solo se:

$$ \hat{\delta}^{D}(\{q_0\},w)\in F^D. $$

Per definizione di $F^D$, questo equivale a:

$$ \hat{\delta}_D(\{q_0\},w)\cap F\neq\emptyset. $$

Per l'invariante, cioe':

$$ \{q\mid q_0\xrightarrow[\mathcal{N}]{w}q\}\cap F\neq\emptyset. $$

Questa e' esattamente la definizione di accettazione dell'NFA: esiste almeno una computazione che, leggendo tutta $w$, finisce in uno stato finale. Quindi:

$$ w\in L(\mathcal{D}) \iff w\in L(\mathcal{N}). $$

Poiche' vale per ogni $w$, abbiamo:

$$ L(\mathcal{D})=L(\mathcal{N}). $$

Punto orale: quando negli appunti si dice "si dimostra per induzione", l'induzione e' sull'invariante che lo stato-sottoinsieme del DFA coincide con l'insieme degli stati raggiungibili dall'NFA.

2. Vuotezza dei DFA: small model property

Enunciato

Sia $\mathcal{A}=(Q,\Sigma,\delta,q_0,F)$ un DFA con $n=|Q|$ stati. Allora:

$$ L(\mathcal{A})\neq\emptyset \iff \exists w\in L(\mathcal{A})\text{ con }|w|<n. $$

Dimostrazione

Direzione destra-sinistra.

Se esiste $w\in L(\mathcal{A})$ con $|w|<n$, allora esiste almeno una parola accettata. Quindi:

$$ L(\mathcal{A})\neq\emptyset. $$

Direzione sinistra-destra.

Supponiamo:

$$ L(\mathcal{A})\neq\emptyset. $$

Allora esiste almeno una parola accettata. Tra tutte le parole accettate scegliamone una di lunghezza minima e chiamiamola $w$.

Vogliamo dimostrare che $|w|<n$.

Supponiamo per assurdo che:

$$ |w|\ge n. $$

Scriviamo:

$$ w=a_1a_2\ldots a_m $$

con $m=|w|\ge n$. Durante la lettura di $w$, il DFA attraversa la sequenza di stati:

$$ q_0,q_1,q_2,\ldots,q_m $$

dove:

$$ q_i=\hat{\delta}(q_0,a_1\ldots a_i). $$

Questa sequenza contiene $m+1$ stati. Poiche' $m\ge n$, contiene almeno $n+1$ occorrenze di stati, ma l'automa ha solo $n$ stati distinti. Per il principio dei cassetti, esistono indici $i<j$ tali che:

$$ q_i=q_j. $$

Allora la parte di parola:

$$ a_{i+1}\ldots a_j $$

descrive un ciclo: partendo da $q_i$ e leggendo quel blocco si ritorna a $q_i$.

Ora rimuoviamo quel ciclo da $w$ e definiamo:

$$ w'=a_1\ldots a_i a_{j+1}\ldots a_m. $$

Leggendo $w'$, il DFA segue lo stesso percorso di $w$ fino a $q_i$, poi salta il ciclo e continua dal medesimo stato $q_j=q_i$ lungo il suffisso. Quindi termina nello stesso stato finale in cui terminava $w$.

Dunque:

$$ w'\in L(\mathcal{A}). $$

Ma $w'$ e' strettamente piu corta di $w$, perche' abbiamo rimosso un blocco non vuoto. Questo contraddice la scelta di $w$ come parola accettata di lunghezza minima.

Quindi l'assunzione $|w|\ge n$ e' falsa, e deve valere:

$$ |w|<n. $$

Punto orale: non serve citare il pumping lemma in modo vago. Basta scegliere una parola accettata minima e rimuovere un ciclo; la contraddizione e' la minimalita'.

3. Infinitudine dei DFA

Enunciato

Sia $\mathcal{A}$ un DFA con $n$ stati. Allora $L(\mathcal{A})$ e' infinito se e solo se esiste una parola accettata $w$ con lunghezza compresa tra $n$ e $2n$ circa. Una forma standard e':

$$ L(\mathcal{A})\text{ infinito} \iff \exists w\in L(\mathcal{A})\text{ con }n\le |w|<2n. $$

Se gli appunti usano $n<|w|<2n$, e' solo una convenzione di indicizzazione: il ragionamento e' lo stesso.

Dimostrazione

Se esiste una parola accettata lunga almeno $n$, allora il linguaggio e' infinito.

Sia $w=a_1\ldots a_m$ una parola accettata con $m\ge n$.

Durante la lettura di $w$, l'automa attraversa:

$$ q_0,q_1,\ldots,q_m. $$

Ci sono $m+1\ge n+1$ occorrenze di stati e solo $n$ stati disponibili. Quindi esistono $i<j$ con:

$$ q_i=q_j. $$

Scriviamo:

$$ w=xyz $$

dove:

$$ x=a_1\ldots a_i,\qquad y=a_{i+1}\ldots a_j,\qquad z=a_{j+1}\ldots a_m. $$

Il blocco $y$ e' non vuoto e porta da $q_i$ a $q_j=q_i$, quindi e' un ciclo. Per ogni $k\ge 0$, la parola:

$$ xy^kz $$

porta l'automa nello stesso stato finale raggiunto da $w$. Quindi:

$$ xy^kz\in L(\mathcal{A}) \quad\text{per ogni }k\ge 0. $$

Poiche' $|y|>0$, le parole $xy^kz$ sono tutte distinte al variare di $k$. Dunque $L(\mathcal{A})$ contiene infinite parole.

Se il linguaggio e' infinito, esiste una parola accettata con $n\le |w|<2n$.

Se $L(\mathcal{A})$ e' infinito, allora contiene parole accettate di lunghezza arbitrariamente grande. In particolare esiste una parola accettata $w$ con:

$$ |w|\ge n. $$

Tra tutte le parole accettate di lunghezza almeno $n$, scegliamone una di lunghezza minima.

Vogliamo mostrare che:

$$ |w|<2n. $$

Supponiamo per assurdo che:

$$ |w|\ge 2n. $$

Guardiamo i primi $n+1$ stati visitati nella lettura di $w$. Per il principio dei cassetti, tra questi compare un ciclo di lunghezza al massimo $n$. Rimuovendo quel ciclo otteniamo una parola $w'$ ancora accettata.

La lunghezza rimossa e' al piu' $n$, quindi:

$$ |w'|\ge |w|-n\ge 2n-n=n. $$

Ma $w'$ e' accettata, ha lunghezza almeno $n$ ed e' piu corta di $w$. Questo contraddice la scelta di $w$ come parola accettata minima tra quelle di lunghezza almeno $n$.

Quindi:

$$ |w|<2n. $$

Abbiamo trovato una parola accettata con:

$$ n\le |w|<2n. $$

Punto orale: la direzione "infinito implica parola nel range" usa una minimalita' vincolata: minima tra le parole accettate di lunghezza almeno $n$.

4. Teorema di Myhill-Nerode

Enunciato

Sia $L\subseteq\Sigma^\ast$. Definiamo la relazione canonica:

$$ x\equiv_L y \iff \forall z\in\Sigma^\ast,\;xz\in L \iff yz\in L. $$

Il teorema dice che sono equivalenti:

1. $L$ e' regolare.
2. $L$ e' unione di classi di una relazione invariante a destra di indice finito.
3. $\equiv_L$ ha indice finito.

Definizioni tecniche

Una relazione $\sim$ su $\Sigma^\ast$ e' invariante a destra se:

$$ x\sim y\Rightarrow xz\sim yz \quad\text{per ogni }z\in\Sigma^\ast. $$

Ha indice finito se ha un numero finito di classi di equivalenza.

Dire che $L$ e' unione di classi di $\sim$ significa:

$$ x\sim y \Rightarrow (x\in L \iff y\in L). $$

Dimostrazione: $1\Rightarrow 2$

Supponiamo che $L$ sia regolare. Allora esiste un DFA:

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

tale che:

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

Definiamo una relazione $\sim_{\mathcal{A}}$ su $\Sigma^\ast$:

$$ x\sim_{\mathcal{A}}y \iff \hat{\delta}(q_0,x)=\hat{\delta}(q_0,y). $$

Questa e' una relazione di equivalenza:

• riflessiva, perche' ogni parola porta allo stesso stato di se stessa;
• simmetrica, perche' l'uguaglianza degli stati e' simmetrica;
• transitiva, perche' l'uguaglianza degli stati e' transitiva.

Ha indice finito, perche' ogni classe corrisponde a uno stato raggiungibile del DFA, e gli stati sono finiti.

Mostriamo che e' invariante a destra. Supponiamo:

$$ x\sim_{\mathcal{A}}y. $$

Allora:

$$ \hat{\delta}(q_0,x)=\hat{\delta}(q_0,y). $$

Per ogni $z\in\Sigma^\ast$:

$$ \hat{\delta}(q_0,xz) = \hat{\delta}(\hat{\delta}(q_0,x),z) $$

e:

$$ \hat{\delta}(q_0,yz) = \hat{\delta}(\hat{\delta}(q_0,y),z). $$

Poiche' $\hat{\delta}(q_0,x)=\hat{\delta}(q_0,y)$, i due risultati coincidono:

$$ \hat{\delta}(q_0,xz)=\hat{\delta}(q_0,yz). $$

Quindi:

$$ xz\sim_{\mathcal{A}}yz. $$

Infine, $L$ e' unione di classi di $\sim_{\mathcal{A}}$. Infatti, se $x\sim_{\mathcal{A}}y$, allora $x$ e $y$ portano allo stesso stato. Quello stato o e' finale o non e' finale. Quindi:

$$ x\in L \iff \hat{\delta}(q_0,x)\in F \iff \hat{\delta}(q_0,y)\in F \iff y\in L. $$

Quindi $2$ vale.

Dimostrazione: $2\Rightarrow 3$

Supponiamo che esista una relazione $\sim$ invariante a destra, di indice finito, tale che $L$ sia unione di classi di $\sim$.

Vogliamo mostrare che $\equiv_L$ ha indice finito.

Mostriamo prima che:

$$ x\sim y\Rightarrow x\equiv_L y. $$

Sia $x\sim y$. Poiche' $\sim$ e' invariante a destra, per ogni $z$ vale:

$$ xz\sim yz. $$

Poiche' $L$ e' unione di classi di $\sim$, due parole nella stessa classe o appartengono entrambe a $L$ o non appartengono entrambe a $L$. Quindi:

$$ xz\in L\iff yz\in L. $$

Questo vale per ogni $z\in\Sigma^\ast$, quindi:

$$ x\equiv_L y. $$

Abbiamo dimostrato che $\sim$ raffina $\equiv_L$: ogni classe di $\sim$ e' contenuta in una classe di $\equiv_L$. Dunque $\equiv_L$ ha al piu' tante classi quante ne ha $\sim$.

Poiche' $\sim$ ha indice finito, anche $\equiv_L$ ha indice finito.

Dimostrazione: $3\Rightarrow 1$

Supponiamo che $\equiv_L$ abbia indice finito.

Costruiamo un DFA:

$$ \mathcal{A}_L=(Q,\Sigma,\delta,[\varepsilon],F) $$

dove:

$$ Q=\{[x]_{\equiv_L}\mid x\in\Sigma^\ast\} $$

e' l'insieme delle classi di equivalenza di $\equiv_L$.

Lo stato iniziale e':

$$ [\varepsilon]. $$

La transizione e':

$$ \delta([x],a)=[xa]. $$

Gli stati finali sono:

$$ F=\{[x]\mid x\in L\}. $$

Bisogna verificare due cose: che la transizione sia ben definita e che il DFA riconosca davvero $L$.

Ben definizione della transizione.

Se $[x]=[y]$, allora $x\equiv_L y$. Per definizione:

$$ \forall z,\;xz\in L\iff yz\in L. $$

Vogliamo mostrare:

$$ [xa]=[ya]. $$

Prendiamo un suffisso arbitrario $z$. Allora:

$$ (xa)z=x(az) $$

e:

$$ (ya)z=y(az). $$

Poiche' $x\equiv_L y$, applicando la definizione al suffisso $az$ otteniamo:

$$ x(az)\in L\iff y(az)\in L. $$

Quindi:

$$ (xa)z\in L\iff (ya)z\in L. $$

Questo vale per ogni $z$, dunque:

$$ xa\equiv_L ya. $$

La transizione $\delta([x],a)=[xa]$ non dipende dal rappresentante scelto.

Correttezza del DFA.

Mostriamo per induzione su $w$ che:

$$ \hat{\delta}([\varepsilon],w)=[w]. $$

Base:

$$ \hat{\delta}([\varepsilon],\varepsilon)=[\varepsilon]. $$

Passo:

$$ \hat{\delta}([\varepsilon],wa) = \delta(\hat{\delta}([\varepsilon],w),a) = \delta([w],a) = [wa]. $$

Quindi l'invariante vale.

Ora:

$$ w\in L(\mathcal{A}_L) \iff \hat{\delta}([\varepsilon],w)\in F \iff [w]\in F \iff w\in L. $$

Quindi:

$$ L(\mathcal{A}_L)=L. $$

Poiche' $\equiv_L$ ha indice finito, $\mathcal{A}_L$ ha un numero finito di stati. Dunque $L$ e' regolare.

Punto orale: la parte da non saltare e' la ben definizione di $\delta([x],a)=[xa]$. Se il docente chiede "perche' posso scegliere un rappresentante qualunque?", devi usare l'invarianza a destra della relazione canonica.

5. Da automi di Büchi a espressioni omega-regolari, e viceversa

Enunciato

Un linguaggio $L\subseteq A^\omega$ e' riconosciuto da un automa di Büchi non deterministico se e solo se e' esprimibile come unione finita:

$$ L=\bigcup_{i=1}^k U_iV_i^\omega $$

dove $U_i,V_i\subseteq A^\ast$ sono linguaggi regolari di parole finite e, per evitare blocchi vuoti nella ripetizione infinita, si assume $V_i\subseteq A^+$.

Direzione Büchi -> espressione omega-regolare

Sia:

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

un NBA.

Per due stati $p,q\in Q$, definiamo:

$$ W_{p,q}=\{w\in A^\ast\mid p\xrightarrow{w}q\}. $$

Definiamo anche:

$$ C_f=\{w\in A^+\mid f\xrightarrow{w}f\}. $$

Entrambi sono linguaggi regolari. Infatti si riconoscono con un automa finito che usa la stessa struttura di $\mathcal{A}$, prendendo $p$ come iniziale e $q$ come finale. Nel caso di $C_f$ si esclude la parola vuota.

Dimostriamo:

$$ L(\mathcal{A}) = \bigcup_{f\in F} W_{q_0,f}C_f^\omega. $$

Inclusione $\subseteq$.

Sia $\alpha\in L(\mathcal{A})$. Allora esiste una run accettante:

$$ \rho=q_0q_1q_2\ldots $$

su $\alpha$. Poiche' la run e' accettante, visita stati finali infinite volte:

$$ Inf(\rho)\cap F\neq\emptyset. $$

Poiche' $F$ e' finito, almeno uno stato finale $f\in F$ e' visitato infinite volte. Siano:

$$ i_0<i_1<i_2<\ldots $$

le posizioni della run in cui compare $f$, cioe':

$$ q_{i_j}=f. $$

Spezziamo $\alpha$ in:

$$ \alpha=u v_1v_2v_3\ldots $$

dove:

• $u$ e' il blocco letto da $q_0$ fino alla prima visita a $f$;
• $v_j$ e' il blocco letto da $f$ alla visita successiva a $f$.

Allora:

$$ u\in W_{q_0,f} $$

e, per ogni $j$:

$$ v_j\in C_f. $$

Quindi:

$$ \alpha\in W_{q_0,f}C_f^\omega. $$

Poiche' $f\in F$, otteniamo:

$$ \alpha\in\bigcup_{f\in F} W_{q_0,f}C_f^\omega. $$

Inclusione $\supseteq$.

Sia:

$$ \alpha\in W_{q_0,f}C_f^\omega $$

per qualche $f\in F$. Allora:

$$ \alpha=uv_1v_2\ldots $$

con:

$$ u\in W_{q_0,f} $$

e:

$$ v_i\in C_f\quad\text{per ogni }i. $$

Per definizione di $W_{q_0,f}$, esiste una computazione che legge $u$ e porta da $q_0$ a $f$. Per definizione di $C_f$, per ogni $v_i$ esiste una computazione che parte da $f$, legge $v_i$ e torna a $f$.

Concatenando queste computazioni otteniamo una run infinita su $\alpha$ che visita $f$ alla fine di ogni blocco $v_i$. Poiche' ci sono infiniti blocchi, $f$ viene visitato infinite volte.

Dato che $f\in F$, la run e' accettante. Quindi:

$$ \alpha\in L(\mathcal{A}). $$

Abbiamo dimostrato l'uguaglianza.

Direzione espressione omega-regolare -> Büchi

Basta costruire un NBA per ogni linguaggio della forma:

$$ UV^\omega $$

con $U,V$ regolari, e poi usare la chiusura per unione.

Siano:

$$ \mathcal{A}_U $$

un automa finito per $U$ e:

$$ \mathcal{A}_V $$

un automa finito per $V$.

Costruiamo un NBA che:

1. simula $\mathcal{A}_U$ per leggere un prefisso in $U$;
2. quando $\mathcal{A}_U$ raggiunge uno stato finale, entra nella componente che simula $\mathcal{A}_V$;
3. ogni volta che la componente $V$ raggiunge uno stato finale, torna nondeterministicamente all'inizio della componente $V$;
4. rende finale lo stato di ritorno o gli stati finali del componente $V$, in modo che completare un blocco di $V$ venga registrato come visita Büchi.

Correttezza.

Se una parola e' in $UV^\omega$, allora ha forma:

$$ \alpha=uv_1v_2\ldots $$

con $u\in U$ e $v_i\in V$. L'automa legge $u$ usando $\mathcal{A}_U$, poi legge ciascun $v_i$ usando $\mathcal{A}_V$ e ritorna all'inizio della componente $V$ infinite volte. Quindi visita stati finali infinite volte e accetta.

Viceversa, se l'automa accetta, allora deve visitare infinite volte la zona finale della componente $V$. Ogni visita corrisponde al completamento di un blocco letto da $\mathcal{A}_V$ e appartenente a $V$. Prima di entrare nella componente $V$ deve aver completato un prefisso appartenente a $U$. Quindi la parola accettata ha forma:

$$ uv_1v_2\ldots $$

con $u\in U$ e $v_i\in V$. Dunque appartiene a $UV^\omega$.

Per una unione finita $\bigcup_i U_iV_i^\omega$, si costruisce un NBA che all'inizio sceglie nondeterministicamente quale componente simulare. Quindi ogni espressione omega-regolare e' riconosciuta da un NBA.

Punto orale: nella direzione Büchi -> espressione, non basta dire "c'e' un ciclo". Devi scegliere uno stato finale $f$ visitato infinite volte e spezzare la run tra visite successive a quello stesso $f$.

6. Intersezione di automi di Büchi e GNBA

Enunciato

Se $L_1$ e $L_2$ sono omega-regolari, allora:

$$ L_1\cap L_2 $$

e' omega-regolare.

Perche' il prodotto semplice non basta

Per parole finite, il prodotto con finali $F_1\times F_2$ funziona. Per Büchi no, perche' le due run potrebbero visitare i rispettivi finali infinite volte in istanti diversi.

Esempio concettuale:

• il primo automa visita un finale ai tempi pari;
• il secondo automa visita un finale ai tempi dispari.

Entrambi accettano, ma il prodotto potrebbe non visitare mai $F_1\times F_2$.

Serve quindi una condizione che dica:

1. visita infinite volte finali della prima componente;
2. visita infinite volte finali della seconda componente.

Questa e' esattamente una condizione di Büchi generalizzata.

Costruzione come GNBA

Siano:

$$ \mathcal{A}_1=(Q_1,A,\Delta_1,q_1^0,F_1) $$

e:

$$ \mathcal{A}_2=(Q_2,A,\Delta_2,q_2^0,F_2). $$

Costruiamo il prodotto:

$$ \mathcal{G}=(Q_1\times Q_2,A,\Delta,(q_1^0,q_2^0),\mathcal{F}) $$

dove:

$$ ((p_1,p_2),a,(r_1,r_2))\in\Delta $$

se e solo se:

$$ (p_1,a,r_1)\in\Delta_1 \quad\text{e}\quad (p_2,a,r_2)\in\Delta_2. $$

La famiglia di accettazione e':

$$ \mathcal{F}=\{F_1\times Q_2,\; Q_1\times F_2\}. $$

Una run del GNBA e' accettante se visita infinite volte almeno uno stato di ciascun insieme della famiglia $\mathcal{F}$.

Correttezza del prodotto

Sia $\alpha\in A^\omega$.

Se $\alpha\in L(\mathcal{A}_1)\cap L(\mathcal{A}_2)$, allora esistono:

• una run accettante $\rho_1$ di $\mathcal{A}_1$ su $\alpha$;
• una run accettante $\rho_2$ di $\mathcal{A}_2$ su $\alpha$.

La run prodotto:

$$ \rho=(\rho_1(0),\rho_2(0))(\rho_1(1),\rho_2(1))\ldots $$

e' valida per costruzione delle transizioni. Poiche' $\rho_1$ visita $F_1$ infinite volte, $\rho$ visita $F_1\times Q_2$ infinite volte. Poiche' $\rho_2$ visita $F_2$ infinite volte, $\rho$ visita $Q_1\times F_2$ infinite volte. Quindi $\rho$ e' accettante per il GNBA.

Se $\alpha$ e' accettata dal GNBA, esiste una run prodotto accettante:

$$ \rho=(p_0,r_0)(p_1,r_1)\ldots $$

Proiettando sulla prima componente otteniamo una run valida di $\mathcal{A}_1$; proiettando sulla seconda otteniamo una run valida di $\mathcal{A}_2$.

Poiche' $\rho$ visita $F_1\times Q_2$ infinite volte, la prima proiezione visita $F_1$ infinite volte. Poiche' $\rho$ visita $Q_1\times F_2$ infinite volte, la seconda proiezione visita $F_2$ infinite volte. Quindi entrambe le run proiettate sono accettanti.

Dunque:

$$ \alpha\in L(\mathcal{A}_1)\cap L(\mathcal{A}_2). $$

Conversione GNBA -> NBA

Sia un GNBA con famiglia:

$$ \mathcal{F}=\{F_1,\ldots,F_k\}. $$

Costruiamo un NBA con stati:

$$ Q'=Q\times\{1,\ldots,k\}. $$

L'indice $i$ significa: "sto aspettando di visitare $F_i$".

La transizione simula quella originale e aggiorna l'indice:

• se lo stato raggiunto appartiene a $F_i$, passo all'indice successivo $i+1$;
• se $i=k$ e visito $F_k$, torno a $1$;
• altrimenti resto nello stesso indice.

Gli stati finali del nuovo NBA possono essere, per esempio:

$$ F'=Q\times\{1\} $$

raggiunti dopo aver completato un ciclo di obblighi.

Correttezza.

Se una run del GNBA visita ogni $F_i$ infinite volte, allora il contatore riesce a completare il ciclo:

$$ F_1,F_2,\ldots,F_k $$

infinite volte. Quindi il nuovo NBA torna infinite volte all'indice $1$ e accetta.

Viceversa, se il nuovo NBA accetta, allora visita infinite volte l'indice $1$. Per tornare infinite volte a $1$, deve aver attraversato infinite volte tutti gli obblighi $F_1,\ldots,F_k$. Quindi la run originale visita ogni $F_i$ infinite volte ed e' accettante per il GNBA.

Punto orale: per l'intersezione non devi imporre finali simultanei. Devi imporre due obblighi Büchi separati e poi convertirli in un solo obbligo usando un contatore.

7. Emptiness degli automi di Büchi

Enunciato

Sia:

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

un NBA. Allora:

$$ L(\mathcal{A})\neq\emptyset $$

se e solo se esiste una componente fortemente connessa raggiungibile da $q_0$ che contiene almeno uno stato finale ed e' attraversabile infinitamente.

Equivalente: esiste uno stato finale $f\in F$ raggiungibile da $q_0$ e da cui e' possibile tornare a $f$ leggendo una parola non vuota.

Dimostrazione

Se il linguaggio e' non vuoto, esiste una SCC finale raggiungibile.

Supponiamo:

$$ L(\mathcal{A})\neq\emptyset. $$

Allora esiste una parola $\alpha$ accettata e una run accettante:

$$ \rho=q_0q_1q_2\ldots $$

Poiche' la run e' accettante:

$$ Inf(\rho)\cap F\neq\emptyset. $$

Scegliamo uno stato finale:

$$ f\in Inf(\rho)\cap F. $$

Lo stato $f$ compare infinite volte nella run. In particolare:

• $f$ e' raggiungibile da $q_0$, perche' appare lungo la run;
• dopo una visita a $f$, la run torna di nuovo a $f$ piu avanti.

Quindi esiste un cammino non vuoto da $f$ a $f$. Gli stati che compaiono infinite volte nella run formano, o contengono, una componente fortemente connessa raggiungibile contenente $f$.

Se esiste una SCC finale raggiungibile, il linguaggio e' non vuoto.

Supponiamo che esista uno stato finale $f$ raggiungibile da $q_0$ e con un ciclo non vuoto da $f$ a $f$.

Sia:

$$ u\in A^\ast $$

una parola che porta da $q_0$ a $f$, e sia:

$$ v\in A^+ $$

una parola che porta da $f$ a $f$.

Allora la parola infinita:

$$ \alpha=uv^\omega $$

ammette una run che:

1. legge $u$ e arriva in $f$;
2. legge $v$ e torna in $f$;
3. ripete il ciclo $v$ infinite volte.

Questa run visita $f$ infinite volte. Poiche' $f\in F$, la run e' accettante. Dunque:

$$ \alpha\in L(\mathcal{A}) $$

e quindi:

$$ L(\mathcal{A})\neq\emptyset. $$

Punto orale: l'emptiness Büchi non cerca solo un finale raggiungibile. Cerca un finale raggiungibile che stia su un ciclo, perche' l'accettazione deve avvenire infinite volte.

8. Complementazione Büchi tramite congruenza e saturazione

Questa e' la dimostrazione piu tecnica degli appunti sui "buchi". Serve a giustificare il fatto che gli omega-regolari sono chiusi per complemento, ma senza fingere che basti invertire gli stati finali.

Definizioni

Sia:

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

un NBA.

Per $u\in A^\ast$ e $p,q\in Q$ scriviamo:

$$ p\xrightarrow{u}q $$

se esiste una computazione finita che parte da $p$, legge $u$ e arriva in $q$.

Scriviamo:

$$ p\xrightarrow[F]{u} q $$

se esiste una computazione finita da $p$ a $q$ su $u$ che visita almeno uno stato finale durante il segmento. Contiamo anche gli estremi del segmento, cosi' una visita finale al bordo tra due blocchi non viene persa.

Definiamo la relazione $\approx_{\mathcal{A}}$ su $A^\ast$:

$$ u\approx_{\mathcal{A}}v $$

se per ogni $p,q\in Q$ valgono entrambe:

$$ p\xrightarrow{u}q \iff p\xrightarrow{v}q $$

e:

$$ p\xrightarrow[F]{u} q \iff p\xrightarrow[F]{v} q. $$

Quindi due parole finite sono equivalenti se producono gli stessi collegamenti tra stati e gli stessi collegamenti che attraversano almeno un finale.

Lemma 1: $\approx_{\mathcal{A}}$ ha indice finito

Per ogni parola $u$, la sua informazione rilevante e' una coppia di relazioni su $Q$:

$$ (R_u,R_u^F) $$

dove:

$$ R_u=\{(p,q)\mid p\xrightarrow{u}q\} $$

e:

$$ R_u^F=\{(p,q)\mid p\xrightarrow[F]{u} q\}. $$

Poiche' $Q$ e' finito, $Q\times Q$ e' finito. Le possibili relazioni su $Q\times Q$ sono finite:

$$ 2^{|Q|^2}. $$

Le possibili coppie $(R_u,R_u^F)$ sono quindi al piu':

$$ 2^{|Q|^2}\cdot 2^{|Q|^2}. $$

Quindi $\approx_{\mathcal{A}}$ ha un numero finito di classi.

Lemma 2: $\approx_{\mathcal{A}}$ e' una congruenza

Vogliamo mostrare:

$$ u\approx u' \quad\text{e}\quad v\approx v' \Rightarrow uv\approx u'v'. $$

Fissiamo $p,r\in Q$.

Per i collegamenti senza vincolo finale:

$$ p\xrightarrow{uv}r $$

se e solo se esiste uno stato intermedio $s$ tale che:

$$ p\xrightarrow{u}s \quad\text{e}\quad s\xrightarrow{v}r. $$

Poiche' $u\approx u'$ e $v\approx v'$, questo equivale a:

$$ p\xrightarrow{u'}s \quad\text{e}\quad s\xrightarrow{v'}r $$

per qualche $s$, cioe':

$$ p\xrightarrow{u'v'}r. $$

Ora consideriamo i collegamenti che visitano un finale:

$$ p\xrightarrow[F]{uv} r. $$

Questo accade se e solo se esiste uno stato intermedio $s$ tale che almeno una delle due parti visita un finale:

$$ (p\xrightarrow[F]{u} s \land s\xrightarrow{v}r) \quad\text{oppure}\quad (p\xrightarrow{u}s \land s\xrightarrow[F]{v} r). $$

Usando $u\approx u'$ e $v\approx v'$, la condizione e' equivalente a:

$$ (p\xrightarrow[F]{u'} s \land s\xrightarrow{v'}r) \quad\text{oppure}\quad (p\xrightarrow{u'}s \land s\xrightarrow[F]{v'} r). $$

Questo equivale a:

$$ p\xrightarrow[F]{u'v'} r. $$

Abbiamo mostrato sia l'equivalenza dei collegamenti semplici sia quella dei collegamenti con visita finale. Quindi:

$$ uv\approx_{\mathcal{A}}u'v'. $$

La relazione e' una congruenza.

Lemma 3: $\approx_{\mathcal{A}}$ satura $L(\mathcal{A})$

Dire che una congruenza $\sim$ satura un linguaggio $L\subseteq A^\omega$ significa:

$$ U V^\omega\cap L\neq\emptyset \Rightarrow U V^\omega\subseteq L $$

per ogni coppia di classi $U,V$ di $\sim$.

Dimostriamolo per $\approx_{\mathcal{A}}$ e $L(\mathcal{A})$.

Supponiamo:

$$ U V^\omega\cap L(\mathcal{A})\neq\emptyset. $$

Allora esiste:

$$ \alpha=uv_1v_2v_3\ldots $$

con:

$$ u\in U,\qquad v_i\in V $$

e:

$$ \alpha\in L(\mathcal{A}). $$

Poiche' $\alpha$ e' accettata, esiste una run accettante. Guardiamo gli stati ai bordi dei blocchi:

$$ q_0=s_0\xrightarrow{u}s_1\xrightarrow{v_1}s_2\xrightarrow{v_2}s_3\xrightarrow{v_3}\ldots $$

La run visita stati finali infinite volte. Poiche' abbiamo contato anche gli estremi dei segmenti, questo implica che per infiniti indici $i$ vale:

$$ s_i\xrightarrow[F]{v_i} s_{i+1}. $$

Ora prendiamo una parola arbitraria:

$$ \beta=u'v_1'v_2'v_3'\ldots $$

con:

$$ u'\in U,\qquad v_i'\in V. $$

Poiche' $u,u'$ sono nella stessa classe:

$$ u\approx_{\mathcal{A}}u'. $$

Quindi, da $q_0\xrightarrow{u}s_1$, otteniamo:

$$ q_0\xrightarrow{u'}s_1. $$

Poiche' $v_i,v_i'$ sono nella stessa classe per ogni $i$:

$$ v_i\approx_{\mathcal{A}}v_i'. $$

Quindi, da:

$$ s_i\xrightarrow{v_i}s_{i+1}, $$

otteniamo:

$$ s_i\xrightarrow{v_i'}s_{i+1}. $$

Inoltre, per gli infiniti indici $i$ in cui:

$$ s_i\xrightarrow[F]{v_i} s_{i+1}, $$

otteniamo:

$$ s_i\xrightarrow[F]{v_i'} s_{i+1}. $$

Dunque possiamo costruire su $\beta$ una run che segue la stessa sequenza di stati-bordo:

$$ q_0=s_0\xrightarrow{u'}s_1\xrightarrow{v_1'}s_2\xrightarrow{v_2'}s_3\ldots $$

e che visita stati finali in infiniti segmenti. Quindi visita stati finali infinite volte.

La run e' accettante, dunque:

$$ \beta\in L(\mathcal{A}). $$

Poiche' $\beta$ era arbitraria in $UV^\omega$:

$$ UV^\omega\subseteq L(\mathcal{A}). $$

Quindi $\approx_{\mathcal{A}}$ satura $L(\mathcal{A})$.

Lemma 4: se una congruenza finita satura $L$, allora satura anche il complemento

Sia $\sim$ una congruenza che satura $L$. Vogliamo mostrare che satura anche:

$$ \overline{L}=A^\omega\setminus L. $$

Prendiamo classi $U,V$ e supponiamo:

$$ UV^\omega\cap\overline{L}\neq\emptyset. $$

Vogliamo dimostrare:

$$ UV^\omega\subseteq\overline{L}. $$

Supponiamo per assurdo che non sia cosi'. Allora esiste una parola in $UV^\omega$ che appartiene a $L$, cioe':

$$ UV^\omega\cap L\neq\emptyset. $$

Poiche' $\sim$ satura $L$, segue:

$$ UV^\omega\subseteq L. $$

Ma questo contraddice:

$$ UV^\omega\cap\overline{L}\neq\emptyset. $$

Quindi l'assurdo e' falso, e:

$$ UV^\omega\subseteq\overline{L}. $$

La congruenza satura il complemento.

Lemma 5: da saturazione finita a omega-regolarita'

Se una congruenza finita $\sim$ satura $L$, allora $L$ e' unione finita di linguaggi della forma:

$$ UV^\omega $$

dove $U,V$ sono classi di $\sim$.

Dimostriamo i passaggi.

Passo 1: decomposizione di una parola infinita.

Sia:

$$ \alpha=a_0a_1a_2\ldots\in A^\omega. $$

Poiche' $\sim$ ha indice finito, ci sono solo finitamente molte classi. Coloriamo ogni coppia di indici $i<j$ con la classe del fattore finito:

$$ \alpha(i,j)=a_i a_{i+1}\ldots a_{j-1}. $$

Per il teorema infinito di Ramsey, esiste una sequenza infinita di indici:

$$ i_0<i_1<i_2<\ldots $$

tale che tutti i fattori:

$$ \alpha(i_r,i_s) \quad\text{con }r<s $$

appartengono alla stessa classe $V$.

Sia $U$ la classe del prefisso:

$$ \alpha(0,i_0). $$

Allora:

$$ \alpha = u v_0v_1v_2\ldots $$

dove:

$$ u=\alpha(0,i_0)\in U $$

e:

$$ v_r=\alpha(i_r,i_{r+1})\in V. $$

Quindi:

$$ \alpha\in U V^\omega. $$

Inoltre vale:

$$ V\cdot V\subseteq V. $$

Infatti, presi $x,y\in V$, abbiamo:

$$ x\sim v_0 \quad\text{e}\quad y\sim v_1. $$

Poiche' $\sim$ e' una congruenza:

$$ xy\sim v_0v_1. $$

Ma:

$$ v_0v_1=\alpha(i_0,i_2) $$

e, per la scelta degli indici di Ramsey, anche $\alpha(i_0,i_2)$ appartiene alla classe $V$. Quindi:

$$ xy\in V. $$

Passo 2: rappresentazione di $L$ come unione di classi omega.

Consideriamo tutte le coppie di classi $(U,V)$ tali che:

$$ UV^\omega\cap L\neq\emptyset. $$

Poiche' il numero di classi e' finito, il numero di coppie $(U,V)$ e' finito.

Definiamo:

$$ R=\bigcup_{\substack{U,V\text{ classi}\\UV^\omega\cap L\neq\emptyset}} UV^\omega. $$

Mostriamo che:

$$ L=R. $$

Prima, $R\subseteq L$. Se $UV^\omega$ compare nell'unione, allora:

$$ UV^\omega\cap L\neq\emptyset. $$

Poiche' $\sim$ satura $L$, segue:

$$ UV^\omega\subseteq L. $$

Quindi ogni pezzo dell'unione e' contenuto in $L$, e dunque:

$$ R\subseteq L. $$

Ora, $L\subseteq R$. Sia $\alpha\in L$. Per il Passo 1, esistono classi $U,V$ tali che:

$$ \alpha\in UV^\omega. $$

Poiche' $\alpha\in L$, abbiamo:

$$ UV^\omega\cap L\neq\emptyset. $$

Quindi quella coppia $(U,V)$ compare nell'unione che definisce $R$, e:

$$ \alpha\in R. $$

Abbiamo dimostrato:

$$ L=R. $$

Passo 3: ogni classe e' regolare.

Sia $C$ una classe di $\sim$. Costruiamo un DFA che riconosce $C$:

• stati: le classi di $\sim$;
• stato iniziale: $[\varepsilon]$;
• transizione: $[x]\xrightarrow{a}[xa]$;
• unico stato finale: $C$.

La transizione e' ben definita perche' $\sim$ e' una congruenza. Per induzione su $w$:

$$ \hat{\delta}([\varepsilon],w)=[w]. $$

Quindi il DFA accetta esattamente le parole $w$ tali che $[w]=C$, cioe' esattamente la classe $C$. Dunque ogni classe e' un linguaggio regolare di parole finite.

Passo 4: omega-regolarita'.

Ogni $U$ e $V$ e' regolare. Quindi ogni linguaggio:

$$ UV^\omega $$

e' omega-regolare. Poiche' $L$ e' unione finita di questi linguaggi, $L$ e' omega-regolare.

Conclusione: chiusura per complemento

Sia $L$ omega-regolare. Allora esiste un NBA $\mathcal{A}$ con:

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

Abbiamo mostrato che $\approx_{\mathcal{A}}$:

1. ha indice finito;
2. e' una congruenza;
3. satura $L$.

Per il Lemma 4, satura anche $\overline{L}$. Per il Lemma 5, $\overline{L}$ e' omega-regolare.

Quindi:

$$ L\text{ omega-regolare} \Rightarrow \overline{L}\text{ omega-regolare}. $$

Punto orale: il complemento Büchi esiste, ma non si ottiene scambiando finali e non finali. La dimostrazione passa da congruenze finite e saturazione.

9. Caratterizzazione dei DBA e non-chiusura per complemento

Enunciato di caratterizzazione

Un linguaggio $L\subseteq A^\omega$ e' riconosciuto da un automa di Büchi deterministico se e solo se:

$$ L=\overrightarrow{W} $$

per qualche linguaggio regolare $W\subseteq A^\ast$, dove:

$$ \overrightarrow{W} = \{\alpha\in A^\omega\mid \exists^\omega n,\; \alpha(0,n)\in W\}. $$

In parole: una parola infinita e' accettata se ha infiniti prefissi appartenenti a $W$.

Direzione DBA -> $\overrightarrow{W}$

Sia:

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

un DBA.

Definiamo:

$$ W=\{w\in A^\ast\mid \hat{\delta}(q_0,w)\in F\}. $$

$W$ e' regolare, perche' e' riconosciuto dal DFA che ha la stessa struttura di $\mathcal{A}$ e gli stessi stati finali.

Ora prendiamo $\alpha\in A^\omega$. La run di un DBA su $\alpha$ e' unica. La parola $\alpha$ e' accettata se e solo se la run visita $F$ infinite volte.

Visitare $F$ dopo aver letto il prefisso $\alpha(0,n)$ significa:

$$ \alpha(0,n)\in W. $$

Quindi:

$$ \alpha\in L(\mathcal{A}) \iff \exists^\omega n,\;\alpha(0,n)\in W \iff \alpha\in\overrightarrow{W}. $$

Dunque:

$$ L(\mathcal{A})=\overrightarrow{W}. $$

Direzione $\overrightarrow{W}$ -> DBA

Supponiamo $W\subseteq A^\ast$ regolare. Esiste un DFA:

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

che riconosce $W$.

Consideriamo lo stesso automa come DBA:

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

Per ogni $\alpha\in A^\omega$, la run del DBA visita $F$ infinite volte se e solo se esistono infiniti prefissi $\alpha(0,n)$ che portano il DFA in $F$, cioe' infiniti prefissi in $W$.

Quindi:

$$ L(\mathcal{A})=\overrightarrow{W}. $$

La caratterizzazione e' dimostrata.

Linguaggio con finitemente molte $a$: riconoscibile da NBA ma non da DBA

Sia:

$$ L_{fin}=\{\alpha\in\{a,b\}^\omega\mid \alpha\text{ contiene solo un numero finito di }a\}. $$

In italiano: le parole infinite con solo un numero finito di occorrenze di $a$.

Questo linguaggio e' riconoscibile da un NBA: l'automa legge liberamente, poi nondeterministicamente indovina il punto dopo l'ultima $a$ e passa in uno stato finale che permette solo $b$.

Dimostriamo che non e' riconoscibile da un DBA.

Supponiamo per assurdo che $L_{fin}$ sia riconoscibile da un DBA. Per la caratterizzazione, esiste un linguaggio regolare $W\subseteq\{a,b\}^\ast$ tale che:

$$ L_{fin}=\overrightarrow{W}. $$

Costruiamo ora una parola con infinite $a$ che pero' ha infiniti prefissi in $W$, ottenendo una contraddizione.

Partiamo da:

$$ b^\omega. $$

Questa parola ha zero occorrenze di $a$, quindi appartiene a $L_{fin}$. Poiche':

$$ L_{fin}=\overrightarrow{W}, $$

deve avere infiniti prefissi in $W$. Quindi esiste $m_0$ tale che:

$$ b^{m_0}\in W. $$

Ora consideriamo:

$$ b^{m_0}ab^\omega. $$

Questa parola ha una sola $a$, quindi appartiene a $L_{fin}$. Dunque ha infiniti prefissi in $W$. In particolare, possiamo scegliere $m_1$ tale che:

$$ b^{m_0}ab^{m_1}\in W. $$

Poi consideriamo:

$$ b^{m_0}ab^{m_1}ab^\omega. $$

Questa parola ha due $a$, quindi appartiene ancora a $L_{fin}$. Quindi ha infiniti prefissi in $W$, e scegliamo $m_2$ tale che:

$$ b^{m_0}ab^{m_1}ab^{m_2}\in W. $$

Continuando cosi', costruiamo una parola infinita:

$$ \beta=b^{m_0}ab^{m_1}ab^{m_2}a\ldots $$

Questa parola contiene infinite occorrenze di $a$, quindi:

$$ \beta\notin L_{fin}. $$

Pero' per costruzione ha infiniti prefissi in $W$:

$$ b^{m_0},\quad b^{m_0}ab^{m_1},\quad b^{m_0}ab^{m_1}ab^{m_2},\ldots $$

Quindi:

$$ \beta\in\overrightarrow{W}. $$

Poiche' $\overrightarrow{W}=L_{fin}$, otteniamo:

$$ \beta\in L_{fin} $$

contraddizione.

Dunque $L_{fin}$ non e' riconoscibile da alcun DBA.

Non-chiusura dei DBA per complemento

Il complemento di $L_{fin}$ e':

$$ L_{\infty a} = \{\alpha\mid \alpha\text{ contiene infinite occorrenze di }a\}. $$

Questo linguaggio e' riconoscibile da un DBA: basta avere uno stato finale visitato ogni volta che si legge $a$.

Se i DBA fossero chiusi per complemento, allora dal DBA per $L_{\infty a}$ otterremmo un DBA per il complemento, cioe' per $L_{fin}$. Ma abbiamo appena dimostrato che $L_{fin}$ non e' riconoscibile da DBA.

Quindi i DBA non sono chiusi per complemento.

Punto orale: il non determinismo serve a "indovinare" l'ultima $a$. Un DBA non puo' farlo perche' ha una sola computazione.

10. Secondo teorema di Büchi: direzione automa -> S1S

Enunciato della direzione

Se $L\subseteq A^\omega$ e' omega-regolare, allora $L$ e' definibile in S1S.

Poiche' $L$ e' omega-regolare, esiste un NBA:

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

tale che:

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

Vogliamo costruire una formula S1S vera esattamente sulle parole accettate da $\mathcal{A}$.

Codifica della parola

Una parola $\alpha\in A^\omega$ viene vista come struttura:

$$ \underline{\alpha}=(\mathbb{N},0,+1,<,\{Q_a\}_{a\in A}) $$

dove:

$$ Q_a(x) $$

significa: "in posizione $x$ della parola compare il simbolo $a$".

Assumiamo che la parola sia ben formata: in ogni posizione vale esattamente un predicato $Q_a$.

Codifica della run

Sia:

$$ Q=\{q_0,q_1,\ldots,q_m\}. $$

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

Interpretazione:

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

La formula avra' forma:

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

L'esistenziale sugli insiemi $Y_i$ rappresenta il non determinismo: stiamo dicendo che esiste una run accettante.

Vincolo 1: stato iniziale

Alla posizione $0$, la run e' nello stato iniziale $q_0$:

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

Vincolo 2: esattamente uno stato a ogni posizione

Almeno uno stato:

$$ \Phi_{atleast}\equiv \forall x\bigvee_{i=0}^m x\in Y_i. $$

Al piu' uno stato:

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

Mettiamo:

$$ \Phi_{state}\equiv \Phi_{atleast}\land\Phi_{atmost}. $$

Questo evita il passaggio spesso saltato negli appunti: gli insiemi $Y_i$ devono formare una partizione delle posizioni.

Vincolo 3: rispetto delle transizioni

Per ogni posizione $x$, la tripla:

• stato corrente;
• simbolo letto;
• stato successivo;

deve essere una transizione dell'automa.

Formula:

$$ \Phi_{trans}\equiv \forall x \bigvee_{(q_i,a,q_j)\in\Delta} \bigl(x\in Y_i\land Q_a(x)\land x+1\in Y_j\bigr). $$

Questa formula dice: per ogni passo, esiste una transizione compatibile con lo stato corrente e il simbolo corrente.

Grazie a $\Phi_{state}$ e alla ben formazione della parola, non possono esserci due stati correnti o due simboli correnti diversi. Quindi la disgiunzione non introduce ambiguita' semantica: sceglie una transizione valida tra quelle disponibili.

Vincolo 4: condizione di Büchi

Almeno uno stato finale deve essere visitato infinite volte:

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

La sottoformula:

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

significa che per ogni posizione $x$ esiste una posizione futura $y$ in cui la run e' in $q_i$. Quindi $q_i$ compare infinite volte.

Formula completa

Definiamo:

$$ \Phi_{\mathcal{A}}\equiv \exists Y_0\ldots\exists Y_m (\Phi_{init}\land\Phi_{state}\land\Phi_{trans}\land\Phi_{acc}). $$

Correttezza: se l'automa accetta, la formula e' vera

Supponiamo:

$$ \alpha\in L(\mathcal{A}). $$

Allora esiste una run accettante:

$$ \rho=r_0r_1r_2\ldots $$

su $\alpha$.

Definiamo:

$$ Y_i=\{x\in\mathbb{N}\mid r_x=q_i\}. $$

Con questa interpretazione:

• $\Phi_{init}$ e' vera perche' $r_0=q_0$;
• $\Phi_{state}$ e' vera perche' in ogni posizione la run ha uno e un solo stato;
• $\Phi_{trans}$ e' vera perche' $\rho$ e' una run valida;
• $\Phi_{acc}$ e' vera perche' la run visita almeno uno stato finale infinite volte.

Quindi:

$$ \underline{\alpha}\models \Phi_{\mathcal{A}}. $$

Correttezza: se la formula e' vera, l'automa accetta

Supponiamo:

$$ \underline{\alpha}\models \Phi_{\mathcal{A}}. $$

Allora esistono insiemi $Y_0,\ldots,Y_m$ che soddisfano tutti i vincoli.

Da $\Phi_{state}$, per ogni posizione $x$ esiste un unico indice $i$ tale che:

$$ x\in Y_i. $$

Definiamo la sequenza di stati:

$$ r_x=q_i \quad\text{se e solo se}\quad x\in Y_i. $$

Da $\Phi_{init}$:

$$ r_0=q_0. $$

Da $\Phi_{trans}$, per ogni $x$, se $\alpha(x)=a$ e $r_x=q_i$, allora esiste $q_j$ tale che:

$$ (q_i,a,q_j)\in\Delta $$

e:

$$ r_{x+1}=q_j. $$

Quindi:

$$ r_0r_1r_2\ldots $$

e' una run valida di $\mathcal{A}$ su $\alpha$.

Da $\Phi_{acc}$, esiste uno stato finale $q_i\in F$ tale che:

$$ \forall x\exists y(x<y\land y\in Y_i). $$

Quindi $q_i$ compare infinite volte nella run. La run e' accettante.

Dunque:

$$ \alpha\in L(\mathcal{A}). $$

Abbiamo dimostrato:

$$ \alpha\in L(\mathcal{A}) \iff \underline{\alpha}\models\Phi_{\mathcal{A}}. $$

Quindi $L$ e' definibile in S1S.

Punto orale: ricordati "almeno uno stato" e "al piu' uno stato". Negli appunti spesso compare solo il divieto di stare in due stati, ma formalmente serve anche dire che la run sta sempre in qualche stato.

11. Secondo teorema di Büchi: direzione S1S -> automa

Enunciato della direzione

Se $L\subseteq A^\omega$ e' definibile da una formula S1S, allora $L$ e' omega-regolare.

In pratica: data una formula S1S $\varphi$, vogliamo costruire un NBA che riconosce esattamente i modelli di $\varphi$.

Strategia formale

La dimostrazione si fa per induzione sulla struttura della formula, dopo aver ridotto S1S a una forma in cui le variabili del primo ordine sono codificate come insiemi singleton.

Una parola letta dall'automa non contiene solo il simbolo originale dell'alfabeto, ma anche la valutazione delle variabili libere della formula. Se le variabili libere sono $X_1,\ldots,X_k$, l'automa legge lettere che indicano, per ogni posizione, quali $X_i$ contengono quella posizione.

Formule atomiche

Per le formule atomiche si costruiscono automi finiti, quindi anche automi di Büchi.

Esempio:

$$ X\subseteq Y. $$

Questa formula significa:

$$ \forall x(x\in X\to x\in Y). $$

L'automa scorre la parola e controlla che non esista una posizione in cui il bit di $X$ vale $1$ e il bit di $Y$ vale $0$. Se trova una violazione va in uno stato morto non finale. Se non trova violazioni, resta in uno stato finale visitato a ogni passo.

Esempio:

$$ Succ(X,Y) $$

nella versione ridotta $S1S_0$ significa: $X$ e $Y$ sono singleton e l'unico elemento di $Y$ e' il successore dell'unico elemento di $X$. Un automa finito puo' verificarlo con memoria finita:

1. non ho ancora visto $X$;
2. ho appena visto l'unica posizione di $X$;
3. controllo che nella posizione successiva ci sia l'unica posizione di $Y$;
4. da quel punto in poi non devo vedere altri $X$ o altri $Y$.

Se una delle condizioni fallisce, va in uno stato morto non finale.

Connettivi booleani

Supponiamo di avere automi per $\varphi$ e $\psi$.

Disgiunzione.

Per:

$$ \varphi\lor\psi $$

costruisco l'unione degli automi. Il nondeterminismo sceglie se verificare $\varphi$ o $\psi$.

Congiunzione.

Per:

$$ \varphi\land\psi $$

costruisco l'intersezione degli automi. Serve il prodotto Büchi/GNBA visto sopra, perche' entrambe le condizioni di accettazione devono essere soddisfatte infinite volte.

Negazione.

Per:

$$ \neg\varphi $$

uso la chiusura degli omega-regolari per complemento. Se l'automa per $\varphi$ riconosce $L(\varphi)$, allora l'automa per $\neg\varphi$ riconosce:

$$ A^\omega\setminus L(\varphi). $$

Qui entra la dimostrazione tecnica della complementazione Büchi.

Quantificatore esistenziale come proiezione

Supponiamo di avere:

$$ \exists X\;\varphi(X,Y_1,\ldots,Y_k). $$

Per ipotesi induttiva esiste un automa $\mathcal{A}_\varphi$ che riconosce le parole annotate con le valutazioni di:

$$ X,Y_1,\ldots,Y_k $$

che soddisfano $\varphi$.

Vogliamo un automa che legga solo:

$$ Y_1,\ldots,Y_k $$

e accetti se esiste una scelta di $X$ che renderebbe vera $\varphi$.

Costruzione: il nuovo automa simula $\mathcal{A}_\varphi$, ma a ogni posizione indovina nondeterministicamente se quella posizione appartiene a $X$ oppure no. In altre parole, proietta via la componente $X$ dell'alfabeto.

Correttezza.

Se una parola sulle variabili $Y_1,\ldots,Y_k$ soddisfa $\exists X\varphi$, allora esiste una interpretazione di $X$ tale che la parola estesa soddisfa $\varphi$. L'automa puo' indovinare esattamente quella interpretazione di $X$ e quindi accetta.

Viceversa, se l'automa proiettato accetta, allora durante una run accettante ha scelto nondeterministicamente un valore per il bit $X$ in ogni posizione. Queste scelte definiscono un insieme $X$. Poiche' la simulazione di $\mathcal{A}_\varphi$ accetta, la formula $\varphi(X,Y_1,\ldots,Y_k)$ e' vera per quell'insieme $X$. Quindi:

$$ \exists X\;\varphi $$

e' vera.

Quantificatore universale

Il quantificatore universale si elimina usando:

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

Poiche' abbiamo gia' costruzioni per negazione ed esistenziale, abbiamo anche la costruzione per il quantificatore universale.

Variabili del primo ordine

Una variabile del primo ordine $x$ viene codificata come una variabile monadica $X$ vincolata a essere un singleton:

$$ Sing(X). $$

Allora:

• $x=y$ diventa $X=Y$ con $Sing(X)$ e $Sing(Y)$;
• $x+1=y$ diventa $Succ(X,Y)$;
• $\exists x\;\theta(x)$ diventa $\exists X(Sing(X)\land\theta(X))$;
• $\forall x\;\theta(x)$ diventa $\forall X(Sing(X)\to\theta(X))$.

Quindi tutto S1S puo' essere ricondotto alla forma trattata sopra.

Conclusione

Per induzione strutturale:

1. le formule atomiche hanno automi;
2. i connettivi booleani preservano omega-regolarita';
3. i quantificatori corrispondono a proiezione e complemento;
4. le variabili del primo ordine sono codificabili come singleton.

Quindi ogni formula S1S definisce un linguaggio omega-regolare.

Punto orale: la frase "il quantificatore esistenziale corrisponde alla proiezione" va saputa spiegare. L'automa non vede piu' la componente quantificata, ma il nondeterminismo la indovina.

12. Behavior graph LTL: componente adeguata implica soddisfacibilita' sul programma

Enunciato

Sia $P$ un programma, $G_P$ il suo grafo delle computazioni e $T_\varphi$ il tableau di una formula LTL $\varphi$.

Costruiamo il behavior graph:

$$ B_{P,\varphi}. $$

Se $B_{P,\varphi}$ contiene una componente adeguata, allora esiste una computazione di $P$ che soddisfa $\varphi$.

Definizioni minime

Un nodo del behavior graph ha forma:

$$ (s,A) $$

dove:

• $s$ e' uno stato del programma;
• $A$ e' un atomo del tableau;
• $s$ e' consistente con le formule locali contenute in $A$.

Un arco:

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

esiste quando:

• $s'$ e' successore di $s$ nel grafo del programma;
• $A'$ e' successore di $A$ nel tableau LTL.

Una componente e' fulfilling se tutte le promesse temporali degli atomi vengono realizzate. E' fair se rispetta i vincoli di justice e compassion del sistema. E' adeguata se e' sia fulfilling sia fair.

Dimostrazione

Supponiamo che esista una componente adeguata $S$ in $B_{P,\varphi}$.

Poiche' $S$ e' una componente fortemente connessa non transiente, possiamo costruire un cammino infinito:

$$ (s_0,A_0),(s_1,A_1),(s_2,A_2),\ldots $$

che rimane dentro $S$ e visita gli elementi necessari di $S$ infinite volte.

Proiettando questo cammino sulla prima componente otteniamo:

$$ s_0,s_1,s_2,\ldots $$

Per definizione degli archi del behavior graph, ogni $s_{i+1}$ e' successore di $s_i$ nel grafo del programma. Quindi questa proiezione e' una computazione valida di $P$.

Proiettando sulla seconda componente otteniamo:

$$ A_0,A_1,A_2,\ldots $$

Per definizione degli archi del behavior graph, ogni $A_{i+1}$ e' successore di $A_i$ nel tableau. Quindi questa proiezione e' un cammino del tableau.

Inoltre, per definizione dei nodi del behavior graph, ogni $s_i$ e' consistente con $A_i$. Quindi la sequenza di atomi:

$$ A_0,A_1,A_2,\ldots $$

e' una trail della computazione:

$$ s_0,s_1,s_2,\ldots $$

Poiche' $S$ e' fulfilling, ogni promessa temporale presente lungo la trail viene realizzata. Per il teorema di correttezza del tableau LTL, una trail fulfilling corrisponde a una computazione che soddisfa $\varphi$.

Poiche' $S$ e' fair, la computazione proiettata rispetta anche i vincoli di fairness del programma: le transizioni justice e compassion non vengono violate.

Dunque esiste una computazione fair di $P$ che soddisfa $\varphi$.

Quindi:

$$ B_{P,\varphi}\text{ contiene una componente adeguata} \Rightarrow P\text{ e' } \varphi\text{-soddisfacibile}. $$

Validita' tramite negazione

La componente adeguata dimostra esistenza di una computazione che soddisfa $\varphi$, non che tutte le computazioni soddisfano $\varphi$.

Per verificare la validita' di $\varphi$ sul programma, si cerca una computazione che violi $\varphi$, cioe' che soddisfi $\neg\varphi$.

Formalmente:

$$ P\models \varphi \iff \text{non esiste computazione di }P\text{ che soddisfa }\neg\varphi. $$

Quindi:

$$ P\models\varphi \iff B_{P,\neg\varphi}\text{ non contiene componenti adeguate}. $$

Punto orale: componente adeguata = esistenza di una computazione buona per quella formula. Per dimostrare che il programma soddisfa sempre una specifica, devi cercare l'assenza di componenti adeguate per la negazione.

13. Traduzioni LTL: forme da saper giustificare

Questa non e' una dimostrazione lunga, ma all'orale la traduzione LTL e' quasi certa. Conviene sapere giustificare semanticamente le forme standard.

Ogni richiesta riceve prima o poi risposta

Requisito:

ogni volta che compare req, prima o poi compare ack.

Formula:

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

Giustificazione:

• $G$ quantifica ogni posizione della computazione;
• se in quella posizione vale req, allora deve valere $F ack$;
• $F ack$ significa che esiste una posizione futura, anche non immediata, in cui vale ack.

Infinite occorrenze di $p$

Formula:

$$ GFp. $$

Giustificazione:

• $G$ dice: da ogni posizione in poi;
• $Fp$ dice: prima o poi nel futuro compare $p$;
• quindi dopo ogni prefisso c'e' ancora un $p$ futuro;
• questo equivale a dire che $p$ compare infinite volte.

Da un certo punto in poi sempre $p$

Formula:

$$ FGp. $$

Giustificazione:

• $F$ dice: esiste una posizione futura;
• $Gp$ dice: da quella posizione in poi $p$ vale sempre;
• quindi c'e' una soglia dopo la quale $p$ non smette piu' di valere.

$p$ finche' non arriva $q$

Strong until:

$$ p\;U\;q. $$

Semantica:

$$ \alpha,i\models pUq $$

se e solo se esiste $j\ge i$ tale che:

$$ \alpha,j\models q $$

e per ogni $k$ con $i\le k<j$:

$$ \alpha,k\models p. $$

Quindi $q$ deve arrivare davvero. Se vuoi permettere che $q$ non arrivi mai e $p$ resti vero per sempre, serve il weak until.

Ogni errore viene preceduto da un allarme

Se si intende "un allarme deve essere avvenuto prima di ogni errore", in LTL futura pura non e' immediato parlare del passato. Una forma con until e' vietare un errore prima del primo allarme:

$$ \neg error\;U\;alarm $$

ma questa richiede anche che alarm prima o poi arrivi. Se invece si vuole dire "error non puo' accadere finche' alarm non e' accaduto, ma alarm potrebbe non accadere mai", serve weak until:

$$ \neg error\;W\;alarm. $$

Punto orale: se usi $U$, stai promettendo che il secondo evento arrivera'. Se non vuoi prometterlo, devi usare weak until o una formula equivalente.

14. Da epsilon-NFA a NFA

Enunciato

Per ogni NFA con mosse $\varepsilon$ esiste un NFA senza mosse $\varepsilon$ che riconosce lo stesso linguaggio.

Sia:

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

un $\varepsilon$-NFA, dove:

$$ \Delta:Q\times(\Sigma\cup\{\varepsilon\})\to 2^Q. $$

Epsilon-closure

Per $S\subseteq Q$, definiamo:

$$ E(S) $$

come l'insieme degli stati raggiungibili da qualche stato di $S$ usando solo mosse $\varepsilon$, incluse zero mosse. In particolare:

$$ S\subseteq E(S). $$

Per uno stato singolo scriviamo:

$$ E(q)=E(\{q\}). $$

Costruzione dell'NFA equivalente

Costruiamo:

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

con gli stessi stati, lo stesso alfabeto e lo stesso stato iniziale.

Per $q\in Q$ e $a\in\Sigma$:

$$ \Delta'(q,a)=E\left(\bigcup_{p\in E(q)}\Delta(p,a)\right). $$

Questa formula dice: prima posso fare qualunque numero di mosse $\varepsilon$, poi leggo davvero $a$, poi posso fare ancora qualunque numero di mosse $\varepsilon$.

Gli stati finali diventano:

$$ F'=\{q\in Q\mid E(q)\cap F\neq\emptyset\}. $$

Questo serve per accettare anche parole che, dopo aver consumato tutto l'input, arrivano a un finale solo tramite mosse $\varepsilon$.

Invariante

Per ogni parola $w\in\Sigma^\ast$:

$$ \hat{\Delta}'(q,w) = E(\hat{\Delta}(E(q),w)). $$

Lettura: gli stati raggiungibili nell'NFA senza $\varepsilon$ dopo aver letto $w$ sono esattamente quelli raggiungibili nell'automa originale leggendo $w$ e permettendo mosse $\varepsilon$ prima, tra e dopo i simboli.

Dimostrazione dell'invariante

Base: $w=\varepsilon$.

Nel nuovo NFA, leggendo $\varepsilon$ da $q$ si resta in $q$:

$$ \hat{\Delta}'(q,\varepsilon)=\{q\}. $$

Pero' l'accettazione tramite mosse finali $\varepsilon$ e' stata spostata in $F'$. Quindi, per il riconoscimento del linguaggio, la closure finale viene recuperata dalla definizione di finalita'. Se invece si vuole un invariante con closure incorporata anche a lunghezza zero, si prende come stato iniziale $E(q_0)$ nella subset construction. Le due presentazioni sono equivalenti.

Passo su $wa$.

Supponiamo che la simulazione sia corretta dopo aver letto $w$. Leggendo il simbolo successivo $a$, il nuovo NFA applica:

$$ \Delta'(q,a)=E\left(\bigcup_{p\in E(q)}\Delta(p,a)\right). $$

Quindi comprime in una singola transizione tutto cio' che l'automa originale poteva fare con:

$$ \varepsilon^\ast a \varepsilon^\ast. $$

Ripetendo questa compressione per ogni simbolo della parola, ogni run dell'automa originale con mosse $\varepsilon$ corrisponde a una run dell'NFA nuovo senza mosse $\varepsilon$, e viceversa ogni transizione nuova espande una sequenza valida di mosse originali.

Uguaglianza dei linguaggi

Se $w$ e' accettata da $\mathcal{A}$, allora esiste una computazione che alterna blocchi di mosse $\varepsilon$ e simboli reali:

$$ \varepsilon^\ast a_1\varepsilon^\ast a_2\varepsilon^\ast\ldots a_n\varepsilon^\ast. $$

Ogni blocco $\varepsilon^\ast a_i\varepsilon^\ast$ e' rappresentato da una transizione di $\mathcal{A}'$. Se l'ultimo stato finale viene raggiunto solo dopo mosse $\varepsilon$, la definizione di $F'$ rende finale lo stato precedente. Quindi $w$ e' accettata da $\mathcal{A}'$.

Viceversa, ogni transizione di $\mathcal{A}'$ e' stata costruita da un cammino reale dell'automa originale composto da mosse $\varepsilon$, una lettera, e altre mosse $\varepsilon$. Espandendo tutte le transizioni della run di $\mathcal{A}'$ si ottiene una run valida di $\mathcal{A}$. Quindi:

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

Punto orale: la frase "metto le epsilon-closure dentro le transizioni" significa precisamente comprimere $\varepsilon^\ast a\varepsilon^\ast$ in una sola transizione su $a$.

15. Teorema automi finiti - espressioni regolari

Enunciato

Per ogni automa finito su parole finite esiste una espressione regolare ristretta equivalente, e per ogni espressione regolare ristretta esiste un automa finito equivalente.

Quindi le seguenti classi descrivono gli stessi linguaggi:

• DFA;
• NFA;
• $\varepsilon$-NFA;
• espressioni regolari ristrette.

Direzione DFA -> espressione regolare

Sia:

$$ \mathcal{A}=(Q,\Sigma,\delta,q_1,F) $$

un DFA con:

$$ Q=\{q_1,\ldots,q_n\}. $$

Definiamo $R_{i,j}^k$ come il linguaggio delle parole che portano da $q_i$ a $q_j$ usando come stati intermedi solo stati con indice al massimo $k$.

Stati intermedi significa: escludiamo lo stato iniziale e quello finale del cammino; guardiamo solo gli stati attraversati nel mezzo.

Caso base

Per $k=0$, non sono ammessi stati intermedi.

Se $i\neq j$:

$$ R_{i,j}^0=\{a\in\Sigma\mid \delta(q_i,a)=q_j\}. $$

Se $i=j$:

$$ R_{i,i}^0=\{a\in\Sigma\mid \delta(q_i,a)=q_i\}\cup\{\varepsilon\}. $$

La parola vuota va inclusa perche' da uno stato si puo' arrivare a se stesso leggendo nulla.

Ogni $R_{i,j}^0$ e' descritto da una espressione regolare finita: unione delle lettere che realizzano transizioni dirette, piu eventualmente $\varepsilon$.

Passo induttivo

Vogliamo descrivere i cammini da $q_i$ a $q_j$ che possono usare come intermedi stati con indice al massimo $k$.

Ci sono due casi.

Caso 1: il cammino non passa per $q_k$.

Allora usa solo intermedi con indice al massimo $k-1$, quindi la parola appartiene a:

$$ R_{i,j}^{k-1}. $$

Caso 2: il cammino passa per $q_k$.

Allora si puo' decomporre in:

1. un tratto da $q_i$ a $q_k$ senza usare $q_k$ come intermedio:

$$ R_{i,k}^{k-1}; $$

1. zero o piu' cicli da $q_k$ a $q_k$, senza usare $q_k$ come intermedio interno:

$$ (R_{k,k}^{k-1})^\ast; $$

1. un tratto da $q_k$ a $q_j$ senza usare $q_k$ come intermedio:

$$ R_{k,j}^{k-1}. $$

Quindi:

$$ R_{i,j}^k = R_{i,j}^{k-1} \cup R_{i,k}^{k-1}(R_{k,k}^{k-1})^\ast R_{k,j}^{k-1}. $$

Per ipotesi induttiva, tutti i pezzi a destra sono descritti da espressioni regolari. Poiche' le espressioni regolari sono chiuse per unione, concatenazione e stella, anche $R_{i,j}^k$ e' descritto da una espressione regolare.

Espressione finale

Una parola e' accettata da $\mathcal{A}$ se parte da $q_1$ e termina in uno stato finale. Quando $k=n$, non ci sono piu' restrizioni sugli stati intermedi.

Quindi:

$$ L(\mathcal{A})=\bigcup_{q_j\in F}R_{1,j}^n. $$

Il lato destro e' una espressione regolare.

Direzione espressione regolare -> automa

Procediamo per induzione strutturale sull'espressione regolare $r$.

Base $\emptyset$.

Un automa con nessuno stato finale riconosce il linguaggio vuoto.

Base $\varepsilon$.

Un automa con stato iniziale anche finale riconosce $\{\varepsilon\}$.

Base $a$.

Un automa con una transizione:

$$ q_0\xrightarrow{a}q_f $$

riconosce $\{a\}$.

Unione $r_1\cup r_2$.

Per ipotesi induttiva abbiamo automi $\mathcal{A}_1$ e $\mathcal{A}_2$. Rendiamo disgiunti gli insiemi di stati, aggiungiamo un nuovo iniziale $q_0$ e un nuovo finale $f_0$, con mosse:

$$ q_0\xrightarrow{\varepsilon}q_1 \quad\text{e}\quad q_0\xrightarrow{\varepsilon}q_2 $$

verso gli iniziali dei due automi, e mosse $\varepsilon$ dai vecchi finali verso $f_0$.

La computazione accetta se sceglie il ramo di $r_1$ oppure quello di $r_2$.

Concatenazione $r_1r_2$.

Colleghiamo ogni finale di $\mathcal{A}_1$ all'iniziale di $\mathcal{A}_2$ con una mossa $\varepsilon$. I finali del nuovo automa sono i finali di $\mathcal{A}_2$.

Una parola e' accettata se si spezza in:

$$ w=uv $$

con $u\in L(r_1)$ e $v\in L(r_2)$.

Stella $r_1^\ast$.

Aggiungiamo un nuovo iniziale $q_0$ e un nuovo finale $f_0$. Mettiamo:

• una mossa $\varepsilon$ da $q_0$ a $f_0$, per accettare $\varepsilon$;
• una mossa $\varepsilon$ da $q_0$ all'iniziale di $\mathcal{A}_1$;
• mosse $\varepsilon$ dai finali di $\mathcal{A}_1$ a $f_0$;
• mosse $\varepsilon$ dai finali di $\mathcal{A}_1$ all'iniziale di $\mathcal{A}_1$, per ripetere.

L'automa accetta zero o piu' blocchi appartenenti a $L(r_1)$.

Per induzione ogni espressione regolare ha un $\varepsilon$-NFA equivalente, quindi un NFA e un DFA equivalenti.

Punto orale: nella direzione DFA -> regex, il passaggio non ovvio e' la ricorrenza con $(R_{k,k}^{k-1})^\ast$, che rappresenta un numero arbitrario di ritorni su $q_k$.

16. Chiusura booleana dei linguaggi regolari finiti

Complemento

Sia $L\subseteq\Sigma^\ast$ regolare. Prendiamo un DFA completo:

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

che riconosce $L$.

Costruiamo:

$$ \overline{\mathcal{A}}=(Q,\Sigma,\delta,q_0,Q\setminus F). $$

Per ogni parola $w$ il DFA ha una e una sola computazione completa, perche' e' deterministico e completo.

Allora:

$$ w\in L(\overline{\mathcal{A}}) \iff \hat{\delta}(q_0,w)\in Q\setminus F \iff \hat{\delta}(q_0,w)\notin F \iff w\notin L(\mathcal{A}). $$

Quindi:

$$ L(\overline{\mathcal{A}})=\Sigma^\ast\setminus L. $$

La completezza e' essenziale: se una transizione manca, una parola potrebbe non avere computazione completa e lo scambio finali/non-finali non rappresenterebbe il complemento.

Intersezione

Siano $L_1,L_2$ regolari. Per De Morgan:

$$ L_1\cap L_2 = \overline{\overline{L_1}\cup\overline{L_2}}. $$

Poiche' i regolari sono chiusi per complemento e unione, sono chiusi anche per intersezione.

In alternativa, dato due DFA:

$$ \mathcal{A}_1=(Q_1,\Sigma,\delta_1,q_1,F_1) $$

e:

$$ \mathcal{A}_2=(Q_2,\Sigma,\delta_2,q_2,F_2), $$

si costruisce il prodotto:

$$ Q=Q_1\times Q_2 $$

con transizione:

$$ \delta((p,r),a)=(\delta_1(p,a),\delta_2(r,a)) $$

e finali:

$$ F=F_1\times F_2. $$

Per induzione su $w$:

$$ \hat{\delta}((q_1,q_2),w) = (\hat{\delta}_1(q_1,w),\hat{\delta}_2(q_2,w)). $$

Quindi $w$ e' accettata dal prodotto se e solo se e' accettata da entrambi gli automi.

Punto orale: per il complemento finito puoi scambiare finali solo dopo aver reso il DFA deterministico e completo.

17. Chiusure base degli omega-regolari: $V^\omega$ e $V\cdot L$

Se $V$ e' regolare, allora $V^\omega$ e' omega-regolare

Sia $V\subseteq A^\ast$ regolare. Prendiamo un automa finito:

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

che riconosce $V$.

Assumiamo senza perdita di generalita':

$$ \varepsilon\notin V. $$

Infatti:

$$ V^\omega=(V\setminus\{\varepsilon\})^\omega, $$

perche' inserire blocchi vuoti non cambia la parola infinita prodotta.

Costruiamo un automa di Büchi $\mathcal{B}$ che simula $\mathcal{D}$ e, ogni volta che completa un blocco di $V$, puo' tornare allo stato iniziale.

Formalmente, per ogni transizione:

$$ (s,a,f)\in\Delta \quad\text{con }f\in F, $$

aggiungiamo anche una transizione:

$$ (s,a,q_0). $$

Lo stato finale Büchi e':

$$ \{q_0\}. $$

L'idea e' che tornare in $q_0$ segnala "ho appena terminato un blocco di $V$ e sono pronto a leggerne un altro".

Correttezza.

Se:

$$ \alpha\in V^\omega, $$

allora:

$$ \alpha=v_0v_1v_2\ldots $$

con ogni $v_i\in V$. L'automa legge $v_0$ simulando $\mathcal{D}$, al completamento usa la transizione aggiunta per tornare a $q_0$, poi fa lo stesso per $v_1,v_2,\ldots$. Quindi visita $q_0$ infinite volte e accetta.

Viceversa, se $\mathcal{B}$ accetta, visita $q_0$ infinite volte. Tra due visite consecutive a $q_0$ legge un blocco non vuoto che corrisponde a una computazione di $\mathcal{D}$ terminata in uno stato finale. Quindi quel blocco appartiene a $V$. La parola accettata e' quindi concatenazione infinita di blocchi di $V$:

$$ \alpha\in V^\omega. $$

Se $V$ e' regolare e $L$ omega-regolare, allora $V\cdot L$ e' omega-regolare

Sia $\mathcal{D}$ un automa finito per $V$ e sia $\mathcal{A}$ un NBA per $L$.

Costruiamo un NBA che:

1. simula $\mathcal{D}$ per leggere un prefisso finito in $V$;
2. quando $\mathcal{D}$ raggiunge un finale, passa nondeterministicamente allo stato iniziale di $\mathcal{A}$;
3. da quel momento simula $\mathcal{A}$;
4. usa come stati finali quelli di $\mathcal{A}$.

Se $\alpha\in V\cdot L$, allora:

$$ \alpha=u\beta $$

con $u\in V$ e $\beta\in L$. L'automa legge $u$ nella parte finita, passa alla parte Büchi, e segue una run accettante di $\mathcal{A}$ su $\beta$.

Viceversa, se l'automa accetta, prima di entrare nella parte Büchi deve aver completato una parola di $V$; poi la parte infinita residua viene accettata da $\mathcal{A}$, quindi appartiene a $L$. Dunque la parola e' in $V\cdot L$.

Punto orale: in $V^\omega$ l'automa deve completare infiniti blocchi finiti; in $V\cdot L$ completa un solo prefisso finito e poi lascia l'accettazione alla parte Büchi.

18. Parole ultimamente periodiche

Definizione

Una parola infinita e' ultimamente periodica se ha forma:

$$ \alpha=uv^\omega $$

con:

$$ u,v\in A^\ast,\qquad v\neq\varepsilon. $$

Il prefisso $u$ puo' essere arbitrario; da un certo punto in poi si ripete sempre lo stesso blocco $v$.

Corollario: ogni omega-regolare non vuoto contiene una parola ultimamente periodica

Sia $L$ omega-regolare e non vuoto. Per il teorema Büchi - omega-regex:

$$ L=\bigcup_{i=1}^n U_iV_i^\omega $$

con $U_i,V_i$ regolari.

Poiche' $L\neq\emptyset$, esiste un indice $i$ e una parola:

$$ \alpha\in U_iV_i^\omega. $$

Quindi:

$$ \alpha=uv_0v_1v_2\ldots $$

con:

$$ u\in U_i $$

e:

$$ v_j\in V_i. $$

In particolare esiste almeno un blocco $v_0\in V_i$ non vuoto. Allora:

$$ uv_0^\omega $$

appartiene ancora a:

$$ U_iV_i^\omega $$

perche' e' ottenuta scegliendo sempre lo stesso blocco $v_0\in V_i$.

Quindi:

$$ uv_0^\omega\in L. $$

Abbiamo trovato una parola ultimamente periodica in $L$.

Esempio di linguaggio non omega-regolare

Sia $\beta\in A^\omega$ una parola non ultimamente periodica. Definiamo:

$$ L(\beta)=\{\alpha\in A^\omega\mid \alpha\text{ ha un suffisso in comune con }\beta\}. $$

Chiaramente:

$$ \beta\in L(\beta), $$

quindi:

$$ L(\beta)\neq\emptyset. $$

Supponiamo per assurdo che $L(\beta)$ sia omega-regolare. Allora, per il corollario precedente, contiene una parola ultimamente periodica:

$$ \alpha=uv^\omega. $$

Ma $\alpha\in L(\beta)$ significa che $\alpha$ e $\beta$ condividono un suffisso infinito. Un suffisso di una parola ultimamente periodica e' ancora ultimamente periodico. Quindi anche $\beta$ avrebbe un suffisso ultimamente periodico, e allora $\beta$ sarebbe ultimamente periodica da un certo punto in poi.

Questo contraddice la scelta di $\beta$ come non ultimamente periodica.

Dunque:

$$ L(\beta) $$

non e' omega-regolare.

Punto orale: il corollario e' utile per dimostrare non omega-regolarita': se un linguaggio non vuoto non contiene parole ultimamente periodiche, non puo' essere omega-regolare.

19. Decidibilita' per automi di Büchi

Universality

Vogliamo decidere:

$$ L(\mathcal{A})=A^\omega. $$

Questo equivale a:

$$ \overline{L(\mathcal{A})}=\emptyset. $$

Poiche' gli omega-regolari sono chiusi per complemento, possiamo costruire un automa per $\overline{L(\mathcal{A})}$ e poi usare l'algoritmo di emptiness Büchi.

Inclusion

Vogliamo decidere:

$$ L(\mathcal{A})\subseteq L(\mathcal{B}). $$

Questo equivale a dire che non esiste una parola accettata da $\mathcal{A}$ e rifiutata da $\mathcal{B}$:

$$ L(\mathcal{A})\cap\overline{L(\mathcal{B})}=\emptyset. $$

Costruiamo l'automa per il complemento di $\mathcal{B}$, poi l'intersezione con $\mathcal{A}$, e controlliamo emptiness.

Questa e' la forma automata-theoretic del model checking: cerco un comportamento del sistema che violi la specifica.

Equivalence

Vogliamo decidere:

$$ L(\mathcal{A})=L(\mathcal{B}). $$

Si puo' fare con doppia inclusione:

$$ L(\mathcal{A})\subseteq L(\mathcal{B}) \quad\text{e}\quad L(\mathcal{B})\subseteq L(\mathcal{A}). $$

Oppure con la differenza simmetrica:

$$ (L(\mathcal{A})\cap\overline{L(\mathcal{B})}) \cup (\overline{L(\mathcal{A})}\cap L(\mathcal{B})). $$

I due linguaggi sono uguali se e solo se questa differenza simmetrica e' vuota.

Punto orale: tutte queste decisioni si riducono a emptiness grazie a intersezione e complementazione Büchi.

Fingerprint ultimamente periodico

Per un linguaggio omega-regolare $L$, indichiamo con $UP(L)$ l'insieme delle parole ultimamente periodiche in $L$.

Teorema:

$$ UP(L_1)=UP(L_2)\Rightarrow L_1=L_2 $$

per $L_1,L_2$ omega-regolari.

Dimostrazione. Supponiamo per assurdo:

$$ UP(L_1)=UP(L_2) \quad\text{ma}\quad L_1\neq L_2. $$

Allora, senza perdita di generalita':

$$ L=L_1\setminus L_2\neq\emptyset. $$

Poiche' gli omega-regolari sono chiusi per complemento e intersezione:

$$ L=L_1\cap\overline{L_2} $$

e' omega-regolare.

Poiche' $L$ e' omega-regolare non vuoto, contiene una parola ultimamente periodica $\alpha$.

Allora:

$$ \alpha\in UP(L_1) $$

ma:

$$ \alpha\notin UP(L_2), $$

perche' $\alpha\notin L_2$. Questo contraddice:

$$ UP(L_1)=UP(L_2). $$

Quindi:

$$ L_1=L_2. $$

Punto orale: sugli omega-regolari le parole ultimamente periodiche sono una sorta di impronta del linguaggio.

20. Tableau LTL: soddisfacibilita' tramite fulfilling MSCS

Obiettivo

Per una formula LTL $\varphi$, vogliamo decidere se esiste un modello che la soddisfa. Il tableau costruisce un grafo finito $T_\varphi$ di atomi e riduce la soddisfacibilita' all'esistenza di un cammino infinito buono.

Promesse

Una formula promettente e' una formula che richiede una realizzazione futura. Esempi:

• $Fr$ promette $r$;
• $pUr$ promette $r$;
• $\neg G\neg r$ promette $r$.

Un atomo $A$ realizza, o fulfills, una promessa $\psi$ che promette $r$ se:

$$ \neg\psi\in A \quad\text{oppure}\quad r\in A. $$

Un cammino:

$$ \pi=A_0,A_1,A_2,\ldots $$

e' fulfilling se, per ogni formula promettente $\psi$, il cammino contiene infiniti atomi che realizzano $\psi$.

Dai modelli ai cammini fulfilling

Supponiamo che $\sigma$ sia un modello di $\varphi$. Per ogni posizione $j$, definiamo:

$$ A_j=\{\psi\in\Phi_\varphi\mid \sigma,j\models\psi\}. $$

Allora:

1. ogni $A_j$ e' un atomo, perche' contiene una scelta coerente tra ogni formula e la sua negazione e rispetta le regole $\alpha/\beta$;
2. se $X\psi\in A_j$, allora $\psi\in A_{j+1}$, quindi c'e' un arco $A_j\to A_{j+1}$ nel tableau;
3. poiche' $\sigma,0\models\varphi$, vale $\varphi\in A_0$.

Resta da verificare fulfilling. Se $\psi$ promette $r$ ed e' vera lungo il modello, la semantica LTL impone che la promessa venga realizzata, oppure che a un certo punto la promessa non sia piu' richiesta. Formalmente, ci sono infinite posizioni $j$ tali che:

$$ \sigma,j\models\neg\psi \quad\text{oppure}\quad \sigma,j\models r. $$

Per definizione di $A_j$, questo significa:

$$ \neg\psi\in A_j \quad\text{oppure}\quad r\in A_j. $$

Quindi il cammino indotto e' fulfilling.

Dai cammini fulfilling ai modelli

Supponiamo ora di avere un cammino fulfilling:

$$ \pi=A_0,A_1,A_2,\ldots $$

Costruiamo un modello $\sigma$ facendo valere in posizione $j$ esattamente le proposizioni atomiche contenute in $A_j$.

Vogliamo mostrare, per induzione sulla struttura di $\psi\in\Phi_\varphi$:

$$ \sigma,j\models\psi \iff \psi\in A_j. $$

Caso atomico.

Vero per costruzione del labeling di $\sigma$.

Connettivi booleani.

Seguono dalle regole degli atomi: ogni atomo contiene formule coerenti con le regole per $\land,\lor,\neg$.

Caso $X\psi$.

Per semantica:

$$ \sigma,j\models X\psi \iff \sigma,j+1\models\psi. $$

Per ipotesi induttiva:

$$ \sigma,j+1\models\psi \iff \psi\in A_{j+1}. $$

Per definizione degli archi del tableau:

$$ \psi\in A_{j+1} \iff X\psi\in A_j. $$

Quindi il caso $X$ e' dimostrato.

Caso $F r$.

Supponiamo prima:

$$ Fr\in A_j. $$

Poiche' il cammino e' fulfilling, esiste $k\ge j$ tale che $A_k$ realizza la promessa $Fr$. Prendiamo il primo tale $k$.

Se $k=j$, allora, dato che $Fr\in A_j$ e $A_j$ realizza $Fr$, deve valere:

$$ r\in A_j. $$

Per ipotesi induttiva:

$$ \sigma,j\models r, $$

quindi:

$$ \sigma,j\models Fr. $$

Se $k>j$, allora fino a $k-1$ la promessa non e' realizzata. Le regole $\beta$ per $F$ impongono di propagare:

$$ XFr $$

e quindi $Fr$ resta nel successore. Al primo punto $k$ in cui la promessa e' realizzata, deve valere:

$$ r\in A_k. $$

Per ipotesi induttiva:

$$ \sigma,k\models r. $$

Quindi:

$$ \sigma,j\models Fr. $$

Viceversa, supponiamo:

$$ \sigma,j\models Fr $$

ma:

$$ Fr\notin A_j. $$

Allora:

$$ \neg Fr\in A_j. $$

La formula $\neg Fr$ equivale a $G\neg r$. Le regole degli atomi e degli archi propagano $\neg r$ e $\neg Fr$ in tutti i successori. Per induzione avremmo:

$$ \sigma,k\models\neg r \quad\text{per ogni }k\ge j, $$

contraddicendo $\sigma,j\models Fr$.

Quindi:

$$ \sigma,j\models Fr \iff Fr\in A_j. $$

Gli altri casi promettenti, come $pUr$, si trattano nello stesso modo: la parte fulfilling garantisce che la promessa dell'until venga prima o poi realizzata.

Teorema principale

Una formula $\varphi$ e' soddisfacibile se e solo se il tableau $T_\varphi$ contiene un cammino fulfilling:

$$ A_0,A_1,A_2,\ldots $$

con:

$$ \varphi\in A_0. $$

La direzione da sinistra a destra usa il cammino indotto dal modello. La direzione da destra a sinistra usa la costruzione del modello dal cammino fulfilling.

Riduzione a fulfilling MSCS

Poiche' $T_\varphi$ e' finito, un cammino infinito prima o poi resta in una componente fortemente connessa.

Un SCS non transiente $S$ e' fulfilling se per ogni promessa $\psi$ esiste almeno un atomo $A\in S$ che realizza $\psi$.

Allora:

$$ \varphi\text{ e' soddisfacibile} \iff T_\varphi\text{ contiene un fulfilling MSCS raggiungibile da un atomo che contiene }\varphi. $$

Direzione cammino -> MSCS.

Se esiste un cammino fulfilling, considera gli atomi visitati infinite volte. Essi stanno dentro una componente fortemente connessa raggiungibile. Poiche' il cammino e' fulfilling, per ogni promessa qualche atomo visitato infinite volte la realizza. Quindi la componente e' fulfilling.

Direzione MSCS -> cammino.

Se esiste un fulfilling MSCS raggiungibile, percorri un cammino finito fino alla componente e poi, usando la forte connessione, costruisci un cammino infinito che visita ogni atomo della componente infinite volte. Poiche' la componente contiene un realizzatore per ogni promessa, il cammino e' fulfilling.

Punto orale: gli atomi garantiscono coerenza locale e propagazione dei next; la condizione fulfilling serve esattamente a impedire che una promessa futura venga rimandata per sempre.

21. CTL tramite punti fissi: $EG$ ed $EU$

Questa parte appare negli appunti di model checking. Non e' il blocco piu probabile se l'orale insiste su Büchi, ma chiude il quadro sulla differenza tra LTL e CTL.

Lemma: monotonia

Sia $S$ l'insieme finito degli stati di una struttura di Kripke. Un trasformatore:

$$ \tau:2^S\to 2^S $$

e' monotono se:

$$ X\subseteq Y\Rightarrow \tau(X)\subseteq\tau(Y). $$

Per:

$$ \tau(Z)=Sat(f)\cap Pre_\exists(Z) $$

dove $Pre_\exists(Z)$ e' l'insieme degli stati con almeno un successore in $Z$, la monotonia vale. Infatti, se $Z_1\subseteq Z_2$, ogni stato che ha un successore in $Z_1$ ha anche un successore in $Z_2$. Quindi:

$$ Pre_\exists(Z_1)\subseteq Pre_\exists(Z_2) $$

e intersecando con $Sat(f)$:

$$ \tau(Z_1)\subseteq\tau(Z_2). $$

$EG f$ come massimo punto fisso

La formula:

$$ EG f $$

significa: esiste un cammino infinito lungo cui $f$ vale sempre.

Definiamo:

$$ \tau(Z)=Sat(f)\cap Pre_\exists(Z). $$

Allora:

$$ Sat(EG f)=\nu Z.\,\tau(Z), $$

dove $\nu$ indica il massimo punto fisso.

Perche' $Sat(EG f)\subseteq \nu Z.\tau(Z)$.

Se $s\models EG f$, esiste un cammino:

$$ s=s_0,s_1,s_2,\ldots $$

tale che ogni $s_i\models f$. Inoltre $s_1$ soddisfa ancora $EG f$, perche' il suffisso del cammino da $s_1$ in poi e' ancora un cammino infinito tutto in $f$.

Quindi:

$$ s\in Sat(f) $$

e $s$ ha un successore in $Sat(EG f)$. Dunque:

$$ Sat(EG f)\subseteq \tau(Sat(EG f)). $$

In realta' vale uguaglianza, quindi $Sat(EG f)$ e' un punto fisso. Essendo $\nu Z.\tau(Z)$ il massimo punto fisso, contiene $Sat(EG f)$.

Perche' $\nu Z.\tau(Z)\subseteq Sat(EG f)$.

Sia:

$$ Z^\ast=\nu Z.\tau(Z). $$

Se $s\in Z^\ast$, poiche' $Z^\ast=\tau(Z^\ast)$, allora:

1. $s\in Sat(f)$;
2. esiste un successore $s_1\in Z^\ast$.

Applicando lo stesso ragionamento a $s_1$, otteniamo $s_2\in Z^\ast$, e cosi' via. Costruiamo quindi un cammino infinito:

$$ s=s_0,s_1,s_2,\ldots $$

in cui ogni stato sta in $Z^\ast$ e quindi soddisfa $f$. Dunque:

$$ s\models EG f. $$

Quindi:

$$ Sat(EG f)=\nu Z.\,(Sat(f)\cap Pre_\exists(Z)). $$

$E[f_1 U f_2]$ come minimo punto fisso

La formula:

$$ E[f_1 U f_2] $$

significa: esiste un cammino in cui prima o poi vale $f_2$, e fino a quel momento vale $f_1$.

Definiamo:

$$ \tau(Z)=Sat(f_2)\cup(Sat(f_1)\cap Pre_\exists(Z)). $$

Allora:

$$ Sat(E[f_1 U f_2])=\mu Z.\,\tau(Z), $$

dove $\mu$ indica il minimo punto fisso.

Intuizione costruttiva.

Partiamo da:

$$ Z_0=\emptyset. $$

Poi:

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

• $Z_1$ contiene gli stati che soddisfano gia' $f_2$;
• $Z_2$ aggiunge gli stati che soddisfano $f_1$ e possono andare in uno stato di $Z_1$;
• $Z_3$ aggiunge gli stati che possono raggiungere $f_2$ in due passi mantenendo $f_1$ prima;
• e cosi' via.

Poiche' $S$ e' finito e la sequenza e' crescente:

$$ Z_0\subseteq Z_1\subseteq Z_2\subseteq\ldots $$

prima o poi si stabilizza. Il limite e' il minimo punto fisso.

Correttezza.

Se $s$ entra in qualche $Z_i$, allora esiste un cammino di lunghezza al piu' $i$ che arriva a uno stato che soddisfa $f_2$, e tutti gli stati precedenti soddisfano $f_1$. Quindi:

$$ s\models E[f_1 U f_2]. $$

Viceversa, se:

$$ s\models E[f_1 U f_2], $$

allora esiste un cammino:

$$ s=s_0,s_1,\ldots,s_k $$

con:

$$ s_k\models f_2 $$

e:

$$ s_i\models f_1\quad\text{per }0\le i<k. $$

Per induzione all'indietro:

• $s_k\in Z_1$;
• $s_{k-1}\in Z_2$;
• ...
• $s_0\in Z_{k+1}$.

Quindi $s$ appartiene al minimo punto fisso.

Punto orale: CTL model checking e' locale perche' calcola insiemi di stati tramite punti fissi; LTL invece richiede ragionare su cammini interi/tableau/automi.

22. Chiusura di DBA per unione e intersezione

Negli appunti questa parte compare come esercizio:

dimostrare che gli automi di Büchi deterministici sono chiusi per unione e intersezione.

La chiusura per unione e' semplice; quella per intersezione richiede un piccolo contatore di turno, perche' due stati finali possono essere visitati infinitamente spesso ma non nello stesso istante.

Unione

Siano:

$$ \mathcal{A}_1=(Q_1,\Sigma,\delta_1,q^1_0,F_1) $$

e:

$$ \mathcal{A}_2=(Q_2,\Sigma,\delta_2,q^2_0,F_2) $$

due DBA.

Costruiamo:

$$ \mathcal{A}^{\cup}=(Q_1\times Q_2,\Sigma,\delta,(q^1_0,q^2_0),F^{\cup}) $$

dove:

$$ \delta((p_1,p_2),a)=(\delta_1(p_1,a),\delta_2(p_2,a)) $$

e:

$$ F^{\cup}=(F_1\times Q_2)\cup(Q_1\times F_2). $$

Prendiamo una parola infinita:

$$ \alpha=a_0a_1a_2\cdots. $$

Poiche' gli automi sono deterministici, su $\alpha$ esistono tre run uniche:

$$ \rho_1=p^1_0p^1_1p^1_2\cdots, $$

$$ \rho_2=p^2_0p^2_1p^2_2\cdots, $$

e:

$$ \rho=(p^1_0,p^2_0)(p^1_1,p^2_1)(p^1_2,p^2_2)\cdots. $$

La run prodotto visita $F^{\cup}$ infinitamente spesso se e solo se:

$$ \exists^\omega i\; p^1_i\in F_1 $$

oppure:

$$ \exists^\omega i\; p^2_i\in F_2. $$

La prima condizione significa $\alpha\in L(\mathcal{A}_1)$; la seconda significa $\alpha\in L(\mathcal{A}_2)$.

Quindi:

$$ L(\mathcal{A}^{\cup})=L(\mathcal{A}_1)\cup L(\mathcal{A}_2). $$

Intersezione

Per l'intersezione non basta prendere:

$$ F_1\times F_2. $$

Motivo: puo' succedere che $\mathcal{A}_1$ visiti $F_1$ infinitamente spesso e $\mathcal{A}_2$ visiti $F_2$ infinitamente spesso, ma mai nello stesso momento.

Costruiamo allora un automa che alterna due obblighi:

1. vedere un finale di $\mathcal{A}_1$;
2. poi vedere un finale di $\mathcal{A}_2$;
3. poi ricominciare.

Definiamo:

$$ \mathcal{A}^{\cap}=(Q_1\times Q_2\times\{1,2\},\Sigma,\delta, (q^1_0,q^2_0,1),F^{\cap}). $$

Il terzo componente indica quale finale stiamo aspettando.

Dato uno stato $(p_1,p_2,t)$ e una lettera $a$, poniamo:

$$ p'_1=\delta_1(p_1,a),\qquad p'_2=\delta_2(p_2,a). $$

Il nuovo turno $t'$ viene deciso guardando lo stato corrente, prima di consumare la prossima lettera.

$$ t'=2\quad\text{se }t=1\text{ e }p_1\in F_1. $$

Se invece $t=2$ e $p_2\in F_2$, poniamo:

$$ t'=1. $$

In tutti gli altri casi poniamo:

$$ t'=t. $$

e:

$$ \delta((p_1,p_2,t),a)=(p'_1,p'_2,t'). $$

Scegliamo come finali gli stati in cui stiamo aspettando il secondo automa e lo abbiamo appena visto finale:

$$ F^{\cap}=Q_1\times F_2\times\{2\}. $$

Correttezza: se il prodotto accetta, entrambi accettano

Supponiamo:

$$ \alpha\in L(\mathcal{A}^{\cap}). $$

Allora accettare significa visitare infinitamente spesso stati in cui:

1. si sta aspettando $\mathcal{A}_2$;
2. il componente di $\mathcal{A}_2$ e' finale.

Ogni visita a $F^{\cap}$ produce, al passo successivo di aggiornamento, il ritorno al turno $1$.

Per tornare poi al turno $2$ serve una nuova visita a uno stato con primo componente in $F_1$.

Quindi:

$$ \exists^\omega i\; p^1_i\in F_1 $$

e:

$$ \exists^\omega i\; p^2_i\in F_2. $$

Dunque:

$$ \alpha\in L(\mathcal{A}_1)\cap L(\mathcal{A}_2). $$

Correttezza: se entrambi accettano, il prodotto accetta

Supponiamo ora:

$$ \alpha\in L(\mathcal{A}_1)\cap L(\mathcal{A}_2). $$

Allora:

$$ \exists^\omega i\; p^1_i\in F_1 $$

e:

$$ \exists^\omega i\; p^2_i\in F_2. $$

Quando il prodotto e' in turno $1$, prima o poi il primo componente entra in $F_1$, quindi il turno passa a $2$.

Quando il prodotto e' in turno $2$, prima o poi il secondo componente entra in $F_2$, quindi viene visitato uno stato di:

$$ Q_1\times F_2\times\{2\} $$

e poi il turno torna a $1$.

Poiche' entrambe le visite finali accadono infinite volte, questo ciclo si ripete infinite volte.

Quindi $\mathcal{A}^{\cap}$ visita $F^{\cap}$ infinitamente spesso e accetta $\alpha$.

Conclusione:

$$ L(\mathcal{A}^{\cap})=L(\mathcal{A}_1)\cap L(\mathcal{A}_2). $$

Punto orale: per l'unione basta il prodotto diretto; per l'intersezione serve ricordare quale dei due finali e' gia' stato visto nel ciclo corrente.

23. Automi di Muller: da Büchi, complemento e operazioni booleane

Un automa di Muller deterministico e':

$$ \mathcal{M}=(Q,\Sigma,\delta,q_0,\mathcal{F}) $$

dove:

$$ \mathcal{F}\subseteq 2^Q. $$

Su una parola infinita $\alpha$, la run deterministica e':

$$ \rho=q_0q_1q_2\cdots. $$

Definiamo:

$$ Inf(\rho)=\{q\in Q\mid \exists^\omega i\; q_i=q\}. $$

La condizione di accettazione Muller e':

$$ \alpha\in L(\mathcal{M}) \quad\Longleftrightarrow\quad Inf(\rho)\in\mathcal{F}. $$

Ogni DBA e' un DMA

Sia:

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

un DBA.

Costruiamo il DMA:

$$ \mathcal{M}=(Q,\Sigma,\delta,q_0,\mathcal{F}) $$

dove:

$$ \mathcal{F}=\{P\subseteq Q\mid P\cap F\neq\emptyset\}. $$

Le due macchine hanno stessa struttura, quindi su ogni parola $\alpha$ hanno la stessa run $\rho$.

Il DBA accetta se e solo se visita qualche stato finale infinite volte:

$$ \exists q\in F\;\exists^\omega i\;q_i=q. $$

Questa condizione equivale a:

$$ Inf(\rho)\cap F\neq\emptyset. $$

Per definizione di $\mathcal{F}$:

$$ Inf(\rho)\cap F\neq\emptyset \quad\Longleftrightarrow\quad Inf(\rho)\in\mathcal{F}. $$

Quindi:

$$ L(\mathcal{A})=L(\mathcal{M}). $$

Ogni NBA e' un NMA

La stessa idea funziona per gli automi non deterministici.

Sia:

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

un NBA.

Costruiamo:

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

con:

$$ \mathcal{F}=\{P\subseteq Q\mid P\cap F\neq\emptyset\}. $$

Ora una parola $\alpha$ e' accettata dall'NBA se e solo se esiste una run $\rho$ su $\alpha$ tale che:

$$ Inf(\rho)\cap F\neq\emptyset. $$

Per la definizione di $\mathcal{F}$, cio' equivale a dire che esiste una run $\rho$ tale che:

$$ Inf(\rho)\in\mathcal{F}. $$

Questa e' esattamente la condizione di accettazione dell'NMA.

Quindi:

$$ L(\mathcal{A})=L(\mathcal{M}). $$

Complemento dei Muller deterministici

Sia:

$$ \mathcal{M}=(Q,\Sigma,\delta,q_0,\mathcal{F}) $$

un DMA che riconosce $L$.

Costruiamo:

$$ \overline{\mathcal{M}}=(Q,\Sigma,\delta,q_0,2^Q\setminus\mathcal{F}). $$

Prendiamo una parola $\alpha$ e sia $\rho$ la sua unica run.

Allora:

$$ \alpha\in L(\overline{\mathcal{M}}) \quad\Longleftrightarrow\quad Inf(\rho)\in 2^Q\setminus\mathcal{F} $$

cioe':

$$ \alpha\in L(\overline{\mathcal{M}}) \quad\Longleftrightarrow\quad Inf(\rho)\notin\mathcal{F}. $$

Ma:

$$ Inf(\rho)\notin\mathcal{F} \quad\Longleftrightarrow\quad \alpha\notin L(\mathcal{M}). $$

Quindi:

$$ L(\overline{\mathcal{M}})=\Sigma^\omega\setminus L(\mathcal{M}). $$

Punto orale: qui il determinismo e' essenziale. Se ci fossero piu run, complementare la famiglia $\mathcal{F}$ non basterebbe, perche' l'accettazione esistenziale delle run cambierebbe il quantificatore.

Unione e intersezione dei Muller deterministici

Siano:

$$ \mathcal{M}_1=(Q_1,\Sigma,\delta_1,q^1_0,\mathcal{F}_1) $$

e:

$$ \mathcal{M}_2=(Q_2,\Sigma,\delta_2,q^2_0,\mathcal{F}_2). $$

Costruiamo il prodotto deterministico:

$$ \mathcal{P}=(Q_1\times Q_2,\Sigma,\delta,(q^1_0,q^2_0),\mathcal{F}) $$

con:

$$ \delta((p_1,p_2),a)=(\delta_1(p_1,a),\delta_2(p_2,a)). $$

Se $\rho$ e' la run prodotto, allora:

$$ Inf(\rho)\subseteq Q_1\times Q_2. $$

Le proiezioni soddisfano:

$$ \pi_1(Inf(\rho))=Inf(\rho_1) $$

e:

$$ \pi_2(Inf(\rho))=Inf(\rho_2). $$

Dimostriamo la prima uguaglianza; la seconda e' identica.

Se $p\in \pi_1(Inf(\rho))$, allora esiste $r\in Q_2$ tale che $(p,r)$ compare infinite volte nella run prodotto. Quindi $p$ compare infinite volte nella prima componente, cioe' $p\in Inf(\rho_1)$.

Viceversa, se $p\in Inf(\rho_1)$, allora $p$ compare infinite volte nella prima componente. Ogni volta che compare, la seconda componente ha uno dei finitemente molti valori di $Q_2$. Per il principio dei cassetti, esiste $r\in Q_2$ tale che $(p,r)$ compare infinite volte nella run prodotto. Quindi $p\in \pi_1(Inf(\rho))$.

Per l'intersezione scegliamo:

$$ \mathcal{F}_\cap=\{R\subseteq Q_1\times Q_2\mid \pi_1(R)\in\mathcal{F}_1 \text{ e } \pi_2(R)\in\mathcal{F}_2\}. $$

Allora:

$$ Inf(\rho)\in\mathcal{F}_\cap $$

se e solo se:

$$ Inf(\rho_1)\in\mathcal{F}_1 \quad\text{e}\quad Inf(\rho_2)\in\mathcal{F}_2. $$

Dunque:

$$ L(\mathcal{P})=L(\mathcal{M}_1)\cap L(\mathcal{M}_2). $$

Per l'unione scegliamo:

$$ \mathcal{F}_\cup=\{R\subseteq Q_1\times Q_2\mid \pi_1(R)\in\mathcal{F}_1 \text{ oppure } \pi_2(R)\in\mathcal{F}_2\}. $$

Con lo stesso ragionamento:

$$ L(\mathcal{P})=L(\mathcal{M}_1)\cup L(\mathcal{M}_2). $$

Il complemento e queste due costruzioni danno la chiusura booleana dei DMA.

24. NMA e S1S: formalizzare la condizione di Muller

Negli appunti, per mostrare che gli NMA hanno lo stesso potere espressivo degli NBA, viene suggerito il passaggio:

$$ NMA \to S1S \to NBA. $$

Il punto che viene lasciato come esercizio e' la formula S1S che esprime la condizione di accettazione Muller.

Sia:

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

un NMA, con:

$$ Q=\{q_0,\ldots,q_m\}. $$

Come nella traduzione automa $\to$ S1S, usiamo variabili monadiche:

$$ Y_0,\ldots,Y_m $$

dove:

$$ Y_i(x) $$

significa: nella posizione $x$ della run siamo nello stato $q_i$.

Le formule di partizione e transizione sono le stesse gia' viste per Büchi:

1. in ogni posizione c'e' esattamente uno stato;
2. in posizione $0$ c'e' lo stato iniziale;
3. le posizioni consecutive rispettano la relazione di transizione.

Resta solo la condizione Muller.

Stati visti infinite volte e finite volte

Per dire che $q_i$ compare infinite volte:

$$ Inf_i(Y_i)\;:=\;\forall x\,\exists y\,(x<y\wedge Y_i(y)). $$

Questa formula dice: dopo ogni posizione $x$ esiste una posizione successiva $y$ in cui la run e' in $q_i$.

Per dire che $q_i$ compare solo finitemente molte volte:

$$ Fin_i(Y_i)\;:=\;\exists x\,\forall y\,(x<y\to \neg Y_i(y)). $$

Questa formula dice: esiste una soglia $x$ dopo la quale $q_i$ non compare piu.

Formula per un insieme Muller fissato

Sia:

$$ P\subseteq Q. $$

Vogliamo esprimere:

$$ Inf(\rho)=P. $$

La formula e':

$$ Exact_P(Y_0,\ldots,Y_m) := \left(\bigwedge_{q_i\in P} Inf_i(Y_i)\right) \wedge \left(\bigwedge_{q_i\notin P} Fin_i(Y_i)\right). $$

Dimostriamo che e' corretta.

Se una run $\rho$ soddisfa $Exact_P$, allora:

• ogni stato in $P$ compare infinite volte;
• ogni stato fuori da $P$ compare solo finitemente molte volte.

Quindi gli stati che compaiono infinite volte sono esattamente quelli di $P$:

$$ Inf(\rho)=P. $$

Viceversa, se $Inf(\rho)=P$, allora ogni $q_i\in P$ compare infinite volte e ogni $q_i\notin P$ non compare infinite volte. Poiche' la run e' indicizzata su $\omega$, "non compare infinite volte" equivale a "compare solo finitemente molte volte". Quindi la run soddisfa $Exact_P$.

Formula Muller completa

La condizione di accettazione Muller e':

$$ Inf(\rho)\in\mathcal{F}. $$

La traduciamo come:

$$ \varphi_{Muller}(Y_0,\ldots,Y_m) := \bigvee_{P\in\mathcal{F}} Exact_P(Y_0,\ldots,Y_m). $$

Questa e' una formula finita perche' $Q$ e' finito, quindi anche $\mathcal{F}\subseteq 2^Q$ e' finita.

Conclusione:

$$ \exists Y_0\cdots\exists Y_m (\varphi_{partizione}\wedge\varphi_{iniziale}\wedge\varphi_{transizione}\wedge\varphi_{Muller}) $$

definisce esattamente le parole accettate dall'NMA.

Poiche' ogni linguaggio S1S e' riconoscibile da un automa di Büchi, otteniamo:

$$ NMA\subseteq NBA. $$

Insieme alla costruzione $NBA\subseteq NMA$ della sezione precedente:

$$ NMA\equiv NBA. $$

Punto orale: se ti chiedono il passaggio lasciato come esercizio negli appunti, devi scrivere $Exact_P$ e poi fare la disgiunzione su tutti i $P\in\mathcal{F}$.

25. Giochi di raggiungibilita': attractor e strategie posizionali

Negli appunti il teorema e':

un reachability game e' determinato, le regioni vincenti sono computabili e le strategie vincenti posizionali sono computabili.

Definizione

Un gioco di raggiungibilita' e':

$$ G=(Q,Q_A,E,F) $$

dove:

• $Q$ e' l'insieme finito degli stati;
• $Q_A\subseteq Q$ sono gli stati controllati dal giocatore $A$;
• $Q_B=Q\setminus Q_A$ sono gli stati controllati dal giocatore $B$;
• $E\subseteq Q\times Q$ e' la relazione delle mosse;
• $F\subseteq Q$ e' il target.

Il giocatore $B$ vince una partita se prima o poi viene visitato uno stato di $F$.

Assumiamo che ogni stato abbia almeno una mossa uscente.

Attractor di B

Definiamo per induzione:

$$ Attr^B_0(F)=F. $$

Poi:

$$ Attr^B_{i+1}(F)=Attr^B_i(F) \cup \{q\in Q_B\mid \exists q'\,(E(q,q')\wedge q'\in Attr^B_i(F))\} $$

$$ \cup \{q\in Q_A\mid \forall q'\,(E(q,q')\to q'\in Attr^B_i(F))\}. $$

Interpretazione:

• se lo stato e' di $B$, basta una mossa verso l'attractor;
• se lo stato e' di $A$, tutte le mosse possibili devono andare nell'attractor.

La sequenza:

$$ Attr^B_0(F)\subseteq Attr^B_1(F)\subseteq Attr^B_2(F)\subseteq\cdots $$

e' crescente.

Poiche' $Q$ e' finito, si stabilizza entro al piu' $|Q|$ passi.

Definiamo:

$$ Attr^B(F)=\bigcup_{i\ge 0}Attr^B_i(F). $$

Se uno stato e' nell'attractor, B vince

Per ogni stato $q\in Attr^B(F)$ definiamo il rango:

$$ r(q)=\min\{i\mid q\in Attr^B_i(F)\}. $$

Se $r(q)=0$, allora $q\in F$ e $B$ ha gia' vinto.

Se $r(q)>0$ e $q\in Q_B$, per definizione di attractor esiste una mossa:

$$ q\to q' $$

con:

$$ q'\in Attr^B_{r(q)-1}(F). $$

B sceglie una di queste mosse. Il rango diminuisce.

Se $r(q)>0$ e $q\in Q_A$, per definizione tutte le mosse di $A$ portano in:

$$ Attr^B_{r(q)-1}(F). $$

Quindi, qualunque scelta faccia $A$, il rango diminuisce.

Il rango e' un numero naturale e diminuisce strettamente finche' non si arriva a $0$.

Dunque in un numero finito di passi si raggiunge $F$.

La strategia di $B$ dipende solo dallo stato corrente: e' quindi posizionale.

Se uno stato e' fuori dall'attractor, A vince

Sia:

$$ C=Q\setminus Attr^B(F). $$

Mostriamo che da ogni stato in $C$, il giocatore $A$ puo' evitare per sempre $F$.

Prima osservazione:

$$ C\cap F=\emptyset, $$

perche' $F=Attr^B_0(F)\subseteq Attr^B(F)$.

Seconda osservazione: $C$ e' chiuso rispetto al gioco nel senso favorevole ad $A$.

Se $q\in C\cap Q_A$, non puo' essere vero che tutte le mosse da $q$ vadano in $Attr^B(F)$; altrimenti $q$ entrerebbe nell'attractor al passo successivo. Quindi esiste almeno una mossa:

$$ q\to q' $$

con:

$$ q'\in C. $$

A sceglie una di queste mosse.

Se $q\in C\cap Q_B$, non puo' esistere una mossa da $q$ verso $Attr^B(F)$; altrimenti, essendo $q$ controllato da $B$, $q$ entrerebbe nell'attractor. Quindi tutte le mosse di $B$ restano in $C$.

Pertanto, se la partita parte in $C$, $A$ puo' mantenerla per sempre in $C$.

Poiche' $C$ non contiene stati target, $F$ non viene mai raggiunto.

Quindi $A$ vince da ogni stato fuori dall'attractor.

Conclusione:

$$ W_B=Attr^B(F) $$

e:

$$ W_A=Q\setminus Attr^B(F). $$

Il gioco e' determinato e le strategie vincenti sono posizionali.

26. Weak Muller games come weak parity games

Negli appunti compare la trasformazione:

una condizione weak Muller puo' essere espressa con una condizione weak parity usando l'appearance record.

Qui formalizziamo il caso weak, quello in cui la condizione dipende da:

$$ Occ(\rho)=\{q\in Q\mid q\text{ compare almeno una volta in }\rho\}. $$

Il giocatore $B$ vince se:

$$ Occ(\rho)\in\mathcal{F}. $$

Appearance record weak

Dato un prefisso finito:

$$ q_0q_1\cdots q_i, $$

definiamo:

$$ R_i=\{q_0,\ldots,q_i\}. $$

La sequenza:

$$ R_0\subseteq R_1\subseteq R_2\subseteq\cdots $$

e' crescente e ogni $R_i$ e' un sottoinsieme di $Q$.

Poiche' $Q$ e' finito, la sequenza si stabilizza.

Il limite e':

$$ \bigcup_{i\ge 0}R_i=Occ(\rho). $$

Anzi, esiste un indice $N$ tale che per ogni $i\ge N$:

$$ R_i=Occ(\rho). $$

Colorazione

Associamo a ogni record $R\subseteq Q$ un colore:

$$ c(R)=2|R|\quad\text{se }R\in\mathcal{F}. $$

Se invece $R\notin\mathcal{F}$, poniamo:

$$ c(R)=2|R|-1. $$

La parita' del colore dice se $R$ e' vincente:

$$ c(R)\text{ e' pari} \quad\Longleftrightarrow\quad R\in\mathcal{F}. $$

La grandezza del colore cresce con $|R|$.

Poiche' $R_i$ e' crescente per inclusione, anche $|R_i|$ e' non decrescente.

Dopo l'indice $N$, tutti i record sono uguali a $Occ(\rho)$, quindi tutti i colori sono uguali a:

$$ c(Occ(\rho)). $$

Il massimo colore che compare infinitamente spesso e' dunque:

$$ c(Occ(\rho)). $$

Quindi:

$$ Occ(\rho)\in\mathcal{F} $$

se e solo se:

$$ c(Occ(\rho))\text{ e' pari} $$

se e solo se:

$$ \text{il massimo colore visto infinitamente spesso e' pari.} $$

Questa e' esattamente una condizione di parita'.

Punto orale: nel caso weak basta ricordare l'insieme degli stati gia' visti; nel caso Muller pieno serve il LAR, perche' la condizione dipende dagli stati visti infinite volte, non solo almeno una volta.

27. Da Muller a parity con LAR

Per una condizione di Muller piena, il giocatore $B$ vince una play infinita:

$$ \rho=q_0q_1q_2\cdots $$

se:

$$ Inf(\rho)\in\mathcal{F}. $$

Qui:

$$ Inf(\rho)=\{q\in Q\mid q\text{ compare infinite volte in }\rho\}. $$

Il problema e' che $Inf(\rho)$ non si ottiene guardando solo gli stati gia' apparsi: bisogna distinguere gli stati che appaiono solo finitamente da quelli che tornano per sempre.

Il LAR, Latest Appearance Record, serve a fare questa distinzione con memoria finita.

Stato LAR

Uno stato LAR contiene:

1. una lista senza ripetizioni di stati di $Q$, ordinata per ultima apparizione;
2. un numero $h$, detto hit.

Quando si legge un nuovo stato $q$:

• se $q$ non e' nella lista, lo si mette in testa e si pone $h=0$;
• se $q$ era nella posizione $h>0$, lo si sposta in testa e si registra quell'hit $h$.

Se prima dell'aggiornamento la lista era:

$$ i_1i_2\cdots i_r $$

e $q=i_h$, allora l'hitting set e':

$$ H=\{i_1,\ldots,i_h\}. $$

Intuitivamente, $H$ e' l'insieme degli stati visti dall'ultima occorrenza precedente di $q$ fino alla nuova occorrenza di $q$.

Lemma chiave

Sia $\rho$ una play infinita e sia:

$$ I=Inf(\rho). $$

Dopo un certo prefisso:

• tutti gli stati fuori da $I$ non compaiono piu;
• tutti gli stati in $I$ continuano a comparire.

Da quel punto in poi, la parte rilevante della lista LAR e' formata esattamente dagli stati di $I$, ordinati per ultima apparizione.

Sia:

$$ k=|I|. $$

Dimostriamo che il massimo hit che compare infinite volte e' $k$, e che l'hitting set corrispondente e' proprio $I$.

Il massimo hit infinito non puo' superare k

Dopo il prefisso in cui gli stati fuori da $I$ non compaiono piu, ogni nuovo hit riguarda uno stato di $I$.

Tra gli stati che continuano ad apparire, ce ne sono solo $k$.

Quindi un hit che compare infinite volte non puo' avere valore maggiore di $k$.

Eventuali hit maggiori possono avvenire solo finitamente molte volte, prima che gli stati fuori da $I$ scompaiano definitivamente.

L'hit k compare infinite volte

Dopo il prefisso stabile, considera in ogni momento lo stato di $I$ la cui ultima apparizione e' piu vecchia.

Quando quello stato ricompare, prima della ricomparsa tutti gli altri stati di $I$ sono apparsi piu recentemente.

Quindi, nella lista LAR, quello stato occupa la posizione $k$ tra gli stati di $I$.

Al suo ritorno si genera un hit $k$.

Poiche' ogni stato di $I$ compare infinite volte, questa situazione si ripete infinite volte.

Dunque l'hit $k$ compare infinite volte.

L'hitting set dell'hit k e' I

Quando avviene un hit $k$ dopo il prefisso stabile, l'hitting set contiene i primi $k$ stati della lista rilevante.

Questi sono esattamente gli stati di $I$.

Quindi:

$$ H=I. $$

Colorazione parity

Per ogni LAR con hit $h=0$, poniamo:

$$ c=0. $$

Per ogni LAR con hit $h>0$ e hitting set $H$, poniamo:

$$ c=2h\quad\text{se }H\in\mathcal{F}, $$

e:

$$ c=2h-1\quad\text{se }H\notin\mathcal{F}. $$

Sia $k=|Inf(\rho)|$.

Dal lemma, il massimo hit che compare infinitamente spesso e' $k$ e l'hitting set associato a quell'hit e':

$$ Inf(\rho). $$

Quindi il massimo colore che compare infinitamente spesso e':

$$ 2k\quad\text{se }Inf(\rho)\in\mathcal{F}, $$

e:

$$ 2k-1\quad\text{se }Inf(\rho)\notin\mathcal{F}. $$

Pertanto:

$$ Inf(\rho)\in\mathcal{F} $$

se e solo se:

$$ \text{il massimo colore che compare infinitamente spesso e' pari.} $$

Questa e' la condizione di parita'.

Conclusione: un Muller game puo' essere simulato da un parity game usando una memoria finita LAR.

Il numero di possibili LAR e' finito, dell'ordine di:

$$ |Q|!\cdot |Q|. $$

Punto orale: il LAR non serve a "ricordare tutto il passato"; serve a isolare, tramite il massimo hit che ricorre infinite volte, l'insieme degli stati visti infinite volte.