Links und Funktionen

You are here: Home / Teaching / Winter 2016/17 / Automata Theory


Automata Theory

Lecture, 3 hours per week, Tu 10am-12pm, We 2pm-4pm, Hofmann; Tutorial, 2 hours per week, We noon-2pm, Jost


  • We are offering the opportunity for an individual practical for masters programme CS students. The practical work would continue the topics discussed in this lecture and award 6 ECTS towards the compulsory P1(INF-PfTI) module. Interested students should inquire directly by Prof. Hofmann. 
    (A possibility for a thesis topic for bachelor students might also exist.)
  • It is mandatory to sign up for this course via UniWorX (available from 1st October onwards)


This course is an introduction to the theory of finite automata on infinite words on trees. The main application of such automata is the development of decision procedures for various logics.

Keywords: Büchi-Elgot theorem, Presburger arithmetic, LTL, XML, Rabin theorem, modal mu-calculus.

This course is based on the textbook Automatentheorie und Logik (in German). The lecture notes from 2010 are freely available.


Place and Time

Lecture Tuesday, 10am-12pm Amalienstr. 73A, 120 18.10.2016
Lecture Wednesday, 2pm-4pm Oettingenstr. 67, 165
Tutorial Wednesday, noon-2pm Oettingenstr. 67, 165  2.11.2016

To reach the planned 3 hours per week, lectures will only be held on the dates shown in the table below. Tutorials are held every week.

Type/# Date Topic Sections in textbook
L1 18.10.16 Revision of regular languages and finite automata 1.1.1, 1.1.2
L2 19.10.16 Deterministic finite automata. Decision problems for finite automata. 1.1.3
01.11.16 (Public holiday)
T1 02.11.16 Introduction to finite automata Exercise sheet via Uniworx
L3 08.11.16 Weak monadic second-order logic (WMSO): syntax and semantics. 2.1 2.2
T2 09.11.16
L4 09.11.16 Decision procedure for WMSO, WMSO formulae and finite automate 2.2
L5 15.11.16 the tool MONA, definition of large models in WMSO
Mona files: even.mona adder.mona binary.mona dist.mona
2.3 2.4 (definition of "distnpluseins")
T3 16.11.16
L6 22.11.16 Complexity of the decision problem for WMSO. Presburger arithmetic 2.4 2.5
T4 23.11.16
L7 23.11.16 Büchi Automata, w-regular languages 5.1 5.2
L8 29.11.16 w-regular languages the same as Büchi recognizable, deterministic Büchi automata weaker than nondeterministic ones. 5.2
T5 30.11.16
L9 30.11.16 Complementation of Büchi automata 6
6.12.16 Lecture Cancelled
T6 7.12.16
L10 7.12.16 Other acceptance conditions. Determinisation of automata on infinite words. Motivation, preliminary considerations. 7 8.1
L11 13.12.16 Determinisation of Buchi automata wth Safra Construction 8.2 
T7 14.12.16
L12 14.12.16 Correctness of Safra construction, Piterman construction 8.2 8.3
L13 20.12.16 Algorithms for automata on infinite words. Universality and Emptiness. 9.1 9.2
T8 21.12.16
L14 21.12.16 Ramsey approach to universality. Size-change termination. 9.2 9.3
L15 10.01.17 Automata on finite trees. 12
T9 11.01.17
L16 11.01.17 Applications: higher-order matching, XML 13
T10 18.01.17
L17 18.01.17 Automata on infinite trees, parity games (definition) 14, 15.1
L18 24.01.17 Solution of parity games, positional determinacy. 15.1
T11 25.01.17
L19 25.01.17 Complementation of parity tree automata, Rabin's theorem. 15.2
L20 31.01.17 Synthesis of reactive systems with parity games (Pnueli's theorem), modal mu-calculus 16.3
T12 01.02.17
01.02.17 Slack, revision.

Legend: L means lecture, T means tutorial.


Exercises sheets will be available on UniWorX



The course will be graded by a written exam. The exam will be held on Thursday, 9th February in room S004, Schellingstr.3, from 2pm to 4pm. An advance registration for the exam participation via UniWorX is mandatory! The self registration is open between 9.01.2017 and 31.01.2017.

Every participant must bring along to the exam a valid photo id and their university matriculation card.

There will be a make-up exam at the beginning of the following term. Details to follow here. Participants that did not partake in the first exam are also allowed to register for the make-up exam, provided that they acknowledge that there will not be third exam offered. 

Document Actions