University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity