## Giannos Stamoulis gave a talk on the model checking for first-order logic extended with disjoint paths predicates in H-minor-free graphs at the Discrete Math Seminar

On December 6, 2022, Giannos Stamoulis from Université de Montpellier gave at the Discrete Math Seminar on a fixed-parameter tractable algorithm for the model checking for the first-order logic extended with disjoint paths predicates in H-minor-free graphs. The title of his talk was “Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes“.

## Giannos Stamoulis, Model-Checking for First-Order Logic with Disjoint Paths Predicates in Proper Minor-Closed Graph Classes

The disjoint paths logic, FOL+DP,  is an extension of First Order Logic (FOL) with the extra atomic predicate $\mathsf{dp}_k(x_1,y_1,\ldots,x_k,y_k),$ expressing the existence of internally vertex-disjoint paths between $x_i$ and $y_i,$ for $i\in \{1,\ldots, k\}$. This logic can express a wide variety of problems that escape the expressibility potential of FOL. We prove that for every minor-closed graph class, model-checking for FOL+DP can be done in quadratic time. We also introduce an extension of FOL+DP, namely the scattered disjoint paths logic, FOL+SDP, where we further consider the atomic predicate $\mathsf{s-sdp}_k(x_1,y_1,\ldots,x_k,y_k),$ demanding that the disjoint paths are within distance bigger than some fixed value $s$. Using the same technique we prove that model-checking for FOL+SDP can be done in quadratic time on classes of graphs with bounded Euler genus.
Joint work with Petr A. Golovach and Dimitrios M. Thilikos.

기초과학연구원 수리및계산과학연구단 이산수학그룹
대전 유성구 엑스포로 55 (우) 34126
IBS Discrete Mathematics Group (DIMAG)
Institute for Basic Science (IBS)
55 Expo-ro Yuseong-gu Daejeon 34126 South Korea
E-mail: dimag@ibs.re.kr, Fax: +82-42-878-9209