- 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
Lectures will be given in English; depending on the audience we may also provide English course notes.
- Volume: 3+2 academic hours per week, 6 ECTS
- Lecture: Prof. Dr. Martin Hofmann
- Tutorials: Gordon Cichon
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|
|T4||Nov. 3rd||wMSO formulae and finite automata||Exercise sheet 2 in Uniworx|
the tool MONA, definition of large models in WMSO
|2.3 2.4 (definition of "distnpluseins")|
|L6||Nov. 6th||Complexity of the decision problem for WMSO. Presburger arithmetic||2.4 2.5|
|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|
|L9||Nov. 18th||Complementation of Büchi automata||6|
|L10||Nov. 20th||Complementation of Büchi automata cont'd, other acceptance conditions||7|
|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|
|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|
|L13||Dec. 9th||Automata on finite trees||12|
|L16||Dec. 11th||Automata on finite trees, cont'd.||12|
|L17||Dec. 16th||Applications: higher-order matching, XML||13|
|L18||Dec. 18th||Automata on infinite trees, parity games (definition)||14, 15.1|
|L19||Jan. 20th||Solution of parity games, positional determinacy.||15.1|
|L20||Jan. 22nd||Complementation of parity tree automata, Rabin's theorem.||15.2|
|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.
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.
- There is a student discussion about this lecture in German on the following web site: die-informatiker.net.