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
- Algorithmics
- Verification
- Embedded Systems.
The lectures will be given in German or, on request, in English.
News
-
Thursday, the 28th of July, from 09:00 to 11:00 there is an extra meeting in building 34, room 420.
- A note on the correctness of pre* can be found here.
- The tree automata part was inspired by chapter 8 in this book.
-
Please email wishes for exam dates (05th of August, 08th of August, or October) to Georg Zetzsche or Roland Meyer.
-
Friday, the 01th of July, at 10:00 we will have an additional lecture in building 34, room 420.
-
The 1st round of oral examinations will take place on Friday, the 05th of August and on Monday, the 08th of August. There will be a 2nd round of exams in October.
-
There will be no lectures on Monday, the 04th of July and on Tuesday, the 05th of July. We will compensate the missing lessons by two additional appointments, the first of which will be a regular lecture, the second will be a recapitulation at the end of the lecture period. The dates are to be agreed upon.
-
The tutorials will take place on Thursdays, 10:00-11:30 in
building 34, room 420. The exercise sheets will be available on
Wednesdays. The solutions are due on Tuesdays at noon. Please try to solve and
turn in the exercises in groups of 2-3 people.
-
There will be oral exams. To be admitted, you
need 60 percent of your exercises marked by a plus
(useful answer). Moreover, two presentations of your
exercises on the board are mandatory.
Lecture Notes
The notes can only be accessed from within the university network.
- Overview of the topics presented in this lecture.
- Basics on regular languages.
- Results about regular languages and finite automata. Including Arden's lemma and powerset construction of Rabin and Scott.
- Introduction to weak MSO. Started with Büchi's theorem.
- Finished first half of Büchi's theorem. Construction for second half.
- Finished Büchi's theorem. Application to Presburger arithmetic.
- Part 1 on Ehrenfeucht-Fraïssé games.
- Ehrenfeucht-Fraïssé theorem. Started with star-free languages.
- Star-free languages, result of McNaughton and Papert.
- ω-regular languages. Introduction to Büchi automata. Note that the definition of ω-iterations has changed slightly.
- Intersection of Büchi automata, König's theorem, Ramsey's theorem.
- 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 →.
- Ramsey-based universality checking of Fogarty and Vardi.
- From inclusion to universality and emptiness. Syntax and semantics of LTL.
- Basics of LTL.
- From LTL to Büchi automata with Vardi and Wolper.
- Started with pre*-algorithm for model checking pushdown systems.
- Continued with pre*-algorithm for model checking pushdown systems.
- Proofs for pre*-algorithm.
- Example for pre*-algorithm. Introduction to trees.
- Bottom-up and top-down tree automata.
- Expressiveness of tree automata and decision procedures.
- Application of regular tree languages to solving term equations in λ-calculus.
- XML schema languages and hedge automata.
- Validity of XML documents via membership for hedge automata.
- Note on correctness of the pre*-algorithm.
Exercises
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.
- Download Exercise Sheet 1 here.
- Download Exercise Sheet 2 here.
- Download Exercise Sheet 3 here. Sorry for the delay, please hand in until Wednesday (noon). Gave a name to universal WMSO. In Exercise 1, you may simplify your automaton as soon as you know the final states are no longer reachable. You may also use the modified parallel composition over three automata.
- Download Exercise Sheet 4 here. In Exercise 2 you need the fact that i ≠ j. Thanks to those who spotted the bug!
- Download Exercise Sheet 5 here.
- Download Exercise Sheet 6 here.
- Download Exercise Sheet 7 here.
- Download Exercise Sheet 8 here.
- Download Exercise Sheet 9 here.
- Download Exercise Sheet 10 here.
- Download Exercise Sheet 11 here.
If you have questions or encounter problems with the exercises, please contact us — just pass by our offices or drop us a mail.
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
Click here for a full description (in German).
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.
- H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi. Tree Automata Techniques and Applications. Available on 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.
- 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
- 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.
