Theoretical Computer Science

Applied Automata Theory 2012/2013

• Algorithmics
• Verification
• Embedded Systems.

News

• The exams take place in Prof. Meyer's office 34-428.
• In the next days we will publish a bonus exercise sheet for those who want to practice some more assignments or who still need points for admission to the exam.
• Please send us your preferred exam dates until January 8th 2013.
• There will be no exams between March 6th and March 8th. Please choose out of the remaining dates or (the added date) March 11th.
• There will be two exam sessions for our Applied Automata Theory course: from February 25th until March 8th, respectively from April 8th until April 12th. Please email us with your preferred dates -- out of the given ones -- so that we can schedule the exams. Please be as generous as possible about the dates you prefer.
• There is a new text on Büchi automata complementation (example). You may submit the corresponding exercise sheet on Wednesday.
• There is no lecture on Wednesday, 5th December. We will compensate for it by an additional appointment at the end of the lecture period. The date of the future appointment is to be agreed upon.
• The article on program termination can be found here.
• There are lecture notes by Javier Esparza that cover a good deal of topics we discuss in this course. In particular the construction of DFAs for Presburger arithmetic is due to Esparza and can be found in Chapter 10.
• The room for the tutorials on Wednesday 11:45 - 13:15 is 48-210. All rooms are fixed now.
• Due to a prior conflicting appointment of Prof. Meyer, the lecture next Tuesday, 30th October and the tutorial on Wednesday, 31st October have to be exchanged. Moreover, there will be no tutorial on Thursday, 1st November (Allerheiligen religious holiday). For this reason, we kindly ask you to hand in your solutions to the 2nd exercise sheet anytime before the tutorial on Tuesday, 30th October.
• The lecture classrooms are 46-268 (Tuesdays 10:00 - 11:30), respectively 48-462 (Wednesdays 10:00 - 11:30).
• The first tutorial is on Wednesday, 24th October after the lecture (11:45 - 13:15).
• There will be oral exams. To be admitted, you need 60 percent of your exercises marked by a plus (useful answer). Moreover, a presentation of your exercises on the board is mandatory.

Organisation

• The dates and rooms of the lecture are:
  • Tuesdays 10:00 - 11:30 in 46-268
  • Wednesdays 10:00 - 11:30 in 48-462
• Tutorials take place on Wednesdays, 11:45 - 13:15 in 48-210 and Thursdays 11:45 - 13:15 in 32-439.
• There will be oral exams. To be admitted, you have to fulfil the following requirements:
  • 60 percent of your exercises have to be marked by a plus (useful answer).
  • You have to present some of your exercises on the board .

Lecture Notes

1. Overview of the topics presented in this course. (Week 1)
2. Regular languages - Text 1. (Week 1)
3. Regular languages - Text 2. (Week 1)
4. Introduction to WMSO. Büchi's theorem - Text 1. (Week 2)
5. Büchi's theorem - Text 2. (Week 2)
6. Büchi's theorem - Text 3. (Week 2/3, we defer the Presburger part for a moment)
7. Ehrenfeucht-Fraïssé games - Text 1. (Week 3)
8. Ehrenfeucht-Fraïssé games - Text 2. Star-free languages - Text 1. (Week 3/4)
9. Star-free languages - Text 2. (Week 4)
10. Correction of the finite index proof. (Week 4)
11. Presburger arithmetic - Text 1: automata for solution spaces. (Week 4)
12. Presburger arithmetic - Text 2: quantifier elimination. (Week 5)
13. Semi-linear sets. (Week 5)
14. Ginsburg and Spanier's theorem. Parikh's theorem. (Week 6)
15. ω-regular Languages. Büchi automata - Text 1. (Week 6)
16. Intersection of ω-regular languages. König's theorem. Ramsey's theorem. (Week 7)
17. Complementation of Büchi automata. Decision procedures - Text 1. (Week 7/8)
18. Example on the complementation of Büchi automata. (Week 8)
19. Decision procedures - Text 2. (Week 9)
20. Decision procedures - Text 3. LTL - Text 1. (Week 9)
21. LTL - Text 2. (Week 10)
22. Pushdown systems - Text 1. (Week 11)
23. Pushdown systems - Text 2. (Week 11)
24. Pushdown systems - Text 3. (Week 11)
25. Pushdown systems - Examples. (Week 11)
26. Regular tree languages - Text 1. (Week 12)
27. Regular tree languages - Text 2. (Week 12)
28. Lambda equations and tree languages. (Not in the lecture)
29. XML and tree languages - Text 1. (Week 13)
30. XML and tree languages - Text 2. (Week 13)
31. Parity games - Text 1. (Week 13)
32. Parity games - Text 2. (Week 14)
33. Parity games - Text 3. (Week 14)

Exercises

• Download Exercise Sheet 1 here. Download a conceivable solution here.
• Download Exercise Sheet 2 here. Download a conceivable solution here.
• Download Exercise Sheet 3 here. Download a conceivable solution here.
• Download Exercise Sheet 4 here. Download a conceivable solution here.
• Download Exercise Sheet 5 here. Download a conceivable solution here.
• Download Exercise Sheet 6 here. Download a conceivable solution here.
• Download Exercise Sheet 7 here. Download a conceivable solution here.
• Download Exercise Sheet 8 here. Download a conceivable solution here.
• Download Exercise Sheet 9 here. Download a conceivable solution here.
• Download Exercise Sheet 10 here. Download a conceivable solution here.
• Download Exercise Sheet 11 here. Download a conceivable solution here.
• Download Exercise Sheet 12 here. Download a conceivable solution here.
• Download Exercise Sheet 13 here. Download a conceivable solution here.
• The not mandatory exercise sheet is out there.

Content

• Finite state systems
• Büchi automata
• MSO and Büchi's theorem
• LTL and Presburger arithmetic
• Recursive programs
• Pushdown automata, pre* and post*
• Bounded context switching
• Tree automata, Rabin's theorem
• Parameterised systems
• Regular model checking
• LTL(MSO)
• Quotients, abstraction, and extrapolation

Literature

• J. Esparza. Automata theory - an algorithmic approach. Lecture notes for a course on finite and omega-automata. Available online under http://www.model.in.tum.de/~esparza/automatanotes.html, 2012.
• H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi. Tree Automata Techniques and Applications. Available online under http://tata.gforge.inria.fr, 2007.
• M. Hofmann and M. Lange. Automatentheorie und Logik. Springer-Verlag, 2011.
• W. Thomas. Languages, Automata, and Logic. In Handbook of Formal Languages, volume 3, pages 389-455, Springer-Verlag, 1996. Free version can be found here.
• A. Bouajjani, J. Esparza, O. Maler. Reachability analysis of pushdown automata: application to model checking. In Proc. of the 8th International Conference on Concurrency Theory, CONCUR, volume 1243 of LNCS, pages 135-150, Springer-Verlag, 1997. Free version can be found here
• E. Best. Model Checking. Lecture notes from 2010/2011. Available here, the page contains interesting literature.
• L. Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 2004.

Seminar on Applied Automata Theory 2012/2013

• Topic bounded tree-width already taken.
• Topic nested words already taken.
• Topic timed automata already taken.
• Topic regular model checking already taken.
• Topic automatic structures already taken.