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:

  • 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.

  • References:

  • 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.

  • June 5
    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.

  • June 7
    Lecture 3: Translating MSO (inductively) to automata
    Lecture 4: Deciding Presburger arithmetic using automata