Logic and Automata
Course descriptors: Level
Professor: Leonid Libkin
Office hours: by appointment
Class meets Wednesdays, 11:10-13:00, AT 2.04
- 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.
- Automata on finite strings
- First-order, Second-order, and Monadic
- Buchi's theorem, automata/logic
- 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,
- Infinite strings and logics over them
over infinite strings; closure properties; logical characterisation
First-order over infinite words, temporal logics, verification
- LTL to automata translation
- Automata over infinite trees
- Rabin's theorem
- Decidability of logical theories; applications in
3 simple homeworks, worth 5% each; 2 assignments, worth 30% each; one
presentation, worth 25% (no exam)
Homeworks and Assignments
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,
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
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:
broken for lecture 17
lecture 19 (scanned notes; smartboard didn't save)
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
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
Source: Orna Kupferman, Moshe Y. Vardi, Pierre Wolper: An
automata-theoretic approach to branching-time model checking. J.
ACM 47(2): 312-360 (2000)
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
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)
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.
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)