Theoretical Computer Science

Advanced Automata Theory 2016

News

• The exam dates are 18th and 19th of August. Please contact Sebastian for appointments.

Organisation

• The lecture will be given by Emanuele D'Osualdo.
• The dates and rooms of the lecture are:
  • Tuesdays, 08:15 - 09:45 in 48-210
  • Wednesdays, 13:45 - 15:15 in 46-280
• The tutorials in the second half of the term will be given by Sebastian Schweizer. The tutorials in the first half of the term were given by Sebastian Muskalla.
• The dates and rooms of the tutorials are:
  • Tuesdays, 10:00 - 11:30 in 44-336
  starting in the second week (April 26).
  • Please hand in your solution in groups of 2 to 3 people.
  • Exercises will be made available here on Wednesday evenings.
  • Submit until the following Monday, 12:00.
  • Put your submissions into the box in the staircase of building 34, 4th floor, close to room 401 and the SoftTech AG.
• 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 3)
8. Ehrenfeucht-Fraïssé games - Text 2. (Week 3)
9. Star-free languages (Week 3/4)
10. Presburger arithmetic - Text 1: automata for solution spaces. (Week 4)
11. Presburger arithmetic - Text 2: quantifier elimination. (Week 4/5)
12. Semi-linear sets. (Week 5)
13. Ginsburg and Spanier's theorem. Parikh's theorem. (Week 5)
14. Reversal-bounded Counter Machines. (Week 6)
15. ω-regular Languages. Büchi automata - Text 1. (Week 6)
16. Intersection of ω-regular languages. Ramsey's theorem. (Week 7)
17. Complementation of Büchi automata. (Week 7)
18. Example on the complementation of Büchi automata. (Week 7)
19. Decision procedures - Text 1. (Week 8)
20. Decision procedures - Text 2. LTL - Text 1. (Week 8)
21. LTL - Text 2. (Week 9)
22. Pushdown systems - Text 1. (Week 9)
23. Pushdown systems - Text 2. (Week 10)
24. Pushdown systems - Text 3. (Week 10)
25. Pushdown systems - Examples. (Week 10)
26. Regular tree languages - Text 1. (Week 11)
27. Regular tree languages - Text 2. (Week 11)
28. Parity games - Text 1. (Week 12)
29. Parity games - Text 2. (Week 12)
30. Parity games - Text 3. (Week 12)
31. Parity tree automata - Text 1. (Week 13)
32. Parity tree automata - Text 2. (Week 13)
33. Parity tree automata - Text 3. Rabin's theorem. (Week 13)
34. A sneak peek at our research:
    First-Order with reachability for infinite-state systems (for the paper see below)
35. My big fat last recap

Additional resources

• More on First-order-definable languages
• More on NFA for Presburger Arithmetics (Chapter 10)
• More on Pushdown analysis via pre*
• The paper on FO[R] for Valence Automata presented in the last lecture can be found here

Exercises

• Exercise Sheet 1
• Exercise Sheet 2
• Exercise Sheet 3
• Exercise Sheet 4 (Updated, May 12)
• Exercise Sheet 5 (Updated twice, May 19: Ex 2 c) was missing, Bug in Ex 4 fixed)
• Exercise Sheet 6 (solutions)
• Exercise Sheet 7
• Exercise Sheet 8
• Exercise Sheet 9 (Updated, Jun 16)
• Exercise Sheet 10
• Exercise Sheet 11
• Exercise Sheet 12
• Exercise Sheet 13 (solution 1b)

Contents

• Finite state automata
  • Finite state automata on words, ω-words, ranked trees and infinite trees
  • Standard constructions: union, concatenation, projection, iteration, intersection, powerset.
  • Complementation for NFA, NBA, BUTA and PTA
  • Decision procedures: emptyness, universality, inclusion
  • Equivalence of various finite state automata with MSO
  • NFA as data structures for solving Presburger arithmetic
• Logics
  • MSO over words, ω-words, ranked trees and infinite trees
  • First-order fragment
  • Presburger Arithmetic and Semilinear sets
  • LTL
• Pushdown analysis
  • Parikh's Theorem
  • Pushdown automata, pre*
  • LTL model-checking via Büchi Pushdown systems and pre*
• Games
  • Ehrenfeucht-Fraïssé games
  • Parity games

Literature

• J. Esparza. Automata theory - an algorithmic approach. Lecture notes for a course on finite and omega-automata, 2012. [Available online]
• H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi. Tree Automata Techniques and Applications, 2007. [Available online]
• 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. Signature in library is INF 360/140-3. [Available online]
• 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. Signature in library is INF 485/109-1997. [Available online]
• 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 online]
• K. N. Verma, H. Seidl, T. Schwentick, On the Complexity of Equational Horn Clauses. [Available online]