Lune

LICS2024Top-tier venue

Elementary first-order model checking for sparse graphs

Jakub Gajarský, Michal Pilipczuk, Marek Sokolowski, Giannos Stamoulis, Szymon Torunczyk

2024Year
2Citations
2Top-tier citations

Abstract

It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula size is non-elementary, and in fact, this is unavoidable even for the class of all trees [Frick and Grohe, LICS 2002]. On the other hand, it is known that the dependency is elementary for classes of bounded degree [Frick and Grohe, LICS 2002] as well as for classes of bounded pathwidth [Lampis, ICALP 2023]. In this paper we generalise these results and almost completely characterise subgraph-closed graph classes for which the model checking problem is fixed-parameter tractable with an elementary dependency on the formula size. Those are the graph classes for which there exists a number d such that for every r, some tree of depth d and size bounded by an elementary function of r is avoided as an (≤r)-subdivision in all graphs in the class. In particular, this implies that if the class in question excludes a fixed tree as a topological minor, then first-order model checking for graphs in the class is fixed-parameter tractable with an elementary dependency on the formula size.

Ask about this paper

Your agent reads all of it.

Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.

Questions to start from

Your agent calls

Luneget_paper_fulltext

Ask in Lune

Free to start. No credit card required.

lune papers fulltext 3bc61cf3-7a37-4ca5-8dbc-1226982a95be

Cited by top-tier papers2

Ask how each one uses it

Builds on6

Related papers

Dusk over the sea between two cliffs drawn in fine vertical lines