Professor: Leonid Libkin

Office hours: by appointment

Class meets Wednesdays, 11:10-13:00, AT 2.04

Announcements

- There will be no class on Wednesday 13 October. Howework 1 can be dropped at the ITO before 4:30pm on the 13th, or alternatively left in my mailbox on the 5th floor of the Forum. If you choose to leave it in my mailbox, please put it in an envelope.

Topics

- Automata on finite strings
- First-order, Second-order, and Monadic Second-order logics
- Buchi's theorem, automata/logic connection
- Automata for deciding logical theories; complexity issues
- First-order logic on strings, star-free languages
- Tree automata on finite trees, Thatcher-Wright theorem
- Automata over unranked trees, XML applications
- Infinite strings and logics over them
- Automata over infinite strings; closure properties; logical characterisation
- First-order over infinite words, temporal logics, verification problems
- LTL to automata translation
- Automata over infinite trees
- Rabin's theorem
- Decidability of logical theories; applications in software verification

Evaluation

3 simple homeworks, worth 5% each; 2 assignments, worth 30% each; one presentation, worth 25% (no exam)

Homeworks and Assignments

- Homework 1 assigned 6 October; due 13 October
- Homework 2 assigned 12 November; due 17 November
- Homework 3 assigned 19 November; due 25 November
- Assignment 1 assigned 5 November; due 12 November
- Assignment 2 assigned 22 November; due 8 December

Lecture materials

There is no text on the subject at the moment.

Students taking the course will be given (incomplete) 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

- 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 - XML reasoning and 2-variable logic

Source: Two-variable logic on data trees and XML reasoning, by Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, J. ACM 56(3): (2009)

paper - Query automata

Source 1: Frank Neven, Thomas Schwentick: Query automata over finite trees. Theor. Comput. Sci. 275(1-2): 633-674 (2002)

Source 2: Markus Frick, Martin Grohe, Christoph Koch: Query Evaluation on Compressed Trees (Extended Abstract). LICS 2003.

paper 1

paper 2 **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)