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
Bernd Finkbeiner
Felix Klein

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.
  • There was another error in the construction of Problem 4 on Problem Set 6. It is corrected now.
  • There was an error in the automaton of Problem 3 on Problem Set 6. A corrected version is now online.
  • There was an error in the equation of Problem 5.c on Problem Set 5. A corrected version is now online.
  • We permanently moved to E1.3, HS 001 for the tutorial.
  • There was an error in the automaton of Problem 4 on Problem Set 4. A corrected version is now online.
  • The fourth problem set and warm-up questions are now online.
  • The third problem set and warm-up questions are now online.
  • The tutorial on May 7th will be again in E1.3, HS 001.
  • The second problem set and warm-up questions are now online.
  • There is a room change for the tutorial on April 30th. The tutorial will be in E1.3, HS 001.
  • The first problem set and the first warm-up questions are now online.
  • The first part of the lecture notes, as handed out in Lecture 1, is now available online.
  • The website is online.

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

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

Online Version (Access is free of charge if you connect from a department IP. If you encounter any problems, let us know.)

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

Past Editions