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 \leq 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