» This course is given in English.
» There is an L2P learning room for this course.
Lecture in Winter Term 2009/2010
|V3||Tue 10:00–11:30, AH VI
Wed 08:15–09:45, AH I
14 October 2009
|Ü2||Fri 14:00–15:30, AH II||23 October 2009||Thomas, Spelten, Olschewski|
The first lecture will take place on Wednesday, 14 October 2009, 09:00–09:45 AH I.
This course corresponds to the first half (and a little more) of the standard course "Automata and Reactive Systems" offered in previous years for diploma students. The second part of "Automata and Reactive Systems" (on tree automata and infinite games) will follow in the summer semester 2010.
The course is addressed to MSc students and diploma students. In a slightly reduced format, titled "Introduction to Infinite Computations", BSc students can take part in the course; in this case, the problems class will involve simpler exercises. Diploma students can reach the amount of 4 hours per week by adjoining the first half of the course "Regular and Context-Free Languages: Advanced Results"
The aim of this course is to introduce automata over infinite words and to treat several of their applications in computer science. This theory is both beautiful and a powerful basis of program verification (for non-terminating programs such as control systems).Structure of the course
- Part I: Automata on infinite words
1. Büchi automata and regular omega-languages
2. Deterministic automata on infinite words
3. Classification of sequence properties (safety, recurrence, etc.)
- Part II: Applications
4. Decidability results on logical systems
5. Automata theoretic approach to model-checking
6. Algorithmic results on linear constraints for real numbers
- Part III: Outlook
7. Context-free omega-languages
8. The Borel hierarchy
LiteratureWill be announced in the course. The main source is:
W. Thomas, Automata and Reactive Systems, Lecture Notes,
From inside the RWTH network an electronic version can be downloaded from our collection of lecture notes.
Knowledge of automata theory as presented in basic courses is required for participation.