在排除拓扑 minors 的图类上检查不相交路径逻辑
Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes
AI总结：
研究在排除拓扑 minor 的图类上，证明不相交路径逻辑的模型检查问题固定参数可处理，并指出其在子图闭类上的可处理性。
摘要：
不相交路径逻辑，记为 FO+dp，扩展了一阶逻辑（FO），加入了原子谓词 dp_r[(x_1,y_1),…,(x_r,y_r)]，表达存在顶点不相交的路径连接 x_i 和 y_i，对于 1≤i≤r。我们证明，对于排除某个固定图作为拓扑 minor 的每一个图类，FO+dp 的模型检查问题都是固定参数可处理的。这基本上解决了该逻辑在子图闭类上的可处理模型检查问题，因为该问题在不排除拓扑 minor 的子图闭类上是难的（假设进一步的编码效率条件）。
英文摘要：
Disjoint-paths logic, denoted $\mathsf{FO}$+$\mathsf{dp}$, extends first-order logic ($\mathsf{FO}$) with atomic predicates $\mathsf{dp}_r[(x_1,y_1),\ldots,(x_r,y_r)]$, expressing the existence of vertex-disjoint paths between $x_i$ and $y_i$, for $1\leq i\leq r$. We prove that for every graph class excluding some fixed graph as a topological minor, the model checking problem for $\mathsf{FO}$+$\mathsf{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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
