Possibili argomenti per l’approfondimento / temi d’esame

(lista preliminare):


- algoritmi per giochi di parità 


- il problema della sintesi per logiche temporali (riferimento:

Amir Pnueli and Roni Rosner, On the Synthesis of a Reactive Module, in:

Conference Record of the Sixteenth Annual ACM Symposium on Principles

of Programming Languages, Austin, Texas, USA, 1989, pp. 179--190)


- automi alternanti di Buechi su alberi infiniti e trasformazione 

di automi alternanti di Buechi su alberi infiniti in automi (non 

deterministici) di Buechi (riferimenti principali: David E. Muller, 

Paul E. Schupp: Alternating Automata on Infinite Trees. Theor. 

Comput. Sci. 54: 267-276 (1987) e David E. Muller, Paul E. Schupp: 

Simulating Alternating Tree Automata by Nondeterministic Automata: 

New Results and New Proofs of the Theorems of Rabin, McNaughton 

and Safra. Theor. Comput. Sci. 141(1&2): 69-107 (1995)) 


- legame tra la logica CTL* e (frammenti de) la teoria monadica 

dell'albero binario infinito (riferimento principale: articolo di 

Hafer e Thomas su Computation tree logic CTL* and path quantifiers 

in the monadic theory of the binary tree, ICALP 1987) 


- model cheching per CTL* (lucidi di Mark Reynolds)


- forme canoniche per le formule di LTL / teoremi di separazione

(riferimenti: D. M. Gabbay, The declarative past and imperative future: 

Executable temporal logic for interactive systems, in Temporal Logic in

Specification, ser. Lecture Notes in Computer Science, B. Banieqbal,

H. Barringer, and A. Pnueli, Eds., vol. 398. Springer, 1987, pp. 409–

448; G. Petric Mareti´c, M. Torabi Dashti, and D. Basin, Anchored

LTL separation, in Proceedings of the Joint Meeting of the

Twenty-Third EACSL Annual Conference on Computer Science Logic

(CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on

Logic in Computer Science (LICS), ser. CSL-LICS ’14. New York, 

NY, USA: ACM, 2014, pp. 74:1–74:9)


- Aalta (LTL-to-Büchi Translator and Satisfiability Checker) 


- traduzione di formule LTL in automi di Buechi

(riferimento: P. Gastin and D. Oddoux, Fast LTL to Buechi automata 

translation, in CAV, ser. Lecture Notes in Computer Science, G. Berry, 

H. Comon, and A. Finkel, Eds., vol. 2102. Springer, 2001, pp. 53–65)


- la logica al prim'ordine dell'ordine lineare MFO[<] e la logica 

al prim'ordine del successore MFO[succ] (riferimento principale: 

capitolo 8 del libro Infinite Words, Perrin e Pin, Elsevier 2004)


- chiusura degli automi di Rabin su alberi infiniti rispetto alla

complementazione (riferimenti principali: W. Thomas, Automata 

on Infinite Objects, in Handbook of Theoretical Computer Science, 

Vol B (Capitolo 4), J. van Leeuwen (ed.), Elsevier, 1990, e  W. Thomas, 

Languages, Automata, and Logic, in Handbook of Formal

Languages, Vol. III, G. Rozenberg, A. Solomaa (eds.), Springer,

1997, pp. 389-455)


- nuovi approcci/risultati ai problemi della complementazione

e della determinizzazione degli automi di Buechi su parole

(riferimento principale: Profile Trees for Buechi Word Automata, 

with Application to Determinization, Seth Fogarty, Orna Kupferman, 

Moshe Vardi e Thomas Wilke , in corso di pubblicazione su Information

and Computation)


- Studio del potere espressivo dell'operatore di shuffle

(riferimento principale: The expressive power of the shuffle product

Jean Berstel, Luc Boasson, Olivier Carton, Jean-Éric Pin e Antonio Restivo,

Information and Computation 2010)


- Approfondimento nell'ambito dei sistemi a tableau per logiche temporali 

(implementazione) 


- Approfondimento nell'ambito delle logiche temporali basate sugli 

intervalli 


- Approfondimento nell'ambito della specifica e verifica di sistemi 

a stati infiniti