Algorithmic Automata Theory 2021
News
- August 02
- The exam will be held via BigBlueButton under the following Link: BBB Link.
- April 26
- The date for the first tutorial has been added.
- March 26
- The information on this page is preliminary.
Organization
The course is offered as a self-study course (Selbststudium): there are no lectures (neither in person nor as video). Participants are supposed to work through the below material independently on their own.
There will be online tutorials where participants can ask questions about predefined topics from the lecture notes.
Participants are required to do the exercises listed below. However, the solutions are not marked/graded. Solutions may be discussed during tutorials.
If you have any questions, please contact: Thomas Haas, Sören van der Wall, and Sebastian Wolff.
Tutorials
The tutorials will be given by Thomas Haas, Sören van der Wall, and Sebastian Wolff. Prof. Roland Meyer may join the meetings as well to discuss the material.
Tutorials are optional (not mandatory). Participants are encouraged to prepare questions and send them to the lecturer of the tutorial in advance for smoother operations (in particular, if you have detailed questions on, e.g., some result or proof). We expect to have tutorials every other week. The preliminary schedule for tutorials is as follows:
-
29.04.2021, 11:00: Tutorial for Lecture weeks 1 and 2 (Regular languages, WMSO, Intro to Ehrenfeucht-Fraïssé games).
Lecturer: Sebastian Wolff
The tutorial will take place here: https://webconf.tu-bs.de/seb-wdn-a46 -
18.05.2021, 11:30: Tutorial for Lecture weeks 3 and 4 (Ehrenfeucht-Fraïssé games to Presburger arithmetic).
Lecturer: Roland Meyer and Sebastian Wolff
The tutorial will take place here: https://webconf.tu-bs.de/seb-wdn-a46 -
03.06.2021, 11:30: Tutorial for Lecture weeks 5 and 6 (Semi-linear sets, Verma/Seidl/Schwentick).
Lecturer: Sören van der Wall
The tutorial will take place here: BBB -
17.06.2021, 11:30: Tutorial for Lecture weeks 7 and 8 (Büchi Automata, Ramsey's Theorem, Complementation).
Lecturer: Sören van der Wall
The tutorial will take place here: BBB -
01.07.2021, 11:30: Tutorial for Lecture weeks 9 and 10 (LTL, Pushdown systems).
Lecturer: Thomas Haas
The tutorial will take place here: BBB -
15.07.2021, 11:30: Tutorial for Lecture weeks 11 and 12 (Regular tree languages, Parity Games).
Lecturer: Thomas Haas
The tutorial will take place here: BBB -
22.07.2021, 11:30: Tutorial for Lecture week 13 (Parity Tree Automata).
Lecturer: Thomas Haas
The tutorial will take place here: BBB
Lecture Notes
The lecture comes with slides and handwritten notes:- Overview of the topics presented in this course. (Week 1)
- Regular languages - Text 1. (Week 1)
- Regular languages - Text 2. (Week 1)
- Introduction to WMSO. Büchi's theorem - Text 1. (Week 2)
- Büchi's theorem - Text 2. (Week 2)
- Büchi's theorem - Text 3. (Week 2)
- Ehrenfeucht-Fraïssé games - Text 1. (Week 2/3)
- Ehrenfeucht-Fraïssé games - Text 2. Star-free languages - Text 1. (Week 3)
- Star-free languages - Text 2. (Week 3)
- Correction of the finite index proof. (Week 3)
- Presburger arithmetic - Text 1: automata for solution spaces. (Week 3/4)
- Presburger arithmetic - Text 2: quantifier elimination. (Week 4)
- Semi-linear sets. (Week 4/5)
- Ginsburg and Spanier's theorem. Parikh's theorem. (Week 5)
- Verma, Seidl, Schwentick 2005. (Week 6)
- Reversal-bounded Counter Machines. (Week 6/7)
- ω-regular Languages. Büchi automata - Text 1. (Week 7)
- Intersection of ω-regular languages. König's theorem. Ramsey's theorem. (Week 7)
- Complementation of Büchi automata. (Week 8)
- Example on the complementation of Büchi automata. (Week 8)
- Decision procedures - Text 1. (Week 8)
- Decision procedures - Text 2. LTL - Text 1. (Week 9)
- LTL - Text 2. (Week 9)
- Pushdown systems - Text 1. (Week 9)
- Pushdown systems - Text 2. (Week 9/10)
- Pushdown systems - Text 3. (Week 10)
- Pushdown systems - Examples. (Week 10)
- Regular tree languages - Text 1. (Week 10)
- Regular tree languages - Text 2. (Week 10)
- XML and tree languages - Text 1. (Week 11)
- XML and tree languages - Text 2. (Week 11)
- Parity games - Text 1. (Week 11)
- Parity games - Text 2. (Week 12)
- Parity games - Text 3. (Week 12)
- Parity tree automata - Text 1. (Week 12)
- Parity tree automata - Text 2. (Week 13)
- Parity tree automata - Text 3. Rabin's theorem. (Week 13)
Exercises
The exercise sheets are taken from a previous iteration of the lecture (disregard the due date and meta information from the sheets).
Participants have to hand in their solutions to the exercise sheets by the given due date. Send solutions to: Thomas Haas, Sören van der Wall, and Sebastian Wolff.
- Sheet 1, due 26.04.2021.
- Sheet 2, due 03.05.2021.
- Sheet 3, due 10.05.2021.
- Sheet 4, due 17.05.2021.
- Sheet 5, due 31.05.2021.
- Sheet 6, due 7.06.2021.
- Sheet 7, due 14.06.2021.
- Sheet 8, due 21.06.2021.
- Sheet 9, due 28.06.2021.
- Sheet 10, due 05.07.2021.
- Sheet 11, due 12.07.2021.
- Sheet 12, due 19.07.2021.
- Sheet 13, optional.
Content
- Finite state systems
- Büchi automata
- MSO and Büchi's theorem
- LTL and Presburger arithmetic
- Recursive programs
- Pushdown automata, pre* and post*
- Bounded context switching
- Tree automata, Rabin's theorem
- Parameterised systems
- Regular model checking
- LTL(MSO)
- Quotients, abstraction, and extrapolation
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. Available online under http://www.model.in.tum.de/~esparza/automatanotes.html, 2012.
- H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi. Tree Automata Techniques and Applications. Available online under http://tata.gforge.inria.fr, 2007.
- 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. Free version can be found here, signature in library is INF 360/140-3.
- 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. Free version can be found here, signature in library is INF 485/109-1997.
- 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 here.
- K. N. Verma, H. Seidl, T. Schwentick, On the Complexity of Equational Horn Clauses. Available here.