Logic, Automata and Algorithms
June 4 - June 22, 2007
At Universita degli Studi di Salerno, Salerno, Italy.
The course will consist of 12 lectures, paced slow, and aims to
cover the connections between logic, automata and algorithms for graphs.
The main theme of the lectures will be to show how algorithmic problems
on graphs can be declaratively expressed using logic, and how automata
help in translating this logical problem into algorithms that solve
the problem. In particular, we will show how efficient algorithms can
be built for logically expressed algorithmic problems on graphs of bounded
tree width. We will also show how the satisfiability problem for classes
of graphs can be solved using tree interpretations.
The structure of the course will be roughly as follows:
Automata on finite words: review, closure properties, MSO, equivalence
of MSO and regular languages
Deciding Presburger arithmetic using automata
Automata on trees:
Closure properties, top-down vs bottom-up tree automata, MSO,
equivalence of MSO and regular tree languages.
Deciding MSO on Series parallel graphs using tree interpretations
Deciding MSO on Nested words using tree interpretations;
Applications to XML stream processing
Graphs of bounded tree width; Courcelle's theorem:
MSO on BTW graphs is solvable in linear time
Decidability of satisfiability for logics on graphs
A brief overview of Finite Model Theory.
Wolfgang Thomas: Languages, Automata and Logic
For automata on words and trees, MSO<->Automata, etc.
The TATA book
For definitions and properties of tree automata.
Parameterized Complexity Theory
For bounded tree width graphs, tree interpretations, Courcelle's theorem, etc.
Lecture 1: Overview of the course:
Lecture 2: Automata on finite words, closure properties, MSO,
examples of expressing regular languages using FOL, L_EVEN not expressible
in FOL, MSO: adding set quantifiers; capturing L_EVEN using MSO;
translating a general NFA to MSO; formal semantics of MSO and meaning of
MSO formulas with free variables.
Lecture 3: Translating MSO (inductively) to automata
Lecture 4: Deciding Presburger arithmetic using automata