- Date for exam inspection announced below.
- Make-up exam date announced below.
- 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.
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|
|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|
|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")|
|L6||22.11.16||Complexity of the decision problem for WMSO. Presburger arithmetic||2.4 2.5|
|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|
|L9||30.11.16||Complementation of Büchi automata||6|
|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|
|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|
|L14||21.12.16||Ramsey approach to universality. Size-change termination.||9.2 9.3|
|L15||10.01.17||Automata on finite trees.||12|
|L16||11.01.17||Applications: higher-order matching, XML||13|
|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|
|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|
Legend: L means lecture, T means tutorial.
Exercises sheets will be available on UniWorX.
- Textbook "Automatentheorie und Logik" (in German) by Martin Hofmann und Martin Lange, Springer Verlag
The e-book is available for free to LMU students via our library's E-Medien-Login.
- Lecture notes from 2010 (freely available)
- Homepage of the MONA tool
The course will be graded by a written exam. Every participant must bring along to the exam a valid photo id and their university matriculation card.
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.
Exam inspection: Friday, 17.3., 10:30am at room L109, Oettingenstr.67 (the TCS Meeting room)
The make-up exam be held on Friday, 21th April, from 1pm to 4pm, in room E 004, LMU Main Building, Geschwister-Scholl-Platz 1. The net exam length will again be 90 minutes. An advance registration for the exam participation via UniWorX is mandatory! The self registration is open between 17.03.2017 and 18.04.2017. Students eligible for disadvantage compensation must notify us by email until 31.03.2017. 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.