|Course||References||Lecture Notes||Problem Sets|
Automata, Games, and Verification
|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|
- 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.
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.
- 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
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
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.)
|Bakhadyr Khoussainov, Anil Nerode
Automata Theory and its Applications
1st edition (February 15, 2001),
Vertiefungsvorlesung (6 CP)