Logic and Automata
Course descriptors: Level
Professor: Leonid Libkin
Office hours: by appointment
Class meets Tuesdays and Fridays, 10:00-10:50, in AT 8.01
- 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
- 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)
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,
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
- M. Vardi's course notes on automata
- M. Vardi's Banff
notes on temporal logics and automata.
- E. Grädel, W. Thomas, and Th. Wilke. Automata, logics,
infinite games, volume 2500 of Lecture Notes in Computer
Science. Springer, 2002.
- P. Wolper. Constructing automata from temporal formulas
FWIW, here are the pdf files produced by the smartboard. But keep in
mind that more than 50% of the material was actually on the
whiteboard! Also for reasons unknown to me, the smartboard often
changes the order of pages when it produces a pdf file.
smartboad broken for lecture 17
lecture 19 (scanned notes; smartboard didn't save)
Source: Orna Kupferman, Moshe Y. Vardi, Pierre Wolper: An
automata-theoretic approach to branching-time model checking. J.
ACM 47(2): 312-360 (2000)
- Determinization of automata for unranked trees.
Source: Julien Cristau, Christof Loeding, Wolfgang Thomas:
Deterministic Automata on Unranked Trees. FCT 2005: 68-79
Source: Rajeev Alur, P. Madhusudan: Adding Nesting Structure to
Words. Developments in Language Theory 2006: 1-13
Complementation without determinization
Source: Orna Kupferman: Avoiding Determinization. LICS 2006:
Sources: Achim Blumensath, Erich Graedel: Automatic Structures.
LICS 2000: 51-62
Michael Benedikt, Leonid Libkin, Thomas Schwentick, Luc
Definable relations and first-order query languages over
Journal of the ACM 50(5): 694-751 (2003)
Branching time temporal logics and automata
LTL for pushdown systems.
J. Esparza, A. Kucera, S. Schwoon: Model checking
LTL with regular valuations for pushdown systems. Inf. Comput. 186(2):
Infinite graphs with decidable MSO theories.
Wolfgang Thomas: Constructing Infinite Graphs with a Decidable MSO-Theory. MFCS 2003: 113-124
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)