Automata, Games, and Verification
Advanced Lecture (Vertiefungsvorlesung), Summer Term 2015, 6 CP
Lecture Room: | E1 3, HS 003 | |
Lectures: | Tuesdays, 14:15-16:00 | |
Tutorials: | Thursdays, 16:15-18:00, E1 3, SR 015 | |
Exams: | Endterm: 30.07.2015, 16:00-18:00, E2 2 | |
Re-Exam: 01.10.2015, 10:00-12:00, E2 5, HS II | ||
Contact: | agv15 at react.uni-saarland.de |
News
- The date of the Re-Exam has changed. The new date is the first of October at 10am. If this causes any problems to you, please inform us immediately!
- There was an error in Problem 4 on Problem Set 10. It is corrected now.
- There was another error in the construction of Problem 4 on Problem Set 6. It is corrected now.
Student Profile
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. In the course, we show how to formally describe such systems, how to express properties of them and discuss the neccessary steps to verify and synthesize them.
The course continues on the topics of the core lecture “Verification”, however a prior attendence is not required.
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
Calendar
References
The course will be based on the following two textbooks, supplemented as necessary by various research papers.

Automata, Logics, and Infinite Games:
A Guide to Current Research
Erich Grädel, Wolfgang Thomas,
Thomas Wilke (Eds.)
Springer, 2nd Print (1. November 2005)
LNCS (2500), ISBN 3540003886

Automata Theory and its Applications
Bakhadyr Khoussainov, Anil Nerode
Birkhauser Boston
1st edition (February 15, 2001)
ISBN 0817642072