Document Open Access Logo

First Order Logic on Pathwidth Revisited Again

Author Michael Lampis

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.132.pdf
  • Filesize: 0.75 MB
  • 17 pages

Document Identifiers

Author Details

Michael Lampis
  • Université Paris-Dauphine, PSL University, CNRS, LAMSADE, 75016, Paris, France

Funding

Supported by ANR projects ANR-21-CE48-0022 (S-EX-AP-PE-AL) and ANR-18-CE40-0025 (ASSK).

Cite AsGet BibTex

Michael Lampis. First Order Logic on Pathwidth Revisited Again. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 132:1-132:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ICALP.2023.132

Abstract

Courcelle’s celebrated theorem states that all MSO-expressible properties can be decided in linear time on graphs of bounded treewidth. Unfortunately, the hidden constant implied by this theorem is a tower of exponentials whose height increases with each quantifier alternation in the formula. More devastatingly, this cannot be improved, under standard assumptions, even if we consider the much more restricted problem of deciding FO-expressible properties on trees. In this paper we revisit this well-studied topic and identify a natural special case where the dependence of Courcelle’s theorem can, in fact, be improved. Specifically, we show that all FO-expressible properties can be decided with an elementary dependence on the input formula, if the input graph has bounded pathwidth (rather than treewidth). This is a rare example of treewidth and pathwidth having different complexity behaviors. Our result is also in sharp contrast with MSO logic on graphs of bounded pathwidth, where it is known that the dependence has to be non-elementary, under standard assumptions. Our work builds upon, and generalizes, a corresponding meta-theorem by Gajarský and Hliněný for the more restricted class of graphs of bounded tree-depth.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parameterized complexity and exact algorithms
Keywords
  • Algorithmic Meta-Theorems
  • FO logic
  • Pathwidth

Metrics

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

Related Versions

References

  1. Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. J. Algorithms, 12(2):308-340, 1991. URL: https://doi.org/10.1016/0196-6774(91)90006-K.
  2. Rémy Belmonte, Eun Jung Kim, Michael Lampis, Valia Mitsou, and Yota Otachi. Grundy distinguishes treewidth from pathwidth. In ESA, volume 173 of LIPIcs, pages 14:1-14:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  3. Hans L. Bodlaender, Fedor V. Fomin, Daniel Lokshtanov, Eelko Penninkx, Saket Saurabh, and Dimitrios M. Thilikos. (meta) kernelization. J. ACM, 63(5):44:1-44:69, 2016. Google Scholar
  4. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant. Twin-width I: tractable FO model checking. In FOCS, pages 601-612. IEEE, 2020. Google Scholar
  5. Bruno Courcelle. The monadic second-order logic of graphs. I. recognizable sets of finite graphs. Inf. Comput., 85(1):12-75, 1990. Google Scholar
  6. Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst., 33(2):125-150, 2000. Google Scholar
  7. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. Google Scholar
  8. Anuj Dawar, Martin Grohe, Stephan Kreutzer, and Nicole Schweikardt. Approximation schemes for first-order definable optimisation problems. In LICS, pages 411-420. IEEE Computer Society, 2006. Google Scholar
  9. Zdenek Dvořák, Daniel Král, and Robin Thomas. Testing first-order properties for subclasses of sparse graphs. J. ACM, 60(5):36:1-36:24, 2013. Google Scholar
  10. Eduard Eiben, Robert Ganian, and Stefan Szeider. Meta-kernelization using well-structured modulators. Discret. Appl. Math., 248:153-167, 2018. Google Scholar
  11. Markus Frick. Generalized model-checking over locally tree-decomposable classes. Theory Comput. Syst., 37(1):157-191, 2004. Google Scholar
  12. Markus Frick and Martin Grohe. Deciding first-order properties of locally tree-decomposable structures. J. ACM, 48(6):1184-1206, 2001. Google Scholar
  13. Markus Frick and Martin Grohe. The complexity of first-order and monadic second-order logic revisited. Ann. Pure Appl. Log., 130(1-3):3-31, 2004. Google Scholar
  14. Jakub Gajarský and Petr Hliněný. Kernelizing MSO properties of trees of fixed height, and some consequences. Log. Methods Comput. Sci., 11(1), 2015. Google Scholar
  15. Jakub Gajarský, Petr Hlinený, Daniel Lokshtanov, Jan Obdrzálek, Sebastian Ordyniak, M. S. Ramanujan, and Saket Saurabh. FO model checking on posets of bounded width. In FOCS, pages 963-974. IEEE Computer Society, 2015. Google Scholar
  16. Robert Ganian. Improving vertex cover as a graph parameter. Discret. Math. Theor. Comput. Sci., 17(2):77-100, 2015. Google Scholar
  17. Robert Ganian, Petr Hliněný, Jaroslav Nešetřil, Jan Obdržálek, and Patrice Ossona de Mendez. Shrub-depth: Capturing height of dense graphs. Log. Methods Comput. Sci., 15(1), 2019. Google Scholar
  18. Robert Ganian and Jan Obdržálek. Expanding the expressive power of monadic second-order logic on restricted graph classes. In IWOCA, volume 8288 of Lecture Notes in Computer Science, pages 164-177. Springer, 2013. Google Scholar
  19. Robert Ganian, Friedrich Slivovsky, and Stefan Szeider. Meta-kernelization with structural parameters. J. Comput. Syst. Sci., 82(2):333-346, 2016. Google Scholar
  20. Martin Grohe and Stephan Kreutzer. Methods for algorithmic meta theorems. Model Theoretic Methods in Finite Combinatorics, 558:181-206, 2011. Google Scholar
  21. Dusan Knop, Martin Koutecký, Tomás Masarík, and Tomás Toufar. Simplified algorithmic metatheorems beyond MSO: treewidth and neighborhood diversity. Log. Methods Comput. Sci., 15(4), 2019. Google Scholar
  22. Dusan Knop, Tomás Masarík, and Tomás Toufar. Parameterized complexity of fair vertex evaluation problems. In MFCS, volume 138 of LIPIcs, pages 33:1-33:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  23. Michael Lampis. Algorithmic meta-theorems for restrictions of treewidth. Algorithmica, 64(1):19-37, 2012. URL: https://doi.org/10.1007/s00453-011-9554-x.
  24. Michael Lampis. Model checking lower bounds for simple graphs. Log. Methods Comput. Sci., 10(1), 2014. Google Scholar
  25. Michael Lampis and Valia Mitsou. Fine-grained meta-theorems for vertex integrity. In ISAAC, volume 212 of LIPIcs, pages 34:1-34:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  26. Michal Pilipczuk. Problems parameterized by treewidth tractable in single exponential time: A logical approach. In MFCS, volume 6907 of Lecture Notes in Computer Science, pages 520-531. Springer, 2011. Google Scholar
  27. Detlef Seese. Linear time computable problems and first-order descriptions. Math. Struct. Comput. Sci., 6(6):505-526, 1996. Google Scholar
  28. Stefan Szeider. Monadic second order logic on graphs with local cardinality constraints. ACM Trans. Comput. Log., 12(2):12:1-12:21, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact