Chiusure e closure: dimostrazioni complete

Questa pagina raccoglie, in forma studiabile per l'orale, tutte le "closure" che compaiono negli appunti. Ho separato due usi diversi della parola:

1. chiusura come proprieta' di una classe di linguaggi: parto da oggetti della classe e, dopo un'operazione, resto nella stessa classe;
2. closure come insieme generato da una costruzione: epsilon-closure, closure LTL, chiusura della tabella in L*.

Fonti locali principali: formal_proofs.md, expansions/week01_finite_automata_deepening.md, expansions/week03_infinite_automata_deepening.md, expansions/week03_mso_s1s_deepening.md, expansions/week04_model_checking_procedures_deepening.md, raw/Automi a stati finiti su parole finite.md, raw/Automi a stati finiti su parole infinite.md, raw/Linear Temporal Logic.md e concepts/Closure_by_Projection.md.

Mappa rapida

1. Che cosa significa "essere chiusi"

Una classe $\mathcal{C}$ e' chiusa rispetto a un'operazione $\circ$ quando, se prendo elementi della classe e applico l'operazione, il risultato appartiene ancora alla classe.

Esempio:

$$ L_1,L_2\in\mathcal{C} \quad\Longrightarrow\quad L_1\cup L_2\in\mathcal{C}. $$

Per dimostrarlo in automata theory si fa quasi sempre una dimostrazione costruttiva:

1. assumo di avere automi per i linguaggi di partenza;
2. costruisco un nuovo automa per il linguaggio ottenuto;
3. dimostro le due inclusioni, cioe' che il nuovo automa accetta esattamente quello che deve accettare.

Il punto da ricordare e' che "chiuso" non significa "l'operazione e' banale": per il complemento degli NBA, ad esempio, la chiusura vale ma la costruzione e' tecnica.

2. Linguaggi regolari finiti

Siano $L_1,L_2\subseteq\Sigma^\ast$ linguaggi regolari.

2.1 Unione

Prendo due automi per $L_1$ e $L_2$:

$$ \mathcal{A}_1=(Q_1,\Sigma,\Delta_1,q^1_0,F_1), \qquad \mathcal{A}_2=(Q_2,\Sigma,\Delta_2,q^2_0,F_2). $$

Costruisco un epsilon-NFA con un nuovo stato iniziale $q_0$ e due epsilon-transizioni:

$$ q_0\xrightarrow{\varepsilon}q^1_0, \qquad q_0\xrightarrow{\varepsilon}q^2_0. $$

Gli stati finali sono $F_1\cup F_2$.

Correttezza. Se $w\in L_1\cup L_2$, allora $w$ e' accettata da almeno uno dei due automi. Il nuovo epsilon-NFA sceglie con una epsilon-mossa la componente giusta e segue quella run accettante.

Viceversa, se il nuovo automa accetta $w$, dopo la prima epsilon-mossa ha simulato o $\mathcal{A}_1$ o $\mathcal{A}_2$. Quindi $w$ appartiene a $L_1$ oppure a $L_2$.

Conclusione:

$$ L(\mathcal{A})=L_1\cup L_2. $$

2.2 Concatenazione

Per $L_1\cdot L_2$ collego ogni finale del primo automa all'iniziale del secondo con una epsilon-mossa:

$$ f\xrightarrow{\varepsilon}q^2_0 \qquad\text{per ogni }f\in F_1. $$

Gli stati finali del nuovo automa sono quelli del secondo automa.

Correttezza. Se $w\in L_1L_2$, allora $w=uv$ con $u\in L_1$ e $v\in L_2$. L'automa legge $u$ nella prima componente, usa l'epsilon-mossa da un finale di $\mathcal{A}_1$ all'iniziale di $\mathcal{A}_2$, poi legge $v$.

Viceversa, ogni run accettante deve prima raggiungere un finale del primo automa e poi un finale del secondo. La parola letta si spezza quindi come $uv$, con $u\in L_1$ e $v\in L_2$.

2.3 Stella di Kleene

Per $L^\ast$ aggiungo:

• una epsilon-mossa dal nuovo iniziale al nuovo finale, per accettare $\varepsilon$;
• una epsilon-mossa dal nuovo iniziale all'iniziale dell'automa di $L$;
• epsilon-mosse dai finali dell'automa di $L$ al nuovo finale;
• epsilon-mosse dai finali dell'automa di $L$ di nuovo all'iniziale, per ripetere il blocco.

Correttezza. Una run accettante sceglie zero o piu' attraversamenti dell'automa per $L$. Ogni attraversamento completo produce un blocco in $L$, quindi la parola e' in $L^\ast$.

Viceversa, se $w=u_1\cdots u_k$ con ogni $u_i\in L$, l'automa legge ogni blocco con la componente di $L$ e usa le epsilon-mosse di ritorno per cominciare il blocco successivo. Se $k=0$, usa direttamente la epsilon-mossa per $\varepsilon$.

2.4 Complemento

Qui gli appunti grezzi vanno letti con una correzione importante: non si scambiano "iniziali e finali". Si parte da un DFA completo e si scambiano finali e non finali.

Sia:

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

un DFA completo per $L$. Costruisco:

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

Per ogni parola $w$, essendo il DFA deterministico e completo, esiste una sola computazione:

$$ \hat{\delta}(q_0,w). $$

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 serve perche' nel complemento ogni parola deve essere classificata. Se una transizione manca, aggiungo prima uno stato pozzo.

2.5 Intersezione

Ci sono due prove.

Via 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 per intersezione.

Via prodotto. Prendo due DFA completi:

$$ \mathcal{A}_1=(Q_1,\Sigma,\delta_1,q^1_0,F_1), \qquad \mathcal{A}_2=(Q_2,\Sigma,\delta_2,q^2_0,F_2). $$

Costruisco:

$$ \mathcal{P}=(Q_1\times Q_2,\Sigma,\delta,(q^1_0,q^2_0),F_1\times F_2) $$

con:

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

Per induzione su $w$:

$$ \hat{\delta}((q^1_0,q^2_0),w) = (\hat{\delta}_1(q^1_0,w),\hat{\delta}_2(q^2_0,w)). $$

Dunque il prodotto e' finale se e solo se entrambe le componenti sono finali:

$$ L(\mathcal{P})=L_1\cap L_2. $$

2.6 Differenza

La differenza non e' una nuova costruzione:

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

Quindi i regolari sono chiusi per differenza perche' sono chiusi per complemento e intersezione.

3. Epsilon-closure

La epsilon-closure di uno stato $q$ in un epsilon-NFA e':

$$ E(q)=\{p\mid q\xrightarrow{\varepsilon^\ast}p\}. $$

Per un insieme di stati:

$$ E(S)=\bigcup_{q\in S}E(q). $$

Serve a eliminare le epsilon-mosse. Se:

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

e' un epsilon-NFA, costruisco un NFA senza epsilon con:

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

I finali diventano:

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

Correttezza. Prima di leggere un simbolo posso fare un numero arbitrario di epsilon-mosse; poi leggo il simbolo; poi posso fare ancora epsilon-mosse. Questa e' esattamente la definizione di $\Delta'$. I nuovi finali catturano il caso in cui, finito l'input, posso raggiungere un vecchio finale solo con epsilon-mosse.

Quindi ogni run dell'epsilon-NFA viene simulata dall'NFA e ogni passo dell'NFA corrisponde a un blocco epsilon-simbolo-epsilon dell'automa originale.

4. Chiusura della tabella in L*

Negli appunti di automata learning una tabella di osservazione ha righe indicizzate da prefissi e colonne indicizzate da suffissi. La riga di $s$ e':

$$ row(s)(e)=T(se). $$

La tabella e' chiusa quando per ogni $s\in S$ e ogni lettera $a\in\Sigma$ esiste $s'\in S$ tale che:

$$ row(sa)=row(s'). $$

Perche' serve. Gli elementi di $S$ rappresentano gli stati del DFA ipotesi. La transizione da $row(s)$ con lettera $a$ dovrebbe andare a $row(sa)$. Se $row(sa)$ non e' rappresentata da nessuna riga in $S$, la transizione uscirebbe dall'insieme degli stati ipotesi.

Dimostrazione dell'utilita'. Se la tabella e' chiusa, definisco il DFA ipotesi:

$$ Q=\{row(s)\mid s\in S\} $$

e:

$$ \delta(row(s),a)=row(sa). $$

La chiusura garantisce che $row(sa)$ e' uguale alla riga di qualche elemento di $S$, quindi $\delta$ atterra ancora in $Q$. In altre parole, la tabella chiusa rende la funzione di transizione totale sugli stati ipotesi.

La consistenza della tabella serve poi a garantire che questa definizione non dipenda dal rappresentante scelto: se $row(s_1)=row(s_2)$, allora anche $row(s_1a)=row(s_2a)$.

5. Chiusure base degli omega-regolari

Ora l'input non e' piu' una parola finita, ma una parola infinita in $A^\omega$. I linguaggi riconosciuti da NBA sono gli omega-regolari.

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

Sia $V\subseteq A^\ast$ regolare e sia:

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

un automa finito per $V$. Possiamo assumere $\varepsilon\notin V$, perche' togliere il blocco vuoto non cambia la parola infinita generata.

Costruisco un NBA che simula $\mathcal{D}$ e, ogni volta che completa un blocco di $V$, puo' tornare a $q_0$. Per ogni transizione:

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

aggiungo anche:

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

Uso $q_0$ come stato finale Büchi.

Correttezza. Se $\alpha\in V^\omega$, allora:

$$ \alpha=v_0v_1v_2\cdots $$

con ogni $v_i\in V$. L'automa legge ogni blocco simulando $\mathcal{D}$ e torna a $q_0$ alla fine di ogni blocco. Quindi visita $q_0$ infinite volte.

Viceversa, se l'NBA accetta, visita $q_0$ infinite volte. Tra due visite successive a $q_0$ ha letto un blocco non vuoto che porta un finale di $\mathcal{D}$ al reset. Ogni blocco appartiene a $V$, quindi la parola e' concatenazione infinita di blocchi di $V$.

5.2 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$.

Costruisco un NBA che:

1. simula $\mathcal{D}$ per leggere un prefisso finito;
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 Büchi quelli di $\mathcal{A}$.

Se $\alpha\in V\cdot L$, allora $\alpha=u\beta$ con $u\in V$ e $\beta\in L$. Il nuovo automa legge $u$ nella parte finita e poi segue una run accettante di $\mathcal{A}$ su $\beta$.

Viceversa, se il nuovo automa accetta, prima di entrare nella componente Büchi deve aver letto una parola di $V$; il suffisso infinito viene accettato da $\mathcal{A}$, quindi appartiene a $L$.

5.3 Unione di omega-regolari

Siano $\mathcal{A}_1$ e $\mathcal{A}_2$ NBA per $L_1$ e $L_2$.

Costruisco un nuovo NBA con un nuovo iniziale che sceglie nondeterministicamente quale automa simulare. Gli stati finali sono quelli della componente scelta.

Se una parola appartiene a $L_1\cup L_2$, esiste una run accettante in almeno uno dei due automi, e il nuovo NBA puo' sceglierla. Se il nuovo NBA accetta, ha simulato una delle due componenti con una run accettante, quindi la parola e' in $L_1$ oppure in $L_2$.

5.4 Intersezione di omega-regolari

Per gli NBA il prodotto con finali $F_1\times F_2$ non basta: le due componenti possono visitare i propri finali infinite volte in istanti diversi.

La costruzione corretta passa da un GNBA.

Siano:

$$ \mathcal{A}_1=(Q_1,A,\Delta_1,q^1_0,F_1), \qquad \mathcal{A}_2=(Q_2,A,\Delta_2,q^2_0,F_2). $$

Costruisco 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 e' accettante se visita infinite volte entrambi gli insiemi della famiglia.

Correttezza. Se $\alpha$ e' accettata da entrambi gli automi, prendo due run accettanti e le metto in prodotto. La run prodotto visita infinite volte $F_1\times Q_2$ perche' la prima componente visita $F_1$ infinite volte, e visita infinite volte $Q_1\times F_2$ perche' la seconda visita $F_2$ infinite volte.

Viceversa, se il GNBA accetta, proietto la run prodotto sulle due componenti. La prima proiezione e' una run accettante di $\mathcal{A}_1$, la seconda e' una run accettante di $\mathcal{A}_2$.

Un GNBA si riconverte in NBA con un contatore che aspetta ciclicamente $F_1,F_2,\ldots,F_k$. Se completa il ciclo infinite volte, ha visitato ogni insieme finale infinite volte.

5.5 Complemento degli omega-regolari

Gli omega-regolari sono chiusi per complemento, ma non basta invertire stati finali e non finali di un NBA.

La dimostrazione degli appunti usa congruenze e saturazione.

Una congruenza finita $\sim$ su $A^\ast$ satura un linguaggio $L\subseteq A^\omega$ se, per ogni coppia di classi $U,V$:

$$ UV^\omega\cap L\neq\emptyset \quad\Longrightarrow\quad UV^\omega\subseteq L. $$

I passaggi sono:

1. se $L$ e' riconosciuto da un NBA $\mathcal{A}$, si costruisce una congruenza finita $\approx_{\mathcal{A}}$ che satura $L$;
2. se una congruenza finita satura $L$, allora satura anche $\overline{L}$;
3. se una congruenza finita satura un linguaggio, quel linguaggio e' unione finita di pezzi $UV^\omega$;
4. ogni $UV^\omega$ e' omega-regolare;
5. un'unione finita di omega-regolari e' omega-regolare.

Quindi:

$$ L\text{ omega-regolare} \quad\Longrightarrow\quad \overline{L}\text{ omega-regolare}. $$

Punto da orale: il complemento Büchi esiste, ma la ragione e' globale. Bisogna controllare l'insieme delle run, non solo cambiare il nome degli stati finali.

6. DBA: unione, intersezione e non-chiusura per complemento

Un DBA e' un automa di Büchi deterministico: su ogni parola infinita ha una sola run.

6.1 Chiusura per unione

Siano:

$$ \mathcal{A}_1=(Q_1,\Sigma,\delta_1,q^1_0,F_1), \qquad \mathcal{A}_2=(Q_2,\Sigma,\delta_2,q^2_0,F_2). $$

Costruisco il prodotto deterministico:

$$ Q=Q_1\times Q_2 $$

con:

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

Per l'unione scelgo:

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

La run prodotto visita $F^\cup$ infinite volte se e solo se la prima run visita $F_1$ infinite volte oppure la seconda visita $F_2$ infinite volte. Quindi:

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

6.2 Chiusura per intersezione

Per l'intersezione il prodotto con $F_1\times F_2$ non basta, per lo stesso motivo visto per gli NBA: le visite finali possono alternarsi.

Si aggiunge un turno:

$$ Q'=Q_1\times Q_2\times\{1,2\}. $$

Il turno $1$ significa "aspetto un finale del primo automa"; il turno $2$ significa "aspetto un finale del secondo automa".

Quando vedo un finale del primo automa passo al turno $2$; quando vedo un finale del secondo passo al turno $1$. Accetto se completo questo ciclo infinite volte, ad esempio scegliendo come finali:

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

Correttezza. Se entrambe le componenti sono accettanti, allora vedo infinitamente spesso finali del primo e del secondo automa. Il turno riesce a completare il ciclo $1\to2\to1$ infinite volte.

Viceversa, se il prodotto con turno accetta, il ciclo viene completato infinite volte. Per completarlo infinite volte devo aver visto infinite volte finali della prima componente e infinite volte finali della seconda. Quindi la parola appartiene a entrambi i linguaggi.

6.3 I DBA non sono chiusi per complemento

Uso la caratterizzazione degli appunti:

$$ L\text{ e' riconosciuto da un DBA} \iff L=\overrightarrow{W} $$

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

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

Considero:

$$ L_{fin}= \{\alpha\in\{a,b\}^\omega\mid \alpha\text{ contiene solo finite }a\}. $$

Questo linguaggio e' riconoscibile da un NBA: l'automa indovina il punto dopo l'ultima $a$ e poi accetta solo $b$.

Mostro che non e' riconoscibile da DBA. Suppongo per assurdo:

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

per un regolare $W$.

La parola $b^\omega$ appartiene a $L_{fin}$, quindi ha infiniti prefissi in $W$. Scelgo $m_0$ con:

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

Anche $b^{m_0}ab^\omega$ appartiene a $L_{fin}$, quindi scelgo $m_1$ con:

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

Ripetendo, costruisco:

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

La parola $\beta$ contiene infinite $a$, quindi non appartiene a $L_{fin}$. Pero' per costruzione ha infiniti prefissi in $W$, quindi:

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

contraddizione.

Il complemento di $L_{fin}$ e' il linguaggio delle parole con infinite $a$, che e' riconoscibile da un DBA semplice: uno stato finale viene visitato ogni volta che si legge $a$. Se i DBA fossero chiusi per complemento, anche $L_{fin}$ sarebbe riconoscibile da DBA. Contraddizione.

7. Muller deterministici

Un automa di Muller deterministico e':

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

dove $\mathcal{F}\subseteq 2^Q$. Su una run unica $\rho$ si guarda:

$$ Inf(\rho)=\{q\in Q\mid q\text{ compare infinite volte in }\rho\}. $$

La parola e' accettata se:

$$ Inf(\rho)\in\mathcal{F}. $$

7.1 Complemento

Se $\mathcal{M}$ riconosce $L$, costruisco:

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

La run e' la stessa, perche' l'automa e' deterministico. Allora:

$$ \alpha\in L(\overline{\mathcal{M}}) \iff Inf(\rho)\in 2^Q\setminus\mathcal{F} \iff Inf(\rho)\notin\mathcal{F} \iff \alpha\notin L(\mathcal{M}). $$

Quindi i Muller deterministici sono chiusi per complemento.

7.2 Unione e intersezione

Per due Muller deterministici costruisco il prodotto:

$$ Q=Q_1\times Q_2. $$

Se $\rho$ e' la run prodotto, allora:

$$ \pi_1(Inf(\rho))=Inf(\rho_1), \qquad \pi_2(Inf(\rho))=Inf(\rho_2). $$

La prova usa il fatto che gli stati sono finiti: se uno stato $p$ compare infinite volte nella prima componente, allora tra le molte ma finite possibili seconde componenti ce n'e' una che compare infinite volte insieme a $p$.

Per l'intersezione scelgo:

$$ \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\}. $$

Per l'unione scelgo:

$$ \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 queste famiglie:

$$ L(\mathcal{P}_\cap)=L(\mathcal{M}_1)\cap L(\mathcal{M}_2), \qquad L(\mathcal{P}_\cup)=L(\mathcal{M}_1)\cup L(\mathcal{M}_2). $$

8. Chiusura per proiezione in S1S

Questa e' la closure che collega direttamente quantificazione esistenziale e automi.

Una tupla di variabili monadiche:

$$ X_1,\ldots,X_n $$

si puo' codificare come una parola infinita su:

$$ \{0,1\}^n. $$

Alla posizione $k$, il bit $i$ vale $1$ se e solo se $k\in X_i$.

Supponiamo che una formula:

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

definisca un omega-linguaggio $L(\varphi)$ riconosciuto da:

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

Voglio eliminare $X_i$:

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

Sul lato automi, cancello la componente $i$ da ogni simbolo. Sia $\pi_i$ la proiezione che elimina quel bit. Costruisco:

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

con:

$$ (p,c,q)\in\Delta' \iff \exists b\in\{0,1\}^n \text{ tale che } \pi_i(b)=c \text{ e } (p,b,q)\in\Delta. $$

Correttezza.

Se $\beta$ e' accettata da $\mathcal{A}'$, ogni transizione usata su $\beta(k)$ esiste perche' c'e' almeno una lettera completa $b_k$ che proietta su $\beta(k)$. Scegliendo un tale $b_k$ per ogni posizione ottengo una parola completa $\alpha$ con $\pi_i(\alpha)=\beta$. La stessa run accetta $\alpha$ in $\mathcal{A}$.

Viceversa, se $\beta=\pi_i(\alpha)$ per una parola completa $\alpha$ accettata da $\mathcal{A}$, ogni transizione di $\mathcal{A}$ su $\alpha(k)$ induce una transizione di $\mathcal{A}'$ su $\pi_i(\alpha(k))$. La stessa run accetta $\beta$.

Conclusione:

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

Quindi la proiezione di un omega-regolare e' omega-regolare. In logica:

$$ \exists X_i $$

corrisponde a nascondere la componente $X_i$ e lasciare che il nondeterminismo dell'automa indovini i bit nascosti posizione per posizione.

9. Star-free

Nei tuoi appunti i linguaggi star-free sono descritti usando:

• unione;
• concatenazione;
• complemento;
• linguaggi base.

Non usano la stella di Kleene. La chiusura per queste tre operazioni e' quindi quasi sintattica.

Dimostrazione per induzione strutturale. Definisco la classe star-free come la piu' piccola classe che contiene i linguaggi base ed e' chiusa per unione, concatenazione e complemento. Se $E_1$ ed $E_2$ sono espressioni star-free, allora anche:

$$ E_1\cup E_2, \qquad E_1E_2, \qquad \overline{E_1} $$

sono espressioni star-free per definizione della grammatica. Quindi il linguaggio denotato resta nella classe star-free.

Il collegamento con il primo ordine si dimostra poi traducendo queste operazioni in connettivi logici e tagli di posizione.

10. Closure LTL della formula

Qui "closure" non significa proprieta' di chiusura di una classe, ma insieme finito di formule necessario per costruire gli atomi del tableau.

Dato una formula LTL $\varphi$, la closure $cl(\varphi)$ contiene:

1. $\varphi$;
2. tutte le sottoformule di $\varphi$;
3. le negazioni delle formule rilevanti;
4. le espansioni temporali necessarie, ad esempio per $U$, $F$, $G$ e $X$, secondo le regole usate nel tableau.

Esempio: se la formula contiene:

$$ G(p\to Fq), $$

la closure contiene almeno:

$$ G(p\to Fq),\quad p\to Fq,\quad p,\quad Fq,\quad q, $$

e le negazioni necessarie.

Dimostrazione: la closure LTL e' finita

La formula $\varphi$ e' una stringa finita. Quindi ha un numero finito di sottoformule. Per ogni sottoformula aggiungo al massimo un numero finito di oggetti: la negazione e, per gli operatori temporali, le formule di espansione che compaiono nella regola del tableau.

Una unione finita di insiemi finiti e' finita. Dunque:

$$ cl(\varphi)\text{ e' finita}. $$

Questo e' il passaggio che rende il tableau un grafo finito: gli atomi sono sottoinsiemi coerenti di $cl(\varphi)$, quindi ce ne sono al massimo $2^{|cl(\varphi)|}$.

Atomi e coerenza

Un atomo decide, per ogni formula nella closure, se tenerla o tenerne la negazione, rispettando le regole booleane:

• non contiene sia $\psi$ sia $\neg\psi$;
• contiene $\psi\land\theta$ se e solo se contiene entrambe;
• contiene $\psi\lor\theta$ se contiene almeno una delle due;
• rispetta le espansioni temporali.

La closure e' quindi la base finita su cui il tableau ragiona; gli atomi sono le fotografie coerenti di una posizione temporale.

11. Chiusura di un ramo nei tableaux proposizionali

Negli appunti sui tableaux compare anche la chiusura di un ramo. Un ramo si chiude quando contiene una contraddizione esplicita:

$$ \psi \quad\text{e}\quad \neg\psi. $$

Perche' e' corretto chiudere il ramo. Un ramo rappresenta un tentativo di costruire un modello in cui tutte le formule del ramo siano vere simultaneamente. Nessuna interpretazione puo' rendere vera sia $\psi$ sia $\neg\psi$. Quindi quel ramo non puo' produrre un modello e puo' essere eliminato.

Per satisfiability, una formula e' soddisfacibile se resta almeno un ramo aperto e coerente. Per validity, si applica il tableau alla negazione della formula e si controlla che tutti i rami si chiudano.

12. Errori tipici da evitare all'orale

• Per il complemento dei linguaggi regolari finiti non invertire iniziali e finali: rendi il DFA completo e scambia finali/non finali.
• Per l'intersezione degli NBA non usare solo $F_1\times F_2$: servono GNBA o un contatore di obblighi.
• Per il complemento degli NBA non scambiare finali/non finali: la chiusura esiste ma passa da una costruzione globale.
• Per i DBA ricorda la differenza: chiusi per unione e intersezione, non per complemento.
• Per Muller deterministico il complemento e' facile perche' la run e' unica: basta complementare la famiglia $\mathcal{F}$.
• Per S1S, $\exists X$ non "butta via" un vincolo: chiede che esista un modo di completare la componente nascosta.
• Per closure LTL, il punto non e' semantico ma combinatorio: ottenere un insieme finito di formule su cui costruire gli atomi.