FO-Definability of Shrub-Depth
Shrub-depth is a graph invariant often considered as an extension of tree-depth to dense graphs. We show that the model-checking problem of monadic second-order logic on a class of graphs of bounded shrub-depth can be decided by AC^0-circuits after a precomputation on the formula. This generalizes a similar result on graphs of bounded tree-depth [Y. Chen and J. Flum, 2018]. At the core of our proof is the definability in first-order logic of tree-models for graphs of bounded shrub-depth.
shrub-depth
model-checking
monadic second-order logic
Theory of computation~Graph algorithms analysis
Mathematics of computing~Graph theory
15:1-15:16
Regular Paper
The collaboration of the authors is funded by the Sino-German Center for Research Promotion (GZ 1518). Yijia Chen is also supported by National Natural Science Foundation of China (Project 61872092).
We thank Abhisekh Sankaran for discussions concerning problems of the last section. Anonymous reviewers' comments also help to improve the presentation.
Yijia
Chen
Yijia Chen
Fudan University, Shanghai, China
https://orcid.org/0000-0001-7033-9593
Jörg
Flum
Jörg Flum
Albert-Ludwigs-Universität Freiburg, Germany
10.4230/LIPIcs.CSL.2020.15
D. A. Mix Barrington, N. Immerman, and H. Straubing. On Uniformity within NC¹. Journal of Computer and System Sciences, 41(3):274-306, 1990.
C. C. Chang and H. J. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier, 3rd edition, 1992.
Y. Chen and J. Flum. Tree-depth, quantifier elimination, and quantifier rank. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 225-234, 2018.
B. Courcelle. Graph Rewriting: An Algebraic and Logic Approach. In Handbook of Theoretical Computer Science, Volume B:, pages 193-242. Elsevier and MIT Press, 1990.
B. Courcelle, J. Makowsky, and U. Rotics. Linear Time Solvable Optimization Problems on Graphs of Bounded Clique-Width. Theory of Computing Systems, 33(2):125-150, 2000.
W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic, 22(3), 1957.
K. Eickmeyer, J. van den Heuvel, K. Kawarabayashi, S. Kreutzer, P. Ossona de Mendez, M. Pilipczuk, D. Quiroz, R. Rabinovich, and S. Siebertz. Model-Checking on Ordered Structures. CoRR, abs/1812.08003, 2018.
M. Elberfeld, M. Grohe, and T. Tantau. Where First-Order and Monadic Second-Order Logic Coincide. ACM Transactions on Computational Logic, 17(4):25:1-25:18, 2016.
M. Frick and M. Grohe. The complexity of first-order and monadic second-order logic revisited. Annals of Pure and Applied Logic, 130(1-3):3-31, 2004.
J. Gajarský and P. Hlinĕný. Faster Deciding MSO Properties of Trees of Fixed Height, and Some Consequences. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India, pages 112-123, 2012.
J. Gajarský and P. Hlinĕný. Kernelizing MSO Properties of Trees of Fixed Height, and Some Consequences. Logical Methods in Computer Science, 11(1), 2015.
J. Gajarský, P. Hlinĕný, D. Lokshtanov, J. Obdrzálek, S. Ordyniak, M. S. Ramanujan, and S. Saurabh. FO model checking on posets of bounded width. In IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 963-974, 2015.
J. Gajarský, P. Hlinĕný, J. Obdrzálek, D. Lokshtanov, and M. S. Ramanujan. A New Perspective on FO Model Checking of Dense Graph Classes. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16, New York, NY, USA, July 5-8, 2016, pages 176-184, 2016.
R. Ganian, P. Hlinĕný, D. Král, J. Obdrzálek, J. Schwartz, and J. Teska. FO model checking of interval graphs. Logical Methods in Computer Science, 11(4), 2015.
R. Ganian, P. Hlinĕný, J. Nesetril, J. Obdrzálek, P. Ossona de Mendez, and R. Ramadurai. When Trees Grow Low: Shrubs and Fast MSO₁. In Mathematical Foundations of Computer Science 2012 - 37th International Symposium, MFCS 2012, Bratislava, Slovakia, August 27-31, 2012. Proceedings, pages 419-430, 2012.
M. Grohe, S. Kreutzer, R. Rabinovich, S. Siebertz, and K. Stavropoulos. Coloring and Covering Nowhere Dense Graphs. SIAM Journal on Discrete Mathematics, 32(4):2467-2481, 2018.
Y. Gurevich. Toward logic tailored for computational complexity. In Computation and Proof Theory, Lecture Notes in Mathematics, pages 1104:175-216, 1984.
W. Hodges. Model theory, volume 42 of Encyclopedia of mathematics and its applications. Cambridge University Press, 1993.
M. Lampis. Algorithmic Meta-theorems for Restrictions of Treewidth. Algorithmica, 64(1):19-37, 2012.
M. Pilipczuk, S. Siebertz, and S. Toruńczyk. Parameterized circuit complexity of model-checking on sparse structures. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 789-798, 2018.
B. Rossman. Homomorphism preservation theorems. Journal of the ACM, 55(3):15:1-15:53, 2008.
Yijia Chen and Jörg Flum
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode