Finite automata on infinite words and trees: Complementation, determinization and algorithms for checking emptiness.
Connections with logic: Finite automata and monadic second order (MSO) logic on words and trees. Decidability of MSO theory of various infinite graphs, methods of interpretation and unfolding.
Applications: Decision procedures for temporal logics. Modelling, verification and synthesis of systems. Effective theory of infinite games.
Miscellaneous : Timed and hybrid automata. Probabilistic transition systems. Visual pushdown automata.
No specific text book. Material will be covered from various survey and research papers. Initial part of the course will be from the following article.
W. Thomas, Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume III, pages 389-455. Springer, New York, 1997.