Institute of Theoretical Computer Science

Lecture: Algorithmic Automata Theory

We offer oral exams on the following dates: August 31, September 1, and September 22. To get an appointment for the exam, please write a mail to Sebastian. It should contain your full name, your Matrikelnummer, the date, and your preferred time (e.g. in the morning or afternoon), and whether you want to do the exam in German or English.
The notes on hedge automata and visibly pushdown automata as well as the corresponding exercise sheet are now online!
The first lecture will take place on Monday, April 3, 9:45 - 11:15 in room IZ 358.
The exercises will start in the second week of the lecture period. More information on the organization will be provided in the first lecture.
Since few of you did not want the due date of the exercise to be immediately after the easter holidays, you can take till 20'th noon to submit your solutions. We will decide on an alternate date for the tutorial by mail.

The lecture will be given by Prof. Roland Meyer and Dr. Prakash Saivasan.
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, 16:30 - 18:00 in IZ 358
The date and room for the exercise class:
- Tuesday, 13:30 - 15:00 in IZ 358

The lecture comes with slides (20.11.2013). Moreover, there are handwritten notes, partly from last year, partly new.

If you have questions or encounter problems with the exercises, please contact Prakash.

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

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 ]