Course

Automata, Games, and Verification

Lecturer:	Bernd Finkbeiner
Teaching Assistant:	Rüdiger Ehlers, Andrey Kupriyanov
Lecture Room:	Seminarraum 0.01, building E 2 1 (bioinformatics)
Lecture Time:	Tuesday 10am-12pm
Tutorial A Room:	Seminarraum 0.01, building E 2 1 (bioinformatics)
Tutorial B Room:	Seminarraum U12, building E 1 1
Tutorial Time:	Thursday 10am-12pm

News

The exam inspection for the end-of-semester exam will take place on Wednesday, October 19, between 15:00 and 16:00, in room 508 and room 532, E 1.3. In case this time is inconvenient for you, please let us know — we will arrange another meeting.
The results of the end-of-semester (backup) exam are now online.
The end-of-semester (backup) exam will be written and will take place on Tuesday, the 27th of September, 2pm-5pm, in Hörsaal 3, building E1.3.
The exam inspection for the end-of-term exam will take place on Wednesday, August 3, between 11:00 and 12:00, at the seminar room 528, E 13. In case this time is inconvenient for you, please let us know — we will arrange another meeting.
The results of the end-of-term exam are now online.
The end-of-term exam will take place on Tuesday, the 26th of July, 9am-12 noon, Hörsaal 2, building E1.3.
There will be two tutorials: A and B. Tutorial A takes place in Seminarraum 0.01, building E2.1 (bioinformatics), and includes student groups with odd numbers (G01,G03,…). Tutorial B takes place in Seminarraum U12, building E 1 1, and includes student groups with even numbers (G02,G04,…).
The first tutorial will take place on the 21st of April 2011, 10:15am.
The first lecture will take place on the 12th of April 2011, 10:15am.

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 (omega-automata)
Infinite two-player 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.) ISBN-10: 0387292373
Bakhadyr Khoussainov, Anil Nerode Automata Theory and its Applications Birkhauser Boston; 1st edition (February 15, 2001), ISBN: 0817642072

Vertiefungsvorlesung (6 CP)
Sommersemester 2011