RequirementsFirst semester computability and incompleteness; the second semester course on model theory can be a plus.
Program requirementsCC+examen
TeacherSylvain Schmitz
Weekly hours 2.0 h CM
Years Master Logique Mathématique et Fondements de l'Informatique

Syllabus

The course is dedicated to the model-checking problem over finite structures, with a particular focus on algorithmic meta-theorems, the main highlight of the course being Courcelle's Theorem.

A number of topics are touched upon through this lens, including some basics in complexity theory, circuit complexity, parameterised complexity, monadic second-order logic, tree languages, logical transductions, structural graph theory, etc.

Contents

Planned Contents

The exact contents might vary.

General finite structures

  • General introduction. Reminders: Trakhtenbrot's Theorem, relational databases. PSPACE completeness of first-order model-checking.
  • Circuit complexity: the class AC⁰, equivalence with first-order logic.
  • Restricting the logic: conjunctive queries. Constraint satisfaction and homomorphisms; NP-completeness of model-checking. Acyclic queries.
  • Tree-width. Parameterised complexity: XP, FPT. Conjunctive queries of bounded tree-width.

Monadic second-order logic

  • Regular tree languages and finite tree automata.
  • Monadic second order logic, decidability of model-checking over finite trees.
  • Incidence graphs and tree-width. Clique-width. Logical transductions.
  • Courcelle's Theorem.
  • Grids. Seese's Theorem and Conjecture.

First-order model-checking over restricted classes of finite graphs

  • Bounded degree graphs.
  • Locality. Locally bounded tree-width.
  • Somewhere dense graph classes. Parameterised complexity: AW[*]-hardness.
  • Stable and NIP classes: relationship with nowhere dense graph classes.
  • Logical transductions again: tree-depth, shrub-depth.

Bibliography