Consider a property of finite graphs written in predicate logic, even allowing quantifiers over sets of vertices and edges. Courcelle (1990) gives an algorithm to check such a property which is linear in the size of the graph, parameterized by a computable function in the treewidth of the graph and the size of the formula describing the property. (Sometimes this is described as a fixed parameter linear time algorithm.) This talk gives a gentle introduction to the logic and the algorithm.
