CS 579, Automata, Logic and Games

Instructor: Purandar Bhaduri

Email: pbhaduri

Phone: ext 2360

Head Teaching Assistant: Siddharth Gaur (Email: sgaur)

Syllabus

• 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;
• 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.

Resources

• Main Sources
  1. Erich Grädel, Wolfgang Thomas and Thomas Wilke, Automata, Logics, and Infinite Games, Lecture Notes in Computer Science, Volume 2500, Springer, 2002.
  2. Wolfgang Thomas, Automata on infinite objects, in J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133–191. Elsevier Science Publishers, 1990.
  3. Wolfgang 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.
  4. Wolfgang Thomas, Lectures on Automata and Reactive Systems, RWTH, Aachen, 2002/2003.
  5. Madhavan Mukund, Finite-state Automata on Infinite Inputs, in Deepak D'Souza and Priti Shankar (eds), Modern Applications of Automata Theory, World Scientific (2012) 257-288.
  6. Madhavan Mukund, Linear-Time Temporal Logic and Büchi Automata, Tutorial talk, Winter School on Logic and Computer Science, ISI, Calcutta, January 1997.
  7. Orna Kupferman, Automata Theory and Model Checking, in Handbook of Model Checking, Springer, 2018.
  8. Meghyn Bienvenu, Finite Automata on Infinite Words and Trees, Course notes at University of Bremen, 2010.
  9. Martin Zimmermann, Felix Klein, and Alexander Weinert, Infinite Games (Lecture Notes), Saarland University, 2016.
• Secondary Sources
  1. Luke Ong, Lectures on Automata, Logic and Games, Oxford University, 2015.
  2. Bernd Finkbeiner, Lecture notes on Automata, Games and Verification, Summer Term, Saarland University, 2015.
  3. Bernd Finkbeiner, Automata, Games, and Verification, Lecture notes and slides, 2011.
  4. Bernd Finkbeiner, Lectures on reactive synthesis at the Winter School on Formal Verification 2017.
  5. Thomas Wilke, ω-Automata, arXiv preprint, 2016.
• References
  1. B. Khoussainov and A. Nerode, Automata Theory and Its Applications, Birkhäuser, 2001.
  2. E.M. Clarke, T.A. Henzinger, H. Veith and R. Bloem, Handbook of Model Checking, Springer, 2018.
  3. Dominique Perrin and Jean-Éric Pin, Infinite Words -- Automata, Semigroups, Logic and Games, Elsevier, 2004.
  4. Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, May 2008.
  5. E.M. Clarke, O. Grumberg, D. Kroening, D. Peled and H. Veith, Model Checking, Second Edition, MIT Press, 2018.

Evaluation

• Term Paper / Seminar: 20%
• Midsem: 30%
• Endsem: 50%