Kernelizing MSO Properties of Trees of Fixed Height, and Some Consequences

TL;DR

This paper proves kernelization results for MSO properties on bounded-height trees, leading to efficient model checking algorithms and showing FO and MSO expressive powers coincide on certain graph classes.

Contribution

It establishes kernel bounds for MSO decision problems on trees of fixed height and derives implications for model checking and logical expressiveness.

Findings

Existence of kernels bounded by elementary functions for MSO problems

Elementary time model checking algorithm for classes with shrub-depth h

Equivalence of FO and MSO expressive powers on certain graph classes

Abstract

Fix an integer h>=1. In the universe of coloured trees of height at most h, we prove that for any graph decision problem defined by an MSO formula with r quantifiers, there exists a set of kernels, each of size bounded by an elementary function of r and the number of colours. This yields two noteworthy consequences. Consider any graph class G having a one-dimensional MSO interpretation in the universe of coloured trees of height h (equivalently, G is a class of shrub-depth h). First, class G admits an MSO model checking algorithm whose runtime has an elementary dependence on the formula size. Second, on G the expressive powers of FO and MSO coincide (which extends a 2012 result of Elberfeld, Grohe, and Tantau).