Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Applied Automata Theory 2011

We offer a new 4+2 first years Master's course on Applied Automata Theory with the following content. It can be chosen as a theory course or specialisation on The lectures will be given in German or, on request, in English.


Lecture Notes

The notes can only be accessed from within the university network.
  1. Overview of the topics presented in this lecture.
  2. Basics on regular languages.
  3. Results about regular languages and finite automata. Including Arden's lemma and powerset construction of Rabin and Scott.
  4. Introduction to weak MSO. Started with Büchi's theorem.
  5. Finished first half of Büchi's theorem. Construction for second half.
  6. Finished Büchi's theorem. Application to Presburger arithmetic.
  7. Part 1 on Ehrenfeucht-Fraïssé games.
  8. Ehrenfeucht-Fraïssé theorem. Started with star-free languages.
  9. Star-free languages, result of McNaughton and Papert.
  10. ω-regular languages. Introduction to Büchi automata. Note that the definition of ω-iterations has changed slightly.
  11. Intersection of Büchi automata, König's theorem, Ramsey's theorem.
  12. Complementation of ω-regular languages based on Ramsey's theorem. Started with decision procedures for ω-regular languages. The next lecture contains a more refined definition of →.
  13. Ramsey-based universality checking of Fogarty and Vardi.
  14. From inclusion to universality and emptiness. Syntax and semantics of LTL.
  15. Basics of LTL.
  16. From LTL to Büchi automata with Vardi and Wolper.
  17. Started with pre*-algorithm for model checking pushdown systems.
  18. Continued with pre*-algorithm for model checking pushdown systems.
  19. Proofs for pre*-algorithm.
  20. Example for pre*-algorithm. Introduction to trees.
  21. Bottom-up and top-down tree automata.
  22. Expressiveness of tree automata and decision procedures.
  23. Application of regular tree languages to solving term equations in λ-calculus.
  24. XML schema languages and hedge automata.
  25. Validity of XML documents via membership for hedge automata.
  26. Note on correctness of the pre*-algorithm.


The exercises will be available from here. The mailbox can be found in building 34, 4th floor, close to room 401 and the SoftTech AG. If you have questions or encounter problems with the exercises, please contact us — just pass by our offices or drop us a mail.


Click here for a full description (in German).


The lectures will be based upon the following books and articles. Most of them are available online, the remaining ones can be found in the library.