**Summer 2007
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:

References:

For automata on words and trees, MSO<->Automata, etc.

For definitions and properties of tree automata.

For bounded tree width graphs, tree interpretations, Courcelle's theorem, etc.

Lecture 1: Overview of the course: Overview Slides

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