One of Courcelle's celebrated results states that if C is a class of graphsof bounded tree-width, then model-checking for monadic second order logic(MSO_2) is fixed-parameter tractable (fpt) on C by linear time parameterizedalgorithms, where the parameter is the tree-width plus the size of the formula.An immediate question is whether this is best possible or whether the resultcan be extended to classes of unbounded tree-width. In this paper we show that in terms of tree-width, the theorem cannot beextended much further. More specifically, we show that if C is a class ofgraphs which is closed under colourings and satisfies certain constructibilityconditions and is such that the tree-width of C is not bounded by log^{84} nthen MSO_2-model checking is not fpt unless SAT can be solved insub-exponential time. If the tree-width of C is not poly-logarithmicallybounded, then MSO_2-model checking is not fpt unless all problems in thepolynomial-time hierarchy can be solved in sub-exponential time.
展开▼
