Automata and Logic

This course considers finite automata that work on finite or infinite words and trees. The course concentrates on the connection between these automata and logics that play an important role in computer science, such as first-order logic, monadic second-order logic, and propositional dynamic logic; in particular, it will be shown how closure and decidability results for the automata can be used to obtain decidability results for these logics.

Prerequisites: Undergraduate course on automata and formal languages. Basic notions from logic would also be helpful.

The lecture takes place twice a week. Additionally, there is a weekly exercise session held by Marcel Lippmann. Exercise sheets will be available approximately one week before the session.

The lectures and exercise sessions will take place in room E05 at the following times: Tuesdays 16.40–18.10, Wednesdays 14.50–16.20, and Thursdays 16.40–18.10. The exact distribution of lectures and exercise sessions can be found in the table below.

Announcements:

• The starred lectures take place at DS 3, i.e. 11.10–12.40.
• The exercise sessions will start on 17 April.
• The lecture will start on 9 April.

	Tuesday	Wednesday	Thursday
8 Apr to 12 Apr	Lecture	Lecture	Lecture
15 Apr to 19 Apr	Lecture	Exercise session (Exercise sheet 1)	Lecture
22 Apr to 26 Apr	Lecture	Exercise session (Exercise sheet 2)	Lecture
29 Apr to 3 May	Lecture	Public Holiday	Lecture
6 May to 10 May	Lecture	Exercise session (Exercise sheet 3)	Public Holiday
13 May to 17 May	Lecture	Exercise session (Exercise sheet 4)	Lecture
20 May to 24 May	—	—	—
27 May to 31 May	Lecture	Lecture	Lecture
3 Jun to 7 Jun	Lecture	Dies academicus	Lecture
10 Jun to 14 Jun	Lecture	Lecture* Exercise session (Exercise sheet 5)	Lecture
17 Jun to 21 Jun	Exercise session (Exercise sheet 6)	Exercise session (Exercise sheet 7)	—
24 Jun to 28 Jun	Exercise session (Exercise sheet 8)	Exercise session (Exercise sheet 9)	—
1 Jul to 5 Jul	Lecture	Lecture	Output DD
8 Jul to 12 Jul	Lecture	Exercise session (Exercise sheet 10)	Lecture
15 Jul to 19 Jul	Lecture	Lecture* Exercise session (Exercise sheet 11)	Lecture

SWS: 4/2/–

This course can be used in the following modules:

• Bachelor-Studiengang Informatik: INF-B-520 (Vertiefung zur Bachelor-Arbeit)
• Master/Diplom-Studiengang Informatik: INF-BAS6 (Theoretische Informatik), INF-VERT6 (Theoretische Informatik)
• Master in Computational Logic: MCL-TCSL (Theoretical Computer Science and Logic), MCL-PI (Principles of Inference), MCL-KR (Knowledge Representation)
• Diplom-Studiengang Informatik (Studienordnung 2004): Fachgebiet Theorie der Programmierung, Fachgebiet Intelligente Systeme

A complete script of this lecture is available, both in German and in English language.

• W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133-192. Elsevier Science Publishers, Amsterdam, 1990.
• W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume III, pages 389-455. Springer, New York, 1997.
• H. Comon et al. Tree Automata Techniques and Applications. Online available at http://www.grappa.univ-lille3.fr/tata
• F. Gecseg and M. Steinby. Tree Automata. Akademiai Kiado, Budapest, 1984.