MSOL-Definability Equals Recognizability for Halin Graphs and Bounded Degree $k$-Outerplanar Graphs

TL;DR

This paper proves that for certain graph classes, recognizability and MSOL-definability are equivalent, extending Courcelle's Theorem to new classes like Halin graphs and bounded degree $k$-outerplanar graphs.

Contribution

It establishes that recognizable properties are MSOL-definable for specific graph classes, confirming a stronger form of Courcelle's conjecture.

Findings

Recognizability equals MSOL-definability for Halin graphs.

Recognizability equals MSOL-definability for bounded degree $k$-outerplanar graphs.

The result applies to graph classes with MSOL-definable tree decompositions.

Abstract

One of the most famous algorithmic meta-theorems states that every graph property that can be defined by a sentence in counting monadic second order logic (CMSOL) can be checked in linear time for graphs of bounded treewidth, which is known as Courcelle's Theorem. These algorithms are constructed as finite state tree automata, and hence every CMSOL-definable graph property is recognizable. Courcelle also conjectured that the converse holds, i.e. every recognizable graph property is definable in CMSOL for graphs of bounded treewidth. We prove this conjecture for a number of special cases in a stronger form. That is, we show that each recognizable property is definable in MSOL, i.e. the counting operation is not needed in our expressions. We give proofs for Halin graphs, bounded degree $k$-outerplanar graphs and some related graph classes. We furthermore show that the conjecture holds for any graph class that admits tree decompositions that can be defined in MSOL, thus providing a useful tool for future proofs.