License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2022.22
URN: urn:nbn:de:0030-drops-157426
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15742/
Go to the corresponding LIPIcs Volume Portal

Gajarský, Jakub ; Gorsky, Maximilian ; Kreutzer, Stephan

Differential Games, Locality, and Model Checking for FO Logic of Graphs

pdf-format:
LIPIcs-CSL-2022-22.pdf (0.7 MB)

Abstract

We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraïssé games in which the game is played on only one graph 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 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 which can be used on various graph classes interpretable in classes of sparse graphs.

BibTeX - Entry

@InProceedings{gajarsky_et_al:LIPIcs.CSL.2022.22,
  author =	{Gajarsk\'{y}, Jakub and Gorsky, Maximilian and Kreutzer, Stephan},
  title =	{{Differential Games, Locality, and Model Checking for FO Logic of Graphs}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/15742},
  URN =		{urn:nbn:de:0030-drops-157426},
  doi =		{10.4230/LIPIcs.CSL.2022.22},
  annote =	{Keywords: FO model checking, locality, Gaifman’s theorem, EF games}
}

Keywords: FO model checking, locality, Gaifman’s theorem, EF games
Collection: 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Issue Date: 2022
Date of publication: 27.01.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI