I present recent developments concerning a very general algebraic theory for languages of infinite trees which is based on the category-theoretical notion of a monad. The main result isolates a class of algebras that precisely captures the notion of regularity for such languages. In particular, we show that these algebras form a pseudo-variety and that syntactic algebras exists. If time permits I will conclude the talk with a few simple characterisation results obtained using this framework.

Residuated lattices are a variety of ordered monoids whose study arises from from three directions: Algebras of ideals of rings, algebras of binary relations, and the semantics of substructural logics. This talk provides a survey of residuated lattices, discussing both their historical origins and current threads of research. We also offer an introduction to some difficult problems that arise their study, in particular connected to structure theorems for special classes of residuated lattices and their duality theory.

Given a system of linear Diophantine equations, how difficult is it to determine whether it has a solution? What changes if equations are replaced with inequalities? If some of the variables are quantified universally? These and similar questions relate to the computational complexity of deciding the truth value of statements in various logics. This includes in particular Presburger arithmetic, the first-order logic over the integers with addition and order.

In this talk, I will survey constructions and ideas that underlie known answers to these questions, from classical results to recent developments, and open problems.

First, we will recall the geometry of integer linear programming and how it interacts with quantifiers. This will take us from classical results due to von zur Gathen and Sieveking (1978), Papadimitriou (1981), and others to the geometry of the set of models of quantified logical formulas. We will look at rational convex polyhedra and their discrete analogue, hybrid linear sets (joint work with Haase (2017)), and see, in particular, how the latter form a proper sub-family of ultimately periodic sets of integer points in several dimensions (the semi-linear sets, introduced by Parikh (1961)).

Second, we will discuss “sources of hardness”: which aspects of the expressive power make decision problems for logics over the integers hard. Addition and multiplication combined enable simulation of arbitrary Turing machines, and restriction of multiplication to bounded integers corresponds to resource-bounded Turing machines. How big can these bounded integers be in Presburger arithmetic? This leads to the problem of representing big numbers with small logical formulae, and we will see constructions by Fischer and Rabin (1974) and by Haase (2014). We will also look at the new “route” for expressing arithmetic progressions (in the presence of quantifier alternation) via continued fractions, recently discovered by Nguyen and Pak (2017).

La structure (R,+,<,Z), où R désigne l'ensemble des réels et Z le prédicat unaire “être un entier”, admet l'élimination des quantificateurs et est décidable. Elle intervient notamment dans le domaine de la spécification et la vérification de systèmes hybrides. Elle peut être étudiée via les automates, en considérant des automates de Büchi qui lisent des réels représentés dans une base entière fixée. Boigelot et al. ont démontré en particulier que la classe des relations définissables dans (R,+,<,Z) coïncide avec celle des relations reconnaissables par automate en toute base. Une autre structure intéressante est (R,+,<,1), qui est moins expressive que (R,+,<,Z) mais définit les mêmes relations bornées. On présente une caractérisation topologique des relations définissables dans (R,+,<,Z) qui sont définissables dans (R,+,<,1), et on en déduit que le problème de savoir si une relation définissable dans (R,+,<,Z) est définissable dans (R,+,<,1) est décidable. Travail en commun avec Christian Choffrut.

I will talk about two fun constructions for reachability analysis of one-clock timed automata, which lead to concise logical characterizations in existential Linear Arithmetic.

The first one describes “punctual” reachability relations: reachability in exact time t. It uses a coarse interval abstraction and counting of resets via Parikh-Automata. The other is a “sweep line” construction to compute optimal time to reach in reachability games played on one-clock TA.

Together, these can be used to derive a (tight) NP complexity upper bound for the coverability and reachability problems in an interesting subclass of Timed Petri Nets, which naturally lends itself to parametrised safety checking of concurrent, real-time systems. This contrasts with known super-Ackermannian completeness, and undecidability results for unrestricted Timed Petri nets.

This is joint work with Lorenzo Clemente and Piotr Hofman, and was presented at CONCUR'19. Full details are available at https://arxiv.org/abs/1907.01240.

A rational series is a noncommutative formal power series whose coefficients are recognized by a weighted finite automaton (WFA). A rational series with coefficients in a field $K$ is a Pólya series if all nonzero coefficients are contained in a finitely generated subgroup of $K^\times$. Generalizing results of Pólya (1921), Benzaghou (1970), and Bézivin (1987) for the univariate case, we show that Pólya series are precisely the ones recognized by unambiguous WFAs.

This is joint work with Jason Bell. arXiv:1906.07271

We study the language inclusion problem L1 ⊆ L2 where L1 is regular or context-free. Our approach checks whether an overapproximation of L1 is included in L2. Such overapproximations are obtained using quasiorder relations on words where the abstraction gives the language of all words “greater than or equal to” a given input word for that quasiorder. We put forward a range of quasiorders that allow us to systematically design decision procedures for different language inclusion problems such as context-free languages into regular languages and regular languages into trace sets of one-counter nets.

A systematic approach to the study of limits of finite structures, motivated by investigations in graph theory, has been developed by Nešetřil and Ossona de Mendez starting in 2012. The basic idea consists in embedding the set of finite structures into a space of measures which is complete, so that every converging sequence of finite structures admits a limit. This limit point can be always realized as a measure.

I will explain how this embedding into a space of measures dually corresponds to enriching First-Order Logic with certain probability operators. Further, I will relate this construction to first-order quantification in logic on words.

This talk is based on joint work with M. Gehrke and T. Jakl.

Several models of automata with outputs (known as transducers) have been defined over the years to describe various classes of “regular-like” functions. Such classes generally have good decidability properties, and they have been shown especially relevant for program verification or synthesis. In this talk, we shall investigate pebble transducers, i.e. finite-state machines that can drop nested marks on their input. We provide various correspondences between these models and transducers that use registers, and we solve related membership problems. These results can be understood as techniques for program optimization, that can be useful in practice. This talk is based on joint work with P. Gastin and E. Filiot.

We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset of states infinitely often. A question left open by T.P. Hill in 1979 is whether there always exist ε-optimal Markov strategies, i.e., strategies that base decisions only on the current state and the number of steps taken so far. We provide a negative answer to this question by constructing a non-trivial counterexample. On the other hand, we show that Markov strategies with only 1 bit of extra memory are sufficient. This work is in collaboration with Stefan Kiefer, Richard Mayr and Patrick Totzke, and is going to be presented in ICALP 2019. A full version is at https://arxiv.org/abs/1904.11573

Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the price of spending time in a state and executing an action, respectively). The goals of the players are to minimise or maximise the price to reach a target location. While one can compute the optimal values that the players can achieve (and their associated optimal strategies) when the weights are all positive, this problem with arbitrary integer weights remains open. In this talk, I will explain what makes this case more difficult and show how to solve the problem for a subclass of priced timed games (the so-called simple priced timed games).

Soit $p$ un nombre premier et soit $G_p$ la variété de tous les langages reconnus par un $p$-groupe fini (i.e. un groupe d'ordre une puissance de $p$). On donne deux façons de construire toutes les fonctions $f$ de $A^*$ dans $B^*$ (et même dans $F(B)$, le groupe libre de base $B$) qui possèdent la propriété suivante: si $L$ est une partie de $F(B)$ reconnue par un $p$-groupe fini, alors $f^{-1}(L)$ a la même propriété. Ce résultat découle d'une version non-commutative des séries de Newton et d'un célèbre théorème de Mahler en analyse $p$-adique.

Probabilistic timed automata are classical timed automata extended with discrete probability distributions over edges. In this talk, clock-dependent probabilistic timed automata, a variant of probabilistic timed automata in which transition probabilities can depend on clock values, will be described. Clock-dependent probabilistic timed automata allow the modelling of a continuous relationship between time passage and the likelihood of system events. We show that the problem of deciding whether the maximum probability of reaching a certain location is above a threshold is undecidable for clock-dependent probabilistic timed automata. On the other hand, we show that the maximum and minimum probability of reaching a certain location in clock-dependent probabilistic timed automata can be approximated using a region-graph-based approach.

The separation problem for a variety of regular languages V asks to decide whether two disjoint regular languages can be separated by a language in V. The covering problem is a generalization of the separation problem to an arbitrary finite list of regular languages.

The covering problem for the variety of star-free languages was shown to be decidable by Henckell. In fact, he gave an algorithm for an equivalent problem, namely, computing the pointlike subsets of a finite semigroup with respect to the variety of aperiodic semigroups, i.e., semigroups all of whose subgroups are trivial.

In this talk, I will present the following wide generalization of Henckell's result. Let H be any decidable variety of groups. I will describe an algorithm for computing pointlike sets for the variety of semigroups all of whose subgroups are in H. The correctness proof for the algorithm uses asynchronous transducers, Schützenberger groups, and self-similarity. An application of our result is the decidability of the covering and separation problems for the variety of languages definable in first order logic with modular counting quantifiers.

This talk is based on our paper S. v. Gool & B. Steinberg, Adv. in Math. 348, 18-50 (2019).

La théorie des espaces de pavages (sous-shifts) a été profondément façonnée par le résultat historique de Berger : un jeu de tuiles fini peut ne paver le plan que de manière apériodique. Ces points apériodiques sont au coeur de nombreuses directions de recherche du domaine, en mathématiques comme en informatique. Dans cette exposé, nous répondons aux questions suivantes en dimension 2 :

Quelle est la complexité calculatoire de déterminer si un jeu de tuiles (espace de type fini) possède un point apériodique ? Comment se comportent les espaces de pavages ne possédant aucun point apériodique ?

Nous montrons qu’un espace de pavage 2D sans point apériodique a une structure très forte : il est “équivalent” (presque conjugué) à un espace de pavage 1D, et ce résultat s’applique aux espaces de type fini ou non. Nous en déduisons que le problème de posséder un point apériodique est co-récursivement-énumérable-complet, et que la plupart des propriétés et méthodes propres au cas 1D s’appliquent aux espaces 2D sans point apériodique. La situation en dimension supérieure semble beaucoup moins claire.

Cet exposé est issu d’une collaboration avec Benjamin Hellouin de Menibus et Pascal Vanier.

A generalized lexicographical order on infinite words is defined by choosing for each position a total order on the alphabet. This allows to define generalized Lyndon words. Every word in the free monoid can be factorized in a unique way as a non-increasing factorization of generalized Lyndon words. We give new characterizations of the first and the last factor in this factorization as well as new characterization of generalized Lyndon words. We also give more specific results on two special cases: the classical one and the one arising from the alternating lexicographical order. This is a joint work with Antonio Restivo and Christophe Reutenauer.

Pour une suite $\mathbb{a} = (a_n)_{n≥0}$ à valeurs dans un corps fini $\mathbb{F}_q$, le théorème de Christol établit une équivalence entre $q$-automaticité de $\mathbb{a}$ ($\mathbb{a}$ calculable par un automate) et l’algebricité de la série formelle $f(x) = \sum a_n x^n$. Dans ce travail nous étudierons le nombre d’états de l’automate en fonction des paramètres du polynôme annulateur minimal de $f(x)$.

Andrew Bridy a récemment donne une démonstration du théorème de Christol en utilisant des outils qui proviennent de la géométrie algébrique. Avec cette démonstration il majore le nombre d’états par une borne qui est optimale. Nous obtenons des bornes presque semblables par une démonstration élémentaire, et nous traçons les liens entre notre démonstration et celle de Bridy. Ceci est un travail en commun avec Boris Adamczewski.

In this talk, we introduce a condition number of stochastic mean payoff games. To do so, we interpret these games as feasibility problems over tropically convex cones. In this setting, the condition number is defined as the maximal radius of a ball in Hilbert's projective metric that is included in the (primal or dual) feasible set. We show that this conditioning controls the number of value iterations needed to decide whether a mean payoff game is winning. In particular, we obtain a pseudopolynomial bound for the complexity of value iteration provided that the number of random positions is fixed. We also discuss the implications of these results for convex optimization problems over nonarchimedean fields and present possible directions for future research.

The talk is based on joint works with X. Allamigeon, S. Gaubert, and R. D. Katz.

It is known that Christoffel words are balanced words on two letters alphabet, where these words are exactly the discretization of line segments of rational slope. Christoffel words are considered also in the topic of synchronization of k process by a word on a k letter alphabet with a balance property in each letter. Some applications for k = 2, we retrieve the usual Christoffel words. While for k > 2, the situation is more complicated and lead to the Fraenkel’s conjecture that is an open conjecture for more than 40 years. In this talk, we show some tools that get us close to this conjecture. Another application to this family of words, we define a second order of balance by using some particular matrices, and we prove a recursive relation in constructing them. An interesting property can be deduced from these matrices, allowing us to give a supplementary characteristic for the Fibonnaci sequence. One more application to Christoffel words is discussed in this talk, in fact, by using all the properties of these words, we can apply them on the reconstruction of digital convex polyominoes. Since the boundary word of the digital convex polyominoe is made of Christoffel words with decreasing slopes. Hence we introduce a split operator that respects the decreasing order of the slopes and therefore the convexity is always conserved which is the first step toward this reconstruction.

Given a query q and a relational structure D the enumeration of q over D consists in computing, one element at a time, the set q(D) of all solutions to q on D. The delay is the maximal time between two consecutive output and the preprocessing time is the time needed to produce the first solution. Ideally, we would like to have constant delay enumeration after linear preprocessing. Since this it is not always possible to achieve, we need to add restrictions to the classes of structures and/or queries we consider.

In this talk I will talk about some restrictions for which such algorithms exist: graphs with bounded degree, tree-like structures, conjunctive queries… We will more specifically consider nowhere dense classes of graphs: What are they? Why is this notion relevant? How to make algorithms from these graph properties?

In this talk, I will introduce a notion of higher-order parity automaton which extends the traditional notion of parity tree automaton on infinitary ranked trees to the infinitary simply-typed lambda-calculus. Our main result is that the acceptance of an infinitary lambda-term by a higher-order parity automaton A is decidable, whenever the infinitary lambda-term is generated by a finite and simply-typed lambda-Y-term. The decidability theorem is established by combining ideas coming from automata theory, denotational semantics and infinitary rewriting theory.

You will find the extended abstract of the talk here: https://www.irif.fr/~mellies/papers/higher-order-parity-automata.pdf

In one dimension, an infinite word is said to be recurrent if every prefix occurs at least twice. A straightforward extension of this definition in higher dimensions turns out to be rather unsatisfying. In this talk, we present several notions of recurrence in the multidimensional case. In particular, we are interested in words having the property to be strongly uniformly recurrent: for each direction q, every prefix occurs in that direction (i.e. in positions iq) with bounded gaps. We will provide several constructions of such words and focus on the strongly uniform recurrence in the case of square morphisms.

The computational model of programs over monoids, introduced by Barrington and Thérien in the late 1980s, gives a way to generalise the notion of (classical) recognition through morphisms into monoids in such a way that almost all open questions about the internal structure of the complexity class NC^1 can be reformulated as understanding what languages (and, in fact, even regular languages) can be program-recognised by monoids taken from some given variety of finite monoids. Unfortunately, for the moment, this finite semigroup theoretical approach did not help to prove any new result about the internal structure of NC^1 and, even worse, any attempt to reprove well-known results about this internal structure (like the fact that the language of words over the binary alphabet containing a number of 1s not divisible by some fixed integer greater than 1 is not in AC^0) using techniques stemming from algebraic automata theory failed. In this talk, I shall present the model of programs over monoids, explain how it relates to “small” circuit complexity classes and present some of the contributions I made during my Ph.D. thesis to the understanding of the computational power of programs over monoids, focusing on the well-known varieties of finite monoids DA and J (giving rise to “small” circuit complexity classes well within AC^0). I shall conclude with a word about ongoing work and future research directions.

We consider the problem of passive symbolic learning in the case of deterministic top-down tree transducers (DTOP). The passive learning problem deals with identifying a specific transducer in normal form from a finite set of behaviour examples. This problem is solved in word languages using the RPNI algorithm, that relies heavily on the Myhill-Nerode characterization of a minimal normal form on DFA. Its extensions to word transformations and tree languages follow the same pattern: first, a Myhill-Nerode theorem is identified, then the normal form it induces can be learnt from examples. To adapt this result in tree transducers, the Myhill-Nerode theorem requires that DTOP are considered with an inspection, i.e. an automaton that recognized the domain of the transformation. In its original form, the normalization (minimal earliest compatible normal form) and learning of DTOP is limited to deterministic top-down tree automata as inspections. In this talk, we show the challenges that an extension to regular inspections presents, and present two concurrent ways to deal with them:

1. first, by an extension of the Myhill-Nerode theorem on DTOP to the regular case, by defining a minimal *leftmost* earliest compatible normal form.
2. second, by reducing the problem to top-down domains, by using the regular inspection as a lookahead

The merits of these methods will be discussed for possible extensions of these methods to data trees.

M. B. Levin constructed a real number x such that the first N terms of the sequence b^n x mod 1 for n >= 1 have discrepancy $O((log N)^2/N)$. This is the lowest discrepancy known for this kind of sequences. In this talk, we present Levin's construction in terms of nested perfect necklaces, which are a variant of the classical de Bruijn sequences. For base 2 and the order being a power of 2, we give the exact number of nested perfect necklaces and an explicit method based on matrices to construct each of them.