Applied Automata Theory 2014/2015
News
- There will be another question session on Friday, 27 March at 11am in 34-420.
- Update: there are no more exams possible in April. If you still need an exam date, please register for 22 May.
- Exams will take place on Tuesday, April 7 and, if necessary, Monday, April 13. Further exams are planned for the beginning of May. Please send an e-mail to Reiner
telling him whether you want to take an exam in April or in May and whether you prefer morning or afternoon.
Organisation
-
This year's course will be based on last year's lecture notes and exercises, but there will be no regular lecture.
However, there will be a tutorial to discuss questions and solutions.
- Exercise sheets will be issued once per week and have to be handed in before the tutorial in the following week.
- There will be oral exams.
To be admitted, 60 percent of your exercises have to be marked with a plus (useful answer).
-
Tutorials take place on Thursdays, 15:30 - 17:00 in 34-420.
- If you are interested in the course, please send an e-mail to Reiner,
especially if you cannot attend the first tutorial.
Lecture Notes
For course material, please refer to last year's Applied Automata Theory lecture.
Exercises
Exercises will be made available here.
Please hand in solutions in groups of 2 to 4 people, either directly to Reiner or in the box 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.
- 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.
- Download Exercise Sheet 9 here.
- Download Exercise Sheet 10 here.
- Download Exercise Sheet 11 here.
- Download Exercise Sheet 12 here.
If you have questions or encounter problems with the exercises, please
contact Reiner.
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.
