Automata, Games, and Verification

Automata, Games, and Verification

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 behavior 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 is addressed to students interested in the theoretical concepts to analyze reactive systems using automata over infinite words, automata over infinite trees, and two-player games. The course continues on the topics of the core lecture “Verification”, the Verification lecture is not, however, a prerequisite for the AG&V course.

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

Organization

• Lectures are every Tuesday from 14:15-16:00 in building E1.3, room HS003 (starting on October 15th).
• Every Tuesday, we publish a new problem set and a new set of "warm-up" (multiple-choice) questions.
• Every Friday, there are 10-minute discussion sessions (starting on October 25th).
• We will arrange individual discussion sessions for groups of at most three people. They will be held either in person at CISPA C0 building (E9.1) in rooms 1.07 and 1.08, or if needed online. While the in-person option is the preferred one, there will be an online option available, depending on specific needs.
• Please bring your solutions to the warm-up questions to the discussion sessions. We will discuss them and any questions you may have about the content of the lectures.
• Attendance to the 10-minute discussion sessions is mandatory. You are allowed to skip at most two sessions in case you cannot make it once or twice. Otherwise, If you encounter any other issues in attending the slot, please contact us as soon as possible.
• Problem sets can be submitted at the beginning of the next lecture after the one where they were given out. The solutions to the problem set will be handed in the week following their publishing.
• Submitting problem set solutions is not mandatory. 
• Office hours are every Wednesday in CISPA C0 building (E9.1) in room 1.07 (starting in the second week of the lecture) from 11:00 until 13:00. Feel free to come and go whenever you like during these two hours.
• During the office hours, you can inspect your corrected solutions and ask questions regarding the problem set, your solution, or the lecture.
• Grade: The grade will be determined only by the grade of the exam. Participation in the weekly discussion sessions is a requirement for admission to the exam. 
• Exams: The exam will take place on February 18, 2025, at 10:00 am; the re-exam on March 25, 2025, at 10:00 am.

Recommended reading

• Lecture notes are available under Materials.
• Automata Theory: An Algorithmic Approach, by Javier Esparza and Michael Blondin, MIT Press. Available from the publisher and open access as a free pdf.
• Automata, Logics, and Infinite Games, by Erich Grädel, Wolfgang Thomas, and Thomas Wilke (editors), Springer Verlag. Available from the publisher as a free pdf from the UdS network/VPN.