Variants of Courcelle's Theorem for complexity classes inside P.

It is well known that monadic-second order logic (MSO) expresses many natural NP-complete problems. However, a famous theorem of Courcelle states that every problem expressible in MSO can be solved in linear time for input graphs whose tree width is bounded by a fixed constant [Courcelle 1990]. Courcelle's Theorem is the prototypical example of an algorithmic "meta theorem", which states an algorithmic upper bound for a whole family of problems. This column reviews a series of meta theorems several of which refine Courcelle's Theorem by more precisely classifying the complexity of natural families of problems.