Logic and
Theory of
Discrete Systems

Informatik 7

Infinite Computations

Lecture in Winter Term 2014/2015

This course is given in English.

V3 Tue 09:15–10:00, AH I
Thu 12:15–13:45, AH II
Löding Campus link
Ü2 Fr   08:30–10:00, AH II Löding, Brütsch Campus link

The first lecture will take place on Tuesday, October 14.
The first tutorial will take place on Friday, October 17.


This course is mainly addressed to M.Sc. students, but 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.

The aim of this course is to introduce automata over infinite words and 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. Survey on more complex types of omega-languages

Previous Knowledge

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