Calcolabilità e Complessità A.A. 2010/2011 (in Italian)

Calendario delle lezioni

  • Giovedì ore 9:00 - 11:00, aula: E3.

Orario di ricevimento

  • Giovedì ore 12:00 - 13:00 13:30 - 14:30, stanza 0F29/A. Ricevimento su appuntamento (contattare l'istruttore via email).

Materiale didattico

  • [RS59] M.O. Rabin and D. Scott. Finite Automata and Their Decision Problems.
  • [HMU07] J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation 3/E.
  • [Cho74] Y. Choueka. Theories of Automata on Omega-Tapes: A Simplified Approach.
  • [Pnu79] A. Pnueli. The Temporal Semantics of Concurrent Programs.
  • [SV89] S. Safra and M.Y. Vardi. On Omega-Automata and Temporal Logic.
  • [Var95] M.Y. Vardi. Alternating Automata and Program Verification.
  • [Var96] M.Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic.
  • [Muk97] M. Mukund. Linear-Time Temporal Logic and Büchi Automata.
  • [Lod98] C. Loding. Methods for the Transformation of Omega-Automata: Complexity and Connection to Second Order Logic.

Piano delle lezioni

1. Prima lezione 10/03/11: Introduzione agli automi su parole infinite.
  1. Esempi di computazioni finite ed idealmente infinite (algoritmi di schedulazione, sistemi interattivi, etc.).
  2. Modellazione delle computazioni tramite automi a stati finiti.
  3. Automi riconoscitori e produttori.
  4. Definizione di automa deterministico a stati finiti su parole finite ed infinite:
    • definizione della struttura (tupla);
    • definizione di parola in input (finita ed infinita) e del relativo concetto di run.
  5. Definizione delle condizioni di accettazione:
    • variazione della struttura (condizione di accettazione);
    • definizione di accettazione dell'input rispetto ai criteri F (parole finite), B (Büchi), C (co-Büchi), GB (Büchi generalizzato), GC (co-Büchi generalizzato), M (Muller), R (Rabin), S (Streett) e P (parity);
    • definizione di linguaggio accettato;
    • esempi di automi DFA, DBA e DCA sull'alfabeto $\Sigma = \{ 0, 1 \}$ che riconoscono, rispettivamente, i seguenti linguaggi: $\Sigma^{*} \cdot 1 \:$ (parole finite che terminano con 1), $\Sigma^{\omega} \setminus \Sigma^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero infinito di 1) e $\Sigma^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero finito di 1).
  6. Definizione di funzione di output:
    • variazione della struttura (insieme dei simboli di output e funzioni di output di Mealy e Moore);
    • definizione di parola e linguaggio di output;
    • esempio di automa di Mealy sugli alfabeti $\Sigma_{I} = \Sigma_{O} = \{ 0, 1 \}$ che produce in output il simbolo $1$ ogniqualvolta due simboli $0$ siano riconosciuti in input;
    • concetto di equivalenza tra automi di Mealy e Moore e relativa trasformazione.
2. Seconda lezione 24/03/11: Nondeterminismo, universalità, concetto di dualità e proprietà di chiusura positiva.
  1. Definizione di automa riconoscitore a stati finiti nondeterministico ed universale:
    • variazione della struttura (nuova funzione di transizione ed insieme degli stati iniziali);
    • definizione dell'insieme dei run su di una parola in input;
    • definizione di accettazione di una computazione nondeterministica ed universale;
    • esempi di automi NBA e UCA sull'alfabeto $\Sigma = \{ 0, 1 \}$ che riconoscono i linguaggi $\Sigma^{\omega} \setminus \Sigma^{*} \cdot 1^{\omega} \:$ (parole infinite con un numero infinito di 0) e $\Sigma^{*} \cdot 1^{\omega} \:$ (parole infinite con un numero finito di 0).
  2. Concetto di dualità e sua apllicazione:
    • dualità tra condizioni di accettazione;
    • dualizzazione di un automa deterministico, nondeterministico ed universale;
    • teorema di dualizzazione.
  3. Teorema sulla non determinizzabilità degli NBA e degli UCA (particolare riferimento ai linguaggi $\Sigma^{*} \cdot 1^{\omega} \:$ e $\Sigma^{\omega} \setminus \Sigma^{*} \cdot 1^{\omega} \:$, sull'alfabeto $\Sigma = \{ 0, 1 \}$).
  4. Proprietà di chiusura booleana positiva degli automi con condizioni di accettazione F, B e C:
    • chiusura rispetto all'unione (risp., all'intersezione) per gli NFA e NBA (risp., UFA e UCA) (automa unione);
    • chiusura rispetto all'intersezione (risp., all'unione) per gli NFA (risp., UFA) (automa prodotto);
    • dimostrazione del fallimento nell'uso diretto dell'automa prodotto come mezzo di prova della chiusura degli NBA (risp., UCA) rispetto all'intersezione (risp., all'unione) (particolare riferimento agli automi non sincronizzati aventi linguaggio $0^{\omega}$);
    • chiusura rispetto all'intersezione (risp., all'unione) per gli NBA (risp., UCA) (automa prodotto modificato).
3. Terza lezione 31/03/11: Espressioni $\omega$-regolari, equivalenze tra automi e proprietà di proiezione.
  1. Espressioni $\omega$-regolari:
    • definizione del concetto di espressione $\omega$-regolare (forma standard) e del relativo linguaggio su parole infinite;
    • richiamo sull'equivalenza tra espressioni regolari e NFA;
    • teorema sull'equivalenza tra espressioni $\omega$-regolari e NBA.
  2. Proprietà di equivalenza tra automi:
    • ogni NBA e NCA / DBA e DCA ha un NMA, NPA, NRA e NSA / DMA, DPA, DRA e DSA equivalente;
    • ogni NGBA / DGBA ha un NBA / DBA equivalente;
    • ogni NGCA ha un NBA equivalente;
    • ogni NGCA ha un NCA equivalente;
    • ogni NMA ha un NBA equivalente;
    • ogni NPA ha un NBA equivalente;
    • ogni NRA ha un NBA equivalente;
    • ogni NSA ha un NBA equivalente.
  3. Proprietà di chiusura rispetto alla proiezione:
    • proiezione esistenziale degli automi nondeterministici;
    • proiezione universale degli automi universali.
4. Quarta lezione 07/04/11: Proprietà di determinizzazione e complementazione.
  1. Richiami sulle proprietà di chiusura rispetto alla determinizzazione ed alla complementazione degli NFA:
    • chiusura rispetto alla determinizzazione degli NFA (automa dei sottoinsiemi);
    • lower bound per la determinizzazione degli NFA;
    • chiusura rispetto alla complementazione degli NFA;
    • lower bound per la complementazione degli NFA.
  2. Proprietà di chiusura rispetto alla complementazione degli NBA:
    • dimostrazione del fallimento nell'uso della costruzione per sottoinsiemi come mezzo di prova della chiusura degli NBA rispetto alla complementazione ed alla determinizzazione (particolare riferimento agli automi riconoscenti i linguaggi $\emptyset\:$ e $0^{\omega} \:$ che non possono essere distinti dopo l'applicazione della costruzione per sottoinsiemi).
    • dimostrazione della non chiusura dei DBA rispetto alla complementazione (particolare riferimento al fallimento nell'uso della automa pseudo-duale);
    • procedura di complementazione di un DBA in un NBA (automa pseudo-duale modificato);
    • enunciato sulla chiusura rispetto alla complementazione degli NBA (excursus storico ed idea generale delle tecniche usate per la complementazione degli NBA: costruzione di Büchi, costruzione di Sistla, Vardi e Wolper, costruzione di Safra, costruzione di Kupferman e Vardi);
    • lower bound per la complementazione degli NBA.
5. Quinta lezione 28/04/11: Automi alternanti.
  1. Definizione di automa alternante a stati finiti:
    • variazione della struttura (nuova funzione di transizione booleana);
    • definizione di albero del run su di una parola in input;
    • definizione di accettazione di una computazione alternante;
    • casi particolari: automi nondeterministici ed universali;
    • dualizzazione dell'alternanza;
    • esempi di automi AFA, ABA e ACA sull'alfabeto $\Sigma = \{ 0, 1 \}$ che riconoscono, rispettivamente, i linguaggi $\Sigma^{*} \cdot 1 \:$ (parole finite che terminano con 1), $\Sigma^{\omega} \setminus \Sigma^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero infinito di 1) e $\Sigma^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero finito di 1).
  2. Risoluzione dell'alternanza per gli AFA, ABA e ACA:
    • trasformazione da AFA a NFA;
    • trasformazione da AFA a UFA;
    • lower bound per la trasformazione da AFA a NFA / UFA;
    • trasformazione da ABA a NBA;
    • trasformazione da ACA a UCA;
    • lower bound per la trasformazione da ABA / ACA a NBA / UCA.
6. Sesta lezione 05/05/11: Giochi dalla durata infinita.
  1. Definizione di arena di gioco:
    • definizione della struttura (tupla);
    • definizione di traccia, percorso e posizione;
    • definizione di strategia (con e senza memoria);
    • definizione di partita.
  2. Definizione di gioco dalla durata infinita:
    • definizione della struttura (tupla);
    • variazione della struttura per giochi particolari;
    • definizione del concetto di vittoria (forte e debole) e di patta;
  3. Proprietà di determinatezza dei giochi:
    • definizione di determinatezza di un gioco;
    • teorema sulla determinatezza dei giochi particolari.
  4. Definizione di gioco di parità:
    • definizione della struttura (tupla);
    • proprietà di determinatezza;
    • teorema sull'assenza di memoria.
  5. Trasformazioni tra automi e giochi:
    • trasformazione da giochi ad automi;
    • trasformazione da automi a giochi di appartenenza;
    • trasformazione da automi a giochi di vuoto.
7. Settima lezione 16/05/11: Proprietà degli automi alternanti.
  1. Proprietà di chiusura booleana positiva:
    • chiusura rispetto all'unione;
    • chiusura rispetto all'intersezione.
  2. Proprietà di chiusura rispetto alla proiezione:
    • proiezione esistenziale;
    • proiezione universale.
  3. Dimostrazione di correttezza della procedura di dualizzazione.
  4. Definizione di automa alternante weak:
    • vincolo sulla struttura di transizione;
    • criterio di accettazione.
  5. Trasformazione di un ABA / ACA in un AWA equivalente:
    • costruzione e sua correttezza;
    • applicazione alla complementazione degli ABA / ACA.
8. Ottava lezione 26/05/10: Risoluzione del problema del vuoto.
  1. Problema del vuoto per gli NFA:
    • caratterizzazione;
    • algoritmo nondeterministico;
    • algoritmo deterministico.
  2. Problema del vuoto per gli NBA:
    • caratterizzazione;
    • algoritmo nondeterministico;
    • algoritmo deterministico.
  3. Problema del vuoto per gli automi alternanti:
    • calcolo del vuoto per mezzo della risoluzione dell'alternanza;
    • problema dell'universalità;
    • sistemi di tiling;
    • lower bound.
9. Nona lezione 30/05/11: Introduzione alle logiche temporali lineari.
  1. Modellazione dei sistemi e strutture di Kripke:
    • definizione di struttura di Kripke e relative computazioni;
    • trasformazione delle strutture di Kripke in automi di Büchi.
  2. La logica temporale lineare LTL:
    • definizione di sintassi, semantica e modello;
    • concetto di equivalenza tra formule, equivalenze di base e forma normale positiva;
    • caratterizzazioni di punto fisso per gli operatori temporali "until" e "release";
    • problemi decisionali: soddisfacibilità, validità e model-checking;
    • esempi di proprietà di safety, liveness, etc.
10. Decima lezione 09/06/11: Problemi decisionali per LTL.
  1. Struttura dei modelli delle formule LTL:
    • definizione di chiusura di una formula LTL;
    • definizione di atomo per una formula LTL;
    • definizione di sequenza di Hintikka di una formula LTL;
    • teorema sull'equivalenza tra esistenza di un modello ed esistenza di una sequenza di Hintikka.
  2. Soddisfacibilità e model checking per LTL:
    • costruzione dell'automa nondeterministico generalizzato di Büchi per il riconoscimento dei modelli di una formula;
    • soluzione del problema della soddisfacibilità;
    • soluzione del problema del model checking.

Esercizi

1. Esercizi prima lezione 10/03/11.
  1. Costruire un automa deterministico di Rabin sull'alfabeto $\Sigma = \{ 0, 1, 2 \}$ che accetti il linguaggio delle parole contenenti un numero finito ed infinito, rispettivamente, dei simboli $1$ e $2$.
  2. Costruire un automa di Mealy sugli alfabeti $\Sigma_{I} = \Sigma_{O} = \{ 0, 1 \}$ che emetta in output il simbolo $1$ ogniqualvolta una stringa $010$ sia incontrata in input.
2. Esercizi seconda lezione 24/03/11.
  1. Dimostrare o confutare (anche proponendo un controesempio) le seguenti proposizioni:
    • ogni NFA / NBA / NCA può essere trasformato in un NFA / NBA / NCA con un unico stato iniziale;
    • ogni NFA / NBA / NCA può essere trasformato in un NFA / NBA / NCA con un unico stato finale.
  2. Dimostrare con dovizia di particolari il teorema di dualizzazione.
  3. Dimostrare la correttezza delle proprietà di chiusura booleana positiva.
3. Esercizi terza lezione 31/03/11.
  1. Dimostrare la correttezza delle trasformazioni tra automi.
  2. Dimostrare che le conversioni esponenziali di un NMA ed un NSA in un NBA sono ottimali. Fare riferimento alle famiglie di linguaggi proposte in [SV89].
  3. Dimostrare la correttezza delle proprietà di chiusura rispetto alla proiezione.
4. Esercizi quarta lezione 07/04/11.
  1. Dimostrare la correttezza della proprietà di chiusura rispetto alla determinizzazione degli NFA.
  2. Dimostrare la correttezza della procedura di complementazione dei DBA.
5. Esercizi quinta lezione 28/04/11.
  1. Dimostrare la correttezza delle costruzioni usate per la risoluzione dell'alternanza.
  2. Dimostrare che le classi degli UBA / NCA sono chiuse rispetto alla determinizzazione.
6. Esercizi sesta lezione 05/05/11.
  1. Formalizzare con dettaglio le prove di correttezza delle trasformazioni tra giochi ed automi.
7. Esercizi settima lezione 12/05/11.
  1. Dimostrare la correttezza delle costruzioni usate per le proprietà di chiusura.
8. Esercizi ottava lezione 26/05/11.
  1. Dimostrare che la ricerca di una soluzione per i sistemi di tiling, usati nella prova del lower bound per l'universalità, è un problema PSpace-Complete.

Elaborati

1. Elaborati prima parte.
  • Sulla complementazione degli NBA per mezzo della costruzione di Sistla, Vardi e Wolper.
    • [SVW87] P. Sistla, M.Y. Vardi, and P. Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic.
  • Sulla determinizzazione degli NBA per mezzo della costruzione di Piterman.
    • [Pit06] N. Piterman. From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata.
  • Sulla risoluzione dell'alternanza degli ABA.
    • [BKR10] U. Boker, O. Kupferman, and A. Rosenberg. Alternation Removal in Büchi Automata.
  • Sulla complessità di risoluzione dei giochi di parità.
    • [Jur98] M. Jurdzinski. Deciding the Winner in Parity Games Is in UP and CoUP.
  • Un algoritmo ricorsivo esponenziale per la risoluzione dei giochi di parità.
    • [Zie98] W. Zielonka. Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees.
    • [Fri11] O. Friedmann. Recursive Solving of Parity Games Requires Exponential Time.
  • Un algoritmo ricorsivo subesponenziale per la risoluzione dei giochi di parità.
    • [JPZ08] M. Jurdzinski, M. Paterson, and U. Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games.
  • Misure di progresso per la risoluzione dei giochi di parità.
    • [Jur00] M. Jurdzinski. Small Progress Measures for Solving Parity Games.

Appunti delle lezioni a cura degli studenti

ATTENZIONE! Il materiale di seguito riportato è stato vagliato dall'istruttore solo in modo parziale, pertanto il relativo uso come mezzo esclusivo di preparazione per l'esame non è consigliato.

  1. Appunti della prima lezione (a cura di Domenico Biondi e Massimiliano Di Mella).
    Appunti della prima lezione (a cura di Angelo Russo e Riccardo Tammaro).
  2. Appunti della seconda lezione (a cura di Fabio De Dominicis, Gabriele Iodice e Lorenzo Lucignano).
  3. Appunti della terza lezione (a cura di Jonathan Cacace e Riccardo Caccavale).
  4. Appunti della quinta lezione (a cura di Antonio Napoletano).
  5. Appunti della sesta lezione (a cura di Rosario Nardo e Alessandro Nisci).
  6. Appunti della nona e decima lezione (a cura di Vadim Malvone e Iliana Petrova).
    Appunti della nona e decima lezione (a cura di Alfonso Napolitano e Vincenzo Reggina).

Esercizi svolti a cura degli studenti

ATTENZIONE! Il materiale di seguito riportato è stato vagliato dall'istruttore solo in modo parziale, pertanto il relativo uso come mezzo esclusivo di preparazione per l'esame non è consigliato.

  1. Esercizi svolti (a cura di Alfonso Napolitano e Pietro Neroni).

Prove d'esame

Calcolabilità e Complessità A.A. 2009/2010 (in Italian)

Calendario delle lezioni

  • Lunedì ore 9:00 - 11:00 (teoria), aula: E4.
  • Lunedì ore 16:00 - 16:45 (esercitazioni facoltative), aula: E4.

Orario di ricevimento

  • Lunedì ore 12:00 - 14:00, stanza 0F29/A. Ricevimento su appuntamento (contattare l'istruttore via email).

Materiale didattico

  • [RS59] M.O. Rabin and D. Scott. Finite Automata and Their Decision Problems.
  • [HMU07] J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation 3/E.
  • [Cho74] Y. Choueka. Theories of Automata on Omega-Tapes: A Simplified Approach.
  • [Pnu79] A. Pnueli. The Temporal Semantics of Concurrent Programs.
  • [Wol83] P. Wolper. Temporal Logic Can Be More Expressive.
  • [SC85] A.P. Sistla and E.M. Clarke. The Complexity of Propositional Linear Temporal Logics.
  • [SV89] S. Safra and M.Y. Vardi. On Omega-Automata and Temporal Logic.
  • [Var95] M.Y. Vardi. Alternating Automata and Program Verification.
  • [Var96] M.Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic.
  • [Muk97] M. Mukund. Linear-Time Temporal Logic and Büchi Automata.
  • [Lod98] C. Loding. Methods for the Transformation of Omega-Automata: Complexity and Connection to Second Order Logic.

Piano delle lezioni

1. Prima lezione 15/03/10: Introduzione agli automi su parole infinite.
  1. Esempi di computazioni finite ed idealmente infinite.
  2. Modellazione delle computazioni tramite automi a stati finiti.
  3. Definizione di automa deterministico a stati finiti su parole finite ed infinite:
    • definizione della struttura (tupla);
    • definizione di parola in input (finita ed infinita) e del relativo concetto di run;
    • definizione di accettazione dell'input rispetto ai criteri F (parole finite), B (Büchi), C (co-Büchi), GB (Büchi generalizzato), GC (co-Büchi generalizzato), M (Muller);
    • definizione di linguaggio accettato;
    • esempi di automi DFA, DBA e DCA che riconoscono, rispettivamente, i seguenti linguaggi: $\{ 0, 1 \}^{*} \cdot 1 \:$ (parole finite che terminano con 1), $\{ 0, 1 \}^{\omega} \setminus \{ 0, 1 \}^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero infinito di 1) e $\{ 0, 1 \}^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero finito di 1).
  4. Definizione di automa a stati finiti nondeterministico ed universale:
    • variazione della struttura (nuova funzione di transizione ed insieme di stati iniziali);
    • definizione di insieme di run su di una parola in input;
    • definizione di accettazione di una computazione nondeterministica ed universale;
    • esempi di automi NBA e NCA che riconoscono il linguaggio $\{ 0, 1 \}^{*} \cdot 1^{\omega} \:$ (parole infinite con un numero finito di 0).
  5. Teorema sulla non determinizzabilità degli NBA (particolare riferimento al linguaggio $\{ 0, 1 \}^{*} \cdot 0^{\omega}$).
2. Seconda lezione 22/03/10: Espressioni omega-regolari e proprietà di chiusura positiva.
  1. Definizione del concetto di espressioni omega-regolari (forma standard) e dei relativi linguaggi su parole infinite.
  2. Richiamo sull'equivalenza tra espressioni regolari e NFA.
  3. Teorema sull'equivalenza tra espressioni omega-regolari e NBA.
  4. Proprietà di chiusura booleana positiva degli NFA e NBA:
    • chiusura rispetto all'unione per gli NFA e NBA (automa unione);
    • chiusura rispetto all'intersezione per gli NFA (automa prodotto);
    • dimostrazione del fallimento nell'uso diretto dell'automa prodotto come mezzo di prova della chiusura degli NBA rispetto all'intersezione (particolare riferimento agli automi non sincronizzati aventi linguaggio $0^{\omega}$);
    • chiusura rispetto all'intersezione per gli NBA (automa prodotto modificato).
  5. Dimostrazione del fallimento nell'uso della costruzione per sottoinsiemi come mezzo di prova della chiusura degli NBA rispetto alla complementazione ed alla determinizzazione (particolare riferimento agli automi riconoscenti i linguaggi $\emptyset\:$ e $0^{\omega} \:$ che non possono essere distinti dopo l'applicazione della costruzione per sottoinsiemi).
3. Terza lezione 29/03/10: Proprietà di proiezione, determinizzabilità e complementazione.
  1. Proprietà di chiusura rispetto alla proiezione degli NFA, NBA, UFA, e UBA:
    • chiusura rispetto alla proiezione esistenziale degli NFA e NBA;
    • chiusura rispetto alla proiezione universale degli UFA e UBA.
  2. Richiami sulle proprietà di chiusura rispetto alla complementazione ed alla determinizzazione degli NFA:
    • chiusura rispetto alla complementazione dei DFA (automa duale);
    • chiusura rispetto alla determinizzazione degli NFA (automa dei sottoinsiemi);
    • lower bound per la determinizzazione degli NFA;
    • chiusura rispetto alla complementazione degli NFA;
    • lower bound per la complementazione degli NFA.
4. Quarta lezione 19/04/10: Proprietà di inclusione e complementazione (i).
  1. Proprietà di inclusione tra automi a parole infinite:
    • ogni NGBA ha un NBA equivalente;
    • ogni NGCA ha un NCA equivalente;
    • ogni NBA / DBA ha un NMA / DMA equivalente;
    • ogni NCA / DCA ha un NMA / DMA equivalente;
    • ogni DBA / DCA ha un DMA complementare;
    • ogni NMA ha un NBA equivalente;
    • chiusura rispetto alla complementazione dei DMA (automa duale).
  2. Definizione dei criteri di accettazione R (Rabin) e S (Streett).
5. Quinta lezione 26/04/10: Proprietà di inclusione e complementazione (ii).
  1. Proprietà di inclusione tra automi a parole infinite:
    • ogni NBA / NCA ha un NRA / NSA equivalente;
    • ogni NRA ha un NBA equivalente;
    • ogni NSA ha un NBA equivalente.
  2. Proprietà di chiusura rispetto alla complementazione degli NBA:
    • dimostrazione della non chiusura dei DBA rispetto alla complementazione (particolare riferimento al fallimento nell'uso della automa duale);
    • procedura di complementazione di un DBA in un NBA (automa duale modificato);
    • enunciato sulla chiusura rispetto alla complementazione degli NBA (excursus storico ed idea generale delle tecniche usate per la complementazione degli NBA: costruzione di Büchi, costruzione di Sistla, Vardi e Wolper, costruzione di Safra, costruzione di Kupferman e Vardi);
    • lower bound per la complementazione degli NBA.
6. Sesta lezione 03/05/10: Automi alternanti (i).
  1. Definizione di automa a stati finiti alternante:
    • variazione della struttura (nuova funzione di transizione booleana);
    • definizione di albero del run su di una parola in input;
    • definizione di accettazione di una computazione alternante;
    • casi particolari: automi nondeterministici ed universali;
    • esempi di automi AFA, ABA e ACA che riconoscono, rispettivamente, i linguaggi $\{ 0, 1 \}^{*} \cdot 1 \:$ (parole finite che terminano con 1), $\{ 0, 1 \}^{\omega} \setminus \{ 0, 1 \}^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero infinito di 1) e $\{ 0, 1 \}^{*} \cdot 0^{\omega} \:$ (parole infinite con un numero finito di 1).
  2. Proprietà di chiusura booleana positiva degli AFA, ABA, ACA, ARA, ASA e AMA:
    • chiusura rispetto all'unione;
    • chiusura rispetto all'intersezione.
7. Settima lezione 10/05/10: Automi alternanti (ii).
  1. Definizione di automa alternante weak con annesso criterio di accettazione.
  2. Trasformazione di un ABA / ACA in un AWA equivalente.
  3. Proprietà di chiusura rispetto alla complementazione degli AFA, AWA, ABA, ACA, ARA, ASA e AMA:
    • chiusura rispetto alla complementazione per gli AFA, AWA e AMA;
    • trasformazione per dualizzazione da ABA / ACA e ARA / ASA ad ACA / ABA e ASA / ARA;
    • chiusura rispetto alla complementazione per gli ABA / ACA.
  4. Risoluzione dell'alternanza per gli AFA, ABA e ACA:
    • trasformazione da AFA a NFA;
    • trasformazione da AFA a UFA;
    • lower bound per la trasformazione da AFA a NFA / UFA;
    • trasformazione da ABA a NBA;
    • trasformazione da ACA a UCA;
    • lower bound per la trasformazione da ABA / ACA a NBA / UCA.
  5. Proprietà di chiusura rispetto alla proiezione degli AFA, ABA e ACA.
8. Ottava lezione 17/05/10: Risoluzione del problema del vuoto.
  1. Problema del vuoto per gli NFA:
    • caratterizzazione;
    • algoritmo nondeterministico;
    • algoritmo deterministico.
  2. Problema del vuoto per gli NBA:
    • caratterizzazione;
    • algoritmo nondeterministico;
    • algoritmo deterministico.
  3. Problema del vuoto per gli automi alternanti:
    • calcolo del vuoto per mezzo della risoluzione dell'alternanza;
    • problema dell'universalità;
    • sistemi di tiling;
    • lower bound.
9. Nona lezione 24/05/10: Introduzione alle logiche temporali lineari.
  1. Modellazione dei sistemi e strutture di Kripke:
    • macchine di Moore e modellazione formale dei sistemi;
    • definizione di struttura di Kripke e relative computazioni;
    • trasformazione delle macchine di Moore in strutture di Kripke;
    • trasformazione delle strutture di Kripke in automi di Büchi.
  2. La logica temporale lineare LTL:
    • definizione di sintassi, semantica e modello;
    • concetto di equivalenza tra formule, equivalenze di base e forma normale positiva;
    • caratterizzazioni di punto fisso per gli operatori temporali "until" e "release";
    • problemi decisionali: soddisfacibilità, validità e model-checking;
    • esempi di proprietà di safety, liveness, etc.
10. Decima lezione 31/05/10: Problemi decisionali per LTL.
  1. Struttura dei modelli delle formule LTL:
    • definizione di chiusura di una formula LTL;
    • definizione di atomo per una formula LTL;
    • definizione di sequenza di Hintikka di una formula LTL;
    • teorema sull'equivalenza tra esistenza di un modello ed esistenza di una sequenza di Hintikka.
  2. Soddisfacibilità e model checking per LTL:
    • costruzione dell'automa nondeterministico generalizzato di Büchi per il riconoscimento dei modelli di una formula;
    • osservazione sulla dimensione dei modelli e del relativo automa nondeterministico;
    • costruzione dell'automa alternante di Büchi per il riconoscimento dei modelli di una formula;
    • soluzione del problema della soddisfacibilità;
    • soluzione del problema del model checking;
    • mutua riducibilità tra soddisfacibilità e model checking;
    • lower bound per la soddisfacibilità ed il model checking.
11. Undicesima lezione 07/06/10: Confronto tra i poteri espressivi di LTL, QLTL e delle espressioni omega-regolari.
  1. Proprietà non esprimibili in LTL:
    • la proprietà "contare modulo n" e relativa espressione omega-regolare;
    • teorema sulla non esprimibilità in LTL della proprietà "contare modulo n".
  2. Quantificazione sulle proposizioni atomiche in LTL:
    • definizione di sintassi e semantica per QLTL;
    • la proprietà "contare modulo n" in QLTL;
    • riduzione da formula QLTL ad automa di Büchi;
    • riduzione da automa di Büchi a formula QLTL.

Esercizi

1. Esercizi seconda lezione 22/03/10.
  1. Dimostrare o confutare (anche proponendo un controesempio) le seguenti proposizioni:
    • ogni NFA può essere trasformato in un DFA con un unico stato iniziale;
    • ogni NFA può essere trasformato in un NFA / DFA con un unico stato finale;
    • ogni NBA può essere trasformato in un NBA / DBA con un unico stato iniziale;
    • ogni NBA può essere trasformato in un NBA con un unico stato finale.
2. Esercizi terza lezione 29/03/10.
  1. Si consideri un automa $A$ su un alfabeto $\Sigma$ per il quale $L^{*}(A)$, rispettivamente $L^{\omega}(A)$, è il linguaggio riconosciuto quando esso è considerato come un NFA, rispettivamente come un NBA. Inoltre, sia $F : 2^{\Sigma^{*}} -> 2^{\Sigma^{\omega}}$ una funzione di trasformazione non triviale di ogni linguaggio di parole finite in un linguaggio di parole infinite (una funzione è non triviale se trasforma linguaggi di cardinalità infinita in linguaggi di cardinalità infinita, e viceversa). Allora, dimostrare o confutare (anche proponendo un controesempio) le seguenti proposizioni:
    • per ogni funzione di trasformazione $F$, si ha che $L^{\omega}(A) = F(L^{*}(A))$;
    • esiste una funzione di trasformazione $F$ tale che $L^{\omega}(A) = F(L^{*}(A))$;
    • per ogni funzione di trasformazione $F$, si ha che $L^{\omega}(A) = F(L^{*}(A))$ se e solo se esiste un DBA che riconosce $L^{\omega}(A)$ come linguaggio;
    • esiste una funzione di trasformazione $F$ tale che $L^{\omega}(A) = F(L^{*}(A))$ ed esiste un DBA che riconosce $L^{\omega}(A)$ come linguaggio.
  2. Dimostrare la correttezza delle costruzioni usate per le operazioni di proiezione.
3. Esercizi quarta lezione 19/04/10.
  1. Dimostrare la correttezza delle costruzioni usate per le proprietà di inclusione tra gli automi.
  2. Dimostrare che la conversione esponenziale di un NMA in un NBA è ottimale. Fare riferimento alla famiglia di linguaggi proposta in [SV89].
4. Esercizi quinta lezione 26/04/10.
  1. Dimostrare la correttezza delle costruzioni usate per le proprietà di inclusione tra gli automi.
  2. Dimostrare che la conversione esponenziale di un NSA in un NBA è ottimale. Fare riferimento alla famiglia di linguaggi proposta in [SV89].
5. Esercizi sesta lezione 03/05/10.
  1. Dimostrare la correttezza delle costruzioni usate per le proprietà di chiusura degli automi.
6. Esercizi settima lezione 10/05/10.
  1. Dimostrare la correttezza delle costruzioni usate per le proprietà di chiusura degli automi.
  2. Dimostrare la correttezza delle costruzioni usate per la risoluzione dell'alternanza.
  3. Dimostrare che le classi degli UBA / NCA sono chiuse rispetto alla determinizzazione.
7. Esercizi ottava lezione 17/05/10.
  1. Dimostrare che la ricerca di una soluzione per i sistemi di tiling, usati nella prova del lower bound per l'universalità, è un problema PSpace-Complete.

Questioni interessanti

1. Domande quarta lezione 19/04/10.
  • La procedura di traduzione di un NGBA in un NBA è ottimale? Ovvero, può un automa NGBA con $n$ stati e $k$ insiemi di stati finali, essere trasformato in un NBA con un numero di stati inferiore rispetto ai $k \cdot n$ richiesti dalla costruzione classica?
2. Domande quinta lezione 26/04/10.
  • La procedura di complementazione di un DBA è ottimale? Ovvero, può un automa DBA con $n$ stati, $f$ dei quali finali, essere complementato in un NBA con un numero di stati inferiore rispetto ai $2n - f$ richiesti dalla costruzione dell'automa duale modificato?
  • La procedura di determinizzazione secondo Safra di un NBA in un DMA è ottimale? Ovvero, può un automa NBA con $n$ stati essere determinizzato in un DMA con un numero di stati inferiore a $O(2^{n · \log n})$? Il lower bound attualmente noto è $O(2^{n})$ [SV89].

Elaborati

1. Elaborati prima parte.
  • Sulla complementazione degli NBA per mezzo della costruzione di Sistla, Vardi e Wolper.
    • [SVW87] P. Sistla, M.Y. Vardi, and P. Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic.
  • Sulla determinizzazione e complementazione degli NBA per mezzo della costruzione di Safra.
    • [Saf88] S. Safra. On the Complexity of Omega-Automata.
    • [Saf92] S. Safra. Exponential Determinization for Omega-Automata with Strong-Fairness Acceptance Condition.
  • Sulla complementazione degli NBA per mezzo della costruzione di Kupferman e Vardi.
    • [KV97] O. Kupferman and M.Y. Vardi. Weak Alternating Automata Are Not That Weak.
  • Sugli automi two-way su parole finite ed infinite.
    • [Var88a] M.Y. Vardi. A Temporal Fixpoint Calculus.
    • [Var88b] M.Y. Vardi. A Note on the Reduction of Two-Way Automata to One-Way Automata.

Appunti delle lezioni a cura degli studenti

ATTENZIONE! Il materiale di seguito riportato non è stato vagliato dall'istruttore, pertanto il relativo uso come mezzo esclusivo di preparazione per l'esame non è consigliato.

  1. Appunti della prima lezione (a cura di Giuseppe Nigro, Paolo Pisa, e Vincenzo Reggina).
  2. Appunti della seconda lezione (a cura di Antonio Caso e Davide De Tommaso).
  3. Appunti della quarta lezione (a cura di Antonio Marino, Rita Monaco e Valeria Tedesco).
  4. Appunti della quinta lezione (a cura di Carmine Acanfora e Dario Camuso).
  5. Appunti della sesta lezione (a cura di Davide De Tommaso e Mario Marfella).
  6. Appunti della nona lezione (a cura di Carmine Acanfora e Dario Camuso).

Prove d'esame