Monadic second-order logic and linear-time algorithms for graphs of bounded treewidth
Arvind Gupta, Tom Shermer, Damon Kaller · 1996
The treewidth of a graph is a nonnegative integer that measures how closely the graph resembles a tree. For constant k, the class of graphs with treewidth at most k is also known as the class of partial k-trees. Dynamic-programming techniques can be used to solve many different problems in linear time over partial k-trees. For a decision problem of this sort, the corresponding linear-time algorithm can be modeled by a tree automaton--which is finite-state machine that recognizes the subclass of partial k-trees that are yes-instances of the decision problem. It is known that such a tree automaton exists to recognize any subclass that can be defined by a statement of the Counting Monadic Second-order (or CMS) logic: i.e. CMS-definability implies recognizability. It remains an open question whether, conversely, recognizability implies CMS-definability. This converse implication was previously known to hold only over partial 1-trees and partial 2-trees. In this thesis, we show it also holds over partial 3-trees and k-connected partial k-trees. Hence, a subclass of the partial 3-trees and k-connected partial k-trees can be recognized by a tree automaton if and only if it can be defined by a statement of CMS logic. For many commonly-studied graph decision problems, the class (say $\Pi$) of yes-instances is CMS-definable. Thus, for any constant k, the intersection of $\Pi$ with the class ${\cal G}\sb{k}$ of partial k-trees can be recognized by a tree automaton. We define the complement-problem of $\Pi$ to be the class $\bar\Pi$ that contains the graph-theoretic complement of each graph in $\Pi$. For a CMS-definable class $\Pi$, it is often the case that $\bar\Pi$ is also CMS-definable; in other cases, $\bar\Pi$ is not CMS-definable, but \cap {\cal G}\sb{k}$ is CMS-definable. Either way, $\bar\Pi \cap {\cal G}\sb{k}$ is recognizable by a tree automaton: This not only provides a linear-time decision algorithm for $\bar\Pi$ over the class of partial k-trees, but it also provides a linear-time algorithm for $\Pi$ over the class of partial k-tree complements. We will show, however, that \cap {\cal G}\sb{k}$ is not always CMS-definable when $\Pi$ is CMS-definable. To obtain this result, we develop a pumping lemma--which can be applied to an arbitrary subclass of the partial k-trees to (possibly) show that it cannot be recognized by a tree automaton, and hence, is not CMS-definable.