Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs
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.
model-checking
algorithmic meta-theorem
successor-invariant
first-order logic
topological subgraphs
parameterised complexity
18:1-18:15
Regular Paper
Kord
Eickmeyer
Kord Eickmeyer
Ken-ichi
Kawarabayashi
Ken-ichi Kawarabayashi
10.4230/LIPIcs.CSL.2016.18
Matthew Anderson, Dieter van Melkebeek, Nicole Schweikardt, and Luc Segoufin. Locality from circuit lower bounds. SIAM J. Comput., 41(6):1481-1523, 2012.
Michael Benedikt and Luc Segoufin. Towards a characterization of order-invariant queries over tame graphs. J. Symb. Log., 74(1):168-186, 2009.
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.
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.
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.
Anuj Dawar, Martin Grohe, and Stephan Kreutzer. Locally excluding a minor. In Logic in Computer Science (LICS), pages 270-279, 2007.
Reinhard Diestel. Graph Theory. Number 173 in GTM. Springer, 4th edition, 2012.
Rod Downey and Michael R. Fellows. Parameterized Complexity. Springer, 1998.
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.
Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Perspectives in Mathematical Logic. Springer, 2nd edition, 1999.
Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. Mathematical Logic. Springer, 2nd edition, 1994.
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.
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.
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.
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.
Jörg Flum and Martin Grohe. Fixed-parameter tractability, definability, and model-checking. SIAM J. Comput., 31(1):113-145, 2001.
Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Springer, 2006. ISBN 3-54-029952-1.
Markus Frick and Martin Grohe. Deciding first-order properties of locally tree-decomposable structures. Journal of the ACM, 48:1148-1206, 2001.
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.
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.
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.
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.
Martin Grohe and Thomas Schwentick. Locality of order-invariant first-order formulas. ACM Trans. Comput. Logic, 1(1):112-130, July 2000.
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.
http://www.eccc.uni-trier.de/report/2009/147
Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. Spinger-Verlag, 2004.
Sang-Il Oum and Paul D. Seymour. Approximating clique-width and branch-width. Journal of Combinatorial Theory, Series B, 96:514-528, 2006.
Benjamin Rossman. Successor-invariant first-order logic on finite structures. J. Symb. Log., 72(2):601-618, 2007.
Detlef Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Computer Science, 5:505-526, 1996.
William T. Tutte. Graph Theory, volume 21 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2001.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode