Automata and Reactive Systems

» Diese Veranstaltung wird auf englisch gehalten.

Lecture in winter term 2002/2003

V4 Tue 10:00h-11:30h AH VI
Wed 10:00 - 11:30 AH VI
15.10.2002 Thomas
Ü2 Thu 10:00 - 11:30 AH VI Rohde, Wöhrle


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.

The lecture will be recorded with a Screen Recording Tool (Camtasia). After processing and editing the material it will be available as a video file and as slides from here.

The course is also offered within the virtual university project.


Students of the RWTH Aachen register for the exercises as usual by entering his/her name on a list which will be handed out during the first week of the lecture.

Additionally we offer remote support for up to 20 external students of the ULI project. External students have to register at

Previous knowledge

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

Curriculum relevance:

By passing the final written examination we issue an "Übungsschein" or credit points, respectively, which will be accepted by your university.

Credit Points