A New Perspective on FO Model Checking of Dense Graph Classes

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

GAJARSKÝ Jakub HLINĚNÝ Petr LOKSHTANOV Daniel OBDRŽÁLEK Jan RAMANUJAN M S

Year of publication 2020
Type Article in Periodical
Magazine / Source ACM Transactions on Computational Logic
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1145/3383206
Doi http://dx.doi.org/10.1145/3383206
Keywords FO Logic; Model-Checking; Logic Interpretations; Sparse Graph Classes; Parameterized Complexity
Description We study the FO model checking problem of dense graph classes, namely those which are FO-interpretable in some sparse graph classes. Note that if an input dense graph is given together with the corresponding FO interpretation in a sparse graph, one can easily solve the model checking problem using the existing algorithms for sparse graph classes. However, if the assumed interpretation is not given, then the situation is markedly harder. In this paper we give a structural characterization of graph classes which are FO interpretable in graph classes of bounded degree. This characterization allows us to efficiently compute such an interpretation for an input graph. As a consequence, we obtain an FPT algorithm for FO model checking of graph classes FO interpretable in graph classes of bounded degree. The approach we use to obtain these results may also be of independent interest.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.