Document Open Access Logo

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

Authors Jakub Gajarský, Maximilian Gorsky, Stephan Kreutzer

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.22.pdf
  • Filesize: 0.71 MB
  • 18 pages

Document Identifiers

Author Details

Jakub Gajarský
  • University of Warsaw, Poland
Maximilian Gorsky
  • TU Berlin, Germany
Stephan Kreutzer
  • TU Berlin, Germany

Funding

  • Gajarský, Jakub: The research reported in this paper is supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (ERC consolidator grant LIPA, agreement No. 683080).
  • Gorsky, Maximilian: The research reported in this paper has been supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (ERC consolidator grant DISTRUCT, agreement No. 648527).
  • Kreutzer, Stephan: The research reported in this paper has been supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (ERC consolidator grant DISTRUCT, agreement No. 648527).

Cite AsGet BibTex

Jakub Gajarský, Maximilian Gorsky, and Stephan Kreutzer. Differential Games, Locality, and Model Checking for FO Logic of Graphs. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.22

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Theory of computation → Fixed parameter tractability
Keywords
  • FO model checking
  • locality
  • Gaifman’s theorem
  • EF games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. É. Bonnet, E. J. Kim, S. Thomassé, and R. Watrigant. Twin-width i: tractable fo model checking. In FOCS'20, pages 601-612. IEEE Computer Society, 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00062.
  2. B. Courcelle, J. A. Makowsky, and U. Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst., 33(2):125-150, 2000. URL: https://doi.org/10.1007/s002249910009.
  3. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21275-3.
  4. A. Dawar. Finite model theory on tame classes of structures. In International Symposium on Mathematical Foundations of Computer Science, pages 2-12. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74456-6_2.
  5. A. Dawar. Homomorphism preservation on quasi-wide classes. Journal of Computer and System Sciences, 76(5):324-332, 2010. URL: https://doi.org/10.1016/j.jcss.2009.10.005.
  6. A. Dawar, M. Grohe, and S. Kreutzer. Locally excluding a minor. In LICS'07, pages 270-279. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.31.
  7. Z. Dvorák, D. Kráľ, and R. Thomas. Testing first-order properties for subclasses of sparse graphs. J. ACM, 60(5):36:1-36:24, 2013. URL: https://doi.org/10.1145/2499483.
  8. H. Ebbinghaus and J. Flum. Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  9. A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fund. Math, 49(129-141):13, 1961. Google Scholar
  10. K. Eickmeyer and K. Kawarabayashi. FO model checking on map graphs. In FCT 2017, volume 10472 of Lecture Notes in Computer Science, pages 204-216. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-55751-8_17.
  11. R. Fraïssé. Sur une nouvelle classification des systemes de relations. Comptes Rendus Hebdomadaires Des Seances De L' Academie Des Sciences, 230(11):1022-1024, 1950. Google Scholar
  12. R. Fraïssé. Sur quelques classifications des systemes de relations. PhD thesis, Université de Paris, 1955. Google Scholar
  13. M. Frick and M. Grohe. Deciding first-order properties of locally tree-decomposable structures. J. ACM, 48(6):1184-1206, 2001. URL: https://doi.org/10.1145/504794.504798.
  14. H. Gaifman. On local and non-local properties. In Proceedings of the Herbrand Symposium, volume 107 of Stud. Logic Found. Math., pages 105-135. Elsevier, 1982. Google Scholar
  15. J. Gajarský, P. Hliněný, D. Lokshtanov, J. Obdržálek, S. Ordyniak, M. S. Ramanujan, and S. Saurabh. FO model checking on posets of bounded width. In FOCS'15, pages 963-974. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/FOCS.2015.63.
  16. J. Gajarský, P. Hliněný, J. Obdržálek, D. Lokshtanov, and M. S. Ramanujan. A new perspective on FO model checking of dense graph classes. In LICS '16, pages 176-184. ACM, 2016. URL: https://doi.org/10.1145/2933575.2935314.
  17. J. Gajarský, S. Kreutzer, J. Nešetřil, P. Ossona de Mendez, M. Pilipczuk, S. Siebertz, and S. Torunczyk. First-order interpretations of bounded expansion classes. In ICALP 2018, volume 107 of LIPIcs, pages 126:1-126:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.126.
  18. R. Ganian, P. Hliněný, D. Kráľ, J. Obdržálek, J. Schwartz, and J. Teska. FO model checking of interval graphs. Log. Methods Comput. Sci., 11(4:11):1-20, 2015. Google Scholar
  19. M. Grohe, S. Kreutzer, and S. Siebertz. Deciding first-order properties of nowhere dense graphs. J. ACM, 64(3):17:1-17:32, 2017. URL: https://doi.org/10.1145/3051095.
  20. P. Hliněný and S. Oum. Finding branch-decompositions and rank-decompositions. SIAM J. Comput., 38(3):1012-1032, 2008. URL: https://doi.org/10.1137/070685920.
  21. P. Hliněný, F. Pokrývka, and B. Roy. FO model checking on geometric graphs. Comput. Geom., 78:1-19, 2019. URL: https://doi.org/10.1016/j.comgeo.2018.10.001.
  22. J. Nešetřil and P. Ossona de Mendez. First order properties on nowhere dense structures. J. Symb. Log., 75(3):868-887, 2010. URL: https://doi.org/10.2178/jsl/1278682204.
  23. J. Nešetřil and P. Ossona de Mendez. On nowhere dense graphs. Eur. J. Comb., 32(4):600-617, 2011. URL: https://doi.org/10.1016/j.ejc.2011.01.006.
  24. S. Oum and P. D. Seymour. Approximating clique-width and branch-width. J. Comb. Theory, Ser. B, 96(4):514-528, 2006. URL: https://doi.org/10.1016/j.jctb.2005.10.006.
  25. D. Seese. Linear time computable problems and first-order descriptions. Math. Structures Comput. Sci., 6(6):505-526, 1996. Google Scholar
  26. L. J. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, Massachusetts Institute of Technology, 1974. Google Scholar
  27. M. Y. Vardi. The complexity of relational query languages. In Proceedings of the fourteenth annual ACM symposium on Theory of computing, pages 137-146, 1982. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact