Document

First-Order Logic with Connectivity Operators

File

LIPIcs.CSL.2022.34.pdf
• Filesize: 0.73 MB
• 17 pages

Acknowledgements

We thank Mikołaj Bojańczyk for fruitful discussions. He independently studied FO+conn and suggested the name separator logic for this logic. We also thank Michał Pilipczuk and Szymon Toruńczyk for fruitful discussions.

Cite As

Nicole Schirrmacher, Sebastian Siebertz, and Alexandre Vigny. First-Order Logic with Connectivity Operators. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.34

Abstract

First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. On the other hand, FO cannot express the very simple algorithmic question whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph properties that are commonly studied in parameterized algorithmics. By adding the atomic predicates conn_k(x,y,z_1,…,z_k) that hold true in a graph if there exists a path between (the valuations of) x and y after (the valuations of) z_1,…,z_k have been deleted, we obtain separator logic FO+conn. We show that separator logic can express many interesting problems such as the feedback vertex set problem and elimination distance problems to first-order definable classes. Denote by FO+conn_k the fragment of separator logic that is restricted to connectivity predicates with at most k+2 variables (that is, at most k deletions). We show that FO+conn_{k+1} is strictly more expressive than FO+conn_k for all k ≥ 0. We then study the limitations of separator logic and prove that it cannot express planarity, and, in particular, not the disjoint paths problem. We obtain the stronger disjoint-paths logic FO+DP by adding the atomic predicates disjoint-paths_k[(x_1,y_1),…,(x_k,y_k)] that evaluate to true if there are internally vertex-disjoint paths between (the valuations of) x_i and y_i for all 1 ≤ i ≤ k. Disjoint-paths logic can express the disjoint paths problem, the problem of (topological) minor containment, the problem of hitting (topological) minors, and many more. Again we show that the fragments FO+DP_k that use predicates for at most k disjoint paths form a strict hierarchy of expressiveness. Finally, we compare the expressive power of the new logics with that of transitive-closure logics and monadic second-order logic.

Subject Classification

ACM Subject Classification
• Theory of computation → Finite Model Theory
• Mathematics of computing → Combinatorics
Keywords
• First-order logic
• graph theory
• connectivity

Metrics

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

References

1. Akanksha Agrawal, Lawqueen Kanesh, Fahad Panolan, M. S. Ramanujan, and Saket Saurabh. An FPT algorithm for elimination distance to bounded degree graphs. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021.
2. Mikołaj Bojańczyk. Separator logic and star-free expressions for graphs. arXiv preprint, 2021. URL: http://arxiv.org/abs/2107.13953.
3. Édouard Bonnet, Ugo Giocanti, Patrice Ossona de Mendez, Pierre Simon, Stéphan Thomassé, and Szymon Toruńczyk. Twin-width IV: ordered graphs and matrices. arXiv preprint, 2021. URL: http://arxiv.org/abs/2102.03117.
4. Jannis Bulian. Parameterized complexity of distances to sparse graph classes. Technical report, University of Cambridge, Computer Laboratory, 2017.
5. Jannis Bulian and Anuj Dawar. Graph isomorphism parameterized by elimination distance to bounded degree. Algorithmica, 75(2):363-382, 2016.
6. Michael Buro. Simple amazons endgames and their connection to Hamilton circuits in cubic subgrid graphs. In International Conference on Computers and Games, pages 250-261. Springer, 2000.
7. Bruno Courcelle. The monadic second-order logic of graphs. I. recognizable sets of finite graphs. Information and computation, 85(1):12-75, 1990.
8. Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems, 33(2):125-150, 2000.
9. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015.
10. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Springer Science & Business Media, 2005.
11. Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. Complexity of computation, 7:43-73, 1974.
12. Fedor V. Fomin, Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. An algorithmic meta-theorem for graph modification to planarity and FOL. In 28th Annual European Symposium on Algorithms, ESA 2020, pages 51:1-51:17, 2020.
13. Fedor V. Fomin, Petr A. Golovach, and Dimitrios M. Thilikos. Parameterized complexity of elimination distance to first-order logic properties. arXiv preprint, 2021. URL: http://arxiv.org/abs/2104.02998.
14. Fedor V. Fomin, Daniel Lokshtanov, Fahad Panolan, Saket Saurabh, and Meirav Zehavi. Hitting topological minors is FPT. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, pages 1317-1326, 2020.
15. Robert Ganian, Petr Hliněnỳ, Alexander Langer, Jan Obdržálek, Peter Rossmanith, and Somnath Sikdar. Lower bounds on the complexity of MSO1 model-checking. Journal of Computer and System Sciences, 80(1):180-194, 2014.
16. Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein. Finite Model Theory and its applications. Springer Science & Business Media, 2007.
17. Martin Grohe. Logic, graphs, and algorithms. Logic and automata, 2:357-422, 2008.
18. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. Journal of the ACM (JACM), 64(3):17, 2017.
19. Eva-Maria C. Hols, Stefan Kratsch, and Astrid Pieterse. Elimination distances, blocking sets, and kernels for vertex cover. In STACS, 2020.
20. Bart M. P. Jansen, Jari J. H. de Kroon, and Michał Włodarczyk. Vertex deletion parameterized by elimination distance and even less. In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing, pages 1757-1769, 2021.
21. Stephan Kreutzer and Siamak Tazari. Lower bounds for the complexity of monadic second-order logic. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 189-198. IEEE, 2010.
22. Leonid Libkin. Elements of finite model theory. Springer Science & Business Media, 2013.
23. Alexander Lindermayr, Sebastian Siebertz, and Alexandre Vigny. Elimination distance to bounded degree on planar graphs. In 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic, pages 65:1-65:12, 2020.
24. Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny. Algorithms and data structures for first-order logic with connectivity under vertex failures. arXiv preprint, 2021. URL: http://arxiv.org/abs/2111.03725.
25. Bruce Reed, Kaleigh Smith, and Adrian Vetta. Finding odd cycle transversals. Operations Research Letters, 32(4):299-301, 2004.
26. Neil Robertson and P. D. Seymour. Graph minors. XIII. the disjoint paths problem. J. Combin. Theory Ser. B, 63:65-110, 1995.
27. Wolfgang Thomas. Languages, automata, and logic. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 389-455. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_7.
X

Feedback for Dagstuhl Publishing