Animation scientifique

In this talk, I will introduce the family of neighborhood operator (NEO) logics which are extensions of existential MSO with predicates for querying neighborhoods of vertex sets. NEO logics have interesting modeling powers and nice algorithmic applications for several width parameters such as tree-width, clique-width, mim-width, and treedepth. NEO logics capture many important graphs problems such as Independent Set, generalizations of Dominating Set, and even CNF-SAT via the signed incidence graphs! We can capture more problems by considering various extensions of NEO logics with predicates for checking global constraints, for example, with connectivity constraints we can capture Hamiltonian Cycle and Longest Path.

In terms of algorithmic applications, NEO logics seem to be the perfect candidates for capturing many problems that can be solved efficiently in terms of width parameters.
This is suggested by the following three results:

For tree-width, the most powerful NEO logic can be model checked in single exponential time in terms of tree-width as implied by a result of Michal Pilipczuk [MFCS 2011] (arxiv.org/abs/1104.3057) and an equivalence between the modal logic used by Pilipczuk and this NEO logic proved in the following paper.

Jan Dreier, Lars Jaffke and I proved that, for an extension of one NEO logic, we can obtain an efficient model-checking algorithm in terms of several width parameters more general than tree-width such as clique-width, rank-width and mim-width [SODA 2023] (arxiv.org/abs/2202.13335).

Vera Checkan, Giannos Stamoulis and I proved that the most powerful NEO logic can be model checked in single exponential time and polynomial space for tree-depth [SODA 2026] (arxiv.org/abs/2510.19793).

These three results provide algorithmic meta-theorems that generalize and unify the most efficient algorithms based on these width parameters. The running times of the model checking algorithms are tight under ETH for each width parameter.