Logic and Automata

Course descriptors: Level 10 Level 11

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

Homework 2

Homework 3

Assignment 1

Assignment 2

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

Smartboard from 2008

In 2008, the room had a whiteboard and a smartboard. All smartboard screenshots (roughly 50% of the material) were saved and made available as PDF files. Each corresponds to a 50-minute lecture. FWIW, here they are: 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 broken for lecture 17 lecture 18 lecture 19 (scanned notes; smartboard didn't save) lecture 20 additional lecture

Possible 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
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)