Logspace Versions of the Theorems of Bodlaender and Courcelle

Bodlaender’s Theorem states that for every k there is a linear-time algorithm that decides whether an input graph has tree width k and, if so, computes a width-k tree composition. Cour-celle’s Theorem builds on Bodlaender’s Theorem and states that for every monadic second-order formula φ and for every k there is a linear-time algorithm that decides whether a given logical structure A of tree width at most k satisfies φ. We prove that both theorems still hold when “linear time ” is replaced by “logarithmic space.” The transfer of the powerful theoretical framework of monadic second-order logic and bounded tree width to logarithmic space allows us to settle a number of both old and recent open problems in the logspace world