Infinite Computations

» This course is given in English.

» There is an L2P learning room for this course.

Lecture in Winter Term 2013/2014

TypeTime/PlaceLecturer
V3 Tue 10:15–11:45, AH III
Thu 09:15–10:00, room 5056 10:15–11:00, AH II
Thomas
Ü2 Mo 14:15–15:45, AH III Thomas, Brütsch

Important: The dates of the first lecture and the first exercise class will be swapped:
The first lecture will take place on Monday, October 14 from 14:15 to 15:45 in AH III.
The first exercise class will be on Tuesday, October 15 from 10:15 to 11:45 in AH III.

After that, the lectures and exercise classes will take place as indicated in the table above.

Contents

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.

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

Previous Knowledge

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