First-Order Model Checking on Monadically Stable Graph Classes

Speaker(s)

Michał Pilipczuk

Affiliation

MIMUW

Date

Feb. 28, 2024, 2:15 p.m.

Room

room 5050

Seminar

Seminar Automata Theory

---

A graph class C is monadically stable if one cannot interpret arbitrary long linear orders in colored graphs from C using any fixed first-order interpretation. We prove that on any monadically stable class, the model-checking for first-order logic is fixed-parameter tractable, that is, can be solved in time f(|phi|) * n^c, which culminates a 7 year work on this conjecture. The final piece of the puzzle involves construction of sparse neighborhood covers using Welzl orders, a tool borrowed from discrete geometry. This is a joint work with Jan Dreier, Ioannis Eleftheriadis, Nikolas Mählmann, Rose McCarty, and Szymon Toruńczyk.

---