Course  References  Lecture Notes  Problem Sets 
Automata, Games, and Verification
The final exam will take place on Friday, July 25, 14:0016:00 in Hörsaal 002, building E 1 3. The exam will be open book, i.e., handwritten notes as well as books and other printed materials are allowed.
Syllabus
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.
Topics
 Automata over infinite words and trees (omegaautomata)
 Infinite twoplayer games
 Logical systems for the specification of nonterminating behavior
 Transformation of automata according to logical operations
Textbooks
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.) ISBN10: 0387292373 

Bakhadyr Khoussainov, Anil Nerode Automata Theory and its Applications Birkhauser Boston; 1st edition (February 15, 2001), ISBN: 0817642072 
Instructors
Bernd Finkbeiner and Sven Schewe
Lecture Room: Hörsaal IV, building E 2 4 (Mathematics department)
Lecture Time: Thursdays 14:1515:45
Tutorial Room: SR 016 Building E 1 3
Tutorial Time: A: Tuesdays 10:1511:45 B: Wednesdays 10:1511:45
Office Hours: Wednesdays 15:0016:00
Vertiefungsvorlesung (6 CP)
Sommersemester 2008