Possibili argomenti per l’approfondimento / temi d’esame:

- Algoritmi per giochi di parità 

- Il problema della sintesi per logiche temporali e automi temporizzatori

Zohar Manna and Pierre Wolper, Synthesis of Communicating Processes

from Temporal Logic Specifications

ACM Transactions on Programming Languages and Systems 8(1), 1984, pp. 68--93.

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)

Oded Maler, Amir Pnueli, and Joseph Sifakis,

On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract)},

12th Annual Symposium on Theoretical Aspects of Computer

Science (STACS), LNCS 900, Springer, 1995, pp. 229--242.

- Automi alternanti di Buechi su alberi infiniti e trasformazione di automi  

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

David E. Muller, Paul E. Schupp, 

Alternating Automata on Infinite Trees. Theor. 

Comput. Sci. 54: 267-276, 1987

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 

Thilo Hafer and Wolfgang Thomas, 

Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree, 

14th International Colloquium on Automata, Languages and Programming (ICALP), 

LNCS 267, Springer, 1987, pp. 269--279. 

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

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

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 Maretic, 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), CSL-LICS, ACM, 2014, pp. 74:1–74:9

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

- Traduzione di formule LTL in automi di Buechi

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

translation, CAV, LNCS 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] 

Capitolo 8 del libro Infinite Words, Perrin e Pin, Elsevier 2004

- Chiusura degli automi di Rabin su alberi infiniti rispetto alla complementazione

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

Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, and Thomas Wilke,

Profile trees for Buechi word automata, with application to determinization,

Information and Computation, Volume 245, 2015, pp. 136--151

- Studio del potere espressivo dell'operatore di shuffle

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

The expressive power of the shuffle product

Information and Computation, Volume 208(11), 2010, pp. 1258--1272

- 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