# 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.
- 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

- 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