Theoretical Computer Science

Lecture: Algorithmic Automata Theory

Summer term 2018

News

Mai 28

The lecture of June 4th will be moved to the 15th of June, 11:30 in IZ 349. The new date for the lecture of June 5th will be announced.

March 30

The first lecture will be on Monday, 9th of April at 9:45 in IZ 358.

March 28

Basic information on the course added.

Organisation

• The lecture will be given by Dr. Prakash Saivasan and Peter Chini
• Entry in the list of lectures: Lecture, Exercises.
• The dates and rooms for the lecture are:
  • Monday, 09:45 - 11:15 in IZ 358
  • Tuesday, 15:00 - 16:30 in IZ 358
• The date and room for the exercise class:
  • Wednesday, 13:15 - 14:45 in IZ 358
• 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.
3. Regular languages - Text 2.
4. Introduction to WMSO. Büchi's theorem - Text 1.
5. Büchi's theorem - Text 2.
6. Büchi's theorem - Text 3.
7. Ehrenfeucht-Fraïssé games - Text 1.
8. Ehrenfeucht-Fraïssé games - Text 2.
9. Star-free languages.
10. Greens Relation and star-free languages.
11. Presburger arithmetic - Text 1: automata for solution spaces.
12. Presburger arithmetic - Text 2: quantifier elimination.
13. Semi-linear sets.
14. Ginsburg and Spanier's theorem. Parikh's theorem.
15. Verma, Seidl, Schwentick.
16. ω-regular Languages. Büchi automata.
17. Intersection of ω-regular languages. Ramsey's theorem.
18. Complementation of Büchi automata.
19. Example on the complementation of Büchi automata.
20. Decision procedures - Text 1.
21. Decision procedures - Text 2. LTL - Text 1.

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.

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]
• K. N. Verma, H. Seidl, T. Schwentick, On the Complexity of Equational Horn Clauses. [Available online]
• M. Bojańczyk, Factorization Forests. [ Available online ]