Model-checking Finite Structures
4 ECTS, semestre 2, 12 semaines
| Prérequis | First semester computability and incompleteness; the second semester course on model theory can be a plus. |
| Validation | CC+examen |
| Enseignant | Sylvain Schmitz |
| Horaires hebdomadaires | 2.0 h CM |
| Années | 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.
Sommaire
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.
Bibliographie
- Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, et al., Tree Automata Techniques and Applications. 2008.
- Bruno Courcelle and Joost Engelfriet, Graph Structure and Monadic Second-order Logic. Cambridge University Press, 2012.
- Leonid Libkin, Elements of Finite Model Theory. Springer, 2012.
- Jaroslav Nešetřil and Patrice Ossona de Mendez, Sparsity. Springer, 2012.