Document Open Access Logo

Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs

Authors Kord Eickmeyer, Ken-ichi Kawarabayashi

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.18.pdf
  • Filesize: 0.48 MB
  • 15 pages

Document Identifiers

Author Details

Kord Eickmeyer
Ken-ichi Kawarabayashi

Cite As Get BibTex

Kord Eickmeyer and Ken-ichi Kawarabayashi. Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.18

Abstract

We show that the model-checking problem for successor-invariant first-order logic is fixed-parameter tractable on graphs with excluded topological subgraphs when parameterised by both the size of the input formula and the size of the exluded topological subgraph. Furthermore, we show that model-checking for order-invariant first-order logic is tractable on coloured posets of bounded width, parameterised by both the size of the input formula and the width of the poset.

Results of this form, i.e. showing that model-checking for a certain logic is tractable on a certain class of structures, are often referred to as algorithmic meta-theorems since they give a unified proof for the tractability of a whole range of problems. First-order logic is arguably one of the most important logics in this context since it is powerful enough to express many computational problems (e.g. the existence of cliques, dominating sets etc.) and yet its model-checking problem is tractable on rich classes of graphs. In fact, Grohe et al have shown that model-checking for FO is tractable on all nowhere dense classes of graphs.

Successor-invariant FO is a semantic extension of FO by allowing the use of an additional binary relation which is interpreted as a directed Hamiltonian cycle, restricted to formulae whose truth value does not depend on the specific choice of a Hamiltonian cycle. While this is very natural in the context of model-checking (after all, storing a structure in computer memory usually brings with it a linear order on the structure), the question of how the computational complexity of the model-checking problem for this richer logic compares to that of plain FO is still open.

Our result for successor-invariant FO extends previous results for this logic on planar graphs and graphs with excluded minors, further narrowing the gap between what is known for FO and what is known for successor-invariant FO. The proof uses Grohe and Marx's structure theorem for graphs with excluded topological subgraphs. For order-invariant FO we show that Gajarský et al.'s recent result for FO carries over to order-invariant FO.

Subject Classification

Keywords
  • model-checking
  • algorithmic meta-theorem
  • successor-invariant
  • first-order logic
  • topological subgraphs
  • parameterised complexity

Metrics

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

References

  1. Matthew Anderson, Dieter van Melkebeek, Nicole Schweikardt, and Luc Segoufin. Locality from circuit lower bounds. SIAM J. Comput., 41(6):1481-1523, 2012. Google Scholar
  2. Michael Benedikt and Luc Segoufin. Towards a characterization of order-invariant queries over tame graphs. J. Symb. Log., 74(1):168-186, 2009. Google Scholar
  3. Simone Bova, Robert Ganian, and Stefan Szeider. Model checking existential logic on partially ordered sets. ACM Transactions on Computational Logic (TOCL), 17(2):10, 2015. Google Scholar
  4. Bruno Courcelle. Graph rewriting: An algebraic and logic approach. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume 2, pages 194-242. Elsevier, 1990. Google Scholar
  5. Bruno Courcelle, Johann Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems, 33(2):125-150, 2000. Google Scholar
  6. Anuj Dawar, Martin Grohe, and Stephan Kreutzer. Locally excluding a minor. In Logic in Computer Science (LICS), pages 270-279, 2007. Google Scholar
  7. Reinhard Diestel. Graph Theory. Number 173 in GTM. Springer, 4th edition, 2012. Google Scholar
  8. Rod Downey and Michael R. Fellows. Parameterized Complexity. Springer, 1998. Google Scholar
  9. Zdeněk Dvořák, Daniel Král, and Robin Thomas. Testing first-order properties for subclasses of sparse graphs. Journal of the ACM (JACM), 60(5):36, 2013. Google Scholar
  10. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Perspectives in Mathematical Logic. Springer, 2nd edition, 1999. Google Scholar
  11. Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. Mathematical Logic. Springer, 2nd edition, 1994. Google Scholar
  12. Kord Eickmeyer, Michael Elberfeld, and Frederik Harwath. Expressivity and succinctness of order-invariant logics on depth-bounded structures. In Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, pages 256-266, 2014. Google Scholar
  13. Kord Eickmeyer, Ken-Ichi Kawarabayashi, and Stephan Kreutzer. Model checking for successor-invariant first-order logic on minor-closed graph classes. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '13, pages 134-142. IEEE Computer Society, 2013. Google Scholar
  14. Viktor Engelmann, Stephan Kreutzer, and Sebastian Siebertz. First-order and monadic second-order model-checking on ordered structures. In Logics in Computer Science, pages 275-284, 2012. Google Scholar
  15. Stefan Felsner, Vijay Raghavan, and Jeremy Spinrad. Recognition algorithms for orders of small width and graphs of small dilworth number. Order, 20(4):351-364, 2003. Google Scholar
  16. Jörg Flum and Martin Grohe. Fixed-parameter tractability, definability, and model-checking. SIAM J. Comput., 31(1):113-145, 2001. Google Scholar
  17. Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Springer, 2006. ISBN 3-54-029952-1. Google Scholar
  18. Markus Frick and Martin Grohe. Deciding first-order properties of locally tree-decomposable structures. Journal of the ACM, 48:1148-1206, 2001. Google Scholar
  19. Jakub Gajarský, Petr Hliněný, Daniel Lokshtanov, Jan Obdržálek, Sebastian Ordyniak, MS Ramanujan, and Saket Saurabh. Fo model checking on posets of bounded width. In Foundations of Computer Science (FOCS), 2015 IEEE 56th Annual Symposium on, pages 963-974. IEEE, 2015. Google Scholar
  20. Martin Grohe. Logic, graphs, and algorithms. In E. Grädel, T. Wilke, and J. Flum, editors, Logic and Automata - History and Perspectives. Amsterdam University Press, 2007. Google Scholar
  21. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. In Proceedings of the 46th Annual ACM Symposium on Theory of Computing, STOC '14, pages 89-98. ACM, 2014. Google Scholar
  22. Martin Grohe and Dániel Marx. Structure theorem and isomorphism test for graphs with excluded topological subgraphs. SIAM Journal on Computing, 44(1):114-159, 2015. Google Scholar
  23. Martin Grohe and Thomas Schwentick. Locality of order-invariant first-order formulas. ACM Trans. Comput. Logic, 1(1):112-130, July 2000. Google Scholar
  24. Stephan Kreutzer. Algorithmic meta-theorems. In Javier Esparza, Christian Michaux, and Charles Steinhorn, editors, Finite and Algorithmic Model Theory, London Mathematical Society Lecture Note Series, chapter 5, pages 177-270. Cambridge University Press, 2011. a preliminary version is available at Electronic Colloquium on Computational Complexity (ECCC), TR09-147, URL: http://www.eccc.uni-trier.de/report/2009/147.
  25. Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. Spinger-Verlag, 2004. Google Scholar
  26. Sang-Il Oum and Paul D. Seymour. Approximating clique-width and branch-width. Journal of Combinatorial Theory, Series B, 96:514-528, 2006. Google Scholar
  27. Benjamin Rossman. Successor-invariant first-order logic on finite structures. J. Symb. Log., 72(2):601-618, 2007. Google Scholar
  28. Detlef Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Computer Science, 5:505-526, 1996. Google Scholar
  29. William T. Tutte. Graph Theory, volume 21 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2001. 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 About DROPS Imprint Privacy Contact