research-article

Tree-depth, quantifier elimination, and quantifier rank

Authors:

Jörg FlumAuthors Info & Claims

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 225 - 234

https://doi.org/10.1145/3209108.3209160

Published: 09 July 2018 Publication History

Abstract

For a class K of finite 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-AC0. 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. [12] 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-AC0 (instead of FPT). In [13] it was already shown that the model-checking for a fixed MSO-property on a class of graphs of bounded tree-depth is in AC0.

References

[1]

N. Alon, R. Yuster, and U. Zwick. Color-coding. Journal of the ACM, 42(4):844--856, 1995.

Digital Library

[2]

M. Bannach, C. Stockhusen, and T. Tantau. Fast parallel fixed-parameter algorithms via color coding. In Proceedings of IPEC 2015, pages 224--235, 2015.

[3]

M. Bannach and T. Tantau. Parallel multivariate meta-theorems. In IPEC 2016, pages 4:1--4:17, 2017.

[4]

M. Bannach and T. Tantau. Computing hitting set kernels by AC0-circuits. In Proceedings of STACS 2018, pages 9:1--9:14, 2018.

[5]

D. A. Mix Barrington, N. Immerman, and H. Straubing. On uniformity within NC1. Journal of Computer and System Sciences, 41(3):274--306, 1990.

Digital Library

[6]

P. Beame, R. Impagliazzo, and T. Pitassi. Improved depth lower bounds for small distance connectivity. Computational Complexity, 7(4):325--345, 1998.

Digital Library

[7]

C. C. Chang and H. J. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier, 3rd edition, 1990.

[8]

H. Chen and M. Müller. The fine classification of conjunctive queries and parameterized logarithmic space. TOCT, 7(2):7:1--7:27, 2015.

Digital Library

[9]

Y. Chen and J. Flum. Some lower bounds in parameterized AC0. In Proceedings of MFCS 2016, pages 27:1--27:14, 2016.

[10]

Y. Chen, J. Flum, and X. Huang. Slicewise definability in first-order logic with bounded quantifier rank. In Proceedings of CSL 2017, pages 19:1--19:16, 2017.

[11]

B. Courcelle. Graph rewriting: An algebraic and logic approach. In Handbook of Theoretical Computer Science, Volume B:, pages 193--242. 1990.

Digital Library

[12]

M. Elberfeld, M. Grohe, and T. Tantau. Where first-order and monadic second-order logic coincide. ACM Trans. Comput. Log., 17(4):25:1--25:18, 2016.

Digital Library

[13]

M. Elberfeld, A. Jakoby, and T. Tantau. Algorithmic meta theorems for circuit classes of constant and logarithmic depth. In STAGS 2012, pages 66--77, 2012.

[14]

J. Flum and M. Grohe. Fixed-parameter tractability, definability, and model-checking. SIAM Journal on Computing, 31 (1):113--145, 2001.

Digital Library

[15]

J. Gajarský and P. Hlinený. Kernelizing MSO properties of trees of fixed height, and some consequences. Logical Methods in Computer Science, 11(1), 2015.

[16]

P. G. Kolaitis and M. Y. Vardi. Conjunctive-query containment and constraint satisfaction. In Proceedings of the 17th Symposium on Principles of Database Systems, pages 205--213, 1998.

Digital Library

[17]

J. Nesetril and P. Ossona de Mendez. Tree-depth, subgraph coloring and homomorphism bounds. Eur. J. Comb., 27(6):1022--1041, 2006.

Digital Library

[18]

A. Sankaran. A finitary analogue of the downward Löwenheim-Skolem property. In Proceedings of CSL 2017, pages 37:1--37:21, 2017.

Cited By

Bannach MTantau T(2021)On the Descriptive Complexity of Color CodingAlgorithms10.3390/a1403009614:3(96)Online publication date: 19-Mar-2021
https://doi.org/10.3390/a14030096
Grohe MHermanns HZhang LKobayashi NMiller D(2020)Counting Bounded Tree Depth HomomorphismsProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394739(507-520)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394739
Chen YFlum J(2020)Parameterized Parallel Computing and First-Order LogicFields of Logic and Computation III10.1007/978-3-030-48006-6_5(57-78)Online publication date: 23-May-2020
https://doi.org/10.1007/978-3-030-48006-6_5

Recommendations

Tree-width and the monadic quantifier hierarchy
Logic and complexity in computer science

It is well known that on classes of graphs of bounded tree-width, every monadic second-order property is decidable in polynomial time. The converse is not true without further assumptions. It follows from the work of Robertson and Seymour, that if a ...
Second Order Quantifier Elimination: Foundations, Computational Aspects and Applications
A quantifier-free string theory for alogtime reasoning

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 2018

960 pages

ISBN:9781450355834

DOI:10.1145/3209108

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '18

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 9 - 12, 2018

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
134
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)1

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bannach MTantau T(2021)On the Descriptive Complexity of Color CodingAlgorithms10.3390/a1403009614:3(96)Online publication date: 19-Mar-2021
https://doi.org/10.3390/a14030096
Grohe MHermanns HZhang LKobayashi NMiller D(2020)Counting Bounded Tree Depth HomomorphismsProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394739(507-520)Online publication date: 8-Jul-2020
https://dl.acm.org/doi/10.1145/3373718.3394739
Chen YFlum J(2020)Parameterized Parallel Computing and First-Order LogicFields of Logic and Computation III10.1007/978-3-030-48006-6_5(57-78)Online publication date: 23-May-2020
https://doi.org/10.1007/978-3-030-48006-6_5

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents