M2 course proposal: Graphs, Machines and Logic

Lecturers

• Édouard Bonnet
• Denis Kuperberg
• Stéphan Thomassé
• François Schwarzentruber

Material

• GNN and logic

General description

This course explores various connections between computational models and logical frameworks. Starting with classical equivalences from regular language theory, the course will go towards recent results. We will show how understanding the links between logics and computational models such as automata or graph neural networks allow to get a better grasp of the objects at hand, in particular obtain decidability, complexity and expressivity results. On the one hand, computational models allow to decide certain logics, and on the other hand, logics allow to characterize expressivity of computational models.

Prerequisites

There are no specific prerequisites apart from basic knowledge of logic, computational complexity, graphs, and automata.

Organization

• 15 sessions of 2 hours
• 1 exam session

Tentative outline

Automata and logic (Denis Kuperberg)

• Various formalisms to recognize languages:
  • Automata on finite and infinite words
  • Monadic-Second Order Logic (MSO)
  • Linear Temporal Logic (LTL)
  • Monoids
• Results:
  • Equivalences MSO <-> Automata <-> Monoids
  • Equivalences First-Order Logic (FO) <-> LTL <-> Aperiodic Monoids (some proofs will be sketched only) Ehrenfeuch-Fraïssé games will be introduced
  • Complexity aspects
  • Decidability and expressivity of positive fragments of FO and LTL

Algorithmic meta-theorem such as Courcelle’s theorem (Édouard Bonnet & Stéphan Thomassé)

• Treewidth, twin-width, clique-width (defined with component twin-width)
• FO and MSO transductions, Ehrenfeucht-Fraïssé games
• Courcelle’s theorem
• FO model checking in bounded-degree graphs, and in bounded twin-width graphs

Graph Neural Networks and logics with counting (François Schwarzentruber)

• Modal logics. Tableau method for solving the satisfiability problem of modal logics. Universal modality. Finite model property via filtration.
• Graph neural network and 1-WL test.
• Graded modal logic and GNNs.
• Quantifier-free fragment Boolean Algebra with Presburger Arithmetic (QBFABA)
• Correspondence between GNNs and logic.

Evaluation modalities

There will be an exam at the end of the course, one homework, and an exercise preparing for literature review.