Language-theoretic methods in combinatorial (semi)group theory go back to Anisimov in the 1970s, who proved the existence of a deep link between the set of words over a fixed generating set representing the identity element in a group – the word problem of the group – and the group-theoretic properties of the group. In particular, he proved that the word problem of a group is a regular language if and only if the group is finite. Muller & Schupp extended this in 1983, and proved their now famous theorem: a group has context-free word problem if and only if it is virtually free. In this talk, I'll give some background on the history and main ideas of combinatorial semigroup theory, and then focus on some of my own work on studying the language-theoretic properties of special monoids, including a generalisation of the Muller-Schupp theorem to special monoids and one-relation monoids with non-trivial idempotents.

The notion of delay between finite transducers is a core element of numerous fundamental results of transducer theory. The goal of this work is to provide a similar notion for more complex abstract machines: we introduce a new notion of delay tailored to measure the similarity between streaming string transducers (SST).

We show that our notion is regular: we design a finite automaton that can check whether the delay between any two SSTs executions is smaller than some given bound. As a consequence, our notion enjoys good decidability properties: in particular, while equivalence between non-deterministic SSTs is undecidable, we show that equivalence up to fixed delay is decidable. Moreover, we show that our notion has good completeness properties: we prove that two SSTs are equivalent if and only if they are equivalent up to some (computable) bounded delay.

Together with the regularity of our delay notion, it provides an alternative proof that SSTs equivalence is decidable. Finally, the definition of our delay notion is machine-independent, as it only depends on the origin semantics of SSTs. As a corollary, the completeness result also holds for equivalent machine models such as deterministic two-way transducers, or MSO transducers.

This is joint work with Emmanuel Filiot, Ismaël Jecker, and Christof Löding.

Runtime verification consists in checking whether a program satisfies a given specification by observing the trace it produces during its execution. In the regular setting, Hennessy-Milner logic with recursion (recHML), a variant of the modal $\mu$-calculus, provides a versatile back-end for expressing linear- and branching-time specifications. In this talk, I will discuss an extension of this logic that allows to express properties over data values (i.e. values from an infinite domain) and examine which fragments can be verified at runtime. Data values are manipulated through equality tests in modalities and through first-order quantification outside of them. They can also be stored using parameterised recursion variables.

I then examine what kind of properties can be monitored at runtime, depending on the monitor model. A key aspect is that the logic has close links with register automata with non-deterministic reassignment, which yields a monitor synthesis algorithm, and allows to derive impossibility results. In particular, contrary to the regular case, restricting to deterministic monitors strictly reduces the set of monitorable properties.

This is joint work with the MoVeMnt team (Reykjavik University): Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Adrian Francalanza, Karoliina Lehtinen.

We study subword constraints expressed by existential first-order formulas over the (scattered) subword order. While it has been known that the truth problem is undecidable, little was known on definability, i.e. which languages and relations over words are definable by subword constraints. As a first step towards understanding the expressiveness of subword constraints, we prove that for alphabets of size at least 3, a relation is definable by subwords constraints if and only if it is recursively enumerable. Whether the same characterization holds for binary alphabets remains an open problem.

This presentation is based on joint work with Pascal Baumann, Ramanathan S. Thinniyam, and Georg Zetzsche (MPI-SWS), which has been presented at STACS 2022 .

In this talk we will discuss two topics: Databases and Predicate Modal Logics.

  In the first case we will look at the consistent query answering problem, where a given database violates some specified constraints. We will see why such databases are interesting and how one would evaluate queries in these cases. We will discuss new algorithms that we have introduced and our attempts to solve an open conjecture in the field. This is work in collaboration with Diego Figueira, Luc Segoufin and Cristina Sirangelo. 
  In the second case we will discuss First Order Modal Logic. These logics are notoriously undecidable (for instance restrictions to unary predicates, guarded fragment, two variable fragment are all undecidable). We will discuss some decidable fragments that we have identified. This is a work in collaboration with R. Ramanujam, Yanjing Wang and Mo Liu.
  Finally we will discuss some possible directions to bring these two seemingly unrelated topics together.

We consider zero-sum games on infinite graphs, with objectives specified as sets of infinite words over some alphabet of colors. A well-studied class of objectives is the one of omega-regular objectives, due to its relation to many natural problems in theoretical computer science. We focus on the strategy complexity question: given an objective, how much memory does each player require to play as well as possible? A classical result is that finite-memory strategies suffice for both players when the objective is omega-regular. We show a reciprocal of that statement: when both players can play optimally with a chromatic finite-memory structure (i.e., whose updates can only observe colors) in all infinite game graphs, then the objective must be omega-regular. This provides a game-theoretic characterization of omega-regular objectives, and this characterization can help in obtaining memory bounds and representations for the objectives as deterministic parity automata. Moreover, a by-product of our characterization is a new one-to-two-player lift: to show that chromatic finite-memory structures suffice to play optimally in two-player games on infinite graphs, it suffices to show it in the simpler case of one-player games on infinite graphs.

These results are based on joint work with Patricia Bouyer and Mickael Randour and have been published in the proceedings of STACS 2022.

We survey some recent (and some not-so-recent) progress on an old problem: In the 1990’s, it was shown (Barrington, Compton , Straubing, and Théren) that the regular languages definable by first-order sentences with no restrictions on the numerical predicates (i.e., the atomic formulas giving relations on the positions in a string) could be defined by sentences in which all these relations could themselves be computed by finite automata (the regular numerical predicates). More succinctly, regular languages require only regular numerical predicates in their logical definitions. This simple-sounding characterization of first-order definable regular languages was proved by appeal to a famous result in circuit complexity, the theorem of Furst, Saxe and Sipser showing that the circuit complexity class AC0 cannot count the number of 1’s in an input string modulo any n>1. In fact, the characterization in turn implies the circuit complexity result. This led to a number of questions, which for the most part remain unsolved: First, does the property hold for logics other than first-order logic? For example, does it continue to hold for Sigma-k formulas, or for Boolean combinations of Sigma-k formulas, or for generalized first-order sentences containing modular counting quantifiers? Second, a somewhat more vague question: is there an ‘elementary’ proof of this fact about logic and automata, one that does not depend on circuit lower bounds? Such a proof for modular quantifiers would settle a long-standing open question in circuit complexity. (It should be stressed here that ‘elementary’ is not the same thing as ‘easy’!) Much of the talk will be devoted to a 2020 paper (Borlido, Gehrke, Krebs, Straubing) giving such an elementary proof of the property for Boolean combinations of Sigma-1 sentences. I will also mention recent progress (Barloy, Cadilhac, Papeman, Zeume, LICS 2022) on establishing the property for Sigma-2 sentences.

In this talk, we present a new construction of a finite automaton associated with a rational (or regular) expression. It is very similar to the one of the so-called Thompson automaton, but it overcomes the failure of the extension of that construction to the case of weighted rational expressions. At the same time, it preserves all of the properties of the Thompson automaton.

This construction has two supplementary outcomes.

The first one is the reinterpretation in terms of automata of a data structure introduced by Champarnaud, Laugerotte, Ouardi, and Ziadi for the efficient computation of the position (or Glushkov) automaton of a rational expression, and which consists in a duplicated syntactic tree of the expression decorated with some additional links.

The second one supposes that this construction devised for the case of weighted expressions is brought back to the domain of Boolean expressions. It allows then to describe, in terms of automata, the construction of the Star Normal Form of an expression that was defined by Brüggemann-Klein, and also with the purpose of an efficient computation of the position automaton.

This is joint work with Sylvain Lombardy (Labri, U. Bordeaux)

A function f uniformizes a relation R(X,Y) if R(X,f(X)) holds for every X in the domain of R. The uniformization problem for a logic L asks whether for every L-definable relation there is an L-definable function that uniformizes it. Gurevich and Shelah proved that no Monadic Second-Order ($\MSO$) definable function uniformizes relation ``Y is a one element subset of X in the full binary tree. In other words, there is no MSO definable choice function in the full binary tree. The cross-section of a relation R(X,Y) at D is the set of all E such that R(D,E) holds. Hence, a function that uniformizes R chooses one element from every non-empty cross-section. The relation ``Y is a one element subset of X has finite and countable cross-sections.

We prove that in the full binary tree the following theorems hold:

Theorem (Finite cross-section) If every cross-section of an MSO definable relation is finite, then it has an MSO definable uniformizer.

Theorem (Uncountable cross-section) There is an MSO definable relation R such that every MSO definable relation included in R and with the same domain as R has an uncountable cross-section.

This talk is about the Radical Identity Testing problem (RIT): Given an algebraic circuit representing a polynomial $f \in \mathbb{Z}[x_1, \dots, x_k]$ and nonnegative integers $a_1, \dots, a_k$ and $d_1, \dots,$ $d_k$, written in binary, test whether the polynomial vanishes at the real radicals $\sqrt[d_1]{a_1}, \dots,\sqrt[d_k]{a_k}$, i.e., test whether $f(\sqrt[d_1]{a_1}, \dots, \sqrt[d_k]{a_k}) = 0$. We will talk about our recent result, placing the problem in coNP assuming the Generalised Riemann Hypothesis (GRH), improving on the straightforward PSPACE upper bound obtained by reduction to the existential theory of reals. Next we focus on a restricted version, called 2-RIT, where the radicals are square roots of prime numbers, written in binary. It was known since the work of Chen and Kao that 2-RIT is at least as hard as the polynomial identity testing problem, however no better upper bound than PSPACE was known prior to our work. We show that 2-RIT in coRP assuming GRH and in coNP unconditionally.

This work is in collaboration with Klara Nosan, Mahsa Shirmohammadi and James Worrell. The results are going to be presented at LICS 2022, and the full-version of the paper can be found here: https://arxiv.org/abs/2202.07961.

This talk investigates the relativisation of the Łós-Tarski Theorem in the finite through the study of existential local sentences. This method yields new well-behaved classes of finite structures where preservation under extensions holds, namely, we show that under mild assumptions on the class of structures, preservation under extensions holds if and only if it holds locally.

The robustness of this proof scheme is explained by its behavior over arbitrary structures, over which we show that existential local sentences match exactly the first-order sentences preserved under local elementary embeddings. Furthermore, we prove that existential local sentences are exactly those that can be written using a positive variant of the Gaifman normal form.

Le monoïde stylique Styl(A) est un quotient fini du monoïde plaxique de Lascoux et Schützenberger. Il est obtenu par l'action naturelle (insertion de Schensted à gauche) du monoïde libre A* sur l'ensemble des (tableaux) colonnes sur A. Il est en bijection avec un ensemble de tableaux semi-standards particuliers, appelés N-tableaux; la bijection consiste en une variante de l'algorithme de Schensted. On en déduit une bijection avec les partitions (ensemblistes) des sous-ensembles de A, et la cardinalté de Styl(A) est le nombre de Bell B_{n+1}, n=|A|. Une présentation de ce monoïde est obtenue en ajoutant aux relations de Knuth les relations d'idempotence a^2=a, pour chaque générateur a dans A. L'involution naturelle de A*, qui retourne les mots et renverse l'ordre de l'alphabet, induit un anti-automorphisme de Styl(A); il se calcule directement sur les N-tableaux par une variante de l'évacuation de Schützenberger. Le monoïde stylique apparaît comme le monoïde syntaxique de la fonction qui à un mot associe la longueur de son plus long sous-mot décroissant.

During the talk, we will study set systems formed by neighborhoods in graphs of bounded twin-width. In particular, we will show how, for a given graph from a class of graphs of bounded twin-width, to efficiently encode the neighborhood of a vertex in a given set of vertices A of the graph. For the encoding we will use only a constant number of vertices from A. The obtained encoding can be decoded using FO formulas. This will prove that the edge relation in graphs of bounded twin-width, seen as first-order structures, admits a definable distal cell decomposition, which is a notion from model theory. From this fact we will derive that we can apply to such classes strong combinatorial tools based on the Distal cutting lemma and the Distal regularity lemma (a stronger version of Szemerédi regularity lemma).

The class of polyregular functions is composed of the string-to-string functions computed by pebble transducers. While this machine model (which extends two-way finite transducers) is two decades old, several alternative characterizations of polyregular functions have been discovered recently [Bojańczyk 2018; Bojańczyk, Kiefer & Lhote 2019], demonstrating their canonicity. The name comes from the polynomial bound on the growth rate of these functions: |f(w)| = |w|^O(1) where |w| is the length of the string w.

In this talk, after recalling this context, I will present some subsequent developments in which I have been involved: * the subclass of comparison-free polyregular (or “polyblind”) functions, definable through a natural restriction of pebble transducers, which Pierre Pradic and I actually discovered while studying a linear λ-calculus; * some results that either relate the growth rate of a polyregular function (comparison-free or not) to the “resources” needed to compute it (number of pebbles or MSO-interpretation dimension), or show that there is no such relationship.

This last item is joint work with Mikołaj Bojańczyk, Gaëtan Douéneau-Tabot, Sandra Kiefer and Pierre Pradic, and builds upon a previous work by Nathan Lhote [2020].

I will present a new result, asserting that a winning condition (or, more generally, a valuation) which admits a neutral letter is positional over arbitrary arenas if and only if for all cardinals there exists a universal graph which is monotone and well-founded. Here, “positional” refers only to the protagonist; this concept is sometimes also called “half-positionality”.

This is the first known characterization in this setting. I will explain the result, quickly survey existing related work, show how it is proved and try to argue why it is interesting.

One important research endeavour at the intersection of circuit complexity theory, algebraic automata theory and logic is the classification of regular languages according to their localisation within the internal structure of NC^1, the class of languages decided by Boolean circuits of polynomial size, logarithmic depth and with gates of constant fan-in. In some sense, the search for such a classification concentrates most of the open questions we have about the relationship between NC^1 and its well-studied subclasses.

While many questions are still open, one of the greatest successes of this research endeavour has been the characterisation of the regular languages in AC^0, the subclass of NC^1 corresponding to Boolean circuits of polynomial length, constant depth and with gates of unbounded fan-in. This characterisation takes the form of a triple languages-algebra-logic correspondence: a regular language is in AC^0 if and only if its syntactic morphism is quasi-aperiodic if and only if it is definable in first-order logic over words with linear order and modular predicates.

It is natural to try to extend such results to classes of formal languages greater than the class of regular languages. A well studied and robust such class is given by visibly pushdown languages (VPLs): languages recognised by pushdown automata where the stack-height-behaviour only depends on the letters read from the input. Over the previous decade, a series of works concentrated on the fine complexity of VPLs, with several achievements: one of those was a characterisation of the class of visibly counter languages (basically VPLs recognised by visibly pushdown automata with only one stack symbol) in AC^0 by Krebs, Lange and Ludwig. However, the characterisation of the VPLs in AC^0 still remains open.

In this talk, I shall present a conjectural characterisation of the VPLs in AC^0 obtained with Stefan Göller at the Universität Kassel. It is inspired by the conjectural characterisation given by Ludwig in his Ph.D. thesis as a generalisation of the characterisation for visibly counter languages, but that is actually false. In fact, we give a more precise general conjectural characterisation that builds upon recognisability by morphisms into Ext-algebras, an extension of recognisability by monoid-morphisms proposed by Czarnetzki, Krebs and Lange to suit the case of VPLs. This characterisation classifies the VPLs into three categories according to precise conditions on the Ext-algebra-morphisms that recognise them: - those that are TC^0-hard; - those that are in AC^0; - those that correspond to a well-identified class of “intermediate languages” that we believe to be neither in AC^0 nor TC^0-hard.

We consider two-player zero-sum games with winning objectives beyond regular languages, expressed as a parity condition in conjunction with a Boolean combination of boundedness conditions on a finite set of counters which can be incremented, reset to 0, but not tested. A boundedness condition requires that a given counter is bounded along the play. Such games are decidable, though with non-optimal complexity, by an encoding into the logic WMSO with the unbounded and path quantifiers, which is known to be decidable over infinite trees. Our objective is to give tight or tighter complexity results for particular classes of counter games with boundedness conditions, and study their strategy complexity. In particular, counter games with conjunction of boundedness conditions are easily seen to be equivalent to Streett games, so, they are CoNP-complete. Moreover, finite-memory strategies suffice for Eve and memoryless strategies suffice for Adam. For counter games with a disjunction of boundedness conditions, we prove that they are in solvable in NP and in CoNP, and in PTime if the parity condition is fixed. In that case memoryless strategies suffice for Eve while infinite memory strategies might be necessary for Adam. Finally, we consider an extension of those games with a max operation. In that case, the complexity increases: for conjunctions of boundedness conditions, counter games are EXPTIME-complete.

We consider infinitely sorted tree algebras recognising regular language of finite trees. We pursue their analysis under the angle of their asymptotic complexity, i.e. the asymptotic size of the sorts as a function of the number of variables involved.

Our main result establishes an equivalence between the languages recognised by algebras of polynomial complexity and the languages that can be described by nominal word automata that parse linearisation of the trees. On the way, we show that for such algebras, having polynomial complexity corresponds to having uniformly boundedly many orbits under permutation of the variables, or having a notion of bounded support (in a sense similar to the one in nominal sets).

We also show that being recognisable by an algebra of polynomial complexity is a decidable property for a regualr language of trees.

This is joint work with Thomas Colcombet.

We consider the problem of computing the Zariski closure of a finitely generated group of matrices. Algorithms for this problem have been applied in automata theory and program analysis, e.g., for showing decidability of the language emptiness problem for quantum automata and for computing polynomial invariants for affine programs.

In this talk we introduce the problem of computing the Zariski closure and describe an existing algorithm, due to Derksen, Jeandel and Koiran, before moving to our main result, which is to obtain an upper bound on the degree of the polynomials that define the Zariski closure. Having an a priori bound allows us to give a simple algorithm for the problem, via linear algebra, similar to Karr's algorithm for obtaining affine invariants for affine programs.

In games with Imperfect information players only have partial knowledge about their position in the game. This makes the task of computing optimal strategies hard especially when players forget previously gained information. To further substantiate this hardness we consider two player zero-sum games with imperfect information modeled in the extensive form and provide several new complexity results on computing maxmin value for various classes of imperfect information. For these lower bound results we consider problems such as the Square-root sum problem and also complexity classes which involve computation over reals, more precisely Existential Theory of Reals (ETR) and other fragments of the First Order Theory of Reals (FOT(R)). This is joint work with Hugo Gimbert and B. Srivathsan.

I will discuss vector spaces spanned by orbit-finite sets. These spaces are infinite-dimensional, but their sets of dimensions are so highly symmetric that the spaces have many properties enjoyed by finitely-dimensional spaces.

Applications of this include a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with the same complexity, language equivalence for unambiguous register automata.

(Joint work with Mikołaj Bojańczyk and Joshua Moerman.)

Awali is a software suite for computing with finite weighted automata and transducers with any number of tapes. Many algorithms are implemented including most of the classical ones. Automata and transducers may be weighted over a classical number sets (N,Z,Q,R,C,Z/nZ) but also over several other weightsets (such as the tropical semirings).

Awali may be accessed in C++ (awalidyn, or directly using templates) or in Python (awalipy). Awali can also be used interactively from its command-line interface (Cora) or using awalipy together with Jupyter, a top-level Python interpreter.

Awali may be downloaded from http://vaucanson-project.org/Awali/2.1/ and I'll be happy to address possible installation issues after the presentation.

In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulas or automata over infinite sequences of signals (omega‑words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite.

The aim of this talk is to investigate the case of infinite alphabets. Correspondingly, executions are modelled as data omega-words. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers, used to store and compare data values. We consider different instances, depending on whether the specification is nondeterministic, universal (a.k.a. co-nondeterministic) or deterministic: contrary to the finite-alphabet case, those classes are expressively distinct.

When the number of registers of the target implementation is unbounded, the synthesis problem is undecidable, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but decidability is recovered for universal ones.

The study was initially conducted over data domains with the equality predicate only, but the techniques can be lifted to the dense order (Q,<) and so-called oligomorphic data domains, over which register automata behave in an omega-regular way. A further exploration of the problem allows to extend the results to the discrete order (N,<), where the behaviours can be regularly approximated. Finally, decidability can be transferred to the case of words with the prefix relation (A^*,<) through a notion of reducibility between domains.