Lecture: Algorithmic Automata Theory
Summer term 2018
News
- April 3
-
The first lecture will take place on Monday, April 8.
- April 25
-
There will be no exercise this week.
- May 24
-
There will be no exercise this week.
-
There will be no class on 17/Jul/2019.
Organisation
-
The lecturer and examiner is Dr. Prakash Saivasan.
-
Entry in the list of lectures:
Lecture,
Exercises.
-
The dates 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
Lecture Notes
The lecture comes with slides (20.11.2013).
Moreover, there are handwritten notes, partly from former courses, partly new.
Exercises
The exercise sheet will be made available here.
- 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.
If you have questions or encounter problems with the exercises, please contact Prakash.
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
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.
- 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 ]
