## Authors: Yijia Chen and Jörg Flum

## Paper Information

Title: | Tree depth, quantifier elimination, and quantifier rank |

Authors: | Yijia Chen and Jörg Flum |

Proceedings: | LICS PDF files |

Editors: | Anuj Dawar and Erich Grädel |

Keywords: | tree-depth, quantifier rank, model-checking problems, parameterized AC^0 |

Abstract: | 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. |

Pages: | 10 |

Talk: | Jul 10 11:40 (Session 54D) |

Paper: |