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


  • 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
L10 6.12.16 Complementation of Büchi automata cont'd, other acceptance conditions 7
T6 7.12.16
L11 7.12.16

other acceptance conditions cont'd. Determinisation of automata on infinite words. Motivation, preliminary considerations.
7 8.1
L12 13.12.16 Determinisation of Buchi automata wth Safra Construction 8.2 
T7 14.12.16
L13 14.12.16 Correctness of Safra construction, Piterman construction 8.2 8.3
L14 20.12.16 Algorithms for automata on infinite words. Size-change termination 9.1 9.3
T8 21.12.16
L15 21.12.16 Automata on finite trees 12
L16 10.01.17 Automata on finite trees, cont'd. 12
T9 11.01.17
L17 11.01.17 Applications: higher-order matching, XML 13
L18 17.01.17 Automata on infinite trees, parity games (definition) 14, 15.1
T10 18.01.17
L19 18.01.17 Solution of parity games, positional determinacy. 15.1
L20 24.01.17 Complementation of parity tree automata, Rabin's theorem. 15.2
T11 25.01.17
L21 25.01.17 Synthesis of reactive systems with parity games (Pnueli's theorem), modal mu-calculus 16.3
L22 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. More information to follow.

Document Actions