V&V in AI — Appunti

Settimana 3

✦
Indice← PrecedenteSuccessivo →
Capitolo 5

Capitolo 5 — Automi su parole infinite

Linguaggi ω-regolari; automi di Büchi (NBA vs DBA); GNBA.

Automi a stati finiti su parole infinite - Riassunto

Fonte: raw/Automi a stati finiti su parole infinite.md

Punti chiave

Concetti collegati

Automi di Büchi

Un automa di Büchi e' un automa finito che legge parole infinite, cioe' elementi di $\Sigma^\omega$. E' centrale nella verifica di sistemi reattivi, perche questi sistemi producono computazioni non terminanti.

Condizione di accettazione

Una parola infinita e' accettata se esiste una run in cui almeno uno stato finale viene visitato infinitamente spesso.

Determinismo e non determinismo

Sulle parole finite DFA e NFA hanno lo stesso potere espressivo. Sulle parole infinite, invece, gli automi di Büchi deterministici (DBA) sono strettamente meno espressivi degli automi di Büchi non deterministici (NBA).

Per recuperare determinismo pieno si usano condizioni di accettazione piu ricche, come Muller o Rabin.

Collegamenti

Automi di Büchi generalizzati

Un GNBA e' un automa di Büchi con piu insiemi di accettazione $F_1,\ldots,F_k$.

Una run e' accettante se visita infinitamente spesso almeno uno stato di ciascun insieme $F_i$.

Conversione in NBA

Un GNBA si trasforma in un NBA aggiungendo memoria finita che tiene traccia dell'insieme di accettazione attualmente da soddisfare.

Collegamenti

Linguaggi omega-regolari

I linguaggi omega-regolari estendono i linguaggi regolari alle parole infinite.

Definizione

Un omega-linguaggio puo essere definito come unione finita di espressioni del tipo: $$U\cdot V^\omega$$

dove $U$ e $V$ sono linguaggi regolari su parole finite e $V^\omega$ indica concatenazione infinita di parole di $V$.

Caratterizzazione

Sono esattamente i linguaggi riconosciuti da automi di Büchi non deterministici, e anche da automi di Muller.

Proprieta

Sono chiusi per: - unione; - intersezione; - complemento.

Collegamenti

Automi di Muller

Gli automi di Muller sono automi su parole infinite con una condizione di accettazione basata sull'insieme degli stati visitati infinitamente spesso.

Condizione di accettazione

Data una famiglia $\mathcal{F}\subseteq 2^Q$, una run e' accettante se: $$Inf(\rho)\in\mathcal{F}$$

Importanza

Gli automi di Muller deterministici sono abbastanza espressivi da riconoscere tutti gli omega-linguaggi regolari e sono chiusi per complemento in modo semplice: basta complementare la famiglia $\mathcal{F}$.

Collegamenti

Approfondimento completo settimana 3 - Automi su parole infinite e Buchi

Questa e' la versione estesa e autocontenuta del capitolo 5. Il focus e': capire perche' servono automi su parole infinite, come funziona la condizione di Buchi, perche' NBA e DBA non hanno lo stesso potere, come si usano GNBA, emptiness, parole ultimamente periodiche e automi di Muller.

Di cosa parla davvero questo capitolo

I DFA/NFA dei capitoli precedenti leggono parole finite. Una parola finita ha un ultimo simbolo: quando la lettura termina, guardo se lo stato corrente e' finale.

Nei sistemi reattivi, pero', le computazioni non terminano:

Quindi servono automi che leggono parole infinite:

$$\alpha=\alpha(0)\alpha(1)\alpha(2)\ldots$$

Il punto delicato e':

se la parola non finisce mai, cosa significa "accettare"?

Gli automi di Buchi rispondono cosi':

una run e' accettante se visita stati finali infinitamente spesso.

La mappa del capitolo e':

  1. Parte I: parole infinite e notazione.
  2. Parte II: NBA, run infinite e condizione di Buchi.
  3. Parte III: linguaggi omega-regolari ed esempi base.
  4. Parte IV: operazioni $W^\omega$ e $\overrightarrow{W}$.
  5. Parte V: chiusure e GNBA.
  6. Parte VI: espressioni omega-regolari.
  7. Parte VII: emptiness, SCC e parole ultimamente periodiche.
  8. Parte VIII: complementazione e perche' non basta invertire finali.
  9. Parte IX: DBA vs NBA.
  10. Parte X: automi di Muller.
  11. Parte XI: esercizi, errori tipici e risposta orale.

0. Richiami minimi

NFA su parole finite. Un NFA accetta una parola finita se esiste una run che, dopo aver letto tutta la parola, finisce in uno stato finale.

Sistemi reattivi. Producono computazioni infinite. Per questo non basta una condizione sullo stato "alla fine".

LTL e model checking. Le formule temporali parlano spesso di proprieta' su computazioni infinite. Gli automi di Buchi saranno il ponte fra formule LTL e verifica automatica.

Parte I - Parole infinite

1. Omega-parole

Dato un alfabeto finito $A$, una parola infinita su $A$ e' una sequenza:

$$\alpha=\alpha(0)\alpha(1)\alpha(2)\ldots$$

dove:

$$\alpha(i)\in A$$

per ogni $i\ge 0$.

L'insieme di tutte le parole infinite su $A$ e':

$$A^\omega.$$

Useremo:

2. Sottoparole e suffissi

Se:

$$n\le m,$$

allora:

$$\alpha(n,m)=\alpha(n)\alpha(n+1)\cdots\alpha(m-1)$$

e' una parola finita.

Il suffisso infinito da $n$ in poi e':

$$\alpha(n,\omega)=\alpha(n)\alpha(n+1)\alpha(n+2)\ldots$$

Questa notazione serve per parlare di cio' che accade "da un certo punto in poi".

3. Infinitamente spesso e finitamente spesso

Scriviamo:

$$\exists^\omega n.\ P(n)$$

per dire:

esistono infiniti indici $n$ tali che $P(n)$ vale.

E:

$$\exists^{<\omega} n.\ P(n)$$

per dire:

esistono solo finitamente molti indici $n$ tali che $P(n)$ vale.

Esempio:

$$\exists^\omega n.\ \alpha(n)=a$$

significa:

nella parola $\alpha$, la lettera $a$ compare infinitamente spesso.

4. L'insieme In(alpha)

Per una parola infinita $\alpha$, definiamo:

$$In(\alpha)=\{a\in A\mid \exists^\omega n.\ \alpha(n)=a\}.$$

Lettura:

$In(\alpha)$ contiene le lettere che compaiono infinitamente spesso in $\alpha$.

Poiche' $A$ e' finito e $\alpha$ e' infinita, $In(\alpha)$ non puo' essere vuoto: almeno una lettera deve ripetersi infinite volte.

Questa idea ritornera' negli automi di Muller, dove guardiamo gli stati visitati infinitamente spesso.

Parte II - Automi di Buchi non deterministici

5. Definizione di NBA

Un automa di Buchi non deterministico, NBA, e':

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

Dove:

La struttura sembra quella di un NFA. Cambia la semantica di accettazione.

6. Run su una omega-parola

Data una parola:

$$\alpha=\alpha(0)\alpha(1)\alpha(2)\ldots,$$

una run di $\mathcal{A}$ su $\alpha$ e' una sequenza infinita di stati:

$$\sigma=q_0q_1q_2\ldots$$

tale che per ogni $i\ge 0$:

$$(q_i,\alpha(i),q_{i+1})\in\Delta.$$

Quindi la run consuma un simbolo per ogni passo, ma non finisce mai.

7. Condizione di accettazione di Buchi

Una run e' accettante se visita stati finali infinitamente spesso:

$$In(\sigma)\cap F\ne\emptyset.$$

Equivalentemente:

$$\exists q\in F.\ \exists^\omega i.\ q_i=q.$$

Lettura:

almeno uno stato finale viene visto infinite volte lungo la run.

L'automa accetta $\alpha$ se esiste almeno una run accettante su $\alpha$.

8. Differenza con NFA su parole finite

In un NFA su parole finite:

conta dove sei quando la parola finisce.

In un NBA:

conta quali stati ricompaiono infinitamente spesso.

Uno stato finale in un NBA non significa "ho finito". Significa:

questo stato deve essere visitato ancora e ancora, senza limite.

9. Perche il non determinismo conta

Come negli NFA, l'NBA accetta se esiste una run accettante.

Questo e' cruciale. Il non determinismo puo' "indovinare" un punto della parola in cui iniziare un comportamento accettante.

Esempio che tornera':

parole con solo finitely many $a$.

Un NBA puo' indovinare l'ultima $a$ e poi controllare che da li' in poi compaiano solo $b$.

Un DBA, invece, non puo' indovinare: ha una sola run.

Parte III - Linguaggi omega-regolari

10. Definizione

Un linguaggio:

$$L\subseteq A^\omega$$

e' omega-regolare se esiste un automa di Buchi che lo riconosce.

In simboli:

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

per qualche NBA $\mathcal{A}$.

11. Esempio: infinite occorrenze di a

Linguaggio:

$$L_{\infty a}=\{\alpha\in\{a,b\}^\omega\mid a\text{ compare infinitamente spesso}\}.$$

NBA, anzi anche DBA, semplice:

Transizioni:

stato leggo $a$ leggo $b$
$q_a$ $q_a$ $q_b$
$q_b$ $q_a$ $q_b$

Finale:

$$F=\{q_a\}.$$

La run visita $q_a$ infinitamente spesso se e solo se legge $a$ infinitamente spesso.

12. Esempio: finitely many a

Linguaggio:

$$L_{fin\,a}=\{\alpha\in\{a,b\}^\omega\mid a\text{ compare solo finitely many times}\}.$$

Un NBA puo' riconoscerlo cosi':

  1. finche' vuole, resta in una fase iniziale;
  2. a un certo punto indovina: "da qui in poi non compariranno piu' $a$";
  3. passa a uno stato finale che accetta solo $b$;
  4. se vede una $a$ dopo l'indovinata, quella run muore.

Se la parola ha davvero solo finite $a$, esiste una scelta corretta: indovinare dopo l'ultima $a$.

Se la parola ha infinite $a$, ogni scelta viene prima o poi smentita.

13. Linguaggio con vincolo fra due a

Negli appunti compare un esempio su:

$$A=\{a,b,c\}.$$

Vincolo:

fra due occorrenze consecutive di $a$ deve comparire un numero pari di simboli diversi da $a$.

L'idea dell'automa:

Questo esempio serve a fissare un punto:

gli stati finali non indicano "terminazione", ma situazioni che devono ricorrere infinite volte o comunque rimanere compatibili con una run infinita.

Parte IV - Due operazioni su linguaggi finiti

14. Omega-chiusura $W^\omega$

Dato:

$$W\subseteq A^\ast,$$

definiamo:

$$W^\omega=\{\alpha\in A^\omega\mid \alpha=w_0w_1w_2\ldots,\ w_i\in W\}.$$

Lettura:

parole infinite ottenute concatenando infinitamente molte parole finite prese da $W$.

Esempio:

$$W=\{ab\}.$$

Allora:

$$W^\omega=(ab)^\omega=ababab\ldots$$

15. Chiusura vettoriale $\overrightarrow{W}$

Dato:

$$W\subseteq A^\ast,$$

definiamo:

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

Lettura:

parole infinite che hanno infinitamente molti prefissi appartenenti a $W$.

Esempio:

Se:

$$W=A^\ast a,$$

cioe' parole finite che terminano con $a$, allora:

$$\overrightarrow{W}$$

e' il linguaggio delle parole infinite con infinite occorrenze di $a$.

16. Perche queste operazioni sono importanti

Sono due modi diversi di descrivere infinito:

Queste operazioni anticipano due idee:

Parte V - Chiusure e GNBA

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

Sia:

$$V\subseteq A^\ast$$

regolare.

Vogliamo riconoscere:

$$V^\omega.$$

Intuizione:

  1. uso un automa finito per riconoscere un blocco di $V$;
  2. quando raggiungo un finale, posso tornare all'inizio;
  3. devo farlo infinitamente spesso;
  4. quindi rendo l'inizio, o il punto di reset, finale nel senso di Buchi.

La run accettante passa infinitamente spesso dal punto di reset, cioe' riconosce infiniti blocchi di $V$.

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

Qui:

$$V\subseteq A^\ast,\qquad L\subseteq A^\omega.$$

Il linguaggio:

$$V\cdot L$$

contiene parole infinite con un prefisso finito in $V$ seguito da una parola in $L$.

Costruzione intuitiva:

19. Unione

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

$$L_1\cup L_2$$

e' omega-regolare.

Con NBA, basta usare nondeterminismo:

20. Perche l'intersezione non e' il prodotto banale

Per parole finite, il prodotto per intersezione usa finali:

$$F_1\times F_2.$$

Per NBA non basta. Infatti, una parola deve far visitare:

Ma queste visite non devono accadere nello stesso istante.

Esempio:

Entrambi accettano, ma il prodotto potrebbe non visitare mai una coppia $(F_1,F_2)$ simultaneamente.

Serve una condizione piu' generale.

21. GNBA

Un Generalized Buchi Automaton, GNBA, ha una famiglia di insiemi finali:

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

Una run e' accettante se visita ogni $F_i$ infinitamente spesso:

$$\forall i,\ \exists^\omega n.\ q_n\in F_i.$$

Quindi una GNBA puo' dire:

visita infinitamente spesso finali del primo tipo, del secondo tipo, ecc.

22. Intersezione tramite GNBA

Dati due NBA:

$$\mathcal{A}_1,\quad \mathcal{A}_2,$$

costruiamo il prodotto:

$$Q=Q_1\times Q_2.$$

La condizione GNBA e':

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

Lettura:

Questo riconosce:

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

23. Da GNBA a NBA

GNBA e NBA hanno lo stesso potere espressivo.

Se:

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

costruiamo $k$ copie dell'automa. La copia corrente indica quale insieme finale stiamo aspettando.

Schema:

  1. nella copia 1 cerco una visita a $F_1$;
  2. quando la trovo, passo alla copia 2;
  3. nella copia 2 cerco $F_2$;
  4. ...
  5. dopo $F_k$, torno alla copia 1.

Se completo questo ciclo infinitamente spesso, ho visitato tutti gli $F_i$ infinitamente spesso.

La dimensione cresce di un fattore circa $k$.

Parte VI - Espressioni omega-regolari

24. Forma delle omega-espressioni

Una espressione omega-regolare ha forma finita:

$$\bigcup_{i=1}^n U_i\cdot V_i^\omega,$$

dove $U_i,V_i\subseteq A^\ast$ sono linguaggi regolari.

Lettura:

scelgo un prefisso finito in $U_i$, poi concateno infinitamente molti blocchi presi da $V_i$.

25. Da Buchi a omega-espressione

Dato un NBA:

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

per ogni coppia di stati $s,s'$ definiamo:

$$W_{ss'}=\{w\in A^\ast\mid s\xrightarrow{w}s'\}.$$

Questo linguaggio e' regolare, perche' si riconosce con un automa finito che parte da $s$ e ha finale $s'$.

Se una run accettante visita infinitamente spesso uno stato finale $f$, allora:

Quindi:

$$L(\mathcal{A})=\bigcup_{f\in F} W_{q_0f}\cdot (W_{ff})^\omega.$$

Questa formula e' una lettura potente:

una parola accettata ha un prefisso fino a un finale e poi ritorna infinitamente spesso a quel finale.

26. Da omega-espressione a Buchi

Per:

$$U\cdot V^\omega,$$

costruiamo:

  1. un automa finito per $U$;
  2. un automa per $V$;
  3. una struttura che, dopo il prefisso $U$, riconosce infiniti blocchi in $V$;
  4. una condizione di Buchi che forza il ritorno infinitamente spesso al punto di reset dei blocchi.

La chiusura per unione gestisce la somma finita:

$$\bigcup_i U_i\cdot V_i^\omega.$$

Quindi:

linguaggi omega-regolari = linguaggi riconosciuti da NBA = linguaggi descritti da omega-espressioni regolari.

Parte VII - Emptiness, lasso e parole ultimamente periodiche

27. Parole ultimamente periodiche

Una parola infinita e' ultimamente periodica se:

$$\alpha=u\cdot v^\omega$$

con:

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

Lettura:

dopo un prefisso finito $u$, ripete per sempre lo stesso blocco $v$.

Questa forma si chiama anche lasso:

28. Ogni omega-regolare non vuoto contiene un lasso

Se un linguaggio omega-regolare non e' vuoto, contiene almeno una parola ultimamente periodica.

Intuizione da automi:

Quindi se un NBA accetta qualcosa, accetta anche una parola del tipo:

$$u\cdot v^\omega.$$

29. Emptiness problem

Il problema di vuotezza chiede:

$$L(\mathcal{A})=\emptyset?$$

Per un NBA, la risposta e' no se e solo se esiste:

Equivalentemente:

esiste una SCC raggiungibile che contiene almeno uno stato finale e ha un ciclo infinito.

30. Algoritmo di emptiness

Procedura:

  1. calcola gli stati raggiungibili da $q_0$;
  2. calcola le SCC del grafo delle transizioni;
  3. cerca una SCC raggiungibile che contiene uno stato finale;
  4. verifica che la SCC permetta una run infinita, cioe' contenga un ciclo.

Se esiste, il linguaggio non e' vuoto.

Se non esiste, il linguaggio e' vuoto.

Questa e' una riduzione a raggiungibilita' e SCC su grafo finito.

31. Perche emptiness e' centrale nel model checking

Nel model checking automata-theoretic si controlla spesso:

$$L(S)\cap L(\neg\varphi)=\emptyset.$$

Lettura:

non esiste un comportamento del sistema che violi la proprieta'.

Quindi l'emptiness degli automi di Buchi diventa il motore della verifica LTL.

Parte VIII - Complementazione

32. L'errore: invertire gli stati finali

Per DFA su parole finite, il complemento si ottiene invertendo finali e non finali.

Per NBA questo non funziona.

Perche'?

Un NBA accetta se:

esiste una run che visita $F$ infinitamente spesso.

La negazione e':

tutte le run non visitano $F$ infinitamente spesso.

Invertire $F$ controlla invece:

esiste una run che visita stati non finali infinitamente spesso.

Questa non e' la negazione corretta.

33. Esempio intuitivo del fallimento

Una parola puo' avere:

Allora l'automa originale accetta, ma anche l'automa con finali invertiti potrebbe accettare.

Questo e' il problema del non determinismo.

34. Chiusura per complemento

Gli omega-linguaggi regolari sono chiusi per complemento, ma la costruzione e' molto piu' difficile rispetto al caso DFA.

Gli appunti introducono strumenti come:

L'idea concettuale:

per complementare un NBA bisogna catturare globalmente tutte le run, non solo cambiare etichetta ai finali.

Per l'orale, la cosa fondamentale e' sapere:

35. Congruenza e saturazione, lettura leggera

Una congruenza su $A^\ast$ raggruppa parole finite che si comportano allo stesso modo rispetto alla concatenazione.

Dire che una congruenza satura un omega-linguaggio significa:

su ogni blocco del tipo $U\cdot V^\omega$, o tutto il blocco sta nel linguaggio, o nessuna parola rilevante del blocco lo attraversa parzialmente.

Il punto tecnico degli appunti e':

se una congruenza satura $L$, allora satura anche il complemento.

Questo permette di ragionare sul complemento con un numero finito di classi.

Parte IX - DBA vs NBA

36. Definizione di DBA

Un DBA e' un automa di Buchi deterministico:

37. NBA e DBA non hanno lo stesso potere

Sulle parole finite:

$$DFA \equiv NFA$$

come potere espressivo.

Sulle parole infinite:

$$DBA \subsetneq NBA.$$

Il non determinismo aggiunge potere espressivo.

38. Linguaggio "finitely many a"

Il linguaggio:

$$L_{fin\,a}=\{\alpha\mid a\text{ compare finitely many times}\}$$

e' riconoscibile da un NBA:

Ma non e' riconoscibile da un DBA.

Intuizione:

un deterministico non puo' sapere quando ha visto l'ultima $a$, perche' una nuova $a$ potrebbe sempre arrivare piu' avanti.

39. Complemento e DBA

Il complemento di "finitely many a" e':

$$L_{\infty a}=\{\alpha\mid a\text{ compare infinitely often}\}.$$

Questo e' riconoscibile da un DBA semplice, come visto prima.

Se i DBA fossero chiusi per complemento, allora anche "finitely many a" sarebbe DBA. Ma non lo e'. Quindi i DBA non sono chiusi per complemento come i DFA.

Per recuperare chiusure robuste in forma deterministica servono condizioni piu' ricche, come Muller o Rabin.

40. Caratterizzazione utile dei DBA

Gli appunti collegano i DBA a linguaggi del tipo:

$$\overrightarrow{W}$$

dove $W$ e' regolare.

Intuizione:

un DBA accetta se lungo la sua unica run incontra stati finali infinitamente spesso; quindi i prefissi che portano a finali formano un linguaggio regolare visto infinitamente spesso.

Questa caratterizzazione spiega perche' i DBA sono meno espressivi degli NBA.

Parte X - Automi di Muller

41. Perche introdurre Muller

Gli automi di Buchi guardano se almeno uno stato finale viene visitato infinitamente spesso.

Gli automi di Muller guardano l'intero insieme degli stati visitati infinitamente spesso.

Questo e' piu' espressivo e funziona meglio con determinismo.

42. Definizione

Un automa di Muller e':

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

dove:

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

Data una run:

$$\rho=q_0q_1q_2\ldots,$$

definiamo:

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

La run e' accettante se:

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

43. Buchi come caso particolare di Muller

Un automa di Buchi con finali $F$ accetta se:

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

Questo si traduce in Muller ponendo:

$$\mathcal{F}=\{P\subseteq Q\mid P\cap F\ne\emptyset\}.$$

Quindi Buchi e' un caso particolare di Muller.

44. Complemento nei Muller automata

Per un automa di Muller deterministico, complementare e' semplice:

$$\mathcal{F}'=2^Q-\mathcal{F}.$$

Stessa struttura, stessa run unica, ma accetti gli insiemi ricorrenti che prima erano rifiutati.

Questo e' uno dei motivi per cui Muller e' utile:

mantiene determinismo ed e' chiuso per complemento in modo diretto.

45. Collegamento col capitolo 10

Nel capitolo 10, Buchi-Landweber usa automi deterministici di Muller per trasformare specifiche logiche in giochi.

Ora dovrebbe essere chiaro perche':

Parte XI - Automata per fairness

46. Justice come proprieta' omega

Una condizione di justice dice:

se una transizione resta abilitata da un certo punto in poi, allora deve essere presa infinitamente spesso.

Questa e' una proprieta' su computazioni infinite, quindi e' naturale rappresentarla con automi di Buchi.

47. Stato critico della justice

Negli appunti, per una transizione $a_i$, si distingue:

Lo stato problematico e':

enabled ma non taken.

Se resto per sempre in una situazione in cui $a_i$ e' abilitata e non la prendo mai, violo justice.

Un automa di Buchi puo' avere come unico stato non finale proprio lo stato critico "enabled-not-taken". Accettare significa non restare per sempre bloccati in quella violazione.

48. Perche questo esercizio e' importante

Collega tre parti del corso:

All'orale, se ti chiedono "perche servono gli automi di Buchi?", puoi rispondere anche:

perche' condizioni come fairness e liveness non parlano di una fine, ma di cio' che accade infinitamente spesso lungo una computazione.

Parte XII - Errori tipici

49. Pensare che finale significhi "ultimo stato"

Nelle parole infinite non c'e' ultimo stato.

Uno stato finale di Buchi deve essere visitato infinitamente spesso.

50. Confondere esiste una run con tutte le run

Un NBA accetta se esiste una run accettante.

Non richiede che tutte le run siano accettanti.

51. Usare il prodotto finito per l'intersezione

Il prodotto con finali $F_1\times F_2$ non basta, perche' le visite finali dei due automi possono non essere sincronizzate.

Serve GNBA o una costruzione equivalente.

52. Invertire i finali per complementare un NBA

Sbagliato. La negazione di "esiste una run buona" e' "tutte le run non sono buone", non "esiste una run che visita finali invertiti".

53. Pensare che DBA e NBA siano equivalenti

Sulle parole infinite il non determinismo aumenta il potere espressivo.

L'esempio standard e' "finitely many $a$": NBA si', DBA no.

54. Confondere Occ e Inf

$$Occ(\rho)$$

conta gli stati visitati almeno una volta.

$$Inf(\rho)$$

conta gli stati visitati infinitamente spesso.

Per Buchi/Muller conta $Inf$, non solo $Occ$.

Parte XIII - Mini-esercizi guidati

Esercizio 1: accettazione Buchi

Una run visita uno stato finale alle posizioni:

$$2,5,9,14,20,\ldots$$

ed esistono infinite posizioni di questo tipo. E' accettante?

Si'. Serve una visita finale infinitamente spesso, non periodica o regolare.

Esercizio 2: visite finite

Una run visita finali solo alle posizioni:

$$3,7,10.$$

Poi mai piu'. E' accettante?

No. Le visite finali sono finite.

Esercizio 3: infinite a

Costruisci un DBA per infinite occorrenze di $a$.

Soluzione:

Esercizio 4: finitely many a

Perche' un NBA riconosce finitely many $a$?

Perche' puo' indovinare il punto dopo l'ultima $a$ e poi controllare che da li' in poi compaiano solo $b$.

Esercizio 5: emptiness

Un NBA ha uno stato finale raggiungibile, ma nessun ciclo che lo contiene. Il linguaggio e' non vuoto?

No. Per accettare bisogna tornare a un finale infinitamente spesso; serve un ciclo con finale raggiungibile.

Esercizio 6: GNBA

Un GNBA ha:

$$\mathcal{F}=\{F_1,F_2,F_3\}.$$

Che cosa deve fare una run accettante?

Deve visitare ciascuno dei tre insiemi $F_1,F_2,F_3$ infinitamente spesso.

Esercizio 7: Muller

Se:

$$Inf(\rho)=\{q_2,q_4\}$$

e:

$$\mathcal{F}=\{\{q_2,q_4\},\{q_1\}\},$$

la run e' accettante?

Si', perche' l'insieme degli stati visitati infinitamente spesso appartiene a $\mathcal{F}$.

Esercizio 8: Occ vs Inf

Per:

$$\rho=q_0,q_1,q_2,q_1,q_2,q_1,q_2,\ldots$$

calcola:

$$Occ(\rho),\qquad Inf(\rho).$$

Soluzione:

$$Occ(\rho)=\{q_0,q_1,q_2\},$$

$$Inf(\rho)=\{q_1,q_2\}.$$

Parte XIV - Mappa per l'orale

55. Percorso consigliato

Per rispondere bene:

  1. Parti dai sistemi reattivi: computazioni infinite.
  2. Spiega perche' NFA/DFA su parole finite non bastano.
  3. Definisci omega-parole e $A^\omega$.
  4. Definisci NBA.
  5. Spiega run infinita e condizione di Buchi.
  6. Sottolinea: accetta se esiste una run con finali infinitamente spesso.
  7. Fai l'esempio "infinite occorrenze di $a$".
  8. Fai l'esempio "finitely many $a$" e spiega il ruolo del non determinismo.
  9. Definisci linguaggio omega-regolare.
  10. Spiega $W^\omega$ e $\overrightarrow{W}$.
  11. Spiega perche' l'intersezione richiede GNBA.
  12. Spiega GNBA e conversione a NBA.
  13. Spiega omega-espressioni regolari.
  14. Spiega emptiness via SCC con finale raggiungibile.
  15. Spiega lasso/ultimately periodic.
  16. Spiega perche' la complementazione non e' invertire finali.
  17. Spiega DBA vs NBA.
  18. Chiudi con Muller e collegamento al capitolo 10.

56. Risposta orale pronta

Una risposta compatta:

Gli automi di Buchi estendono gli automi finiti alle parole infinite, che sono necessarie per modellare sistemi reattivi e computazioni non terminanti. La struttura di un NBA e' simile a quella di un NFA, ma cambia l'accettazione: una run infinita e' accettante se visita stati finali infinitamente spesso, cioe' se $In(\sigma)\cap F\ne\emptyset$. L'automa accetta una parola se esiste una run accettante.

I linguaggi riconosciuti da NBA sono gli omega-regolari. Si possono descrivere anche con espressioni omega-regolari del tipo $\bigcup_i U_iV_i^\omega$. L'emptiness e' decidibile cercando una SCC raggiungibile che contenga uno stato finale: se esiste, posso costruire un lasso $uv^\omega$ accettato. Le chiusure richiedono attenzione: l'unione e' semplice, l'intersezione richiede GNBA perche' le visite finali dei due automi non devono essere sincronizzate, e la complementazione non si ottiene invertendo i finali. Inoltre NBA e DBA non hanno lo stesso potere: per esempio "finitely many $a$" e' NBA ma non DBA. Per recuperare determinismo pieno si introducono condizioni piu' ricche, come Muller, che guardano l'insieme degli stati visitati infinitamente spesso.

57. Riassunto finale

Il capitolo 5 introduce il modo standard di ragionare sulle computazioni infinite:

$$ \text{parole infinite} \to \text{run infinite} \to \text{visite infinitamente spesso} \to \text{accettazione Buchi}. $$

La frase da ricordare e':

su parole infinite non accetto arrivando alla fine; accetto se il comportamento buono ricorre infinitamente spesso.

La catena tecnica e':

$$ \text{NBA} \leftrightarrow \text{omega-regolari} \leftrightarrow \text{omega-espressioni} \to \text{emptiness via SCC/lasso} \to \text{GNBA per intersezione} \to \text{Muller per determinismo e complemento}. $$

Esercizi (piano di studio)

Esercizi e domande — settimana 3

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

Esercizi scritti essenziali

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Domande orali secche

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

Controllo

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

Indice← PrecedenteSuccessivo →