Theoretical Computer Science

Applied Automata Theory 2013/2014

News

• The exams will take place in Prof. Meyer's office 34-428.
• Please email Georgel if you don't yet have (and want) an exam appointment.
• As mentioned in class, there is no lecture on Wednesday, 26th November.
• We have a bigger room for the lecture on Wednesdays: 46-268.
• The first tutorial is on Wednesday, 30th October after the lecture (first exercise sheet is due on the 29th).
• You can check last year's Applied Automata Theory lecture for sample exercises and solutions.

Organisation

• The dates and rooms of the lecture are:
  • Tuesdays 10:00 - 11:30 in 46-220
  • Wednesdays 10:00 - 11:30 in 46-268
• 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 exercise solutions 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)
7. Ehrenfeucht-Fraïssé games - Text 1. (Week 2/3)
8. Ehrenfeucht-Fraïssé games - Text 2. Star-free languages - Text 1. (Week 3)
9. Star-free languages - Text 2. (Week 3)
10. Correction of the finite index proof. (Week 3)
11. Presburger arithmetic - Text 1: automata for solution spaces. (Week 3/4)
12. Presburger arithmetic - Text 2: quantifier elimination. (Week 4)
13. Semi-linear sets. (Week 4/5)
14. Ginsburg and Spanier's theorem. Parikh's theorem. (Week 5)
15. Verma, Seidl, Schwentick 2005. (Week 6)
16. Reversal-bounded Counter Machines. (Week 6/7)
17. ω-regular Languages. Büchi automata - Text 1. (Week 7)
18. Intersection of ω-regular languages. König's theorem. Ramsey's theorem. (Week 7)
19. Complementation of Büchi automata. (Week 8)
20. Example on the complementation of Büchi automata. (Week 8)
21. Decision procedures - Text 1. (Week 8)
22. Decision procedures - Text 2. LTL - Text 1. (Week 9)
23. LTL - Text 2. (Week 9)
24. Pushdown systems - Text 1. (Week 9)
25. Pushdown systems - Text 2. (Week 9/10)
26. Pushdown systems - Text 3. (Week 10)
27. Pushdown systems - Examples. (Week 10)
28. Regular tree languages - Text 1. (Week 10)
29. Regular tree languages - Text 2. (Week 10)
30. XML and tree languages - Text 1. (Week 11)
31. XML and tree languages - Text 2. (Week 11)
32. Parity games - Text 1. (Week 11)
33. Parity games - Text 2. (Week 12)
34. Parity games - Text 3. (Week 12)
35. Parity tree automata - Text 1. (Week 12)
36. Parity tree automata - Text 2. (Week 13)
37. Parity tree automata - Text 3. Rabin's theorem. (Week 13)

Exercises

• Download Exercise Sheet 1 here.
• Download Exercise Sheet 2 here.
• Download Exercise Sheet 3 here.
• Download Exercise Sheet 4 here.
• Download Exercise Sheet 5 here.
• Download Exercise Sheet 6 here.
• Download Exercise Sheet 7 here.
• Download Exercise Sheet 8 here.
• Download Exercise Sheet 9 here.
• Download Exercise Sheet 10 here.
• Download Exercise Sheet 11 here.
• Download Exercise Sheet 12 here.
• Download Exercise Sheet 13 here.

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, signature in library is INF 360/140-3.
• 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, signature in library is INF 485/109-1997.
• 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.
• J. Esparza. Reachability in Live and Safe Free-Choice Petri Nets is NP-complete. Available here.
• K. N. Verma, H. Seidl, T. Schwentick, On the Complexity of Equational Horn Clauses. Available here.