  Possibly the most famous algorithmic meta-theorem is Courcelle's theorem,
which states that all MSO-expressible graph properties are decidable in linear
time for graphs of bounded treewidth. Unfortunately, the running time's
dependence on the MSO formula describing the problem is in general a tower of
exponentials of unbounded height, and there exist lower bounds proving that
this cannot be improved even if we restrict ourselves to deciding FO logic on
trees.
  In this paper we attempt to circumvent these lower bounds by focusing on a
subclass of bounded treewidth graphs, the graphs of bounded vertex cover. By
using a technique different from the standard decomposition and dynamic
programming technique of treewidth we prove that in this case the running time
implied by Courcelle's theorem can be improved dramatically, from
non-elementary to doubly and singly exponential for MSO and FO logic
respectively. Our technique relies on a new graph width measure we introduce,
for which we show some additional results that may indicate that it is of
independent interest. We also prove lower bound results which show that our
upper bounds cannot be improved significantly, under widely believed complexity
assumptions. Our work answers an open problem posed by Michael Fellows.
