| Course Code: CS579 Course Name: Automata, Logic and Games Syllabus: Preamble / Objectives: The objective of this course is to introduce the mathematical theory underlying the formal verification and automated synthesis of reactive systems. The main components of the course are (1) automata on infinite objects (words and trees) as a computational model, (2) various kinds of logic for specifying the behaviour of systems and (3) infinite games on finite graphs for modelling the interaction between a system and its environment. Texts: Automata on Infinite Words: Büchi automata, elementary constructions, omega-regular languages, closure properties; Linear Temporal Logic and Model Checking: Kripke structures, linear-time temporal logic (LTL), model checking problem for LTL, from LTL to Büchi automata; Determinization and Complementation of Omega-automata: omega-automata with different acceptance conditions, deterministic omega-automata, McNaughton’s Theorem, Safra's construction; Games and Winning Strategies: Games, strategies and winning strategies, safety and reachability games, Büchi and parity games, Muller games, latest appearance record construction; Automata on Infinite Trees: Trees and tree automata, parity tree automata, tree automata and games, complementation, emptiness; Monadic Second Order Logic: Syntax and semantics of monadic second order logic of one-successor and two successors, relation to Büchi and tree automata, decidability. References: E.M. Clarke, O. Grumberg, D. Kroening, D. Peled and H. Veith, Model Checking, Second Edition, MIT Press, 2018. E. Grädel, W. Thomas and T. Wilke, Automata, Logics, and Infinite Games, Lecture Notes in Computer Science, Volume 2500, Springer, 2002. B. Khoussainov and A. Nerode, Automata Theory and Its Applications, Birkhäuser, 2001. |