ABSTRACT. For a class K of graphs we consider the following three statements. (i) K has bounded tree-depth. (ii) First-order logic FO has an effective generalized quantifier elimination on K. (iii) The parameterized model checking for FO on K is in para-FO (or equivalently, in para-AC^0). We prove that (i) => (ii) and (ii) <=> (iii). All three statements are equivalent if K is closed under taking subgraphs, but not in general.

By a result due to Elberfeld et al. monadic second-order logic MSO and FO have the same expressive power on every class of graphs of bounded tree-depth. Hence the implication (i) => (iii) holds for MSO, too; it is the analogue of Courcelle's Theorem for tree-depth (instead of tree-width) and para-AC^0 (instead of FPT). In Elberfeld et al. it was already shown that the model-checking for a fixed MSO-property on a class of graphs of bounded tree-depth is in AC^0.