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. Size-change termination 9.1 9.3
T8 21.12.16
L14 21.12.16 Automata on finite trees 12
L15 10.01.17 Automata on finite trees, cont'd. 12
T9 11.01.17
L16 11.01.17 Applications: higher-order matching, XML 13
L17 17.01.17 Automata on infinite trees, parity games (definition) 14, 15.1
T10 18.01.17
L18 18.01.17 Solution of parity games, positional determinacy. 15.1
L19 24.01.17 Complementation of parity tree automata, Rabin's theorem. 15.2
T11 25.01.17
L20 25.01.17 Synthesis of reactive systems with parity games (Pnueli's theorem), modal mu-calculus 16.3
L21 31.01.17 Slack, revision.
T12 01.02.17

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