CS579 | AUTOMATA, LOGIC AND GAMES | 3-0-0-6 |
Pre-requisites : |
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. |