Automata and Reactive Systems

» Diese Veranstaltung wird auf englisch gehalten.

Lecture in winter term 2006/2007

V4 Tue 10:00 - 11:30 AH VI
Wed 08:15 - 9:45 AH VI
Ü2 Tue 12:00 - 13:30 AH VI 19.10.2006 Thomas, Carayol, Spelten


This course offers an introduction to the theory of automata on infinite words. The central application area is the analysis and synthesis of "reactive systems". These are systems such as controllers and communication protocols, in which two features are essential: Usually they do not terminate, and they are in continuous interaction with their environment.

In the first part of the course we concentrate on the specification of non-terminating behaviour. For this purpose one uses finite automata which accept infinite words. Many results of the theory of automata on finite words can be transferred to the case of infinite words, but more complex constructions are necessary. We also present the connection between automata and logical systems and introduce the method of "model-checking", the algorithmic verification of state-based systems.

The second part of the course deals with the interaction between two parties in reactive systems: In an abstract sense, "program" and "environment" are the players in an infinite two-person game. Program construction then amounts to the construction of a winning strategy. We show how to find winning strategies in infinite games when the state space of the system under consideration is finite.

Previous Knowledge

Basic knowledge of automata theory as presented in basic courses is required for participation.


Students register for the exercises by registering for the lecture via the campusOffice system. The deadline for registration is October 24, 2006.

Credit Points