Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

Add to your list(s) Download to your calendar using vCal

• Giannos Stamoulis, University of Montpellier
• Friday 28 April 2023, 14:00-15:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Jamie Vicary.

Disjoint-paths logic, denoted FO+DP, extends first-order logic (FO) with atomic predicates dp_k[(x_1, y_1),…,(x_k, y_k)], expressing the existence of internally vertex-disjoint paths between x_i and y_i, for 1 ≤ i ≤ k. The formulas of FO+DP can be expressed in monadic second-order logic (MSO) and can capture problems that are not definable in FO. We first prove (fixed-parameter) tractability of the model checking problem for FO+DP on graph classes excluding some fixed graph as a minor. Then, we sketch how to extend this tractability result to graph classes excluding some fixed graph as a topological minor. The latter settles the question of tractable model checking for this logic on subgraph-closed graph classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition of efficiency of encoding).

Joint work with Petr A. Golovach and Dimitrios M. Thilikos and Nicole Schirrmacher, Sebastian Siebertz, Dimitrios M. Thilikos, and Alexandre Vigny.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.