Definability equals recognizability of partial 3-trees

Abstract

We show that a graph decision problem can be defined in the Counting Monadic Second-order logic if the partial 3-trees that are yes-instances can be recognized by a finite-state tree automaton. The proof generalizes to also give this result for k-connected partial k-trees. The converse - definability implies recognizability - is known to hold over all partial k-trees. It has been conjectured that recognizability implies definability over partial k-trees; but a proof was previously known only for k ≤ 2. This paper proves the conjecture - and hence the equivalence of definability and recognizability - over partial 3-trees and k-connected partial k-trees.