- 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. Size-change termination||9.1 9.3|
|L14||21.12.16||Automata on finite trees||12|
|L15||10.01.17||Automata on finite trees, cont'd.||12|
|L16||11.01.17||Applications: higher-order matching, XML||13|
|L17||17.01.17||Automata on infinite trees, parity games (definition)||14, 15.1|
|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|
|L20||25.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. 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.