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

2023/02/14 by Nicole Schirrmacher, Schirrmacher, Nicole, Sebastian Siebertz +7 · 1 citation
Computer Science · Chemistry · Engineering · #Formal Methods in Verification #Synthetic Organic Chemistry Methods #Low-power high-performance VLSI design

paper · pdf · doi:10.48550/arxiv.2302.07033

Abstract

Disjoint-paths logic, denoted FO+dp, extends first-order logic (FO) with atomic predicates dp_r[(x₁,y₁),…,(x_r,y_r)], expressing the existence of vertex-disjoint paths between x_i and y_i, for 1≤ i≤ r. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for FO+dp is fixed-parameter tractable. This essentially settles the question of tractable model checking for this logic on subgraph-closed classes, since the problem is hard on subgraph-closed classes not excluding a topological minor (assuming a further mild condition of efficiency of encoding).

Cited by

• The price of homogeneity is polynomial

Related

• Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes
• First-Order Logic with Connectivity Operators
• Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs
• Algorithms and data structures for first-order logic with connectivity under vertex failures
• First-Order Model Checking on Monadically Stable Graph Classes