Related papers: Successor-Invariant First-Order Logic on Graphs wi…
We study the model-checking problem for first- and monadic second-order logic on finite relational structures. The problem of verifying whether a formula of these logics is true on a given structure is considered intractable in general, but…
A successor-invariant first-order formula is a formula that has access to an auxiliary successor relation on a structure's universe, but the model relation is independent of the particular interpretation of this relation. It is well known…
We study the first-order (FO) model checking problem of dense graphs, namely those which have FO interpretations in (or are FO transductions of) some sparse graph classes. We give a structural characterization of the graph classes which are…
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…
Order-invariant formulas access an ordering on a structure's universe, but the model relation is independent of the used ordering. Order invariance is frequently used for logic-based approaches in computer science. Order-invariant formulas…
We study the expressive power of successor-invariant first-order logic, which is an extension of first-order logic where the usage of an additional successor relation on the structure is allowed, as long as the validity of formulas is…
A graph class $\mathscr{C}$ is called monadically stable if one cannot interpret, in first-order logic, arbitrary large linear orders in colored graphs from $\mathscr{C}$. We prove that the model checking problem for first-order logic is…
It is known that for subgraph-closed graph classes the first-order model checking problem is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, STOC 2014]. However, the dependency on the formula…
Inspired by a width invariant defined on permutations by Guillemot and Marx [SODA '14], we introduce the notion of twin-width on graphs and on matrices. Proper minor-closed classes, bounded rank-width graphs, map graphs, $K_t$-free unit…
Algorithmic meta-theorems explain the tractability of large classes of computational problems by linking logical expressibility with structural graph properties. While extensions of first-order logic such as FO+dp admit efficient model…
First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem, parameterized by solution size. On the other hand, FO cannot express the very simple algorithmic question of…
In this article, we study parameterized complexity theory from the perspective of logic, or more specifically, descriptive complexity theory. We propose to consider parameterized model-checking problems for various fragments of first-order…
We introduce a new logic, called \emph{cluster first-order logic}, a restricted fragment of first-order logic specifically designed to study order invariance. An order-invariant formula is one on a vocabulary that contains an order;…
We introduce a new data structure for answering connectivity queries in undirected graphs subject to batched vertex failures. Precisely, given any graph G and integer k, we can in fixed-parameter time construct a data structure that can…
Over the past two decades the main focus of research into first-order (FO) model checking algorithms has been on sparse relational structures - culminating in the FPT algorithm by Grohe, Kreutzer and Siebertz for FO model checking of…
Local-order-invariant (first-order) logic is an extension of first-order logic where formulae have access to a ternary local order relation on the Gaifman graph, provided that the truth value does not depend on the specific order relation…
Over the past two decades the main focus of research into first-order (FO) model checking algorithms have been sparse relational structures-culminating in the FPT-algorithm by Grohe, Kreutzer and Siebertz for FO model checking of nowhere…
The notion of bounded expansion captures uniform sparsity of graph classes and renders various algorithmic problems that are hard in general tractable. In particular, the model-checking problem for first-order logic is fixed-parameter…
We prove that the model checking problem for the existential fragment of first-order (FO) logic on partially ordered sets is fixed-parameter tractable (FPT) with respect to the formula and the width of a poset (the maximum size of an…
One of Courcelle's celebrated results states that if C is a class of graphs of bounded tree-width, then model-checking for monadic second order logic is fixed-parameter tractable on C by linear time parameterised algorithms. An immediate…