FO-Definability of Shrub-Depth

Authors Yijia Chen , Jörg Flum

Thumbnail PDF


  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Yijia Chen
  • Fudan University, Shanghai, China
Jörg Flum
  • Albert-Ludwigs-Universität Freiburg, Germany


We thank Abhisekh Sankaran for discussions concerning problems of the last section. Anonymous reviewers' comments also help to improve the presentation.

Cite AsGet BibTex

Yijia Chen and Jörg Flum. FO-Definability of Shrub-Depth. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Graph algorithms analysis
  • Mathematics of computing → Graph theory
  • shrub-depth
  • model-checking
  • monadic second-order logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. D. A. Mix Barrington, N. Immerman, and H. Straubing. On Uniformity within NC¹. Journal of Computer and System Sciences, 41(3):274-306, 1990. Google Scholar
  2. C. C. Chang and H. J. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier, 3rd edition, 1992. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic, 22(3), 1957. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. Y. Gurevich. Toward logic tailored for computational complexity. In Computation and Proof Theory, Lecture Notes in Mathematics, pages 1104:175-216, 1984. Google Scholar
  18. W. Hodges. Model theory, volume 42 of Encyclopedia of mathematics and its applications. Cambridge University Press, 1993. Google Scholar
  19. M. Lampis. Algorithmic Meta-theorems for Restrictions of Treewidth. Algorithmica, 64(1):19-37, 2012. Google Scholar
  20. 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. Google Scholar
  21. B. Rossman. Homomorphism preservation theorems. Journal of the ACM, 55(3):15:1-15:53, 2008. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail