Program

Click on the title to show/hide the abstract.

Sunday 25
19:30—21:00 🍽 Dinner
Monday 26
07:45—08:45 ☕ Breakfast
08:50 Welcome & some information on the week
09:00—10:00
Martin Grohe: Logic and the Power of Recurrent Graph Neural Networks invited talk slides

Graph neural networks (GNNs) are deep learning models for graph data that play a key role in machine learning on graphs. A GNN describes a distributed algorithm carrying out local computations at the vertices of the input graph. Typically, the parameters governing this algorithm are acquired through a data-driven learning process.
    After reviewing GNNs and their basic theory, in this talk, I will focus on the expressiveness of recurrent GNNs. We show that recurrent GNNs can emulate all graph algorithms that respect the natural message-passing invariance induced by the colour refinement (or Weisfeiler-Leman) algorithm. Furthermore, we show that by incorporating random initialisation, recurrent GNNs can emulate all graph algorithms. This emulation introduces only a polynomial overhead in both time and space. In particular, any polynomial-time graph algorithm can be simulated by a recurrent GNN with random initialisation running in polynomial time.
    (This is joint work with Eran Rosenbluth.)

Long break (30 min)
10:30—11:30
Harry Vinall-Smeeth: Unambiguity Makes Context Free Grammars Big slides

A context free grammar (CFG) is unambiguous if each word has a unique derivation. This property can be useful algorithmically, particularly in the case where the grammar represents a finite language. But do we have to pay a cost for this extra algorithmic power? In this talk, we answer this question with a resounding yes: for finite languages, representations by general CFGs can be doubly-exponentially smaller than those by unambiguous CFGs. The talk will focus on the mysterious nature of unambiguous models of computation, how we overcame these difficulties and some promising directions for future research. The talk is based on joint work with Stefan Mengel [1], which will be presented at PODS 2025.
    [1] Mengel, Stefan, and Harry Vinall-Smeeth. "A Lower Bound on Unambiguous Context Free Grammars via Communication Complexity." Available at https://arxiv.org/abs/2412.03199.

Sophie Brinke: Semiring Semantics: Algebraic Properties vs. Logical Results slides

Semiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query — to explain their provenance. To this end, logical statements are not just evaluated to true or false but by values from a commutative semiring. This allows us to track which combinations of atomic facts are responsible for the truth of a statement and to derive practical information about costs, access levels, or confidence scores. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This talk gives an overview of the recent results on the generalisation of model-theoretic properties and methods such as compactness, Ehrenfeucht-Fraïssé games, or locality beyond the Boolean semiring. Many model-theoretic notions admit natural generalisations to the semiring framework (e.g. entailments can be understood as inequalities of semiring valuations) while even simple properties lead to surprisingly difficult questions that require new proof techniques. It turns out that most of the classical logical results and methods can be generalised to some semirings but fail for others. We shall discuss how this is related to algebraic properties of the underlying semirings such as idempotence and absorption.

Christoph Berkholz: Succinct representations for join query evaluation slides

In this talk I will discuss how to represent the result of a multi-way join in a succinct way and how these data structures can be used to support efficient postprocessing such as counting or enumeration tasks. The representation formats we consider are known as factorised databases in the database(theory) literature and are closely connected to variants of DNNF-circuits from knowledge compilation. The main theme of this talk is to present structural characterisations of those input instances where small representations are possible and to provide matching lower bounds. The talk is based on the recent joint work [1] with Harry Vinall-Smeeth
    [1] C. Berkholz, H. Vinall-Smeeth: "Factorised Representations of Join Queries: Tight Bounds and a New Dichotomy." Available at https://arxiv.org/abs/2503.20438

Short break (10 min)
11:40—12:20
Jerzy Marcinkowski: What we can show about the multiset-semantics conjunctive query containment slides

Decidability, and complexity, of multiset-semantics conjunctive query containment is one of the most fascinating and most frustrating open problems in database theory. It has been studied for over 30 years now, and no major progress has been achieved.
    The problem asks, for two given Boolean queries Qs and Qb, whether there exists a database D such that Qs(D)>Qb(D) (notice that Qs(D) and Qb(D) are just natural numbers)
    It has been known for many years that the problem is undecidable if both the queries are unions of conjunctive queries rather than CQs, and also that it is undecidable if (many, I mean MANY) inequalities are allowed in both the CQs in question.
    Tools we developed allowed us to figure out what happens when one of the queries in question is CQ and the other is UCQ (and I doubt you would easily guess the answer), and what happens if one of the queries is a CQ and the other is a CQ with inequalities. We can also show that problem is undecidable if each of the input queries is a CQ with exactly one inequality.
    But the strangest result we can show is that, for every e>0, the problem:
    two given Boolean CQs, Qs and Qb, does there exist a database D such that (1+e)Qs(D) > Qb(D)
    is undecidable (there is some fine print here though).
    This is my joint work with Piotr Ostropolski-Nalewaja and also, to some degree, with Mateusz Orda.

Thomas Zeume: Learning Formal Foundations of Computer Science with Iltis slides

Introductory courses in the formal foundations of computer science are often attended by large numbers of students from diverse backgrounds. In this talk, I will outline how this challenge can be addressed using web-based, interactive exercises provided by Iltis (https://iltis.rub.de/), a modern educational support system covering the foundations of logic, formal languages, and (parts of) complexity theory. I will give a brief introduction to Iltis and outline the research challenges and opportunities for theoretical computer science that arise in the development of such a system.
    This talk is based on a joint article with Marko Schmellenkamp and Fabian Vehlken that appeared in the Educational Column of the EATCS Bulletin (see http://smtp.eatcs.org/index.php/beatcs/article/download/797/842).

12:30—14:30 🍽 Lunch
14:30—15:30
Michał Pilipczuk: Logic through the lens of structural graph theory invited tutorial slides

For a pair of classes of graphs C and D, we say D can be transduced from C if every graph from D can be interpreted in some vertex-colored graph from C using a fixed one-dimensional First-Order interpretation. Transducibility provides a quasi-order on graph classes that naturally stratifies them with respect to their First-Order "complexity" or "expressive power". The goal of the talk is to give a broad overview of a recent line of advances in constructing a logically-motivated structure theory for dense graphs by setting transductions as the cornerstone definition. We will particularly focus on monadically dependent classes — those that do not transduce the class of all graphs — and monadically stable classes — those that do not transduce the class of all total orders. Also, we will discuss analogies between the constructed theory and the classic structure theory for sparse graphs.

Long break (30 min)
16:00—16:40
Patrice Ossona de Mendez: Characterization of stability by quasibounded-size bounded-shrubdepth decompositions slides

The notions of bounded-size and quasibounded-size decompositions with bounded treedepth base classes are central to the structural theory of graph sparsity introduced some years ago, and provide a characterization of both classes with bounded expansions and nowhere dense classes. Strong connections of this theory with model theory led to considering first-order transductions, which are logically defined graph transformations, and to initiate a comparative study of combinatorial and model theoretical properties of graph classes, with an emphasis on the model theoretical notions of dependence (or NIP) and stability.
    In this talk, we present the recent characterization of hereditary stable classes by the existence of quasibounded-size decompositions with bounded shrubdepth base classes. We deduce that every graph $G$ in a stable, hereditary class of graphs $\mathscr C$ has a clique or a stable set of size $\Omega_{\mathscr C,\epsilon}(|G|^{1/2-\epsilon})$, for every $\epsilon>0$, which is tight in the sense that it cannot be improved to $\Omega_{\mathscr C}(|G|^{1/2})$.
    This is a joint work with Sam Braunfeld, Jarik Nesetril, and Sebi Siebertz.

Szymon Toruńczyk: Merge-width and First-Order Model Checking slides

We introduce merge-width, a family of graph parameters that unifies several structural graph measures, including treewidth, degeneracy, twin-width, clique-width, and generalized coloring numbers. Our parameters are based on new decompositions called construction sequences. These are sequences of ever coarser partitions of the vertex set, where each pair of parts has a specified default connection, and all vertex pairs of the graph that differ from the default are marked as resolved. The radius-r merge-width is the maximum number of parts reached from a vertex by following a path of at most r resolved edges. Graph classes of bounded merge-width — for which the radius-r merge-width parameter can be bounded by a constant, for each fixed r=1,2,3,… — include all classes of bounded expansion or of bounded twin-width, thus unifying two central notions from the Sparsity and Twin-width frameworks. Furthermore, they are preserved under first-order transductions, which attests to their robustness. We conjecture that classes of bounded merge-width are equivalent to the previously introduced classes of bounded flip-width.
    As our main result, we show that the model checking problem for first-order logic is fixed-parameter tractable on graph classes of bounded merge-width, assuming the input includes a witnessing construction sequence. This unites and extends two previous model checking results: the result of Dvořák, Král, and Thomas for classes of bounded expansion, and the result of Bonnet, Kim, Thomassé, and Watrigant for classes of bounded twin-width.
    This is joint work with Jan Dreier.

Break (10 min)
16:50—18:00 Open Problem Session
19:00—19:30 🍹 Welcome cocktail
19:30—21:00 🍽 Dinner
Tuesday 27
07:45—08:45 ☕ Breakfast
09:00—10:00
Anuj Dawar: Games and Symmetric Circuits invited tutorial slides

The connection between logical definability and circuit complexity, particularly the tight connection between fixed-point logic with counting and polynomially-uniform symmetric circuits, has highlighted the potential use of pebble games in proving circuit lower bounds. In this tutorial talk, I review the connection between games and circuits with a focus on symmetric algebraic circuits. I end with pointers on current and future directions.

Long break (30 min)
10:30—11:30
Anatole Dahan: Representations of permutation groups in Fixed-point logic slides

I’ll discuss how finite permutation groups can be represented in a logical context, and why this matters for capturing PTIME. While permutation groups have been key to recent progress in efficient algorithms for Graph Isomorphism and Graph Canonization, our ability to represent them concisely often relies on a linear order. In particular, we will see that some computable permutation groups do not admit small symmetric generating sets. In a second time, we will exhibit some structural assumptions under which this issue can be circumvented.

Isolde Adler: Some recent advances in logic and graph property testing slides

Property testing (for a property P) asks for a given graph, whether it has property P, or is "structurally far" from having that property. A "testing algorithm" is a probabilistic algorithm that answers this question with high probability correctly, by only looking at small parts of the input. Testing algorithms are thought of as "extremely efficient", making them relevant in the context of large data sets.
    We discuss some recent advances related to logical meta theorems for property testing in the bounded-degree graph model.

Benjamin Rossman: Equirank Homomorphism Preservation Theorem on Finite Structures slides

The Homomorphism Preservation Theorem (HPT) states that a first-order sentence is preserved under homomorphisms iff it is equivalent to an existential-positive sentence. The classical compactness proof of the HPT, however, (i) yields no computable upper bound on the quantifier rank of the equivalent existential-positive sentence, and (ii) fails to relativize to non-elementary classes such as the finite structures. Previous work by the author [R’08] addressed these drawbacks separately, proving an Equirank HPT (with no blow-up in quantifier rank) and a Finitary HPT (valid over finite structures, but with a large blow-up). In this work we unify the two results by establishing an Equirank Finitary HPT: over finite structures, every homomorphism-preserved sentence is equivalent to an existential-positive sentence with the same quantifier rank. The proof combines the Finitary HPT of [R.08] with an application of the Cai–Furer–Immerman construction to the minimal cores of a homomorphism-preserved sentence’s model class. Paper available at https://users.cs.duke.edu/~br148/equirank-hpt.pdf

Short break (10 min)
11:40—12:20
Colin Geniet: Stability under first-order transduction for variants of twin-width slides

Twin-width is a graph complexity parameter primarily motivated by model checking algorithms for first-order logic. Bounded twin-width is also preserved by first-order transduction. This talk gives a new simple presentation of this proof of stability under transduction. It only uses a standard statement of Gaifman's locality, a variant of the definition of twin-width involving rank, and some elementary logical tools. With this point of view, it becomes easy to observe that the same proof also applies to a class of restrictions of twin-width, such as the so-called reduced bandwidth.
    This is joint work with Édouard Bonnet, Yeonsu Chang, Julien Duron, and O-joung Kwon.

Steffen van Bergerem: Evaluation of First-Order Logic with Counting on Sparse Classes slides

Nowhere dense classes of relational structures are the largest family of sparse classes with a tractable model-checking problem for first-order logic. We study the model-checking and term-evaluation problem for fragments of first-order logic with counting (FOC). Prior work by Grohe and Schweikardt shows that these two problems are fixed-parameter tractable for the fragment FOC1 of FOC on nowhere dense classes, while for the full logic FOC, they are already AW[*]-hard for the class of unranked trees. In this talk, I introduce guarded fragments of FOC that extend FOC1, and I characterise the dividing line of tractability on nowhere dense classes with respect to the expressivity of these fragments.

12:30—14:30 🍽 Lunch
14:30—15:30
Maryanthe Malliaris: New perspectives on model-theoretic complexity invited talk

Part of the power of model-theoretic dividing lines comes from having many different equivalent definitions. The talk will discuss several recent theorems in which certain (infinite) model theoretic dividing lines appear inherently in combinatorics and computer science, and consider what this means from different sides.

Long break (30 min)
16:00—17:00
Samuel Braunfeld: Limits of sequences of finite structures from monadically stable classes slides

In search of a notion of graph limit for sequences of sparse graphs, Nešetřil and Ossona de Mendez introduced first-order convergence for sequences of finite structures (requiring that for every formula, the probability that it is satisfied by a tuple chosen uniformly at random converges) and corresponding analytic limit objects called modeling limits. A modeling limit is a Borel structure, i.e. its domain is a standard Borel space and every parameter-definable relation is Borel, equipped with a probability measure assigning the appropriate limiting value to definable relations. We show that a modeling limit can be constructed for any convergent sequence of finite structures from a monadically stable class. Joint work with Jarik Nešetřil and Patrice Ossona de Mendez.

Ioannis Eleftheriadis: Separability properties of monadically dependent graph classes slides

A graph class C is monadically dependent if one cannot interpret all graphs in coloured graphs from C using a fixed first-order interpretation; this property originates from classical model theory and is conjectured to delimit the tractability of the first-order model checking problem over hereditary classes. Here, we prove a novel characterisation of monadically dependent graph classes in terms flip-separability, a combinatorial property that ensures that local vicinities of graphs coming from this class can be made small after applying a bounded number of flips, i.e. complementations of the adjacency relation on a subset of vertices. Towards this, we introduce a robust toolbox for working with various notions of local separations in monadically dependent classes. This is joint work with Édouard Bonnet, Sam Braunfeld, Colin Genniet, Nikolas Mählmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk.

Pablo Barceló: Separating Automatic Relations slides

We study the separability problem for automatic relations (i.e., relations on finite words definable by synchronous automata) in terms of recognizable relations (i.e., finite unions of products of regular languages). This problem takes as input two automatic relations R and R', and asks if there exists a recognizable relation S that contains R and does not intersect R'. We show this problem to be undecidable when the number of products allowed in the recognizable relation is fixed. In particular, checking if there exists a recognizable relation S with at most k products of regular languages that separates R from R' is undecidable, for each fixed k > 1. Our work reveal tight connections, of independent interest, between the separability problem and the finite coloring problem for automatic graphs, where colors are regular languages.
    Joint work with Diego Figueira and Rémi Morvan

17:01 📷 Group photo
19:30—21:00 🍽 Dinner
Wednesday 28
07:45—08:45 ☕ Breakfast
09:00—10:00
Antoine Mottet: State of the art in infinite-domain constraint satisfaction invited tutorial slides

The complexity of all constraint satisfaction problems with finite templates is by now well understood, but most CSPs cannot be expressed with a finite template. In this tutorial, we will see what is the current state of the field of infinite-domain constraint satisfaction with an emphasis on particular classes of templates for which a “big picture” started to emerge in the recent years.

Long break (30 min)
10:30—11:30
Santiago Guzmán Pro: Hereditary First-Order Logic and Extensional ESO slides

We consider two families of computational problems. The first ones are de- scribed by a fixed first-order sentence φ, and given an input structure A the task is to
    decide A satisfies φ hereditarily, i.e., if every (non-empty) substructure of A satisfies φ. These family of problems is described by hereditary first-order logic (HerFO). The second class consists of problems described by a fixed existential second order (ESO) sentence Ψ, and given an input structure A, the task if to decide if there is an extension B of A that satisfies the first-order part of Ψ, i.e., a structure B such that R^A ⊆ R^B for every existentially quantified predicate R of Ψ, and R^A = R^B for every non-quantified predicate R of Ψ. Extensional ESO is a fragment of ESO that captures these problems. In particular it describes all conservative (pre-coloured) finite-domain CSPs. In this talk we see that extensional ESO and HerFO have the same computational power: the complement of every problem in HerFO is polynomial-time equivalent to a problem in extensional ESO, and vice versa. We also show that extensional ESO describes all CSPs of finitely bounded structures, suggesting no P vs. NP-hard dichotomy for this logic, or for HerFO. However, we also observe that extensional ESO does not have the full computational power of NP: there are problems in NP that are not polynomial-time equivalent to a problem in extensional ESO (unless E=NE) — complementarily, HerFO does not have the full computational power of coNP. If time permits, we will conclude with a description of the quantifier-prefixes for φ such that hereditarily checking φ is in P; we show that for every other quantifier-prefix there exists a formula φ with this prefix such that hereditarily checking φ is coNP-complete. This is based on joint work with Manuel Bodirsky.

Moritz Lichter: Limitations of Affine Relaxations for CSPs via Finite Model Theory and Graph Isomorphism slides

Constraint satisfaction problems (CSPs) provide a universal framework that covers many different computational problems, for example, boolean satisfiability, solving system of equations, or graph coloring. CSPs satisfy a dichotomy: a CSP is tractable, that is, polynomial-time solvable, or NP-complete. For the tractable case, multiple algorithms based on affine relaxations of an integer linear formulation of CSPs were proposed. This line of research has two goals: understanding the power of the affine relaxations and finding a universal algorithm - an algorithm that uniformly solves all tractable CSPs in polynomial time. This talks presents how techniques and constructions from finite model theory and the graph isomorphism problem show limitations of the affine approach: neither Z-affine k-consistency, BLP+AIP, every fixed level of the BA^k-hierarchy, nor the CLAP algorithm solve all polynomial-time CSPs. This answers open problems of Brakensiek, Guruswami, Wrochna, and Živný (ECCC 2020) and of Dalmau and Opršal (LICS 2024). The talk is based in joint work with Benedikt Pago.

Albert Atserias: On Certifying the Chromatic Number of Sparse Random Graphs slides

A simple first-moment calculation shows that for every number of colors q there is a d = d(q) = O(q.log(q)) such that a sparse random graph G(n,d/n) is asymptotically almost surely non-q-colorable. The argument is famously non-constructive in that it fails to provide any easily-checkable certificate for non-q-colorability that applies with asymptotic, not even positive, probability. Motivated by the on-going project of isolating what makes hard instances of the constraint satisfaction problem hard, in this talk I will give a brief overview of the status of the question whether there exist logic-based or algebra-based tests of non-q-colorability that are effective for sparse random graphs.

Short break (10 min)
11:40—12:20
Jakub Opršal: A topological proof of the H-colouring dichotomy slides

As it is well-known, the existence of a colouring of a given graph with $2$ colours can be decided in polynomial-time, and colouring with $k > 2$ colours is NP-complete. In a seminal paper, Hell and Nešetřil [1990] extended this dichotomy to a more general *graph homomorphism problem*, also called the $H$-colouring problem. More precisely, they proved that deciding whether there is a graph homomorphism from a given graph to a fixed graph $H$ is in P if $H$ is bipartite (or contains a self-loop), and is NP-complete otherwise. This dichotomy served as an important test case for the Feder–Vardi dichotomy conjecture, and Bulatov–Zhuk dichotomy of complexity of finite-template CSPs. I will present a new proof of the Hell–Nešetřil theorem using tools from topological combinatorics based on ideas of Lovász [1978] and Brower’s fixed-point theorem. This is joint work with Sebastian Meyer (TU Dresden).

Jaroslav Nešetřil: On orderings slides

Structures which have a linear ordering of their vertices with given local properties have a rich spectrum of complexities. Some have full power of class NP (and thus no dichotomy) but for biconnected patterns we get dichotomy. This also displays the importance of Sparse Incomparability Lemma. This is a joint work with Gabor Kun (Budapest).

12:30—14:30 🍽 Lunch
14:30—15:30
Dan Suciu: The Fine Grained Data Complexity of Conjunctive Query Evaluation invited talk slides

The conjunctive query evaluation problem asks whether there exists a homomorphism between two structures, Q -> D, where Q is called the "query" and D is the "database". In data complexity, the query is fixed and the complexity is a function of the database. Variations of this problem include: enumerating all homomorphisms or counting the number of homomorphisms. This talk is a brief survey of recent results on the fine-grained data complexity of conjunctive query evaluation.
    Central to this study are entropic vectors and entropic inequalities (also called information inequalities). I will start with a brief introduction into this topic. Then I will describe how to use information inequalities to derive an algorithm for conjunctive query evaluation. The algorithm is called PANDA, and its runtime is \tilde O(|D|^{subw(Q)}), where subw(Q) is the "submodular width of Q" (a notion introduced by Marx). This is the best (up to a polylogarithmic factor) upper bound of any combinatorial algorithm known to date.
    Next, I will then describe two approaches to proving lower bounds, both due to Fan, Koutris, and Zhao. One is based on "embeddings" and on a popular fine-grained complexity problem (that no combinatorial algorithm can check the existence of a k-clique in time O(n^{k-eps})). The other proves an absolute lower bound based circuit size. None of these two lower bounds matches the upper bound, except in a few special cases, leaving open the question of which of the two needs to be improved.

Long break (30 min)
16:00—17:00
Antoine Amarilli: Edge-Minimum Walks for RPQs slides

We consider regular path queries (RPQs) on graph databases, i.e., fixing an alphabet Σ, a graph database D is a graph with edges labeled by elements of Σ, and a RPQ Q is simply a regular expression over Σ. For two vertices s and t, a match of Q on D is an st-walk in D where the edge labels form a word of Q. We study the problem of computing *edge-minimum walks*, i.e,. for a fixed query Q, given a graph database D, we want to compute a match of Q in D that uses a minimum number of *distinct* edges. Equivalently, we want to compute a minimum-cardinality subset D' of D which contains a Q-match.
    We will explain how computing edge-minimum walks can be PTIME or NP-hard depending on the fixed RPQ Q, and we will present on ongoing work (with Benoît Groz and Nicole Wein) about classifying the complexity of this problem. The presentation will focus on our recent result (presented at ITCS'25) that the edge-minimum walks problem is in PTIME for fixed modular constraints (i.e., it is PTIME to compute the edge-minimum walk of length p mod q for fixed p and q).

Wim Martens: Rel: Programming in the Large with Data slides

From the moment of their inception, languages for relational data have been described as sublanguages embedded in a host programming language. Rel is a new relational language whose key design goal is to go beyond this paradigm with features that allow for programming in the large, making it possible to fully describe end to end application semantics. With the new approach we can model the semantics of entire enterprise applications relationally, which helps significantly reduce architecture complexity and avoid the well-known impedance mismatch problem. This paradigm shift is enabled by 50 years of database research, making it possible to revisit the sublanguage/host language paradigm, starting from the fundamental principles. We present the main features of Rel: those that give it the power to express traditional query language operations and those that are designed to grow the language and allow programming in the large.

Rémi Morvan: Minimizing Conjunctive Regular Path Queries slides

We study the minimization problem for Conjunctive Regular Path Queries (CRPQs) and unions of CRPQs (UCRPQs). This is the problem of checking, given a query and a number k, whether the query is equivalent to one of size at most k. For CRPQs we consider the size to be the number of atoms, and for UCRPQs the maximum number of atoms in a CRPQ therein, motivated by the fact that the number of atoms has a leading influence on the cost of query evaluation. We show that the minimization problem is decidable, both for CRPQs and UCRPQs. This is joint work with Diego Figueira and Miguel Romero.

19:30—21:00 🍽 Dinner
Thursday 29
07:45—08:45 ☕ Breakfast
09:00—10:00
Tim Seppelt: Homomorphism Indistinguishability: Theory and Applications invited tutorial slides

In 1967, Lovász proved that two graphs G and H are isomorphic if, and only if, they are homomorphism indistinguishable over the the family of all graphs, i.e. for all graphs F the number of homomorphisms from F to G is equal to the number of homomorphisms from F to H. In recent years, many natural relaxations of graph isomorphism from fields as diverse as quantum information theory, algebraic graph theory, convex optimisation, and category theory have been characterised as homomorphism indistinguishability relations over restricted graph classes.
    Abstracting from the wealth of such characterisations, we set out to develop a theory of homomorphism indistinguishability that provides insights into the descriptive and computational complexity of graph isomorphism relaxations. That is, for a graph class 𝓕, we ask
    - what is the distinguishing power of homomorphism counts from graphs F ∊ 𝓕 and - what is the complexity of deciding homomorphism indistinguishability over 𝓕?
    Finally, we show how the answers to these questions help to understand the counting and algebraic complexity of so-called graph motif parameters, i.e. graph parameters that can be expressed by homomorphism counts (Curticapean, Dell, Marx, STOC 2017).

Long break (30 min)
10:30—11:30
Nina Runde: The Complexity of Homomorphism Reconstructibility slides

Representing graphs by their homomorphism counts has led to the beautiful theory of homomorphism indistinguishability in recent years. Moreover, homomorphism counts have promising applications in database theory and machine learning, where one would like to answer queries or classify graphs solely based on the representation of a graph G as a finite vector of homomorphism counts from some fixed finite set of graphs to G. We study the computational complexity of the arguably most fundamental computational problem associated to these representations, the homomorphism reconstructibility problem: given a finite sequence of graphs and a corresponding vector of natural numbers, decide whether there exists a graph G that realises the given vector as the homomorphism counts from the given graphs.
    We show that this problem yields a natural example of an NP^{#P}-hard problem, which still can be NP-hard when restricted to a fixed number of input graphs of bounded treewidth and a fixed input vector of natural numbers, or alternatively, when restricted to a finite input set of graphs. We further show that, when restricted to a finite input set of graphs and given an upper bound on the order of the graph G as additional input, the problem cannot be NP-hard unless P = NP. We also investigate the problem’s parameterised complexity and provide fpt-algorithms for the case that a single graph is given and that multiple graphs of the same order with subgraph instead of homomorphism counts are given.

Eva Fluck: Monotonicity of cops-and-robber-games slides

We study variations of the cops-and-robber-game regarding the following question: If the cop-player has a winning strategy, do they also have a winning strategy that is cop- or robber-monotone? We say the respective variant is cop- or robber-monotone. Here cop-monotonicity denotes that the cop-player is never allowed to move to a position that they previously left and robber-monotonicity denotes that the robber-player can never move to a vertex that was previously occupied by the cops. In the well-known cops-and-robber-game as defined by Seymour and Thomas (1993) these notions coincide.
    We study a variant of this game, where in each round at most one cop may be placed and in each play at most q rounds are played, where q is a parameter of the game. We prove that this game is both cops- and robber-monotone. As a corollary we obtain a new characterization of bounded depth treewidth, and we give a positive answer to an open question by Fluck, Seppelt and Spitzer (2024), thus showing that graph classes of bounded depth tree-width are homomorphism distinguishing closed.
    Furthermore we study a variant, where the robber player is only allowed to move, if the cop-player announces that they will move a cop to the robber-position in the next round. Again we find that these games are robber-monotone, confirming a conjecture by Richerby and Thilikos (2011). In the case where the cop-player does not have any information about the whereabouts of the robber-player, it is known that the number of cops needed to catch the robber equals the tree width of the graph plus one. We show that in order to catch the robber using a cop-monotone strategy one needs path-width plus one may cops, thus this game variant is not cop-monotone.
    This is joint work with Isolde Adler and David Philipps.

Balder ten Cate: Adaptive Query Algorithms for Relational Structures Based on Homomorphism Counts slides

A query algorithm based on homomorphism counts is a procedure to decide membership for a class of finite relational structures using only homomorphism count queries. A left query algorithm can ask the number of homomorphisms from any structure to the input structure and a right query algorithm can ask the number of homomorphisms from the input structure to any other structure. We systematically compare the expressive power of different types of left or right query algorithms, including non-adaptive query algorithms, adaptive query algorithms that can ask a bounded number of queries, and adaptive query algorithms that can ask an unbounded number of queries. We also consider query algorithms where the homomorphism counting is done over the Boolean semiring, meaning that only the existence of a homomorphism is recorded, not the precise number of them.
    Joint work with Phokion G. Kolaitis and Arnar A. Kristjansson (under submission)

Short break (10 min)
11:40—12:20
Benedikt Pago: Symmetric algebraic circuits and homomorphism polynomials slides

Algebraic complexity studies families of polynomials in terms of the size of the smallest algebraic circuits representing them. We study the restriction to symmetric polynomials and symmetric cicuits because it allows to prove strong lower bounds that are out of reach in the general setting: For example, exponential lower bounds on the symmetric circuit complexity of the permanent were shown by Dawar and Wilsenach (2020). In this work, we set out to develop a more general symmetric algebraic complexity theory. Our main result is that a family of symmetric polynomials admits efficient symmetric circuits if and only if they can be written as linear combinations of homomorphism counting polynomials of graphs of bounded treewidth. We also establish a relationship between the symmetric complexity of subgraph counting and the vertex cover number. Finally, we examine the symmetric complexity of immanant families (a generalisation of the determinant and permanent) and show that a known conditional complexity dichotomy due to Curticapean (2021) holds unconditionally in the symmetric setting. Joint work with Anuj Dawar and Tim Seppelt.

Aliaume Lopez: Well-Quasi-Orders and Logic on Graphs slides

In this talk I will give a survey on the results and conjectures on classes of graphs that are (labelled) well-quasi-ordered by the induced subgraph relation. I will discuss how this seemingly purely combinatorial property is deeply connected to logic and structural decompositions of graphs. Starting from the early results of Ding regarding bounded tree-depth, we will explore classes of bounded clique-width, monadically stable classes, monadically dependent classes, and state various conjectures, old and new. The goal of this talk is to give an overview of the questions of interest and is targeted as a broad “Finite and algorithmic model theory” audience.

12:30—14:30 🍽 Lunch
Free (see Excursion for ideas)
19:30—21:00 🍽 Dinner
Friday 30
07:45—08:45 ☕ Breakfast
09:00—10:00
Mikołaj Bojańczyk: Deciding equivalence for first-order interpretations invited talk slides

First-order interpretations are a formalism of defining functions from structures to structures. The idea is that elements of the output structure are represented by k-tuples of elements in the input structure, and the relations of the output structure are defined using first-order logic. In this talk, I will discuss the equivalence problem for such interpretations. This is a problem that is parameterised by two classes of structures C and D. We are given two first-order interpretations that define functions C -> D, and we want to know if they are equivalent, i.e. for every input structure in C, the two output structures in D are isomorphic. I will show that this problem is decidable if both C and D are classes of graphs of bounded tree-depth (joint work with Bartek Klin). I will also place this result in the context of a wider research programme, which considers classes of structures such as strings, or graphs of bounded treewidth.

Long break (30 min)
10:30—11:30
Thomas Colcombet: String-to-string MSO-set-interpretations slides

MSO-set-interpretations are variants of standard logical MSO-interpretations that transform logical structures into logical structures, with the particularity that the elements of the output structure are sets of elements of the original one. It can for instance transform a linear order of length n into a linear order of length 2^n by lexicographically ordering its subsets. A straightforward property of this notion is that the inverse image of an FO-definable property is effectively an MSO-definable property, and can be used for describing the various form of automatic structures [C., Löding 07].
    In this work, we show that for string-to-string (string = labelled finite total orders) MSO-set-interpretations, the MSO-theory of the inverse image of an MSO-definable property is an MSO-definable property.
    This extends results for polyregular functions [Bojańczyk, Kiefer, Lhote 19] (see also the survey [Bojańczyk 22]), which correspond to the special case of MSO-set-interpretations of polynomial size-increase (thanks to [Gallot, Lhote, Tito 25]). During the talk, we shall also see a corresponding notion of transducers (that extends [Clairambault, Murawski 19]), and how this result is related to (not-necessary safe) simply typed lambda-calculus. The decidability of the MSO-theory of omega-automatic words also follows thanks to [Fliot, Lhote, Reynier 25], solving a conjecture from [Barany 08].
    This is a collaboration with Nathan Lhote, Lê Thành Dũng (Tito) Nguyễn and Pierre Ohlmann.

Bartosz Bednarczyk: Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards slides

We study the Guarded Fragment with Regular Guards (RGF), which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2ExpTime-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying, in a natural sense, the maximal ExpSpace-complete fragment of RGF.

David Carral: Expressibility vs Rewritability in Ontology Based Query Answering slides

We consider the problem of checking whether a Boolean conjunctive query (BCQ) is a logical consequence of a knowledge base (KB), which in our context is a pair (R, F) where R and F are finite sets of existential rules and facts. We can sometimes tackle this problem via rewriting into a union of BCQs: given an (existential) rule query (R, q) consisting of a rule set R and a BCQ q, we compute a UBCQ qR such that, for every fact set F, the KB (R, F) entails q if and only if F entails qR. In fact, a uniform procedure exists for computing these rewritings, with guaranteed termination for any input rule query that can be expressed as a UBCQ. This naturally raises the question: can we design a uniform rewriting procedure with similar termination guarantees for more expressive target languages, such as Datalog? What about fragments of this well-known KR language, such as linear or monadic Datalog? Unfortunately, we show that no such terminating uniform procedure exists for either of these languages.

Short break (10 min)
11:40—12:20
Erich Grädel: Semiring Semantics in the Infinite slides

Semiring semantics evaluates database queries or logical statements not just by true or false but by values in some commutative semiring. This permits to track which combinations of atomic facts are responsible for the truth of a statement, and to derive further information, for instance concerning costs, confidence scores, number of successful evaluation strategies, or access levels to protected data. The focus of this approach has originally been on the provenance analysis for positive database query languages, but has later been extended to a systematic semiring semantics for first-order logic and other logical systems, as well as to a method for the strategy analysis of games.
    Traditionally, semiring semantics has been studied for finite structures only. To extend it to possibly infinite ones, the semirings need to be equipped with addition and multiplication operators over infinite collections of values. This needs solid algebraic foundations, and we discuss here the necessary and desirable properties of semirings with infinitary operations, so that they can provide a well-defined and informative semantics also over infinite domains. It turns out that, with suitable definitions of such infinitary semirings, large parts of the theory of semiring semantics can be succesfully generalised to infinite structures.
    This is joint work with Sophie Brinke, Lovro Mrkonjić, and Matthias Naaf.

Wojciech Przybyszewski: Low rank MSO slides

We introduce a new logic for describing properties of graphs, which is called low rank MSO. This is the fragment of monadic second-order logic (MSO), in which set quantification is restricted to sets of bounded rank. We prove that over any class of graphs that is weakly sparse, low rank logic has the same expressive power as separator logic, which is another extension of first-order order logic that can talk about non-local behavior such as connectivity. We also compare the expressive power of low rank MSO with variants of separator logic that involve flips. This is joint work with Mikołaj Bojańczyk, Michał Pilipczuk, Marek Sokołowski, and Giannos Stamoulis.

12:30—14:30 🍽 Lunch