A Proof of Courcelle’s Conjecture on Recognisable Graph Classes
Courcelle’s conjecture says that for classes of bounded treewidth, definability in MSO is the same as recognisability. More precisely, consider the following notions:
(D) a class of graphs is called MSO definable if it can be defined in monadic second-order logic (with counting quantifiers).
(R) a class of graphs is called recognisable if for each k there is a tree automaton which recognises width k tree decompositions of graphs satisfying the property.
Many natural graph classes are easily seen to satisfy (D), e.g. graphs with Hamiltonian (or Euler) paths, or 3-colourable graphs. Courcelle’s Theorem says that (D) implies (R). Courcelle’s Conjecture says that (R) implies (D) for classes of bounded tree width. In the talk, I will discuss a proof of this conjecture.
Joint work with Michał Pilipczuk.