Infinite Computations

 

Lecture in Winter Term 2015/2016

Contact

Wolfgang Thomas

Phone

work
+49 241 80 21710

Email

E-Mail
 
 

Content

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 like safety, recurrence, etc.

Part II: Applications

  1. Decidability results on logical systems
  2. An automata based theoretic approach to model-checking
  3. 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.

 

Organisation

The course will be held in English.

Lecturer

Wolfgang Thomas

 

External Links