🔬 Research > Talks
2025-09-30. Polyregular Model Checking.
M2F Seminar in LaBRI. [slides]
Abstract
We reduce the model checking problem for a subset of Python to the satisfiability of a first-order formula over finite words, which is known to be decidable. The reduction is based on the theory of polyregular functions, a recently developed generalization of regular languages to polynomial output string-to-string functions. We implemented this reduction in a verification tool called PolyCheck, that can use both automata-based solvers and classical SMT solvers as backends. This is a joint work with Rafał Stefański that was pursued at the University of Warsaw, and was published at CAV'2025.2025-06-13. Polyregular Model Checking.
Automata Seminar in IRIF. [slides]
Abstract
We reduce the model checking problem for a subset of Python to the satisfiability of a first-order formula over finite words, which is known to be decidable. The reduction is based on the theory of polyregular functions, a recently developed generalization of regular languages to polynomial output string-to-string functions. We implemented this reduction in a verification tool called PolyCheck, that can use both automata-based solvers and classical SMT solvers as backends. This is a joint work with Rafał Stefański.2025-04-09. Well-Quasi-Orders and Logic on Graphs.
FMT 2025 in Les Houches. [slides]
Abstract
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.2025-04-09. Well-quasi-ordered classes of graphs and bounded linear clique-width.
Automata Seminar in UW. Blackboard talk.
Abstract
A quasi-ordered set (X, ≤) is a well-quasi-order (WQO) whenever it contains neither infinite antichains, nor infinite decreasing sequences. A cornerstone result of structural graph theory is the Graph Minor Theorem of Robertson and Seymour, stating that the class of all graphs is well-quasi-ordered by the graph minor relation. This result has profound implications in graph theory, and algorithmic consequences such as the polynomial-time solvability of whether a graph can be embedded into a given surface. The class of all (finite, undirected) graphs is not well-quasi-ordered by the induced subgraph relation, and there has been considerable interest in characterizing classes 𝒞 of finite graphs that are well-quasi-ordered for this relation. Most proof schemes used to construct such classes will actually prove that they are WQO even in the presence of a finite number of colours on their vertices. A conjecture from Daligault, Rao and Thomassé states that a class that is WQO with two colours has bounded clique width. In this talk, I will explain how to characterize classes of bounded linear clique with that are WQO when coloured with finitely many colours, and show that this property is actually decidable. This will also be an opportunity to connect classical results of WQO theory (Higman’s lemma, Kruskal’s tree theorem) to the study of such graph classes, and answer in this (not so) restricted setting to some open questions of Pouzet.2024-11-12. Which polynomials are computed by N-weighted automata?.
LINKS Seminar in Inria Lille. [slides]
Abstract
Given a semiring K, the notion of K-weighted automata generalizes regular languages to functions from Σ* to K. This model allows us to compute (multivariate) polynomial functions with coefficients in K. We provide a decidable characterization of polynomials with coefficients in Q that can be computed by K-weighted automata for K = (N,+,×) and for K = (Z+,×). As a consequence, we can decide which functions computed by Z-weighted automata are computed by N-weighted automata, under the assumption of commutativity (the order of the letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). This surprisingly allows us to decide whether such functions are star-free, a notion borrowed from the theory of regular languages.2024-11-08. Which polynomials are computed by N-weighted automata?.
MOVE Seminar in LIS. [slides]
Abstract
Given a semiring K, the notion of K-weighted automata generalizes regular languages to functions from Σ* to K. This model allows us to compute (multivariate) polynomial functions with coefficients in K. We provide a decidable characterization of polynomials with coefficients in Q that can be computed by K-weighted automata for K = (N,+,×) and for K = (Z+,×). As a consequence, we can decide which functions computed by Z-weighted automata are computed by N-weighted automata, under the assumption of commutativity (the order of the letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). This surprisingly allows us to decide whether such functions are star-free, a notion borrowed from the theory of regular languages.2024-11-17. Well-quasi-ordered classes of bounded (linear) clique-width: an automata based approach.
Algco Seminar in LIRMM. [slides]
Abstract
A class of graphs is (labelled) well-quasi-ordered (WQO) whenever any infinite subset of this class contains two (labelled) graphs G and H such that G is an induced subgraph of H respecting the labeling. We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is labelled WQO, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and as a byproduct we answer positively to a conjecture of Pouzet: for such classes of graphs, being WQO using finitely many labels is equivalent to being WQO with infinite sets of labels. We also provide an automata based characterization of earlier results of Daligault, Rao and Thomassé [10.1007/s11083-010-9174-0, Theorem 3] by encoding the models into trees ordered with the gap embedding relation of Dershowitz and Tzameret. This work is available on arxiv: https://arxiv.org/abs/2405.10894. }2024-11-04. Well-quasi-ordered classes of bounded (linear) clique-width: an automata based approach.
M2F Seminar in LaBRI. [slides]
Abstract
A class of graphs is (labelled) well-quasi-ordered (WQO) whenever any infinite subset of this class contains two (labelled) graphs G and H such that G is an induced subgraph of H respecting the labeling. We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is labelled WQO, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and as a byproduct we answer positively to a conjecture of Pouzet: for such classes of graphs, being WQO using finitely many labels is equivalent to being WQO with infinite sets of labels. We also provide an automata based characterization of earlier results of Daligault, Rao and Thomassé [10.1007/s11083-010-9174-0, Theorem 3] by encoding the models into trees ordered with the gap embedding relation of Dershowitz and Tzameret. This work is available on arxiv: https://arxiv.org/abs/2405.10894. }2024-09-18. Well-quasi-ordered classes of bounded (linear) clique-width: an automata based approach.
HIGHLIGHTS 2024 in LaBRI. [slides]
Abstract
We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is well-quasi-ordered by the induced subgraph relation in the presence of a labelling of the vertices, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and the proof scheme allows to derive a weak version of the Pouzet conjecture for classes of bounded linear clique-width.2023-12-07. Z-Polyregular functions.
MOVE Seminar in LIS. [slides]
Abstract
Given a semiring K, the notion of K-weighted automata generalises regular languages to functions from Σ* to K. This model allows us to compute (multivariate) polynomial functions with coefficients in K. We provide a decidable characterisation of polynomials with coefficients in Q that can be computed by K-weighted automata for K = (N,+,×) and for K = (Z+,×). As a consequence, we can decide which functions computed by Z-weighted automata are computed by N-weighted automata, under the assumption of commutativity (the order of the letters in the input does not matter) and polynomial growth (the output of the function is bounded by a polynomial in the size of the input). This surprisingly allows us to decide whether such functions are *star-free*, a notion borrowed from the theory of regular languages.2023-11-06. Compositional Techniques for Preservation Theorems over Classes of Finite Structures.
BOREAL Seminar in LIRMM. [slides]
Abstract
Preservation theorems connect syntactic fragments of first-order logic to corresponding "semantic" properties. For instance, the fragment of unions of conjunctive queries is characterized as the fragment of (first-order) queries that are "preserved under homomorphisms", that is, if A is satisfies the query, and there is a homomorphism from A to B, then B also satisfies the query: this is known as the Homomorphism Presrevation Theorem. As an example of application of such theorems, the homomorphism preservation theorem has been used to characterize the termination of the "Core Chase Algorithm" by Deutsch, Nash and Remmel in 2008. Preservation theorems date back to the 1950s, but the classical proofs of these result are done in the framing of Model Theory and rely heavily on the compactness theorem of first order logic. When restricting our attention to classes of finite structures (which model finite databases), the status of the preservation theorems have been investigated in the past years, with positive and negative results on different classes of finite structures, often with carefully built ad-hoc proofs. The goal of this talk is to recall the landscape of preservation theorems in the finite, and propose a compositional approach to constructing classes of structures over which preservation theorems can be guaranteed.2023-10-18. The Łos-Tarski theorem and locality.
Automata Seminar in UW. Blackboard talk.
Abstract
In this talk, we will investigate the tight connection between the locality properties of first-order logic, and the relativisation (or lack thereof) of the Łós-Tarski Theorem to classes of structures. Starting with a gentle introduction to preservation theorems, we will then focus on two particular classes of sentences: existential formulas, and existential local formulas. We prove that existential local sentences are exactly those that can be rewritten in a positive variant of the Gaifman normal form, and can be characterized semantically as sentences that are preserved under local elementary embeddings. As expected, this semantic characterization fails in the finite. Quite surprisingly though, we can leverage this class of sentences to prove the following locality property for classes of finite structures: the Łós-Tarski Theorem relativises to a class C of finite structures if and only if the Łós-Tarski Theorem locally relativises to the class C, provided that the class C is hereditary and closed under disjoint unions. As a consequence of this result, we not only obtain new proofs of relativisation of Łós-Tarski Theorem, but also provide new classes where this relativisation holds.2023-03-02. Preservation theorems and locality of first order logic.
M2F Seminar in LaBRI. [slides]
Abstract
In this talk, we will investigate the tight connection between the locality properties of first-order logic, and the relativisation (or lack thereof) of the Łós-Tarski Theorem to classes of structures. Starting with a gentle introduction to preservation theorems, we will then focus on two particular classes of sentences: existential formulas, and existential local formulas. We prove that existential local sentences are exactly those that can be rewritten in a positive variant of the Gaifman normal form, and can be characterized semantically as sentences that are preserved under local elementary embeddings. As expected, this semantic characterization fails in the finite. Quite surprisingly though, we can leverage this class of sentences to prove the following locality property for classes of finite structures: the Łós-Tarski Theorem relativises to a class C of finite structures if and only if the Łós-Tarski Theorem locally relativises to the class C, provided that the class C is hereditary and closed under disjoint unions. As a consequence of this result, we not only obtain new proofs of relativisation of Łós-Tarski Theorem, but also provide new classes where this relativisation holds.2022-04-11. Generic Noetherian Theorems - Defining Noetherian Topologies Through Iterations.
BRAVAS team seminar in LMF. [slides]
Abstract
The goal of this talk is to provide a canonical way to construct Noetherian topologies as least fixed points. This is done by proving a least fixed point theorem, that extends the work of Hasegawa on well-quasi-orderings to Noetherian spaces. This extension allows us to justify previously introduced Noetherian topologies, and construct new Noetherian spaces. Finally, note that we can apply our result to spaces that are not inductively defined, provided that the topology/ordering is inductively defined, which is a limitation in Hasegawa's approach.2022-03-28. Locality and Preservation Theorems.
Abstract
This talk is a brief introduction to the relationship between locality based techniques and preservation theorems in finite model theory.2022-11-29. Rejoindre l'administration publique avec un doctorat - Comment et pourquoi ?.
Séminaire du Département Informatique de l'ENS Paris-Saclay in ENS Paris-Saclay. [slides]
Abstract
Discussion sur le devenir des docteurs en France, et des normaliens en particulier.2021-12-17. Basic Operational Preorders for Algebraic Effects - With a pinch of non-determinism and probabilities.
PPS Seminar at IRIF in IRIF. [slides]
Abstract
The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.2021-11-19. Preservation theorems - At the crossroads of topology and logics.
ASV Seminar at IRIF in IRIF. [slides]
Abstract
Presenting my research on preservation theorems in finite model theory, and the connection with Noetherian topologies.