Working Seminar on Formal Models, Discrete Structures, and Algorithms

First-order model checking and interpretations

Jakub Gajarský (TU Berlin)

When: Tuesday February 28, 9am

Where: room C417 (at the very end of the corridor)


he model checking problem for first-order logic asks, given a graph G and a formula as input, whether the formula holds true in G. This problem been investigated extensively on sparse graphs and this line of research culminated in a result of Grohe, Kreutzer and Siebertz, who proved the existence of fixed-parameter algorithm for first-order model checking on nowhere dense graph classes. A natural next step in the research of first-order model checking is to attempt to extend this result to classes of (dense) graphs which can be obtained from sparse graphs by first-order interpretations. In order to succeed with this, one has to typically proceed in two steps: 1) Characterise graph classes interpretable in sparse graph classes and 2) use the characterisation to compute ‘inverses’ of interpretations. In the talk we will give an overview of the current state of the art of this problem and sketch some future directions of research