First-Order Logic with Connectivity Operators

Authors Nicole Schirrmacher , Sebastian Siebertz , Alexandre Vigny

Thumbnail PDF


  • Filesize: 0.73 MB
  • 17 pages

Document Identifiers

Author Details

Nicole Schirrmacher
  • University of Bremen, Germany
Sebastian Siebertz
  • University of Bremen, Germany
Alexandre Vigny
  • University of Bremen, Germany


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 AsGet BibTex

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)


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
  • First-order logic
  • graph theory
  • connectivity


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


  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. Google Scholar
  2. Mikołaj Bojańczyk. Separator logic and star-free expressions for graphs. arXiv preprint, 2021. URL:
  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:
  4. Jannis Bulian. Parameterized complexity of distances to sparse graph classes. Technical report, University of Cambridge, Computer Laboratory, 2017. Google Scholar
  5. Jannis Bulian and Anuj Dawar. Graph isomorphism parameterized by elimination distance to bounded degree. Algorithmica, 75(2):363-382, 2016. Google Scholar
  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. Google Scholar
  7. Bruno Courcelle. The monadic second-order logic of graphs. I. recognizable sets of finite graphs. Information and computation, 85(1):12-75, 1990. Google Scholar
  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. Google Scholar
  9. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. Google Scholar
  10. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Springer Science & Business Media, 2005. Google Scholar
  11. Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. Complexity of computation, 7:43-73, 1974. Google Scholar
  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. Google Scholar
  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:
  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. Google Scholar
  15. Robert Ganian, Petr Hliněnỳ, 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. Google Scholar
  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. Google Scholar
  17. Martin Grohe. Logic, graphs, and algorithms. Logic and automata, 2:357-422, 2008. Google Scholar
  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. Google Scholar
  19. Eva-Maria C. Hols, Stefan Kratsch, and Astrid Pieterse. Elimination distances, blocking sets, and kernels for vertex cover. In STACS, 2020. Google Scholar
  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. Google Scholar
  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. Google Scholar
  22. Leonid Libkin. Elements of finite model theory. Springer Science & Business Media, 2013. Google Scholar
  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. Google Scholar
  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:
  25. Bruce Reed, Kaleigh Smith, and Adrian Vetta. Finding odd cycle transversals. Operations Research Letters, 32(4):299-301, 2004. Google Scholar
  26. Neil Robertson and P. D. Seymour. Graph minors. XIII. the disjoint paths problem. J. Combin. Theory Ser. B, 63:65-110, 1995. Google Scholar
  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:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail