Differential games, locality, and model checking for FO logic of graphs

We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraisse games in which the game is played on one graph only and the moves of both players are restricted. We prove that these games are strong enough to capture essential information about graphs from graph classes which are interpretable in nowhere dense graph classes. This, together with the fact that the restriction of possible moves of the players makes it easy to decide the winner of the game in some cases, leads to a new framework for the FO model checking problem which can be used on various graph classes interpretable in classes of sparse graphs. Remark: I gave a talk with a similar title in June 2020. Back then it was mostly about the general idea and it was not clear where it would lead. Since then the idea has led to some concrete outcomes which I would like to present. This is joint work with Stephan Kreutzer and Maximilian Gorsky, accepted to CSL 2022.