Links und Funktionen

You are here: Home / Teaching / Winter 2014/15 / Automata Theory


Automata Theory

Lectures, 3 hours per week, Tue 10am-12pm, Thu 2pm-4pm, Hofmann; Tutorial, 2 hours per week, Mon 12-2pm, Cichon


    • 3/16/2015: Room for Make-up Exam. Date for results inspection of exam.
    • 03/11/2015: Date for Make-up Exam
    • 02/02/2015: ROOM CHANGE: exam will talk place in Room V U104 at Lehrturm!
    • 27/12/2014: Written exam scheduled for 03/02/2015 10:00am Room: V U104 (was: V005 (Tuesday's class room))
    • 11/04/2014: add link to MONA tool
    • 10/27/2014: update of dates
    • 10/16/2014: room change announcement
    • 09/29/2014: first version of english homepage


    This course covers the theory of finite automata acting on infinite strings or trees. The main application of these automata is for designing decision procedures for formal logics.

    Keywords: Büchi-Elgot Theorem, Presburger Arithmetic, LTL, XML, Rabin's Tree Theorem, modal µ-calculus

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

    Lectures will be given in English; depending on the audience we may also provide English course notes.


    Place and Time

    Lecture Tues, 10am-12pm V005 (Lehrturm, Prof.-Huber-Pl. 2) 7.10.2014
    Lecture Thur, 2pm-4pm AU 117 (HGB, Geschwister-Scholl-Platz 1) 9.10.2014
    Tutorial Mon, 12pm-2pm 218 (Amalienstr. 73A) 13.10.2014

    Since there are 4 academic hours per week, and the course itself is only 3 hours per week, there will be no lecture on the following dates: week from Oct. 20th till Oct 31st. From Dec 22nd till Jan 15th.

    Type/# Date Topic Sections in textbook Notes
    L1 Oct. 7th  Revision of regular languages and finite automata 1.1.1, 1.1.2
    L2 Oct. 9th Deterministic finite automata. Decision problems for finite automata. 1.1.3
    T1 Oct. 13th Introduction to finite automata Exercise sheet 1 in Uniworx
    L3 Oct. 14th Weak monadic second-order logic (WMSO): syntax and semantics. 2.1 2.2
    L4 Oct. 16th Decision procedure for WMSO, 2.2
    T2 Oct. 20th wMSO formulae and finite automata Exercise sheet 2 in Uniworx
    T3 Oct. 27th
    T4 Nov. 3rd wMSO formulae and finite automata Exercise sheet 2 in Uniworx
    L5 Nov. 4th

    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")
    L6 Nov. 6th Complexity of the decision problem for WMSO. Presburger arithmetic 2.4 2.5
    T5 Nov. 10th TBA
    L7 Nov. 11th Büchi Automata, w-regular languages 5.1 5.2 first part
    L8 Nov. 13th w-regular languages the same as Büchi recognizable, deterministic Büchi automata weaker than nondeterministic ones. 5.2 second part
    T6 Nov. 17th TBA
    L9 Nov. 18th Complementation of Büchi automata 6
    L10 Nov. 20th Complementation of Büchi automata cont'd, other acceptance conditions 7
    T7 Nov. 24th TBA
    L11 Nov. 25th other acceptance conditions cont'd. Determinisation of automata on infinite words. Motivation, preliminary considerations. 7 8.1
    L12 Nov. 27th Determinisation of Buchi automata wth Safra Construction 8.2
    T8 Dec. 1st TBA
    L13 Dec. 2nd Correctness of Safra construction, Piterman construction 8.2 8.3
    L14 Dec. 4th Algorithms for automata on infinite words. Size-change termination 9.1 9.3
    T9 Dec. 8th TBA 11
    L13 Dec. 9th Automata on finite trees 12
    L16 Dec. 11th Automata on finite trees, cont'd. 12
    T10 Dec. 15th TBA
    L17 Dec. 16th Applications: higher-order matching, XML 13
    L18 Dec. 18th Automata on infinite trees, parity games (definition) 14, 15.1
    T11 Jan. 12th TBA
    T12 Jan. 19th TBA
    L19 Jan. 20th Solution of parity games, positional determinacy. 15.1
    L20 Jan. 22nd Complementation of parity tree automata, Rabin's theorem. 15.2
    T13 Jan. 26th TBA
    L21 Jan. 27th Synthesis of reactive systems with parity games (Pnueli's theorem), modal mu-calculus 16.3
    L22 Jan. 29th Slack, revision.

    Legend: L means lecture, T means tutorial.



    Exercises and problem solving sessions will be available on Uniworx. There will be points on successful homeworks which can be used to improve grading in the finals.




    The exam will talk place on 03/02/2015 at 10:00am in Room V U104 at Lehrturm (close to Tuesday's lecture room). Inspection of exam results will be possible on 03/31/2015 between 9am and 10am in room E109.

    Make-up Exam

    The make-up exam will talk place on 04/15/2015 between 4pm and 6pm in room V 005 at Lehrturm, Prof.-Huber-Platz 2.

    More Information

        • There is a student discussion about this lecture in German on the following web site:

    Document Actions