Logic and Automata
Course descriptors: Level
10 Level
11
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
Smartboard
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.
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
Presentation topics:
- 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)