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

TL;DR

This paper introduces differential games for first-order logic on graphs, providing a new approach to FO model checking on nowhere dense graph classes by using game-based techniques and differential locality.

Contribution

It develops differential games for FO logic of graphs, linking them to graph classes interpretable in nowhere dense classes and enabling new model checking methods.

Findings

Differential games effectively capture graph properties.

Deciding game outcomes is easier with move restrictions.

New approach improves FO model checking on certain graph classes.

Abstract

We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fra\"{i}ss\'e games in which the game is played on only one graph and the moves of both players restricted. We prove that, in a certain sense, 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 newly introduced notion of differential locality and the fact that the restriction of possible moves by the players makes it easy to decide the winner of the game in some cases, leads to a new approach to the FO model checking problem on interpretations of nowhere dense graph classes.