Course References Lecture Notes Problem Sets Exams

Automata, Games, and Verification

Lecturer: Bernd Finkbeiner
Teaching Assistant: Markus N. Rabe, Hazem Torfah, Felix Klein
Lecture Room: HS 001, building E1.3
Lecture Time: Tuesday 2pm-4pm
Tutorial Time: Thursday 2pm-4pm, Room 010 building E1.7



The theory of automata over infinite objects provides a succinct, expressive and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment.

In this course we will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.



The course will be based on the following two textbooks, supplemented as necessary by various research papers.

Erich Grädel, Wolfgang Thomas, Thomas Wilke (Eds.)
Automata, Logics, and Infinite Games: A Guide to Current Research
Springer, Berlin;
Lecture Notes in Computer Science 2500
2nd Print (1. November 2005)
Online Version (Online access is free of charge if you connect from a department IP. If you encounter problems, let us know.)
ISBN-10: 0387292373
Bakhadyr Khoussainov, Anil Nerode
Automata Theory and its Applications
Birkhauser Boston;
1st edition (February 15, 2001),
ISBN: 0817642072

Vertiefungsvorlesung (6 CP)
Wintersemester 2012/2013