Recognizability Equals Definability for k-Outerplanar Graphs

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 give two types of self-contained proofs of this conjecture for a number of special cases. First, we show that it holds in a stronger form, that is, we prove that recognizability implies MSOL-definability (the counting operation of CMSOL is not needed) for Halin graphs, 3-connected or bounded degree k-outerplanar graphs and some related graph classes. Second, we show that recognizability implies CMSOL-definability for general k-outerplanar graphs.