Recognizability equals definability for partial k-paths

Valentine Kabanets

Abstract

It is well-known that a language is recognizable iff it is definable in a monadic second-order logic (MS). The same holds for sets of finite ranked trees (or finite unranked trees, in which case a counting monadic second-order logic (CMS) is used). Courcelle initiated research into the problem of definability vs. recognizability for finite graphs. Unlike the case of words and trees, recognizability does not equal definability for arbitrary families of graphs. Courcelle and others have shown that definability implies recognizability for partial k-trees (graphs of bounded tree-width), and conjectured that the converse also holds. (The converse implication was proved for k≤3, as well as for families of k-connected partial k-trees.) We show that a recognizable family of partial k-paths (graphs of bounded path-width) is definable in CMS, thereby proving the equality of definability and recognizability for families of partial k-paths. Since a partial k-path is recognizable in linear time, our result also means that a problem on partial k-paths is solvable in linear time using a finite automaton iff this problem is definable in CMS. A by-product of our solution is the formula in MS that defines the class of all partial k-paths (for every k). This implies that the obstruction set of each such class is computable.

Versions