Abstract
We study the expressive power and succinctness of order-invariant sentences of first-order (FO) and monadic second-order (MSO) logic on graphs of bounded tree-depth. Order-invariance is undecidable in general and, therefore, in finite model theory, one strives for logics with a decidable syntax that have the same expressive power as order-invariant sentences. We show that on graphs of bounded tree-depth, order-invariant FO has the same expressive power as FO, and order-invariant MSO has the same expressive power as the extension of FO with modulo-counting quantifiers. Our proof techniques allow for a fine-grained analysis of the succinctness of these translations. We show that for every order-invariant FO sentence there exists an FO sentence whose size is elementary in the size of the original sentence, and whose number of quantifier alternations is linear in the tree-depth. Our techniques can be adapted to obtain a similar quantitative variant of a known result that the expressive power of MSO and FO coincides on graphs of bounded tree-depth.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Benedikt, M.A., Segoufin, L.: Towards a characterization of order-invariant queries over tame graphs. Journal of Symbolic Logic 74(1), 168–186 (2009)
Bouland, A., Dawar, A., Kopczyński, E.: On tractable parameterizations of graph isomorphism. In: Thilikos, D.M., Woeginger, G.J. (eds.) IPEC 2012. LNCS, vol. 7535, pp. 218–230. Springer, Heidelberg (2012)
Chandra, A., Harel, D.: Structure and complexity of relational queries. JCSS 25(1), 99–128 (1982)
Courcelle, B.: The monadic second-order logic of graphs x: linear orderings. Theoretical Computer Science 160(1-2), 87–143 (1996)
Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic – A Language-Theoretic Approach. Cambridge University Press (2012)
Elberfeld, M., Grohe, M., Tantau, T.: Where first-order and monadic second-order logic coincide. In: Proc. LICS 2012, pp. 265–274. IEEE Computer Society (2012)
Gajarský, J., Hliněný, P.: Faster deciding MSO properties of trees of fixed height, and some consequences. In: Proc. FSTTCS 2012, pp. 112–123 (2012)
Grohe, M., Schweikardt, N.: The succinctness of first-order logic on linear orders. Logical Methods in Computer Science 1(1:6), 1–25 (2005)
Libkin, L.: Elements of Finite Model Theory. Springer (2004)
Nešetřil, J., Ossona de Mendez, P.: Sparsity: Graphs, Structures, and Algorithms. Springer, Heidelberg (2012)
Schweikardt, N.: A short tutorial on order-invariant first-order logic. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 112–126. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag GmbH Berlin Heidelberg
About this paper
Cite this paper
Eickmeyer, K., Elberfeld, M., Harwath, F. (2014). Expressivity and Succinctness of Order-Invariant Logics on Depth-Bounded Structures. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds) Mathematical Foundations of Computer Science 2014. MFCS 2014. Lecture Notes in Computer Science, vol 8634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44522-8_22
Download citation
DOI: https://doi.org/10.1007/978-3-662-44522-8_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44521-1
Online ISBN: 978-3-662-44522-8
eBook Packages: Computer ScienceComputer Science (R0)