Professor: Leonid Libkin

Office hours: by appointment

Class meets Tuesdays and Fridays, 10:00-10:50, in AT 8.01

Announcements

- The first class will meet in the seminar area on level 2 of
Appleton Tower (do
**not**confuse this with room 2.02! Use the other door.)

- Appleton Tower is likely to be evacuated this evening (21/02). It is supposed to reopen tomorrow at 8am. However, before heading here, please check this page and the university webpage as there is a chance the building will remain closed.
- Due to maintanence works in AT, we won't be able to use 8.01 next week. The class will meet in AT 7.02 on Tuesday the 26th, and AT 6.01 on Friday the 29th.
- Room change: on 11 March, the class will be in AT 6.01.
**Presentations**: 31 March, 10am, room AT 8.02.

Homeworks and Assignments

- Homework 1 assigned 25 January; due 5 February (AT 2.13 or AT 2.17, before 3pm)
- Homework 2 assigned 14 February; due 22 February (AT 2.13 or AT 2.17, before 3pm)
- Homework 3 assigned 7 March; due 14 March (AT 2.13 or AT 2.17, before 3pm)
- Assignment 1 assigned 22 February; due 29 February (AT 2.13 or AT 2.17, before 5pm)
- Assignment 2 assigned 1 April; due 10 April (AT 2.13 or AT 2.17, before 3pm)

Lecture materials

There is no text on the subject at the moment.

Students taking the course will be given class notes from 2007.

Other useful references are:

**Infinite Words: Automata, Semigroups, Logic and Games**, by D. Perrin and J.-E.Pin,

chapter "Automata and infinite words"- W. Thomas.
**Languages, automata and logic**. Chapter in the*Handbook of Formal Languages*. Linked here is a technical report whose contents are very close to the chapter. - F. Neven. Automata theory for XML researchers. A nice short survey presenting tree automata.
- I. Walukiewicz. Automata and Logic. (these notes concentrate on the mu-calculus).
- L. Libkin. Elements of Finite Model Theory, Chapter 7.
- M. Vardi's course notes on automata in verification.
- M. Vardi's Banff notes on temporal logics and automata.
- E. Grädel, W. Thomas, and Th. Wilke.
**Automata, logics, and infinite games**, volume 2500 of*Lecture Notes in Computer Science*. Springer, 2002. - P. Wolper. Constructing automata from temporal formulas

lecture 2 lecture 3 lecture 4 lecture 5 lecture 6 lecture 7 lecture 8 lecture 9 lecture 10 lecture 11 lecture 12 lecture 13 lecture 14

lecture 15 lecture 16 smartboad broken for lecture 17 lecture 18 lecture 19 (scanned notes; smartboard didn't save) lecture 20 additional lecture

- Determinization of automata for unranked trees.

Source: Julien Cristau, Christof Loeding, Wolfgang Thomas: Deterministic Automata on Unranked Trees. FCT 2005: 68-79

paper -
Nested words.

Source: Rajeev Alur, P. Madhusudan: Adding Nesting Structure to Words. Developments in Language Theory 2006: 1-13

paper -
Complementation without determinization

Source: Orna Kupferman: Avoiding Determinization. LICS 2006: 243-254

paper -
Automatic structures

Sources: Achim Blumensath, Erich Graedel: Automatic Structures. LICS 2000: 51-62

Michael Benedikt, Leonid Libkin, Thomas Schwentick, Luc Segoufin: Definable relations and first-order query languages over strings. Journal of the ACM 50(5): 694-751 (2003)

paper 1

paper 2 -
Branching time temporal logics and automata
Source: Orna Kupferman, Moshe Y. Vardi, Pierre Wolper: An
automata-theoretic approach to branching-time model checking. J.
ACM 47(2): 312-360 (2000)

paper - LTL for pushdown systems.

J. Esparza, A. Kucera, S. Schwoon: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2): 355-376 (2003)

paper - Infinite graphs with decidable MSO theories.

Wolfgang Thomas: Constructing Infinite Graphs with a Decidable MSO-Theory. MFCS 2003: 113-124

paper **NOTE:**all these papers are only available from the School of Informatics machines (unless you have your own subscriptions to Springer Link, ACM DL, etc)