Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

TL;DR

This paper introduces a fixed-parameter tractable algorithm for first-order model checking on interpreted graph classes with bounded local cliquewidth, including planar and bounded genus graphs.

Contribution

It develops a new general tool for dependent classes, enabling efficient model checking on broader graph classes with bounded local cliquewidth.

Findings

Algorithm is fixed-parameter tractable for these graph classes

Includes interpretations of planar graphs and bounded genus classes

Introduces a new versatile tool for dependent classes

Abstract

We present a fixed-parameter tractable algorithm for first-order model checking on interpretations of graph classes with bounded local cliquewidth. Notably, this includes interpretations of planar graphs, and more generally, of classes of bounded genus. To obtain this result we develop a new tool which works in a very general setting of dependent classes and which we believe can be an important ingredient in achieving similar results in the future.