A rationally dynamically algebraic (RDA) power series is one that arises as (a component of) the solution of a system of differential equations of the form y′=F(y), where F is a vector of rational functions that is defined at y(0). RDA power series subsume algebraic power series and are a proper subclass of differentially algebraic power series (those that satisfy a univariate polynomial-differential equation). We give a combinatorial characterisation of RDA power series in terms of exponential generating functions of regular languages of labelled trees. Motivated by this connection, we define the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata by allowing the transition weights to be rational functions of the tree size. Our main result is that the ordinary generating functions of the formal tree series recognised by differential tree automata are exactly the differentially algebraic power series. The proof of this result establishes a general form of recurrence satisfied by the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. As a corollary we obtain a procedure for determining equality of differential tree automata.

The talk is based on a joint work with Rida Ait El Manssour, Vincent Cheval, and James Worrell and can be found here: https://arxiv.org/abs/2407.08218

Computational problems concerning the orbit of a point under the action of a matrix group occur in numerous subfields of computer science, including complexity theory, program analysis, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and several points and asks questions about the orbit closure of the points under the action of the group, e.g., whether two given orbit closures intersect.

In this talk, I will introduce and motivate several problems involving groups and orbit closures, focusing on computation and determination tasks. In regards to computation, we are given a set of matrices and tasked with computing the defining ideal of the algebraic group generated by those matrices. The determination task, on the other hand, involves starting with a given variety and determining whether and how it can be represented as an algebraic group or an orbit closure. The “how” question often asks whether the underlying group can be topologically generated by s matrices for a given s. The talk is based on several joint works:

(ISSAC 22) https://dl.acm.org/doi/10.1145/3476446.3536172

(Submitted) https://arxiv.org/abs/2407.04626

(POPL25) https://arxiv.org/abs/2407.09154

Joint work with Bharat Adsul (IIT Bombay), Paul Gastin (LMF), Saptarshi Sankar (IIT-B), Shantanu Kulkarni (IIT-B), through papers at CONCUR 2020, LMCS 2020, CONCUR 2022, LICS 2024

We examine the following problem for regular languages of (Mazurkiewicz) traces: given a regular trace language, can it be recognized by a cascade product of very simple localized asynchronous automata — essentially, 2-state reset automata and group automata? This is a trace version of the Krohn-Rhodes theorem, a deep result on languages of finite words, which goes back to the early 1960s.

Solving this problem in the positive (such a cascade product always exists) was surprisingly (?) non-trivial. It involves giving a proper definition of local cascade products of asynchronous (or Zielonka) automata, very much in the spirit of the notion of transducers, and describing an expressively complete fragment of PDL (propositional dynamic logic) for traces.

Specialists of the topic will remember the time stamping mechanism in Zielonka's proof of the equivalence between regularity and asynchronous automata, and the related notion of a gossip automaton, introduced by Mukund and Sohoni. A large part of the proof consists in showing that certain PDL primitives which correspond to the gossip automaton, can be done without.

There are compelling and long-established connections between automata theory and model theory, including Büchi automata and the additive group of real numbers. We say a subset X of the reals is “k-regular” if there is a Büchi automaton that accepts (one of) the base-k representations of every element of X, and rejects the base-k representations of each element in its complement. These sets often exhibit fractal-like behavior–e.g., the Cantor set is 3-regular. In this talk we will discuss the hierarchy of B\“uchi automata in terms of their expressive power–what other automata can we build from a few basic ones and (most of) the classic automata operations? We will unpack the connection between this question and first-order structures on the reals whose definable sets are all recognized by Büchi-automata.

I will present recent work (with Valérie Berthé, Carl-Fredrik Nyberg-Brodda, Dominique Perrin and Karl Petersen) about densities of group languages under ergodic probability measures. Group languages are the rational languages recognized by morphisms onto finite groups, or equivalently recognized by automata where letters act as permutations of the states. I will explain how to obtain a simple formula for the density which holds under some ergodicity condition on the skew product between the group recognizing the language and the support of the probability measure. I will also explain how to describe these minimal components and how they are related with return words. If time permits, I will also briefly touch on our recent efforts, with Valérie Berthé and Dominique Perrin, to extend these techniques to general rational languages.

Combinatorial automata theory can be seen as studying reachability in transformation semigroups. An interesting way of generalising this setting is by lifting it up to reachability in finite semigroups of rational matrices. Here, besides finite automata theory, other areas come into play, for example weighted automata, algebraic number theory, and multilinear algebra. I will explain several nice questions (such as mortality and minimum rank) that transfer from transformation semigroups to finite matrix semigroups. I will also explain the lack of mathematical structure that is brought by certain PSPACE-complete transformation semigroup problems.

Joint work with Louis-Marie DANDO

Two-way automata are natural models of computation. Nevertheless, it was proven in 1959 (both by Jefferson, and by Rabin and Scott) that they are not more powerful than one-way automata.

In the framework of weighted automata, things are more complicated, thus interesting. We focus in this talk on automata where weights are rational numbers. We present a hierarchy of Q-automata: rotating, sweeping and 2-way automata. We show a natural extension of the Kleene-Schützenberger theorem between rotating Q-automata and Hadamard series which are extensions of rational series. Finally, we prove that 2-way Q-automata are not more powerful than rotating Q-automata.

The model, due to Jurdzinski in his PhD thesis 1999 under the direction of Kutylovski, is a finite collection of one-way or two-way deterministic automata working synchronously on the same input and dispatching messages when reaching certain so-called broadcasting states. The input is accepted if a predetermined automaton reaches a final state when it arrives at the right end of the input. The message complexity of the system is the function f(n) which, to every integer, assigns the minimum number of messages required in a run over inputs of length n.

Jurdzinski and Kutylovski, 2002, proved in the one-way case that if the system requires a nonconstant number of messages then it requires at least log(n) messages and claimed a result of the same kind for two-way systems.

I show that when the input is unary, i.e., over an alphabet with a unique letter, the language accepted is rational (or equivalently ultimately periodic) if and only if the number of messages is finite.

In a paper of 1976, Rauzy studied two complexity notions, $\underline{β}$ and $\overline{β}$, for infinite sequences over a finite alphabet. The function $\underline{β}$ is maximum exactly in the Borel normal sequences and $\overline{β}$ is minimum exactly in the sequences that, when added to any Borel normal sequence, the result is also Borel normal. Although the definition of $\underline{β}$ and $\overline{β}$ do not involve finite-state automata, we establish some connections between them and the lower $\underline{\dim}$ and upper $\overline{\dim}$ finite-state dimension (or other equivalent notions like finite-state compression ratio, entropy or cumulative log-loss of finite-state predictors). We show tight lower and upper bounds on $\underline{\dim}$ and $\overline{\dim}$ as functions of $\underline{β}$ and $\overline{β}$, respectively. In particular this implies that sequences with $\overline{\dim}$ zero are exactly the ones that that, when added to any Borel normal sequence, the result is also Borel normal. We also show that the finite-state dimensions $\underline{\dim}$ and~$\overline{\dim}$ are essentially subadditive.

Measuring the informational content of real numbers has been a significant area of inquiry in algorithmic information theory. Finite-state compressibility (or finite-state dimension) of a real number is a value in [0, 1] which quantifies the amount of information/randomness in the real number as measured using finite-state automata. Finite-state dimension is the lower asymptotic ratio of compression achievable on an infinite string using information-lossless finite-state compressors. Interestingly, the finite-state dimension of a real number is also equal to the block Shannon entropy rate of the infinite sequence representing the expansion of the real number in a base b. A line of work, originating from Schnorr and Stimm (1972), has established that a number is Borel normal in base b if and only if its base b expansion has finite-state compressibility equal to 1, i.e., is incompressible. Hence, normal numbers are precisely the class of numbers that are incompressible using finite-state compressors.

Most of the prior research on finite-state dimension has relied on combinatorial methods. In this talk we explore how tools from Fourier analysis can be employed to gain new insights into the compressibility of real numbers and we answer an open question posed by Lutz and Mayordomo.

Absolutely normal numbers, being finite-state incompressible in every base of expansion, are precisely those numbers which have finite-state dimension equal to 1 in every base. At the other extreme, for example, every rational number has 0 finite-state dimension in every base. Generalizing this, Lutz and Mayordomo asked the following question: Does there exist any s strictly between 0 and 1 and a real number r such that r has finite state dimension equal to s in every base?. In this talk we use several tools involving exponential sums and techniques from Schmidt's work in 1960 to construct, for any given s in (0,1], a real number r having finite-state compressibility equal to s in every base. We thereby answer the open question affirmatively.

In description logic, the query entailment problem asks the following question: given an ABox A (i.e. basic finite structure, to be completed), an ontology T (or a TBox, a finite set of constrains), and a request q (= a conjunctive query, = a subgraph), does any structure satisfying the ABox and the ontology necessarily also satisfy the request? In ALC, the basic description logic (which is nothing more than modal logic in disguise), this problem is well understood, as it is known to be ExpTime-complete in combined complexity, and coNP-complete in data complexity (i.e. with TBox and query fixed) [Lutz '08].

However, the exact complexity for S, the extension of ALC where some roles (= binary relations) are specified to be transitive, was not known yet. The status being that the problem is coNExpTime-hard [Eiter et al. '09] and in 2ExpTime [Calvanese et al. '98]. An article of 2010 tried to close the gap in a special case, but sadly contains a technical mistake, which could not be repaired so far [personal communication].

In this seminar, we propose an alternative solution to the problem, that even works in the most general case: we prove that if the entailment does not hold, then there exists a counter-model admitting a representation of exponential size (although being most possibly infinite). Hence, we conclude that the query entailment for S is indeed coNExpTime-complete. The construction of such a counter-model elegantly implies a variant of automata over infinite trees.

Abstract: Automata over finite words are amazing (no need to justify this in the automata seminar). A central reason for their amazingness is the existence of canonical models, which allows for efficient minimization and learning algorithms, as well as for plenty of other theoretical applications. Automata have been extended to operate over richer classes of structures (such as infinite words, trees and graphs), and to define functions using various forms of transducers. However, the theory of these more general automata is often limited, due to the absence of canonical models. In this talk, I will present the subject of my CNRS project: Identifying canonical models for automata over richer classes of structures, with a special focus on automata over infinite words.

Joint work with Shuo Li (U. Winnipeg) and Wolfgang Steiner (IRIF)

Hofstadter's G function is recursively defined via $G(0)=0$ and then $G(n)=n-G(G(n-1))$. Following Hofstadter, a family $(F_k)$ of similar functions is obtained by varying the number $k$ of nested recursive calls in this equation. We present here a few nice properties of these functions. In particular, they can be described via some infinite morphic words generalizing the Fibonacci word. This was crucial for proving that this family is ordered pointwise: for all $k$ and $n$, $F_k(n) \le F_{k+1}(n)$. Moreover, these functions have a simple behavior on well-chosen numerical representations (Zeckendorf decompositions for some Fibonacci-like sequences). Thanks to that, we were also able to estimate the discrepancies for these $F_k$, i.e. the maximal distances between each $F_k$ and its linear equivalent. This whole work was formally proved using the Coq proof assistant (except for a beautiful fractal!) and we will give a gentle introduction to this Coq development.

Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. In this talk, I will present how we can achieve efficient composition of two-way transducers, mainly through the use of Reversible Transducers. Reversible machines are machine that are both deterministic and codeterministic. I will show how any two-way transducers can be made reversible, while being easily composable. I will also show how these results can be extended to the setting of infinite words, which is the dedicated setting for model-checking for example.

We investigate two-player win/lose games over finite graphs. In all generality, these games are concurrent, i.e. at each state of the graph, there is a concurrent interaction between the two players to determine the next state visited. In the special case where, at every state of the graph, there are no real concurrent interaction, i.e. only one player is truly playing, the game is turn-based. Various desirable properties hold on turn-based games, but do not on arbitrary concurrent games; e.g. there exist subgame optimal strategies in all prefix-independent turn-based games, while there do not in very simple prefix-independent concurrent games. A possible way to circumvent this issue is to define a subclass of concurrent games, that is a proper superclass of turn-based games, while enjoying several of their nice properties. The goal of this talk is to introduce such a subclass of concurrent games, namely finitely maximizable games, and to show step by step how we came up with this definition. The novel way that we use to define such a subclass of well-behaving concurrent games constitutes a promising approach for investigating more general concurrent games, such as non-antagonistic two-player games, or even multi-player games.

Well quasi orderings (WQOs) are at the heart of the theory of Well-Structured Systems (WSTS), a class of computational models that brought numerous important advances for the automatic verification of infinite-state systems. Recent developments in this field links the complexity of WQO-based algorithms to ordinal measures of WQOs : the maximal order type, ordinal height and ordinal width.

One main challenge is to compute the ordinal invariants of complex well quasi-orders built from simpler well quasi-orders through classical operation, such as the Cartesian product, and high-order constructions, like the finite words embedding. In my thesis, I computed compositionally the maximal order type of the direct product, the width of the multiset embedding, and the height and width of the multiset ordering. Furthermore, I compute the width of the Cartesian product in restricted cases and studied the ordinal measures of the finite powerset.In the process, I developed several tools and techniques, notably a game-theoretical approach to computing width using the notion of quasi-incomparable families of subsets. To tackle the width of the multiset ordering, I introduced and studied a fourth ordinal invariant, the friendly order type.

In this talk, I will show how logic and automata theory can help research in distributed computing.

I will start with an attempt to use logic to extend standard complexity theory to the distributed setting. It turns out that several classical concepts generalize well, including the polynomial hierarchy (and hence the complexity classes P and NP), the Cook-Levin theorem (which identifies Boolean satisfiability as a complete problem for NP), and Fagin's theorem (which characterizes NP as the problems expressible in existential second-order logic). But perhaps more surprisingly, separating complexity classes becomes easier in the general case: when extended to multiple computers, the polynomial hierarchy is provably infinite, while it remains notoriously open whether the same holds in the case of a single computer.

In the second part of the talk, I will use the previous results to address a central question in distributed computing: which problems are purely local, which problems are inherently global, and which problems lie between these extremes? The idea will be to measure locality using quantifier alternation, the key concept underlying the polynomial hierarchy.

The talk is based on my paper “A LOCAL View of the Polynomial Hierarchy”. - Proceedings version: https://doi.org/10.1145/3662158.3662774 - Full version: https://arxiv.org/abs/2305.09538

Büchi's seminal 1962 paper established the decidability of the monadic second-order (MSO) theory of the structure (Nat; <), and in so doing brought to light the profound connections between mathematical logic and automata theory. This talk presents our recent results on the decidability of expansions (Nat; <, P1, …, Pd) for various unary predicates P1, …, Pd. We focus in particular on predicates of arithmetic origin, such as Pow-k (powers of k) and N-k (k-th powers). The following is a representative sample of the results yielded by our techniques, which combine automata theory, algebra, number theory, dynamical systems, and combinatorics:

- The MSO theory of (Nat; <, Pow-2, Pow-3) is decidable.

- The MSO theory of (Nat; <, Pow-2, Pow-3, Pow-6) is decidable.

- The MSO theory of (Nat; <, Pow-2, Pow-3, Pow-5) is decidable subject to Schanuel's conjecture.

- The MSO theory of (Nat; <, Squares, Pow-4) is decidable.

- The MSO theory of (Nat; <; Squares, Pow-2) is Turing-equivalent to the MSO theory of (Nat; <, S), where S is the unary predicate corresponding to the binary expansion of s = sqrt(2). As s is widely believed to be a weakly normal number, the corresponding MSO theory is in turn expected to be decidable.

The talk will give an overview of our techniques in general, and the automata theory and algebra that enable the above results in particular.

Deterministic automata are often less expressive or at least less succinct than nondeterministic ones, but offer often better algorithmic and closure properties. History-determinism, a limited form of nondeterminism constitutes an appealing middle ground as history-deterministic automata often combine the best of both worlds, e.g., increased expressiveness in comparison to deterministic automata and better algorithmic and closure properties than fully nondeterministic ones.

History-deterministic pushdown automata live up to that promise: their expressiveness lies strictly between that of deterministic and nondeterministic automata while solving games with history-deterministic winning conditions is EXPTIME-complete, while it is undecidable for nondeterministic pushdown automata.

But where there is light, there must be shadow: history-deterministic pushdown automata have poor closure properties and checking whether a pushdown automaton is history-deterministic is undecidable.

To end on a high note, we present several open problems related to history-deterministic pushdown automata.

Based on joint work with Ismaël Jecker, Shibashis Guha and Karoliina Lehtinen.

Querying data sometimes calls for a logical layer between the user and the data to solve issues that arise with distributed datasets, overspecific vocabulary or incompleteness. Existential rules are an expressive knowledge representation language used for this purpose. In the literature, they are often supposed to be in some normal form that simplifies technical developments. Such assumptions are considered to be made without loss of generality as long as all sets of rules can be normalised while preserving entailment. However, an important question is whether the properties that ensure the decidability of reasoning are preserved as well. In this talk, I will start with presenting the chase algorithm, which is used to query data in the presence of existential rules. I will then discuss the impact of a normalisation procedure called atomic decomposition over termination of the chase. This discussion will lead me to present other results related to chase termination of (not so) independent interest.

In this talk, we focus on unary temporal logic over words (UTL). It is known that languages definable in this logic have several equivalent characterizations based on different formalisms. Additionally, it is known that one can decide whether a regular language can be expressed in UTL.

First, I will present these various characterizations. Then, I will introduce a general approach that encompasses all known results and allows us to obtain new ones. This approach relies on the use of an “operator” whose repeated application yields a hierarchy of classes of regular languages. Finally, I will present some results about this new hierarchy, in particular its relationship with the so-called concatenation hierarchy. This is joint work with Thomas Place.

I will present the main results of this joint work with Lia Schütze, available online from arXiv (https://arxiv.org/abs/2310.02847), starting with Rackoff's 1978 upper bound for the coverability problem in vector addition systems, followed by the 2013 breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Wegrzycki on this upper bound, and finally presenting the `ideal' viewpoint on these results and its consequences for various extensions of vector addition systems.

In a paper to appear at ICALP'24 [*], Gallot, Maneth, Nakano and Peyrat show that, given a tree-to-tree function f computed by a macro tree transducer (a natural register-based machine model, which will be recalled in the talk), the following problems are decidable: (1) is height(f(t)) = O(height(t)) ? (2) is height(f(t)) = O(size(t)) ? We sketch a tentative proof of a generalization of (2) by different and arguably simpler means. More precisely, we show that the quantity inf {k | height(f(t)) = O(size(t)^k)} ∈ ℕ∪{+∞} is computable by reduction to ambiguity of (ordinary) tree automata. (Joint work with Paul Gallot and Nathan Lhote, in preparation.) [*] https://arxiv.org/abs/2307.16500

In this talk, I will present a recent result obtained in collaboration with Amina Doumane and Denis Kuperberg on the properties definable in MSO which are bisimulation invariant over finite transition systems. We show that these coincide with mu-calculus-definable properties. This is a variant of a result from Janin and Walukiewicz over general (ie possibly infinite) transition systems [JW96].

Our proof techniques involve developing an algebraic theory of infinite regular trees, in particular establishing on the way that recognizable languages of regular trees coincide (over regular trees) with MSO definable language of trees.

In this talk, we look at the refined understanding of language-logic-algebra inter-play in an algebraic framework (called o-monoids) over countable words. We develop a seamless integration of the block product operation in the countable setting, and generalize well-known decompositional characterizations of FO and some fragments and extensions. We also show that aperiodic o-monoids cannot be decomposed using a finite-basis.

I will first give a quick overview of decidability problems for weighted automata. Then, up to you! I can talk about any of the following topics, we'll vote! - decidability of the Big-O problem for max-plus automata - the many undecidability results via the halting problems of two-counter machines - learnability of weighted automata

Direct Access is the operation of returning, given an index j, the j-th answer of a conjunctive query Q on a given database for some given order on the answers set of Q. While this problem is #P-hard in general (wrt combined complexity), many conjunctive queries are structured enough so that for some lexicographical ordering of their answers, one can have a direct access to the answer of Q that takes polylogarithmic time in the size of the database after polynomial time precomputation. Previous work have precisely characterized the tractable classes and given fine grained lower bounds on the time needed for precomputation depending on the structure of the query. We give a generalization of these tractability results to the case of signed conjunctive queries, that is, conjunctive queries that may contain negative atoms. Our technique is based on solving the ranked access for a class of circuits that can represent relational data. Our result then follows from the fact that the tractable (signed) conjunctive queries can be transformed into polynomial size circuit. We recover the known tractable classes from the literature in the case of positive conjunctive queries using this technique and also discover new island of tractability for signed conjunctive queries. In particular, our result generalizes to the Ranked Access Problem the known tractabilities of counting the number of answers to beta-acyclic negative queries and of deciding whether a negative query with bounded nested-width has an answer. This is join work with Oliver Irwin and appeared at ICDT 2024:

- ArXiv version: https://arxiv.org/abs/2310.15800 - Published version: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.13

In this talk we are interested in the problem of learning linear temporal logic (over finite traces, LTL_f) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is comprehensible for humans. We initiate the study of the computational complexity of the problem. Our main results are hardness results: we show that the LTL_f learning problem is NP-complete for almost all of its fragments, but also hard to approximate within a o(log n) factor in some cases. This motivates the search for efficient heuristics, and highlights the complexity of expressing separating properties in concise natural language.

A question was asked 35 years: can we store an infinite set in a database? Turns out the answer is yes, and for this a set has to be finitely representable. In databases we use logic for querying, and thus finitely represent sets by logical formulas over infinite models. The next question was: what can you ask about such databases? To answer this question we had to go back to the finite world, and thus embedded finite models were born, a mix of finite and the infinite. While theoreticians were happy to talk about AC0 and o-minimality, cell decomposition, and local triviality in the same paper, practitioners asked whether something useful can be built based on these ideas. The 1990s answer was no, computers were too slow, solvers were too immature. But the world doesn’t stand still, and we have witnessed signs of rebirth of this area that at the very least gave us theoreticians lots of fun. In the talk I’ll tell this story and share some thoughts on making finitely representable databases great again.

We study monoidal transducers, transition systems arising as deterministic automata whose transitions also produce outputs in an arbitrary monoid, for instance allowing outputs to commute or to cancel out. In a first part I'll explain how Vilar's algorithm for the active learning à la Angluin of (normal) transducers generalize to monoidal transducers. In a second part I'll then discuss how this is an instance of the categorical framework for minimization and learning of Colcombet, Petrişan and Stabile: the active learning algorithm was obtained by instantiating monoidal transducers in this framework.

This talk focuses on automatic (aka synchronous) relations, defined as the binary relations of finite words that can be recognized by finite-state synchronous automata. We study two orthogonal approaches.

- Graph theoretic properties: we show that given an automatic graph (a graph defined by an automatic relation), the problem of whether the graph can be regularly 2-coloured (meaning that it can be 2-coloured, and for every colour, the set of words having this colour is a regular language) is surprisingly undecidable; this results yields the undecidability of the separation problem of automatic relations by a subclass of recognizable relations.

- Language-theoretic properties: on the contrary, we show that most of the reasonable language-theoretic properties of automatic relations are decidable. We develop an algebraic theory for automatic relations, called “synchronous algebras”, which are to relations as monoids are to languages. The three pillars of algebraic language theory hold in our settings, namely (1) all relations admit a syntactic synchronous algebra, which is finite if and only if the relation is automatic, (2) classes of automatic relations with nice closure properties (called pseudovarieties) are in natural correspondence with pseudovarieties of finite synchronous algebras and (3) the latter are exactly the classes of finite synchronous algebras which can be described by “profinite dependencies”, a generalization of classical profinite equations. Building on these results, we show how algebraic characterizations of pseudovarieties of regular languages can be lifted to the pseudovarieties of synchronous relations that they induce.

The graph-colourability part the talk is based on a joint work with Pablo Barceló and Diego Figueira published at MFCS '23.

We review the different ways tractability is defined in enumeration using as complexity measure total time, incremental time, delay and space. We present the associated complexity classes, typical problems and algorithmic methods.

The focus is on understanding incremental polynomial time and polynomial delay which are the classes containing most problems. In particular we present an attempt to classify which saturation problems naturally in incremental polynomial time are in fact in polynomial delay and give separation and collapses for general classes. We also briefly present low complexity classes and way to completely avoid exhaustive enumeration, through compact representation and approximation of the solution set.

In two-player turn-based stochastic parity games, both players have positional optimal strategies. On the other hand, in two-player concurrent parity games, optimal strategies may not exist and playing (almost-)optimally may require infinite memory. In this talk, I will present how to identify a local condition that ensures the existence of positional optimal strategies for both players; this local condition is satisfied by more than only turn-based games. I will discuss how we have proved this result — by adapting to the concurrent setting techniques used in the turn-based deterministic setting — and what we can say about this local condition.

This is a joint work with my former PhD advisors Patricia Bouyer and Stéphane Le Roux, and it is based on a paper published in CSL 2024.

Description Logics (DLs) are a family of logic-based knowledge representation formalisms with appealing computational properties and various applications at the confluence of artificial intelligence, databases and other areas. In particular, DLs are well-suited for representing and reasoning about ontologies; therefore, they stand as the formal foundations of the Semantic Web. The different DL formalisms that have been proposed in the literature provide us with a wide choice of constructors in the object language. Nevertheless, these are intended to represent only classical, unquestionable knowledge and, therefore, cannot express and cope with the different aspects of uncertainty and vagueness that often appear in everyday life. Examples of these comprise the various guises of exceptions, typicality (and atypicality), approximations and many others, as usually encountered in the different forms of everyday human reasoning. A similar argument can be put forward when moving to the level of entailment, that of the sanctioned conclusions from an ontology. DL systems provide a variety of (standard and non-standard) reasoning services. Still, the underlying notion of entailment remains classical. Therefore, depending on the application one has in mind, DLs inherit most of the criticisms raised in the development of the so-called non-classical logics. In this talk, I make a case for endowing DLs and their associated reasoning services with the ability to cope with defeasibility. I start by introducing the notion of defeasible class subsumption, which allows for the specification of and reasoning about defeasible inheritance. I also show how it can be given an intuitive semantics in terms of preference relations. Next, I show how to take defeasibility to the level of entailment through the notion of rational closure of a defeasible ontology. Of particular interest is the fact that our constructions do not negatively affect the decidability or complexity of reasoning with defeasible inheritance for a wide class of DLs.

Speaker's short CV: Ivan Varzinczak is an associate professor at Université Paris 8. He holds a PhD (2006) in artificial intelligence from Université Paul Sabatier, France. Ivan has co-authored over 75 peer-reviewed publications on logic-based approaches to knowledge representation and reasoning in AI. In 2019 he defended his habilitation at Université d'Artois, France. Ivan is an associate editor of Artificial Intelligence and of the Journal of Artificial Intelligence Research and chairman of the steering committee of the International Workshop on Nonmonotonic Reasoning. In 2022, he served as program chair of the 12th International Symposium on Foundations of Information and Knowledge Systems (FoIKS). He has had several visiting researcher appointments and taught courses and tutorials worldwide, including two courses at ESSLLI and two tutorials at IJCAI.

Ésik and Kuich extended the theory of weighted formal languages to infinite words in 2005. There, automata are matrices over a semiring and Büchi acceptance is an operation over those matrices. We are trying to extend the theory to other acceptance conditions (Muller, generalized Büchi, etc.) and face several challenges. Mainly, the former operator allows for a disjunction of constraints but now we need conjunction.

I will introduce the theory and detail those challenges.

Joint work with Uli Fahrenberg.

Often, a formal language can be described in several ways. The different descriptions bring with them different perspectives. One constraint might appear to be complex by one analysis but simple under another. This talk discusses a few of the classes that have arisen with good motivation in the study of natural languages, with perspectives from algebra and learning theory in addition to the languages and their automata.

Distributed systems are ubiquitous and their implementation is complex and error-prone. In order to check for errors, they can be modeled as systems of communicating automata, where each automaton represents the behavior of an element of the system. In general, verification problems are undecidable in such a model. The use of (under or over) approximations is necessary. This talk presents k-synchronizable systems, which are a subclass of systems of communicating automata, and some results on them.

Dynamic algorithms constitute an established and rich research area. “Dynamic Complexity” refers to a much less known research area, in which dynamic algorithms are specified by formulas of first-order logic. The class of problems for which this is possible is called DynFO.

The talk gives a short introduction to Dynamic Complexity and presents a recent and ongoing line of research that tries to bring Dynamic Complexity closer to Dynamic Algorithms through the study of constant-time parallel dynamic algorithms. It also takes a look at constant-time parallel “static” algorithms.

Automata can be characterized in terms of their expressive power, as well as their learnability, i.e. under what cases a canonical representation can be induced from data. This talk will overview recent insights in the learnability of subclasses of the regular transductions. I will overview polynomial time learning algorithms in a variety of settings, and show how in some cases one can reduce even further in time and space for certain subclasses (those that coincidentally characterize natural language patterns). I will then show how classes of functions can be used to create rigorous experiments testing the learning capacity of sequential neural networks. If there is time I will overview some ongoing work connecting newer neural net varieties to aperiodic transducers.

During my thesis, I studied a subclass of Petri nets called observation Petri nets. The complexity results obtained show that this class is particularly suited for checking parameterized properties, where the parameter is the number of tokens present in the net. Observation Petri nets were introduced for their application to population protocols, a distributed computing model. Population protocols are part of a class of models of concurrent systems in which we are interested in parameterized verification, and in which there are identical agents which synchronize through “simple” communication primitives. I studied other models of this class, like reconfigurable broadcast networks and register protocols and in the future I would like to turn my research towards the analysis of these kinds of distributed systems for which the parameterized problems are not immediately undecidable, broadening the range of formal method techniques used.

Primary key constraints in databases state there can be at most one tuple for every primary key in a given relation. However, these days it is common to have situations where this property cannot be maintained. Databases that violate constraints are called « inconsistent databases ». In particular, if a database violates primary key constraint, it will contain more than one tuple for the same primary key. In this setting, the notion of a repair is defined by picking exactly one tuple for each primary key (maximal consistent subset of the database). A Boolean conjunctive query q is certain for an inconsistent database D if q evaluates to true over all repairs of D. In this context, there is a dichotomy conjecture that states that for a fixed boolean conjunctive query q, testing whether q is certain for an input database D is either polynomial time or coNP-complete.

The conjecture is open in general and has been open for more than two decades. In this talk we will introduce two new algorithms that we have devised, one based on fix-point computation and the other based on bipartite matching. We will also see how these algorithms can be used to prove the dichotomy for the cases that were previously open.

These results were obtained in collaboration with Diego Figueira, Luc Segoufin and Cristina Sirangelo and combine the results that were presented at ICDT 2023 and what will be presented at PODS 2024.

In the study of MSO on graphs, especially on graphs of bounded treewidth, an important tool is MSO transductions. I will show that tool is not only useful, but also somehow canonical: MSO transductions are exactly those graph-to-graph transformations which respect the structure of graphs.

A Timed Automaton is said to be robust if properties (such as reachability) can still be verified despite small perturbations. Our goal in this work is to model perturbations on delays and to quantify them in a function called permissiveness. We present how we compute the maximally permissive strategies to reach a location in a timed automaton.

We will discuss how one may solve modal equations by constructing homomorphisms between graphs. To “solve a modal equation” means: given two modal formulas A and B, to find a syntactic substitution of the propositional variables which renders A and B equivalent. Such a substitution, if it exists, is called a “unifier” of the modal equation A = B, and the problem of deciding whether or not a given equation has a unifier is called the “unifiability” problem. We show that one may construct, for any modal equation E, a relational structure G(E) and a bijection between the set of unifier classes of E and the set of homomorphisms from a fixed sequence of structures to G(E).

Instantiating this construction to the neXt-fragment of Linear Temporal Logic (LTL-X), the unifiability problem for LTL-X becomes equivalent to the following purely graph-theoretic problem. Given a finite edge-colored graph G, decide whether or not G is the homomorphic image, also called “folding”, of a de Bruijn graph B_n for some n. (Here, the de Bruijn graph B_n is the graph underlying the minimal DFA that recognizes the languages A* a A^(n-1) for a in the alphabet A.) We show that this problem is decidable, by giving a complete characterization of the graphs that are foldings of de Bruijn graphs. This then allows us to conclude in particular that the unifiability problem for LTL-X is decidable.

We also apply our method to prove PSPACE-completeness of unifiability for a logic called Alt1, and we formulate a problem about hypergraphs which is equivalent to the unifiability problem for normal modal logic K. The decidability of the latter problem remains open.

This is joint work with Johannes Marti and Michelle Sweering; a preliminary version of part of the work was presented at the workshop UNIF'23 and we are currently working on the full version.

Presheaf automata are presheaves over a fixed directed category. Depending on the choice of the underlying category we obtain different “species” of automata: eg. finite state automata, Petri nets, vector addition systems and, last but not least, various variants of higher dimensional automata. For each such choice, one can define notions of run, language recognized by an automaton, regular and rational languages, bisimulation, determinism, etc. Furthermore, functors between directed categories induce translations between different types of presheaf automata.

Discrete linear dynamical systems (LDS) are a fundamental modelling paradigm in several branches of science, and have been the subject of extensive research for many decades. Within Computer Science, LDS are used, for example, to analyse linear loops and Markov chains, and also arise in areas such as automata theory, differential privacy, control theory, and the study of formal power series, among others.

Perhaps surprisingly, many decision problems concerning LDS (such as reachability of a given hyperplane, known as the Skolem Problem) have been open for many decades. In this talk, we explore the landscape of such problems, focussing in particular on model-checking questions.

In the context of infinite duration games over graphs, a central question is: For which objectives can the existential player always play optimally using positional (memoryless) strategies? In this talk, we characterize omega-regular objectives with this property. Using this characterization, we obtain decidability of half-positionality in polynomial time, get finite-to-infinite and 1-to-2-players lifts, and show the closure under union of prefix-independent half-positional objectives, answering a conjecture by Kopczyński. This is joint work with Pierre Ohlmann.

End of july 2023 Jeff Shallit asked me the following question: assuming that a synchronous automaton (two tapes read simultaneously) recognizes an ordering on the free monoid, is it decidable whether or not this ordering has infinite chains? infinite antichains? and questions of the like. I suspect(ed) that this is not the case but I started to work in the special unary case (the alphabet has a unique letter). I proved that these questions are decidable (it's easy), I characterized the orders that are linear and showed that the equivalence of two linear orders is polynomial (more interesting). I posted it on arxiv on september 19. Then I thought that I should enrich my introduction … and found out that these were (very) old results.

The characterization of linear synchronous orderings on the integers is mentioned in a paper of Liu and Minnes (2009), which refers to a paper of Khoussainov and Rubin (2001) where it is implicit and is obtained as a general result on unary relations (not necessarily orderings). In my talk I will also comment on these results and propose some possible (hopefully genuinely novel!) extensions.

Church’s Problem asks for the construction of a procedure which, given a logical specification φ(I, O) between input ω-strings I and output ω-strings O, determines whether there exists an operator F that implements the specification in the sense that φ(I, F(I)) holds for all inputs I. Büchi and Landweber gave a procedure to solve Church’s problem for MSO specifications and operators computable by finite-state automata. We investigate a generalization of the Church synthesis problem to the continuous time of the non-negative reals. It turns out that in the continuous time there are phenomena which are very different from the canonical discrete time domain of the natural numbers.

Most database management systems use the relational model: data is stored in tables and the SQL query language is used to extract information. Another data model, property graphs, has seen increasing practical use over the last fifteen years.

Most query languages for property graphs are based on the theoretical formalism of Regular Path Queries (RPQs). The query is a regular expression that searches for walks in the graph labeled by words that match the expression.

There is no real consensus on what the correct answer to an RPQ is, or even what the nature of the answer should be. Different real-world languages use different semantics, and these fundamentally differ from the traditional semantics of RPQs used in theory. The core of this talk is about all these differences and their implications.

A seminal paper published in 2012 by Berstel et al. in the Journal of Algebra initiated the systematic study of intersections of recurrent languages and complete bifix codes. One of the main results of this line of research, obtained in 2015 by Berthé et al., states that if F is a uniformly recurrent dendric language (for example, a Sturmian language), then every complete bifix decoding of F is also uniformly recurrent dendric. A delicate part of the proof is showing that the decoding is indeed uniformly recurrent. We introduce a method, relying on the free profinite monoid, giving a new proof of that part, and in fact a significant generalization based on the notion of F-charged bifix code.

Timed languages contain sequences of discrete events (“letters”) separated by real-valued delays, they can be recognized by timed automata, and represent behaviors of various real-time systems. The notion of bandwidth of a timed language defined in a previous paper characterizes the amount of information per time unit, encoded in words of the language observed with some precision ε.

In this paper, we identify three classes of timed automata according to the asymptotics of the bandwidth of their languages with respect to this precision ε: automata are either meager, with an O(1) bandwidth, normal, with a Θ(log (1/ε)) bandwidth, or obese, with Θ(1/ε) bandwidth. We define two structural criteria and prove that they partition timed automata into these 3 classes of bandwidth, implying that there are no intermediate asymptotic classes.

Both criteria are formulated using morphisms from paths of the timed automaton to some finite monoids extending Puri's orbit graphs, and the proofs are based on Simon's factorization forest theorem.

Joint work with A.Degorre, C.Dima, B. Jacobo Inclán

We will introduce the new graph parameter, twin-width, and present some of its structural and algorithmic properties. One of them is that on graphs of bounded twin-width, one can efficiently solve many different problems, in particular those that correspond to a FO formula.

While the twin-width of several graph classes is well known, we will show that determining whether an n-vertex graph has twin-width at most 4 is NP-complete, and that it requires time 2^Ω(n/log n) under ETH.

This talk is based on joint work with Pierre Bergé and Édouard Bonnet.

Given two finite automata A1, A2, recognising languages L1, L2, respectively, the state complexity of union (or intersection, or complement, etc.) is how many states (in terms of the number of states in A1, A2) may be needed in the worst case for an automaton that recognises L1 union L2 (or L1 intersect L2, or the complement of L1, etc.). The state complexity of complementing unambiguous finite automata has long been open, and as late as 2015 Colcombet asked whether unambiguous automata can be complemented with a polynomial blowup. I will report on progress on this question in recent years, both in terms of lower and upper bounds. For the currently best lower bound, techniques from communication complexity play an essential role.

Previous work reduces the problem of deciding whether a weighted finite automaton (WFA) over a field is equivalent to a sequential, respectively, unambiguous, WFA to the computation of the linear hull. The linear hull is the topological closure of the reachability set in a certain linear version of the Zariski topology. We discuss an algorithm to compute the linear hull that works essentially entirely in the realm of linear algebra (i.e., without first resorting to the computation of the finer Zariski topology). Further, we show how this leads to double-exponential bounds on the size of the linear hull.

This talk is on joint work with J. Bell.

Joint work with Nadime Francis, Amélie Gheerbrant, Paolo Guagliardo, Leonid Libkin, Victor Marsault, Wim Martens, Filip Murlak, Liat Peterfreund and Domagoj Vrgoč The development of practical query languages for graph databases runs well ahead of the underlying theory. The ISO committee in charge of database query languages is currently developing a new standard called Graph Query Language (GQL), the main component of which is the pattern matching facility. In many aspects, it goes well beyond RPQs, CRPQs, and similar queries on which the research community has focused for years. In this talk, I will present our distillation of the lengthy standard into a simple Graph Pattern Calculus (GPC) that reflects all the key pattern matching features of GQL.

Given a metric over words, define the distance between two transducers with identical domain as the supremum of the distances of their respective outputs over all inputs. This is a useful generalization for comparing transducers that goes beyond the equivalence problem. Two transducers are said to be close (resp. k-close) if their distance is finite (resp. at most k). We will discuss the decidability of the problem that asks whether two given transducers are close (resp. k-close), for common edit distances.

This is a joint work with Amaldev Manuel (IIT Goa) and Saina Sunny (IIT Goa).

Guarded tuple-generating dependencies (GTGDs) are a natural extension of description logics and referential constraints. It has long been known that queries over GTGDs can be answered by a variant of the chase —a quintessential technique for reasoning with dependencies. However, there has been little work on concrete algorithms and even less on implementation. To address this gap, we revisit Datalog rewriting approaches to query answering, where GTGDs are transformed to a Datalog program that entails the same base facts on each base instance. In our work, we show that the rewriting can be seen as containing “shortcut” rules that circumvent certain chase steps, we present several algorithms that compute the rewriting by simulating specific types of chase steps, and we discuss important implementation issues. Finally, we show empirically that our techniques can process complex GTGDs derived from synthetic and real benchmarks and are thus suitable for practical use.

In recent years we have witnessed an unprecedented confluence of methods from discrete and continuous mathematics, especially in subjects having to do with logic and topology. One can cite fields such as continuous model theory, homotopy type theory and, most relevant to this talk, combinatorial limits. The latter have started from the notion of graphons and have been generalised to other contexts, including the very general Stone pairings. In this subject one looks at uncountable limits of a countable sequence of finite objects, with various logical properties that carry through. In the context of first order logic, one can think of Los’s theorem for ultraproducts, but various other transfer theorems have been obtained in other contexts. In this talk we shall review some of these notions and then connect them with the study of abstract logics through new satisfaction relations, and the comparison between such logics using Chu transforms.

Free profinite monoids are compact totally disconnected monoids obtained in a natural way by “completing” free monoids, roughly similar to how Q is obtained from R. Inside free profinite monoids, various combinatorial or algebraic statements about languages admit topological counterparts. A well-known example of this is the topological characterization of regular languages: a language is regular if and only if its topological closure in the free profinite monoid is open. A second, much subtler example is the correspondence with symbolic dynamics discovered by Almeida in the late 2000s. Almeida showed that minimal shift spaces can be represented inside free profinite monoids as regular J-classes.

In the first part of the talk, I will present basic concepts related with free profinite monoids and survey some key results, including the connections with regular languages and with symbolic dynamics. In the second part, I will explain how free profinite monoids can be used in a practical way to study dynamical systems defined by primitive substitutions. More precisely, I will explain how Almeida's representation produces easy-to-compute numerical invariants for these systems.

This talk is about winning strategies in Markov decision processes and stochastic games and is aimed at a general computer science audience. We start by recalling some of the basic notions in game theory, such as values, strategies, and the memory requirements of optimal and ε-optimal strategies. We will describe a set of recent advances on strategy complexity of verification-centered objectives, such as subclasses of parity objectives, in terms of parameters such as the cardinality of the state space, branching factor of the transition function, and whether the game is concurrent or turn-based.

This talk is about the identification of ω-automata from sets of positive and negative ultimately periodic example words. We'll recap the core mechanisms underlying learning algorithms for deterministic finite automata, then illustrate the difficulties one faces in extending these approaches to deterministic ω-automata and finally, we'll discuss a polynomial time algorithm for constructing a deterministic parity automata (DPA) from a given set of positive and negative ultimately periodic example words. This is joint work with Christof Löding. The talk is aimed at a general computer science audience.

Ontology-mediated query answering (OMQA) is a promising approach to data access and integration that has been actively studied in the knowledge representation and database communities for more than a decade. The vast majority of work on OMQA focuses on conjunctive queries, whereas more expressive queries that feature counting or other forms of aggregation remain largely unexplored. We introduce a general form of counting conjunctive query (CCQ), relate it to previous proposals, and study the complexity of answering such queries in the presence of ontologies expressed in the description logic ALCHI or its sublogics. As the general case of CCQ answering is intractable and often of high complexity over such ontologies, we consider two practically relevant restrictions, namely rooted CCQs and Boolean atomic CCQs, for which we establish improved complexity bounds.

Nous revisitons le problème de la réduction des machines de Mealy incomplètement spécifiées avec la synthèse réactive en tête. Nous proposons deux techniques : la première est inspirée de l’outil MeMin et résout le problème de minimisation, la seconde est une nouvelle approche dérivée des réductions basées sur la simulation mais ne garantit pas forcément une machine minimale. Nous soutenons cependant qu’elle offre un assez bon compromis entre la taille de la machine résultante et les performances. Les méthodes proposées sont comparées à MeMin sur une large collection de cas de test composés d’instances bien connues ainsi que de nouvelles instances.

In his article “Teaching Concurrency” (L. Lamport. Teaching concurrency. ACM SIGACT News Distrib. Com- put. Column 40(1), 58-62 (2009)) Lesely Lamport presents a very short program (see below) and challenges the reader to find an invariance with which the program's correctness can be proved. Here I reproduce the program.

`` 1. x[i] := 1; 2. y[i] := x[(i − 1) mod N] ``

Here N is the number of processes, and p0, . . . , pN−1 are the processes. Process pi writes on register x[i] and all other processes can read it. The registers are serial. The invariant should be good enough to prove the following statement:

After every process has stopped executing its simple protocol, 
   at least one process pi has set y[i] = 1. 

Try to find an invariant and prove this statement. This algorithm will serve to discuss the notion of invariants and to describe a method that can help in developing invariants for more sophisticated algorithms. We will also discuss the question ``what is a state'' (which is relevant to the notion of invariance of course).

Two finite words u and v are called abelian equivalent if each letter of the alphabet occurs the same number of times in both u and v. The abelian subshift A_x of an infinite word x is the set of words y such that, for each factor u of y, there exists a factor v of x such that u and v are abelian equivalent. The notion of an abelian subshift gives a new characterization of Sturmian words: among binary uniformly recurrent words, Sturmian words are exactly those words for which A_x equals the subshift \Omega_x generated by x. In this talk, we are going to discuss general properties of abelian subshifts of binary words, as well as possible extensions of the property A_x =\Omega_x to the non-binary alphabets.

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. In this talk, I will present the extension of the classical Parikh automaton framework onto infinite inputs: We will analyse reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words, and study their expressiveness, their closure properties, and the complexity of the related verification problems.

The growing amount of data collected by sensors or generated by human interaction has led to an increasing use of graph databases, an efficient model for representing intricate data. Techniques to keep track of the history of computations applied to the data inside classical relational database systems are also topical because of their application to enforce Data Protection Regulations (e.g., GDPR). Our research work mixes the two by considering a semiring-based provenance model for navigational queries over graph databases. In the first part, we will focus on the model itself by introducing a toolkit of provenance-aware algorithms, each targeting specific properties of the semiring of use. We notably introduce a new method based on lattice theory permitting an efficient provenance computation for complex graph queries. We propose an open-source implementation of the above-mentioned algorithms, and we conduct an experimental study over real transportation networks of large size, witnessing the practical efficiency of our approach in practical scenarios. From the richness of the literature, we notably obtain a lower bound for the complexity of the full provenance computation in our setting. We finally consider how this framework is positioned compared to other provenance models such as the semiring-based Datalog provenance model. We make explicit how the methods we applied for graph databases can be extended to Datalog queries, and we show how they can be seen as an extension of the semi-naïve evaluation strategy. To leverage this fact, we extend the capabilities of Soufflé, a state-of-the-art Datalog solver, to design an efficient provenance-aware Datalog evaluator. Experimental results based on our open-source implementation entail the fact this approach stays competitive with dedicated graph solutions, despite being more general. In a final round, we discuss some research ideas for improving the model, and state open questions raised by this work.

This is joint work with Silviu Maniu and Pierre Senellart.

I will give a gentle introduction to higher-dimensional automata (HDAs) and their language theory. HDAs have been introduced some 30 years ago as a model for non-interleaving concurrency which generalizes, for example, Petri nets while retaining some automata-theoretic intuition. They have been studied mostly for their operational and geometric aspects and are one of the original motivations for directed algebraic topology. In a series of papers we have recently started to work on the language theory of HDAs: we have introduced languages of HDAs as weak sets of interval pomsets with interfaces and shown that HDAs satisfy Kleene and Myhill-Nerode type theorems. The picture which emerges is that, even though things can sometimes get hairy in proofs, HDAs have a rather pleasant language theory, a fact which should be useful in the theory of non-interleaving concurrency and its applications. Joint work with Christian Johansen, Georg Struth, and Krzysztof Ziemiański

A context-free language is inherently ambiguous if any grammar recognizing it is ambiguous, i.e. there is a word that is generated in two different ways. Deciding the inherent ambiguity of a context-free language is a difficult problem, undecidable in general. The first examples of inherently ambiguous languages were discovered in the 1960s, using iteration techniques on derivation trees. They belonged to a particular subfamily of context-free languages, called bounded context-free languages.

    Although they made it possible to prove the inherent ambiguity of several languages, as for example the language L = a^n b^m c^p with n=m or m=p, iteration techniques are still very laborious to implement, are very specific to the studied language, and seem even sometimes unadapted. For instance, the relative simplicity of the proof of inherent ambiguity of L completely collapses by replacing the constraint "n=m or m=p" by "n≠m or m≠p". 
    In this talk, I will present two useful criteria based on generating series to prove easily the inherent ambiguity of some bounded context-free languages. These languages, which have a rational generating series, resisted both the classical iteration techniques developed in the 1960’s and the analytic methods introduced by Philippe Flajolet in 1987.

Schensted a montré comment on insère un nouvel élément dans un tableau de Young. Cet algorithme consiste à insérer cet élément dans la ligne (=suite non décroissante d’entiers) du bas du tableau puis à itérer vers le haut du tableau si un élément est chassé de la ligne au cours de l'exécution. On s’intéresse ici à l’action du monoide libre sur une seule ligne sans poursuivre sur les lignes supérieures (si un élément est chassé il est perdu). Pour rappel dans un séminaire de Mai 2022 Christophe Reutenauer s’était intéressé à l’action sur les colonnes. Dans ce dernier cas le monoide de transition, qu'il appelle stylique, est fini (il y a un nombre fini de colonnes pour une alphabet donné) alors que l’action sur les lignes définit un monoide infini, le monoide grammique.

La relation qui met ensemble deux mots qui ont la même action sur l’ensemble des lignes est une congruence plus grossière que le congruence plaxique (celle des tableaux de Young) et elle est décidable. Je considère le cas d’un alphabet à 3 lettres pour lequel elle est obtenue en ajoutant aux règles de Knuth une seule nouvelle règle très simple. Je m’aventurerai à proposer un conjecture sur les alphabets à plus de 3 lettres et en passant je parlerai des (très jolis et peut-être utiles) travaux de Okninski et al. sur les algèbres de monoids plaxiques.

—

Schensted showed how to insert a new element in a Young tableau. It consists of inserting this element in the bottom row (row= nondecreasing sequence of elements) and iterating the process further up in case an element of the bottom row is bumped. I am interested in the action of the free monoid which assigns to a row, the row obtainded by Schensted insertion, but ignoring the possible bumped element. Christophe Reutenauer considered in his May seminar the action on the set of columns. His (stylic) monoid is finite (there exist finitely many columns for a fixed alphabet) while mine, the grammic monoid, is infinite.

The relation between two words having the same action on the set of rows is a congruence which is coarser than the plactic congruence (that defining the Young tableaux) and decidable. I consider the case of a 3 letter alphabet for which the congreunce is generated by the Knuth rules plus a unique simple rule. I will risk a conjecture for alphabets of more than 3 letters and say a few words on the (very nice and possibly related) works of Okninski and al. on the algebras of the plactic monoids.

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.

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. Two of the most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e., satisfiability is undecidable for both logics. We settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is \Sigma_1^1-complete and HyperCTL* satisfiability is \Sigma_1^2-complete. To prove \Sigma_1^2 membership for HyperCTL*, we prove that every satisfiable HyperCTL* formula has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. This is joint work with Louwe B. Kuijer, Patrick Totzke and Martin Zimmermann.

Regular languages can be actively learned with membership and equivalence queries in polynomial time. The learning algorithm, called the L^* algorithm, constructs iteratively the right congruence relation of a given regular language L, and returns the minimal DFA recognizing L. The L^* algorithm has been adapted to various types of automata: tree automata, weighted automata, nominal automata. However, an extension to infinite-word automata has been elusive. In this talk, I will present an extension of the active learning framework, in which the algorithm can ask syntactic queries about the automaton representing a given infinite-word language.

First, I will discuss why extending L^*, which asks only semantic queries, to infinite-words languages is difficult. Next, I will present an alternative approach; instead of learning some automaton for a hidden language, we assume that there is a hidden automaton and the algorithm is supposed to learn an equivalent automaton. In this approach, the learning algorithm is allowed to ask standard semantic queries (membership and equivalence) and loop-index queries regarding the structure of the hidden automaton. These queries do not reveal the full structure of the automaton and hence do not trivialize the learning task.

In the extended framework, there are polynomial-time learning algorithms for various types of infinite-word automata: deterministic Buechi automata, LimSup-automata, deterministic parity automata and limit-average automata.

Finally, the idea to incorporate syntactic queries can be adapted to the pushdown framework; I will briefly discuss the learning algorithm for deterministic visibly pushdown automata.

To the classical way of playing in finite extensive-form games, we add a bidding mechanism: at each node of the game tree, each non-controlling player bids some amount of utility for one subgame. When the controller chooses one subgame, the utilities that were bid for this subgame are transferred to her.

The notion of subgame perfect equilibrium (SPE) is naturally extended to these bidding games, and they always always exist like in the classical games. They also enjoy new properties: - If the game tree is binary-branching, payoff-sum-maximizing SPE always exist. - If the game involves only two players, all SPE are payoff-sum-maximizing with the same payoff-tuple, which is called the bidding value of the game. - This value is computable, whereas SPE payoff-tuples are not even continuous in classical games.

This is joint work with Valentin Goranko

We wish to identify the queries that can be solved with close to optimal time guarantees over relational databases. Computing all query answers requires at least linear time before the first answer (to read the input and determine the answer's existence), and then we must allow enough time to print all answers (which may be many). Thus, we aspire to achieve linear preprocessing time and constant or logarithmic time per answer. A known dichotomy classifies Conjunctive Queries into those that admit such enumeration and those that do not: the main difficulty of query answering is joining tables, which can be done efficiently if and only if the join query is acyclic. However, the join query usually does not appear in a vacuum; for example, it may be part of a larger query, or it may be applied to a database with dependencies. We show how to use this context for more efficient computation and study how the complexity changes in these settings. Next, we aspire for an even more powerful solution for query answering: a structure that simulates an array containing the query answers. Such a structure can be used for example to enumerate all answers in a statistically meaningful order or to efficiently compute a boxplot of query answers. We call this simulation random access and study for which queries random access can be achieved with near-optimal guarantees. Our results are accompanied by conditional lower bounds showing that our algorithms can be applied to all tractable queries in some cases. Among our results, we show that a union of tractable Conjunctive Queries may be intractable w.r.t. random access, but a union of intractable Conjunctive Queries may be tractable w.r.t. enumeration.

We present a model of games with imperfect information that features explicit communication actions, by which a player can send her entire observation history to another player. Such full-information protocols are common in asynchronous distributed systems, here we consider a synchronous setting and cast it as a game on word-automatic trees. The information structures arising from such games are again automatic trees, but their branching degree can be unbounded, and then the synthesis problem becomes challenging. We present a method for constructing a finite bisimulation quotient for a representative subcase, which solves the problem effectively. The construction is a guess; if time allows, we will speculate on how to find such quotients systematically.

The talk is based on joint work (in progress) with Laurent Doyen; a part of the material is presented in [D. Berwanger, L. Doyen (2019): Observation and distinction in infinite games, https://arxiv.org/abs/1809.05978]

We give an algebraic characterisation of first-order logic with the neighbour relation, on finite words. For this, we consider languages of finite words over alphabets with an involution on them. The natural algebras for such languages are involution semigroups. To characterise the logic, we define a special kind of semidirect product of involution semigroups, called the locally hermitian product. The characterisation theorem for FO with neighbour states that a language is definable in the logic if and only if it is recognised by a locally hermitian product of an aperiodic commutative involution semigroup, and a locally trivial involution semigroup. We then define the notion of involution varieties of languages, namely classes of languages closed under Boolean operations, quotients, involution, and inverse images of involutory morphisms. An Eilenberg-type correspondence is established between involution varieties of languages and pseudovarieties of involution semigroups. This is joint work with Dhruv Nevatia.

We show that the existence of a first-order formula separating two monadic second order formulas over countable ordinal words is decidable. This extends the work of Henckell and Almeida on finite words, and of Place and Zeitoun on $\omega$-words. This is a joint work with Rémi Morvan and Sam van Gool

The topic of this talk is, once again, the transformation of rational expressions into finite automata, a much laboured subject. In our last joint work, Sylvain Lombardy and I take a shifted perspective on the derivation of expressions method (due to Brzozowski and Antimirov) which reveals that there is indeed no derivation involved. This broadens the scope of the method to expressions over non free monoids.

Automata and games over infinite words are widely used in verification and synthesis of reactive systems. Several different kinds of acceptance conditions can be used in these systems, which may differ in their complexity and expressive power. For their simplicity and usefulness, parity conditions are of special relevance. However, in many applications such as LTL-synthesis, the automata that are obtained in the first place use more complex conditions (Muller conditions) and we have to transform them in parity ones.

In this talk, I will present a construction that takes as input a Muller automaton and transforms it into a parity automaton in an optimal way. More precisely, the resulting parity automaton has minimal size and uses a minimal number of priorities among those automata that admit a locally bijective morphism to the original Muller automaton. This transformation and the optimality result can also be applied to games and other types of transition systems.

We show two applications: an improvement on the determinisation of Büchi automata into deterministic parity automata and characterisations of automata that admit parity, Rabin or Streett conditions in top of them.

This is joint work with Thomas Colcombet and Nathanaël Fijalkow, and it will appear at ICALP 2021.

We study tree-to-tree transformations that can be defined in first-order logic or monadic second-order logic. We prove a decomposition theorem, which shows that every transformation can be obtained from prime transformations, such as tree-to-tree homomorphisms or pre-order traversal, by using combinators such as function composition.

We study the dynamic membership problem for regular languages: fix a language L, read a word w, build in time O(|w|) a data structure indicating if w is in L, and maintain this structure efficiently under substitution edits on w. We consider this problem on the unit cost RAM model with logarithmic world length, where the problem always has a solution in O(log |w| / log log |w|). We show that the problem is in O(log log |w|) for languages in an algebraically-defined class QSG, and that it is in O(1) for another class QLZG. We show that languages not in QSG admit a reduction from the prefix problem for a cyclic group, so that they require \Omega(log n/ log log n) operations in the worst case; and that QSG languages not in QLZG admit a reduction from the prefix problem for the monoid U_1, which we conjecture cannot be maintained in O(1). This yields a conditional trichotomy. We also investigate intermediate cases between O(1) and O(log log n). Our results are shown via the dynamic word problem for monoids and semigroups, for which we also give a classification. We thus solve open problems of the paper of Skovbjerg Frandsen, Miltersen, and Skyum on the dynamic word problem, and additionally cover regular languages.

The concept of bounded expansion provides a robust way to capture sparse graph classes with interesting algorithmic properties. Most notably, every problem definable in first-order logic can be solved in linear time on bounded expansion graph classes. First-order interpretations and transductions of sparse graph classes lead to more general, dense graph classes that seem to inherit many of the nice algorithmic properties of their sparse counterparts.

The leading question of this talk is: “How can we generalize the beautiful existing algorithmic results of sparse graphs to dense graphs?” We start with an overview over sparse and dense graph classes and then introduce lacon- and shrub-decompositions. We show that dense graph classes can be exactly characterized by having a sparse lacon- or shrub-decoposition. If one could efficiently compute such a decomposition then one could solve every problem definable in first-order logic in linear time on these classes.

The monadic second order theory of a linear order (A,<) can be understood using the first order structure M(A,<) = (P(A),⊆,<) where P(A) is the powerset of A, ⊆ is the usual set-theoretic inclusion, and < is the ordering of (A,<) given on singleton subsets. By the pseudofinite monadic second order theory of linear order we mean the intersection of the first order theories of the structures M(A,<) across all finite linear orders (A,<).

I will present an explicit axiomatisation of this shared theory, and characterise the non-standard completions (i.e. those admitting infinite models) in terms of residue functions. I will then talk about a connection with profinite monoids using extended Stone duality. In particular I will discuss a special case of a theorem due to Gehrke, Grigorieff, and Pin saying that the free profinite monoid on one generator is the extended Stone dual of the Boolean algebra of regular languages over a singleton alphabet (together with the binary operation of concatenation).

Let n be a positive integer and M a set of rational n×n-matrices such that M generates a finite multiplicative semigroup. We show that any matrix in the semigroup is a product of matrices in M whose length is at most O(n2logn), where g(n) is the maximum order of finite groups over rational n×n-matrices. This result implies algorithms with an elementary running time for deciding finiteness of weighted automata over the rationals and for deciding reachability in affine integer vector addition systems with states with the finite monoid property.

In this talk we are going to prove the decidability of several properties on the dynamics of additive cellular automata over finite abelian groups. In the first part, we prove the results for a restricted class of additive CA, namely the linear CA by using a new ‘ad hoc’ result from algebra. In the second part, we show how to lift the all the properties to the whole class of additive CA over finite abelian groups.

In this talk, I discuss the time-bounded reachability problem for continuous-time Markov decision processes. I show that the problem is decidable subject to Schanuel’s conjecture. The decision procedure relies on the structure of optimal policies and the conditional decidability (under Schanuel’s conjecture) of the theory of reals extended with exponential and trigonometric functions over bounded domains. I further discuss that any unconditional decidability result would imply unconditional decidability of the bounded continuous Skolem problem, or equivalently, the problem of checking if an exponential polynomial has a non-tangential zero in a bounded interval. The latter problems are also decidable subject to Schanuel’s conjecture but finding unconditional decision procedures remain longstanding open problems. Time permitting, I can also discuss some algorithmic approximate computations using Lyapunov theory of dynamical systems. This talk is based on an ICALP 2020 paper joint with Rupak Majumdar and Mahmoud Salamati at MPI-SWS.

I will present FO+, a restriction of first-order logic where letters are required to appear positively, and the alphabet is partially ordered, for instance by inclusion order if letters are sets of atoms. Restricting predicates to appear positively is very natural when considering for instance logics with fixed points, or various extensions of regular languages. Here we will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters, but can every FO-definable monotone language be defined in FO+ ? On general structures, Lyndon's theorem gives such a syntax/semantics equivalence for monotone first-order formulas, but it is known to fail on finite structures. We will see that it also fails on finite words, giving a much simpler proof for the failure of Lyndon's theorem on finite structures. Finally we will investigate whether FO+-definability is decidable for regular languages on ordered alphabets.

The talk is based on joint work with Thomas Colcombet. We initiate a study of the expressive power of tree algebras, and more generally infinitely sorted algebras, based on their asymptotic complexity.

Tree algebras in many of their forms, such as clones, hyperclones, operads, etc, as well as other kind of algebras, are infinitely sorted: the carrier is a multi sorted set indexed by a parameter that can be interpreted as the number of variables or hole types. Finite such algebras - meaning when all sorts are finite - can be classified depending on the asymptotic size of the carrier sets as function of the parameter, that we call the complexity of the algebra. This naturally defines the notions of algebras of bounded, linear, polynomial, exponential or doubly exponential complexity…

Our main result precisely characterizes the tree algebras of bounded complexity based on the languages that they recognize as Boolean closures of simple languages. Along the way, we prove that such algebras that are syntactic are exactly those in which, as soon as there are sufficiently many variables, the elements are invariant under permutation of the variables.

We consider the decidability of state-to-state reachability in linear time-invariant control systems over continuous time. We analyze this problem with respect to the allowable control sets, which are assumed to be the image under a linear map of the unit hypercube (\emph{i.e.} zonotopes). This naturally models bounded (sometimes called saturated) controls. Decidability of the version of the reachability problem in which control sets are affine subspaces of R^n is a fundamental result in control theory. We obtain some decidability results in low dimension or when the spectrum of the matrix is special. We also obtain some decidability conditioned on the decidability of the first-order theory of the reals with the exponential function. Finally we obtain a hardness result for a mid generalization of the problem. In this case, we show that the problem is at least as hard as the Continuous Positivity problem if the control set is a singleton, or the Nontangential Continuous Positivity problem if the control set is $[-1,1]$.

he talk will be based on joint work with Lê Thành Dũng (Tito) Nguyễn.

This work is part of an exploration of the expressiveness of the simply-typed λ-calculus (STLC) and related substructural variants (linear, affine, planar) using Church encodings of datatypes. More specifically, we are interested in the connection with automata theory for string transductions and languages.

I will first introduce the setting and motivate the problems using Hillebrand and Kanellakis' result stating that the classes of STLC-definable and regular languages coincide. I will then focus on a result stating that star-free languages correspond exactly to those obtained in a non-commutative refinement of STLC based on linear logic. I will sketch an alternative proof of this result using a semantic evaluation argument and discuss related work-in-progress concerning characterizations in the non-commutative λ-calculus of first-order regular string transductions using planar reversible 2DFTs and tree-walking automata.

(the results I will present are based on https://hal.archives-ouvertes.fr/hal-02476219 and http://nguyentito.eu/2021-01-links.pdf)

A probabilistic context-free grammar (PCFG) defines a distribution over trees: each (finite) tree has some probability of being generated. We consider the following game: a (secret) tree is generated by a PCFG. The PCFG is known and given as input, and the goal is to find the tree. How many equality queries are needed? We'll discuss algorithms for solving this problem, using either enumeration or sampling, and applications to program synthesis.

Joint (ongoing) work with Pierre Ohlmann and Guillaume Lagarde.

A numeration system associates to each element of a given set a finite word. The best known of these systems is the decimal system, which associates each positive integer with a word of the alphabet $\{0,1,\ldots,9\}$. This idea can easily be generalised to other positive integers as base such as the binary system or the hexadecimal system.

The first part deals with signed numeration systems. In these systems, we add digits to the alphabet such as the digit $-1$ in the binary system. Under certain conditions, on consecutive digits, we obtain unique representations. This is related to the concept of abstract numeration systems. We will study the shift and odometer from the point of view of dynamical systems.

Digital restrictions also play an important role in another numeration system: the Zeckendorf expansion. This is an example of the larger class of numeration systems based on linear recurrent sequences, which we discuss in the second part. A way to analyse a numeration system is to examine functions operating on the digital representation. The most famous of these functions is the sum-of-digits function and we investigate it from an analytic point of view.

In the expansion of a randomly chosen real, we expect each block of digits to occur with the same frequency. This leads to the concept of normal numbers and the related notion of uniformly distributed sequences. In the last part, we adopt a probabilistic point of view and construct normal numbers and uniformly distributed sequences related to numeration systems.

The design of SQL is based on a three-valued logic (3VL), rather than the usual two-valued Boolean logic. This 3VL accommodates the additional truth value “unknown” for handling nulls, representing missing values. This third truth value is viewed as indispensable for SQL expressiveness, but is at the same time being criticized a lot for leading to unintuitive behavior of queries and for being a source of programmer mistakes.

In a joint work with Leonid Libkin, we show that, contrary to the widely held view, SQL could have been designed based on the standard two-valued logic, without any loss of expressiveness and without giving up nulls. We show that conflating unknown, resulting from conditions referring to nulls, with false leads to an equally expressive version of SQL. Queries written under the two-valued semantics can be efficiently translated into the standard SQL and thus executed on any existing RDBMS. Our results cover the core of the SQL 1999 Standard, including SELECT-FROM-WHERE-GROUP BY-HAVING queries extended with subqueries and IN/EXISTS/ANY/ALL conditions, and recursive queries. In addition, we show that no other many-valued logic for treating nulls could have possibly led to a more expressive language.

Successor-invariant first-order logic is the extension of first-order logic where one has access to an additional successor relation on the elements of the structure, as long as the validity of formulas doesn't depend on the choice of a particular successor. It has been shown by Rossman that this formalism allows to express properties that are not FO-definable. However, his separating example involves dense classes of structures, and the expressive power of successor-invariant first-order logic is an open question for sparse classes of structures. We prove that when the degree is bounded, successor-invariant first-order logic is no more expressive than first-order logic.

It is shown that if a pushdown system is bisimulation equivalent to a finite system, there is already such a finite system whose size is elementary in the description size of the pushdown system. As a consequence, it is elementarily decidable if a pushdown system is bisimulation-finite. This is joint work with Pawel Parys.

In this talk we present a categorical approach to learning automata over words, in the sense of the $L^*$-algorithm of Angluin. This yields a new generic $L^*$-like algorithm which can be instantiated for learning deterministic automata, automata weighted over fields, as well as subsequential transducers. The generic nature of our algorithm is obtained by adopting an approach in which automata are simply functors from a particular category representing words to a “computation category”. We establish that the sufficient properties for yielding the existence of minimal automata in combination with some additional hypotheses relative to termination ensure the correctness of our generic algorithm.

This is joint work with Thomas Colcombet and Riccardo Stabile.

Register automata are finite automata equipped with a finite set of registers in which they can store data, i.e. elements from an infinite alphabet, and compare this data for equality. They provide a simple formalism to specify the behaviour of reactive systems operating data. Initially defined with the equality predicate only, they can be extended to allow for comparison of data with regards to a linear order, like (N,<) or (Q,<). We study the synthesis problem for those specifications. To that end, we extend the classical Church synthesis game to infinite alphabets: two players, Adam and Eve, alternately pick some data, and Eve wins whenever their interaction satisfies the specification, which is a language of infinite words over infinite data alphabet. Unfortunately, such games are undecidable already for specifications described by deterministic register automata. Therefore, we study one-sided Church games, where Eve uses a finite alphabet but Adam still manipulates data. We show such games are decidable in exponential time in the number of registers in the specification, both for Q and N, are determined, and strategies describable by finite-state register transducers suffice for Eve to win. To obtain this result we study constraint sequences, which abstract the behaviour of register automata and allow for reduction of Church games to omega-regular games. Finally, we apply these results to the transducer-synthesis problem. I will end the talk with the discussion of bounded synthesis. There, specification automata are universal (aka co-nondeterministic), and we search for a realizing transducer with an a-priori given number of registers (hence the term 'bounded synthesis'). This problem is known to be decidable for register automata comparing data for equality only, and we will look at the challenges arising for the case of (N,<).

(This is the joint work by Léo Exibard, Emmanuel Filiot, Ayrat Khalimov)

We study a cyclic proof system C over regular expression types, inspired by linear logic and non-wellfounded proof theory. Proofs in C can be seen as strongly typed goto programs. We show that they denote computable total functions and we analyse the relative strength of C and Gödel's system T. In the general case, we prove that the two systems capture the same functions on natural numbers. In the affine case, i.e., when contraction is removed, we prove that they capture precisely the primitive recursive functions—providing an alternative and more general proof of a result by Dal Lago, about an affine version of system T.

Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I will give an overview of the area, and in particular will present a select survey of known and original results on decision problems for holonomic sequences and functions. I will also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I will relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier.

Parts of this talk will be based on the paper “On Positivity and Minimality for Second-Order Holonomic Sequences”, https://arxiv.org/abs/2007.12282 .

We consider the rational subset membership problem for Baumslag-Solitar groups. These groups form a prominent class in the area of algorithmic group theory, and they were recently identified as an obstacle for understanding the rational subsets of GL(2,ℚ). We show that rational subset membership for Baumslag-Solitar groups BS(1,q) with q ≥ 2 is decidable and PSPACE-complete. To this end, we introduce a word representation of the elements of BS(1,q): their pointed expansion (PE), an annotated q-ary expansion. Seeing subsets of BS(1,q) as word languages, this leads to a natural notion of PE-regular subsets of BS(1,q): these are the subsets of BS(1,q) whose sets of PE are regular languages. Our proof shows that every rational subset of BS(1,q) is PE-regular. Since the class of PE-regular subsets of BS(1,q) is well-equipped with closure properties, we obtain further applications of these results. Our results imply that (i) emptiness of Boolean combinations of rational subsets is decidable, (ii) membership to each fixed rational subset of BS(1,q) is decidable in logarithmic space, and (iii) it is decidable whether a given rational subset is recognizable. In particular, it is decidable whether a given finitely generated subgroup of BS(1,q) has finite index.

This is joint work with Michaël Cadilhac and Dmitry Chistikov.

We show that a polyregular word-to-word function is regular if and only if its output size is at most linear in its input size. Moreover a polyregular function can be realized by: a transducer with two pebbles if and only if its output has quadratic size in its input, a transducer with three pebbles if and only if its output has cubic size in its input, etc. Moreover the characterization is decidable and, given a polyregular function, one can compute a transducer realizing it with the minimal number of pebbles. We apply the result to mso interpretations from words to words. We show that mso interpretations of dimension k exactly coincide with k-pebble transductions.

I will present the tools we used to study tilings that are both substitutive and planar (a relaxed version of cut-and-project) in order to present our main result that there exist planar substitution tilings with 2n-fold rotational symmetry for any odd n.

In this talk we will focus on the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional vector addition systems with states (VASS). We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. We will also generalize the problem to allow disequality constraints on transitions (i.e., we allow transitions to be disabled if the accumulated weight is equal to a specific value). For this generalization, we show that the coverability problem is solvable in polynomial time even though a shortest run may have exponential length.

In the setting of regular languages of infinite words, Good-for-Games (GFG) automata can be seen as an intermediate formalism between determinism and nondeterminism, with advantages from both worlds. Indeed, like deterministic automata, GFG automata enjoy good compositional properties (useful for solving games and composing automata and trees) and easy inclusion checks. Like nondeterministic automata, they can be exponentially more succinct than deterministic automata. I will focus in this talk on the following problem: given a nondeterministic parity automaton on infinite words, is it GFG ? The complexity of this problem is one of the main remaining open questions concerning GFG automata, motivated by the potential applications that would come with an efficient algorithm. After giving the necessary context, I will explain the current understanding on this question, and describe a simple polynomial-time algorithm that is conjectured to solve the problem, but has only been proven correct if the input is a Büchi or a co-Büchi automaton.

I will show that the universality problem is ExpSpace-complete for unambiguous VASS, which is in strong contrast with Ackermann-completeness of the same problem for nondeterministic VASS. I also plan to present some more results concerning the interplay between unambiguity and VASS.

(joint work with Diego Figueira and Piotr Hofman)

We study the universality and inclusion problems L(A)⊆L(B) for register automata over equality data. We show that the universality and inclusion problems can be solved in 2-EXPTIME when both automata A, B are without guessing and B is unambiguous, which improves on the recent 2-EXPSPACE upper bound by Mottet and Quaas. We proceed by reducing inclusion to universality, and then universality to the problem of counting the number of orbits of runs of the automaton. We show that the orbit-counting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), which generalises analogous recurrences for the Stirling numbers of the second kind, and then we show that universality reduces to the zeroness problem for linrec sequences. While such a counting approach is classical and has successfully been applied to unambiguous finite automata and grammars over finite alphabets, its application to register automata over infinite alphabets is novel.

We provide two algorithms to decide the zeroness problem for the linrec sequences arising from orbit-counting functions. Both algorithms rely on skew polynomials. The first algorithm performs variable elimination and has elementary complexity. The second algorithm relies on the computation of the Hermite normal form of matrices over a skew polynomial field. This yields an EXPTIME decision procedure for the zeroness problem, which in turn yields the claimed bounds for the universality and inclusion problems of register automata.

We will discuss the expressive and computational power of Ordinary Differential Equations (ODEs). We present the general theory of discrete ODEs for computation theory, we illustrate this with various examples of algorithms, and we provide several implicit characterizations of complexity and computability classes.

In this talk, I will present algorithms to learn deterministic finite automata (due to Angluin) and weigthed automata over the usual semiring R with addition and multiplication (due to Beimel, Bergadano, Bshouty, Kushilevitz and Varricchio). I will then present some related open questions and pinpoint the difficulty that arise when trying to generalise these algorithms to any semiring.

We investigate weighted context-free languages of infinite words, a generalization of ω-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted languages, or ω-algebraic series, can be represented as solutions of ω-algebraic systems of equations and by weighted ω-pushdown automata.

Our results are threefold. We show that ω-algebraic systems can be transformed into Greibach normal form. Our second result proves that simple ω-pushdown automata recognize all ω-algebraic series. Simple pushdown automata do not use ε-transitions and can change the stack only by at most one symbol. We use these results to prove a logical characterization of weighted ω-context-free languages in the sense of Büchi, Elgot and Trakhtenbrot.

This is joint work with Manfred Droste and Werner Kuich.

Abstract: Detectability is a basic property of partially observed dynamic systems. If a system satisfies such a property, then one can use an observed output sequence generated by the system to determine its internal states after some time. This property plays an important role in many problems such as state estimation and controller synthesis. Finite automata and labeled Petri nets are two widely-studied models in discrete-event systems, which consist of transitions between discrete states driven by spontaneous occurrences of events, and can be seen as abstractions of many practical systems. (A supervisory control framework for synthesising controllers in discrete-event systems was initiated by Ramadge and Wonham in the late 1980s.) In this talk, we introduce recent verification results on a particular property called strong detectability, for finite automata and labeled Petri nets, and several related further topics.

The Strahler number is a measure of branching complexity of rooted trees. We define the Strahler number of a parity game to be the the smallest Strahler number of the tree of any of its attractor decompositions. In this talk, we will argue that the Strahler number of a parity game is a robust, and hence arguably natural, parameter: it coincides with its alternative version based on trees of progress measures and— remarkably—with the register number defined by Lehtinen (2018). We will also look at how parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices n and linear in (d/2k)^k , where d is the number of priorities and k is the Strahler number. This complexity is quasi-polynomial because the Strahler number is at most logarithmic in the number of vertices. This significantly improves the running times and space achieved for parity games of bounded register number by Lehtinen (2018) and by Parys (2020).

The framework of document spanners abstracts the task of information extraction from text as a function that maps every document (a string) into a relation over the document’s spans (intervals identified by their start and end indices). For instance, the regular spanners are the closure under the Relational Algebra (RA) of the regular expressions with capture variables, and the expressive power of the regular spanners is precisely captured by the class of vset-automata - a restricted class of transducers that mark the endpoints of selected spans. In this work, we embark on the investigation of document spanners that can annotate extractions with auxiliary information such as confidence, support, and confidentiality measures. To this end, we adopt the abstraction of provenance semirings by Green et al., where tuples of a relation are annotated with the elements of a commutative semiring, and where the annotation propagates through the (positive) RA operators via the semiring operators. Hence, the proposed spanner extension, referred to as an annotator, maps every string into an annotated relation over the spans. As a specific instantiation, we explore weighted vset-automata that, similarly to weighted automata and transducers, attach semiring elements to transitions. We investigate key aspects of expressiveness, such as the closure under the positive RA, and key aspects of computational complexity, such as the enumeration of annotated answers and their ranked enumeration in the case of numeric semirings. For a number of these problems, fundamental properties of the underlying semiring, such as positivity, are crucial for establishing tractability. This is a joint work with Johannes Doleschal, Benny Kimelfeld and Wim Martens.

Automata for infinite alphabets, despite undeniable appeal, are a bit of a theoretical mess. Almost all models are non-equivalent as language recognisers: deterministic/nondeterministic/alternating, one-way/two-way, etc. Also monoids give a different class of languages, and mso gives yet another.

In this talk, I will describe how the single-use restriction can bring some order into this zoo. The single-use restriction says that once an atom from a register is queried, then that atom disappears. Among our results: a Factorisation Forest Theorem, a Krohn-Rhodes decomposition, and a class of “regular” transducers which admits four equivalent characterisations.

Joint work with Rafał Stefański.

In this paper we show that given a max-plus automaton (over trees, and with real weights) computing a function f and a min-plus automaton (similar) computing a function g such that f ⩽ g, there exists effectively an unambiguous tropical automaton computing h such that f ⩽ h ⩽ g. This generalizes a result of Lombardy and Mairesse of 2006 stating that series which are both max-plus and min-plus rational are unambiguous. This generalization goes in two directions: trees are considered instead of words, and separation is established instead of characterization (separation implies characterization). The techniques in the two proofs are very different.

We investigate the connection between properties of formal languages and properties of their generating series, with a focus on the class of holonomic power series.

It is a classical result that regular languages have rational generating series and that the generating series of unambiguous context-free languages are algebraic. This connection between automata theory and analytic combinatorics has been successfully exploited. For instance, Flajolet used it in the eighties to prove the inherent ambiguity of some context-free languages using criteria from complex analysis.

Settling a conjecture of Castiglione and Massazza, we establish an interesting link between unambiguous Parikh automata and holonomic power series, which also yields characterizations of inherent ambiguity and algorithmic byproducts for these automata models.

This is a joint work with Alin Bostan, Arnaud Carayol and Cyril Nicaud.

Finite automata pose an interesting alternative way to present groups and semigroups. Some of these automaton groups became famous for their peculiar properties and have been extensively studied. In addition to that, there exists also a line of research on the general properties of the class of automaton groups.

One aspect of this research is the study of algorithmic properties of automaton groups and semigroups. While many natural algorithmic decision problems have been proven or are generally suspected to be undecidable for these classes, the word problem forms a notable exception. In the group case, it asks whether a given word in the generators is equal to the neutral element in the group in question and is well-known to be decidable for automaton groups. In fact, it was observed in a work by Steinberg published in 2015 that it can be solved in nondeterministic linear space using a straight-forward guess and check algorithm. In the same work, he conjectured that there is an automaton group with a PSPACE-complete word problem.

In a recent paper presented at STACS 2020, Armin Weiß and I could prove that there indeed is such an automaton group. To achieve this, we combined two ideas. The first one is a construction introduced by Daniele D'Angeli, Emanuele Rodaro and me to show that there is an inverse automaton semigroup with a PSPACE-complete word problem and the second one is an idea already used by Barrington in 1989 to encode NC¹ circuits in the group of even permutation over five elements. In the talk, we will discuss how Barrington's idea can be applied in the context of automaton groups, which will allow us to prove that the uniform word problem for automaton groups (were the generating automaton and, thus, the group is part of the input) is PSPACE- complete. Afterwards, we will also discuss the ideas underlying the construction to simulate a PSPACE-machine with an invertible automaton, which allow for extending the result to the non-uniform case. Finally, we will briefly look at related problems such as the compressed word problem for automaton groups.

Joint work with Salomon Sickert

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of LTL with past operators is equivalent to a formula of the form $\bigwedge_{i=1}^n \G\F \varphi_i \vee \F\G \psi_i $, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for the future fragment of LTL. Both normalisation procedures had a non-elementary worst-case blow-up, and followed an involved path from LTL formulas to counter-free automata to star-free regular expressions and back to LTL. We improve on both points. We present a purely syntactic normalisation procedure from LTL to LTL, with single exponential blow-up, that can be implemented in a few dozen lines of Standard ML code. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.

An assume guarantee (AG) specification is of the form “Assumption implies Guarantee”. AG Synthesis is the following problem: given an AG specification, construct a system satisfying it.

In this talk I will discuss the case where both Assumptions and Guarantees are given by Prompt Linear Temporal Logic (Prompt LTL), which is a logic extending LTL by adding bound requirements such as “every request is answered in bounded time”.

The solution to the AG problem for Prompt LTL will be an invitation to the theory of regular cost functions.

Joint work with Bastien Maubert and Moshe Y. Vardi.

Bertrand et al. (2017) introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min- cut theorem, and of the theory of regular cost functions.

We present a new category theoretic approach to equationally axiomatizable classes of algebras. This approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. We present a generic HSP theorem and a sound and complete equational logic, which encompass numerous flavors of equational axiomizations studied in the literature. In addition, we use the generic HSP theorem as a key ingredient to obtain Eilenberg-type correspondences yielding algebraic characterizations of properties of regular machine behaviours. When instantiated for orbit-finite nominal monoids, the generic HSP theorem yields a crucial step for the proof of the first Eilenberg-type variety theorem for data languages.

We propose a generic framework for learning unknown formal languages of various types (e.g. finite or infinite words, weighted and nominal languages). Our approach is parametric in a monad T that represents the given type of languages and their recognizing algebraic structures. Using the concept of an automata presentation of T-algebras, we demonstrate that the task of learning a T-recognizable language can be reduced to learning an abstract form of algebraic automaton whose transitions are modeled by a functor. For the important case of adjoint automata, we devise a learning algorithm generalizing Angluin’s L*. The algorithm is phrased in terms of categorically described extension steps; we provide for a termination and complexity analysis based on a dedicated notion of finiteness. Our framework applies to structures like ω-regular languages that were not within the scope of existing categorical accounts of automata learning. In addition, it yields new generic learning algorithms for several types of languages for which no such algorithms were previously known at all, including nominal languages with name binding, and cost functions. This talk is based on joint work with Lutz Schröder.

In this talk, we consider multiplayer games on graphs. In such games, each player has his own objective, that does not necessarily clash with the objectives of the other players. In this “non zero-sum” context, equilibria are a better suited solution concept than the classical winning strategy notion. We will focus on a refinement of the well-known Nash Equilibrium concept: Subgame Perfect Equilibrium (SPE for short), where players have to play rationnally in every scenario, even the ones that deviate from the planned outcome. We will explain why this refinement is a relevant solution concept in multiplayer games and show how to handle them in quantitative reachability games, where each player wants to minimize the number of steps to reach its own target set of vertices.

We consider extensions of monadic second order logic over $\omega$-words, which are obtained by adding one language that is not $\omega$-regular. We show that if the added language $L$ has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the $\omega$-regular languages are the only decidable Boolean-closed full trio over $\omega$-words.

(Joint work with Mikołaj Bojańczyk, Edon Kelmendi, and Rafał Stefański)

Transducers extend automata by adding outputs to the transition, thus computing functions over words instead of recognizing languages. Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition. However, the best known algorithms for composing two-way transducers are rather involved and cause a double exponential blow-up in the size of the input machines. This contrasts with the rather direct and polynomial construction for composing one-way machines. In this talk, I will present the class of reversible transducers, which are machines that are both deterministic and co-deterministic. This class enjoys polynomial composition complexity, even in the two-way case. Although this class is not very expressive in the one-way scenario, I will show that any two-way transducer can be made reversible through a single exponential blow-up. As a consequence, the composition of two-way transducers can be done with a single exponential blow-up in the number of states, enhancing the best known algorithm from the 60s.

The window mechanism was introduced by Chatterjee et al. to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields.

In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.

Joint work with : Thomas Brihaye, Florent Delgrange, Mickael Randour.

We study networks of processes which all execute the same finite-state protocol and communicate thanks to a rendez-vous mechanism. Given a protocol, we are interested in checking whether there exists a number, called a cut-off, such that in any networks with a bigger number of participants, there is an execution where all the entities end in some final states. We provide decidability and complexity results of this problem under various assumptions, such as absence/presence of a leader or symmetric/asymmetric rendez-vous.

This is a joint work with Florian Horn.

A language of finite words is star-free when it can be built from letters using Boolean operations and concatenation. A well-known theorem of Schützenberger characterizes star-free languages as those recognized by an aperiodic monoid. Another theorem of Schützenberger gives an alternate definition: these are the languages that can be built using product, union, and, in a limited way, Kleene star (but complement is now disallowed).

These definitions can be rephrased using closure operators operating on classes of languages. In this talk, we investigate these operators and generalize the results of Schützenberger. This is joint work with Thomas Place.

Parity games are central to the verification and synthesis of reactive systems: various model-checking, realisability and synthesis problems reduce to solving these games. Solving parity games – that is, deciding which player has a winning strategy – is one of the few problems known to be in both UP and co-UP yet not known to be in P. So far, the quest for a polynomial algorithm has lasted over 25 years.

In 2017 a major breakthrough occurred: parity games are solvable in quasi-polynomial time. Since then, several seemingly very distinct quasi-polynomial algorithms have been published, both by myself and others, and some of the novel ideas behind them have been applied to address other problems in automata theory.

In this talk, I will give an overview of these developments, including my own contribution to them, and the state-of-the art, with a slight automata-theoretic bias.

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.

Petri nets, also known as vector addition systems, are a long established and widely used model of concurrent processes. The complexity of their reachability problem is one of the most prominent open questions in the theory of verification. That the reachability problem is decidable was established by Mayr in his seminal STOC 1981 work, and the currently best upper bound is non-primitive recursive cubic-Ackermannian of Leroux and Schmitz from LICS 2015. We show that the reachability problem is not elementary. Until this work, the best lower bound has been exponential space, due to Lipton in 1976.

Joint work with Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Filip Mazowiecki.

Rabin's Tree Theorem proceeds by effective translations of MSO-formulae to tree automata. We show that the operations on automata used in these translations can be organized in a deduction system based on intuitionistic linear logic (ILL). We propose a computational interpretation of this deduction system along the lines of the Curry-Howard proofs-as-programs correspondence. This interpretation, relying on the usual technology of game semantics, maps proofs to strategies in categories of two-player games generalizing the usual acceptance games of tree automata.

We present our work on what we call the constrained topological sorting problem (CTS): given a regular language K and a directed acyclic graph G with labeled vertices, determine if G has a topological sort that forms a word in K. This natural problem applies to several settings, e.g., scheduling with costs or verifying concurrent programs. We consider the problem CTS[K] where the target language K is fixed, and study its complexity depending on K.

Our work shows that CTS[K] is tractable when K falls in several language families, e.g., unions of monomials, which can be used for pattern matching. However, we can show that CTS[K] is NP-hard for K = (ab)^* using a shuffle reduction technique that we can use to show hardness for more languages. We also study the special case of the constrained shuffle problem (CSh), where the input graph is a disjoint union of strings, and show that CSh[K] is additionally tractable when K is a group language or a union of district group monomials. We conjecture that a dichotomy should hold on the complexity of CTS[K] or CSh[K] depending on K, and substantiate this by proving a coarser dichotomy under a different problem phrasing which ensures that tractable languages are closed under common operators. 

We present a survey of results obtained on symbolic dynamical systems called dendric shifts. We state and sketch the proofs (sometimes new ones) of the main results obtained on these shifts. This includes the Return Theorem and the Finite Index Basis Theorem which both put in evidence the central role played by free groups in these systems. We also present a series of applications of these results, including some on profinite semigroups and some on dimension groups.

En 2015, Jeandel et Rao ont démontré par des calculs exhaustifs faits par ordinateur que tout ensemble de tuiles de Wang de cardinalité ≤ 10 soit admettent un pavage périodique du plan Z² soit n'admettent aucun pavage du plan. De plus, ils ont trouvé un ensemble de 11 tuiles de Wang qui pavent le plan mais jamais de façon périodique. Dans cet exposé, nous présenterons une définition alternative des pavages apériodiques de Jeandel-Rao comme le codage d'une Z²-action sur le tore et nous décrivons la structure substitutive de ces pavages.

The Pascal triangle and the corresponding Sierpinski gasket are well-studied objects. They exhibit self-similarity features and have connections with dynamical systems, cellular automata, number theory and automatic sequences in combinatorics on words. In this talk, I will first recall the well-known link between those two objects. Then I will exploit it to define Pascal-like triangles associated with different numeration systems, and their analogues of the Sierpinski gasket. This a work in collaboration with Julien Leroy and Michel Rigo (University of Liège, Belgium).

I will present the equivalence of two classes of counter machines and one class of distributed automata. The considered counter machines operate on finite words, which they read from left to right while incrementing or decrementing a fixed number of counters. The two classes differ in the extra features they offer: one allows to copy counter values, whereas the other allows to compute copyless sums of counters. The considered distributed automata, on the other hand, operate on directed path graphs that represent words. All nodes of a path synchronously execute the same finite-state machine, whose state diagram must be acyclic except for self-loops, and each node receives as input the state of its direct predecessor. These devices form a subclass of linear-time one-way cellular automata.

This is joint work with Olivier Carton and Bruno Guillon.

We study approximation algorithms for two closely related problems: the problems of finding a short synchronizing and a short mortal word for a given prefix code. Roughly speaking, a synchronizing word is a word guaranteeing a unique interpretation, and a mortal word is a word guaranteeing no interpretation for any sequence of codewords. We concentrate on the case of finite prefix codes and consider both the cases where the code is defined by listing all its codewords and where the code is defined by an automaton recognizing the star of the code. This is a joint work with Marek Szykuła (University of Wroclaw).

Given any numeration system, we call 'carry propagation' at a number N the number of digits that are changed when going from the representation of N to the one of N+1 , and 'amortized carry propagation' the limit of the mean of the carry propagations at the first N integers, when N tends to infinity, and if it exists.

We address the problem of the existence of the amortized carry propagation and of its value in non-standard numeration systems of various kinds: abstract numeration systems, rational base numeration systems, greedy numeration systems and beta-numeration.

We tackle the problem by means of techniques of three different types: combinatorial, algebraic, and ergodic.

For each kind of numeration systems that we consider, the relevant method allows to establish sufficient conditions for the existence of the carry propagation and examples show that these conditions are close to be necessary.

This is a joint work with Valérie Berthé, Christiane Frougny, and Michel Rigo

I will talk about parity games. There are at least three different recent algorithms which solve them in quasipolynomial time. In this talk, I will show that the three algorithms can be seen as solutions of one automata-theoretic problem. Using this framework, I will show tight upper and lower bounds, witnessing a quasipolynomial barrier.

This is based on two joint works, the first with Wojtek Czerwinski, Laure Daviaud, Marcin Jurdzinski, Ranko Lazic, and Pawel Parys, and the second with Thomas Colcombet.

We develop an algebraic lower bound technique in the context of non-commutative arithmetic circuits. To this end, we introduce polynomials for which the multiplication is also non-associative, and focus on their circuit complexity. We show a connection with multiplicity tree automata, leading to a general algebraic characterization. We use it to derive meta-theorems for the non-commutative case, and highlight numerous consequences in terms of lower bounds.

Automated invariant generation is a fundamental challenge in program analysis and verification, going back many decades, and remains a topic of active research. In this talk I'll present a select overview and survey of work on this problem, and discuss unexpected connections to other fields including algebraic geometry, group theory, and quantum computing. (No previous knowledge of these fields will be assumed.)

This is joint work with Ehud Hrushovski, Amaury Pouly, and James Worrell.

The study on how (semi)groups grow has been highlighted since Milnor's question on the existence of groups of intermediate growth (faster than any polynomial and slower than any exponential) in 1968. A very first example of such a group was given by Grigorchuk in 1983 in terms of an automaton group, and, until Nekrashevych's very recent work, all the known examples of intermediate growth groups were automaton groups or based on automaton groups.

This talk originates in the following question: is it decidable if an automaton group has intermediate growth? I will show that in the case of bireversible automata, whenever there exists at least one element of infinite order, the growth of the group is necessarily exponential.

(This work will be presented at ICALP'18.)

In my presentation, I am going to present joint work with Joel Allred on the complementation of Büchi automata. When constructing the complement automaton, a worst-case state-space growth of O((0.76n)^n) cannot be avoided. Experiments suggest that complementation algorithms perform better on average when they are structurally simple. We develop a simple algorithm for complementing Büchi automata, operating directly on subsets of states, structured into state-set tuples, and producing a deterministic automaton. Then a complementation procedure is applied that resembles the straightforward complementation algorithm for deterministic Büchi automata, the latter algorithm actually being a special case of our construction. Finally, we prove our construction to be optimal, i.e. having an upper bound in O((0.76n)^n), and furthermore calculate the 0.76 factor in a novel exact way.

Looking at some monoids and (semi)rings (natural numbers, integers and p- adic integers), and more generally, residually finite algebras (in a strong sense), we prove the equivalence of two ways for a function on such an algebra to behave like the operations of the algebra. The first way is to preserve congruences or stable preorders. The second way is to demand that preimages of recognizable sets belong to the lattice or the Boolean algebra generated by the preimages of recognizable sets by “derived unary operations” of the algebra (such as trans- lations, quotients,. . . ).

The increasing interest in social networks, knowledge graphs, protein-interaction, and many other types of networks has raised the question how users can explore such large and complex graph structures easily. In this regard, graph exploration has emerged as a complementary toolbox for graph management, graph mining, or graph visualization in which the user is a first class citizen. Graph exploration combines and expands database, data mining, and machine learning approaches with the user eye on one side and the system perspective on the other.

The talk shows how graph exploration can considerably support any analysis on graphs in a fresh and exciting manner, by combining interactive methods, personalized results, adaptive structures, and scalable algorithms. I describe the recent efforts for a graph exploration stack which supports interactivity, personalization, adaptivity, and scalability through intuitive and efficient techniques we recently proposed. The current methods show encouraging results in reducing the effort of experts and novice users in finding the information of interests through example-based approaches, personalized summaries, and active learning theories. Finally, I present the vision for the future in graph exploration research and show the chief challenges in databases, data analysis, and machine learning.

The issue of determinism versus non-determinism is central in computer science. In order to better understand this gap, the intermediary model of Good-for-Games (GFG) automata is currently being explored in its various aspects. A GFG automaton is a non-deterministic automaton on finite or infinite words, where accepting runs can be built on-the-fly on valid input words. I will recall recent advances on this model, and describe a newly introduced generalisation: width. The width of an automaton can be viewed as a measure of its amount of nondeterminism. Width generalises the notion of GFG automata, which correspond to NFAs of width 1. I will describe how GFG or deterministic automata can be built from non-deterministic automata, with width being a crucial parameter in the construction. I will finally mention results and open problems related to the computational complexity of computing GFGness or width of automata.

Cypher is a query-language for property-graphs. It was originally designed and implemented as part of the Neo4j graph database, and it is currently used by several commercial database products and researchers. The semantics of Cypher queries is currently described using natural language and, as a result, it is often not well defined. This work is part of a project to define a full denotational semantics of Cypher queries. The talk will first present the main features of Cypher through examples, including the core mecanism: graph pattern-matching, and then will describe the principle of the formal semantics.

La formalisation et le raisonnement sur des notions non-vérifonctionnelles, telles que la croyance, le savoir ou la certitude, sont des enjeux actuels de l'intelligence artificielle. Ces notions peuvent mener à représenter et évaluer des informations subjectives et sont, en particulier, formalisées en logique modale. Motivés par la modélisation du raisonnement sur les croyances graduelles, dont l'expressivité est enrichie par rapport aux croyances classiques, mes travaux portent sur les extensions pondérées des logiques modales.

Dans le cadre général des logiques modales, je propose d'abord une sémantique proportionnelle pour des opérateurs modaux pondérés, basée sur des modèles de Kripke classiques. J'étudie ensuite la définition d'axiomes modaux pondérés étendant les axiomes classiques et propose une typologie les répartissant en quatre catégories, selon l'enrichissement du cas classique qu'ils produisent et leur correspondance avec la contrainte associée sur la relation d'accessibilité.

D'autre part, je m'intéresse à une formalisation des croyances graduelles, basée sur la conception représentationaliste des croyances et reposant sur un modèle ensembliste flou. J'en étudie plusieurs aspects, comme les propriétés arithmétiques et l'application de la négation.

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into omega-automata by elementary means. In particular, the breakpoint, Safra, and ranking constructions used in other translations are not needed.

Joint work with Jan Kretinsky and Salomon Sickert.

We study the problem of constructing approximations to a weighted automaton. Weighted finite automata (WFA) are closely related to the theory of rational series. A rational series is a function from strings to real numbers that can be computed by a WFA. This includes probability distributions generated by hidden Markov models and probabilistic automata. The relationship between rational series and WFA is analogous to the relationship between regular languages and ordinary automata. Associated with such rational series are infinite matrices called Hankel matrices which play a fundamental role in the theory of minimal WFA. In this talk I describe: (1) an effective procedure for computing the singular value decomposition (SVD) of such infinite Hankel matrices based on their finite representation in terms of WFA; (2) a new canonical form for WFA based on this SVD decomposition; and, (3) an algorithm to construct approximate minimizations of a given WFA. The goal of the approximate minimization algorithm is to start from a minimal WFA and produce a smaller WFA that is close to the given one in a certain sense. The desired size of the approximating automaton is given as input. I will give bounds describing how well the approximation emulates the behavior of the original WFA.

This is joint work with Borja Balle and Doina Precup and was presented at LICS 2015 in Kyoto.

The talk will be based on my habilitation defense talk from Nov. 27 2018, which was dedicated to the algorithmic complexity of well-quasi-orders. The latter find applications in verification, where they allow to tackle systems featuring an infinite state-space, representing for instance integer counters, the number of active threads in concurrent settings, real-time clocks, call stacks, cryptographic nonces, or the contents of communication channels.

The talk gives an overview of the complexity questions arising from the use of well-quasi-orders, including the definition of complexity classes suitable for problems with non-elementary complexity and proof techniques for upper bounds. I will mostly focus on the ideas behind the first known complexity upper bound for reachability in vector addition systems and Petri nets.

Nowhere dense graph classes, introduced by Nesetril and Ossona de Mendez, are a broad family of sparse graph classes for which many algorithmic problems which are hard in general become tractable. In particular, model checking first-order logic is fixed-parameter tractable over such classes, as shown recently by Grohe, Kreutzer, and Siebertz. With the aim of finding generalizations of this result to dense graph classes, I will talk about some recent developments in the study of the connections between nowheredenseness and stability (developed by Shelah).

How is algorithmic randomness related to the classical theory of uniform distribution? In this talk we consider the definition of Martin-Löf randomness for real numbers in terms of uniform distribution of sequences. We present a necessary condition for a real number to be Martin-Löf random, and a strengthening of that condition which is sufficient for Martin-Löf randomness. For this strengthening we define a notion of uniform distribution relative to the computably enumerable open subsets of the unit interval. We call the notion Sigma^0_1-uniform distribution.

This is joint work with Serge Grigorieff and Theodore Slaman.

The problem of querying description logic knowledge bases using database-style queries (in particular, conjunctive queries) has been a major focus of recent description logic research. An important issue that arises in this context is how to handle the case in which the data is inconsistent with the ontology. Indeed, since in classical logic an inconsistent logical theory implies every formula, inconsistency-tolerant semantics are needed to obtain meaningful answers. I will first present a practical approach for querying inconsistent DL-Lite knowledge bases using three natural semantics (AR, IAR, and brave) previously proposed in the literature and that rely on the notion of a repair, which is an inclusion-maximal subset of the data consistent with the ontology. Since these three semantics provide answers with different levels of confidence, I will then present a framework for explaining query results, to help the user to understand why a given answer was or was not obtained under one of the three semantics.

We study Nash equilibria in games on graphs with an imperfect monitoring based on a public signal. In such games, deviations and players responsible for those deviations can be hard to detect and track. We propose a generic epistemic game abstraction, which conveniently allows to represent the knowledge of the players about these deviations, and give a characterization of Nash equilibria in terms of winning strategies in the abstraction. We then use the abstraction to develop algorithms for some payoff functions.

Concurrent Kleene algebras (CKA) and bi-Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets.

In the first part of the talk, I will present an automaton model designed to describe such languages of pomset, which satisfies a Kleene-like theorem. The main difference with previous constructions is that from expressions to automata, we use Brzozowski derivatives.

In a second part, I will use Petri nets to reduce the problem of containment of languages of pomsets to the equivalence of finite state automata. In doing so, we prove decidabilty as well as provide tight complexity bounds.

I will finish the presentation by briefly presenting a recent proof of completness, showing that two series-rational expressions are equivalent according to the laws of CKA exactly when their pomset semantics are equal.

Joint work with Damien Pous, Georg Struth, Tobias Kappé, Bas Luttik, Alexandra Silva, and Fabio Zanasi

My presentation is about effective characterisations: given a representation of a regular language, decide if the language is “simple” in some specific sense. A classical example of such a characterisation is the result by Schutzenberger, McNaughton, and Papert, saying that it is decidable if a given regular language of finite words can be defined in first-order logic. Over the years, such characterisations were provided for many other natural classes of languages, especially in the case of finite and infinite words. It is often assumed that a “golden standard” for such a characterisation is to provide equations that must be satisfied in a respective algebra representing the language.

The aim of my talk is to survey a number of examples in which it is not possible to provide algebraic representation of the considered languages; but instead characterisations can be obtained by a well-designed game of infinite duration. Using these examples, I will try to argue that game-based approach is the natural replacement for algebraic framework in the cases where algebraic representations are not available.

In this talk I will discuss the following natural question: Given a class of computational models C, does there exist two distinct inputs which give the same output for all the models in the class. I will discuss this question more precisely for weighted automata in general and for max-plus automata in particular. Weighted automata are a quantitative extension of automata which allows to compute values such as costs and probabilities. Max-plus automata are a special case of weighted automata, particularly suitable to model gain optimisation problems. We will see that in this last case, we end up with particularly intricate (and open) questions, related to finding identities in the semiring of tropical matrices.

We present a few results and several open problems concerning complete deterministic finite automata in which every non-empty subset of the state set occurs as the image of the whole state set under the action of a suitable input word. In particular, we give a complete description of such automata with minimal transition monoid size.

The robustness of the famous compression algorithm of Lempel and Ziv is still not well understood: in particular, until now it was unknown whether the addition of one bit in front of a compressible word could make it incompressible. This talk will answer that question, advertised by Jack Lutz under the name “one-bit catastrophe” and which has been around since at least 1998. We will show that a “well” compressible word remains compressible when a bit is added in front of it, but some “few” compressible words indeed become incompressible. This is a joint work with Guillaume Lagarde.

A Markov decision process models the interactions between a controller giving inputs and a stochastic environment. In this well-studied model, transitions are fired instantaneously. We study semi-Markov decision processes, where each transition takes some time to fire, determined by a given probabilistic distribution (for instance, an exponential distribution). The question we investigate is how to compare two semi-Markov decision processes. We introduce and study the algorithmic complexity of two relations, “being faster than”, and “being equally fast as”.

Dans le cadre des journées de clôture du projet MealyM (https://mealym.sciencesconf.org/)

Manuscrit disponible ici : https://www.irif.fr/_media/users/godin/these30-06-17.pdf

Dans le cadre des journées de clôture du projet MealyM (https://mealym.sciencesconf.org/)

Manuscrit disponible ici : https://mealym.sciencesconf.org/data/program/HdR.pdf

A new classification scheme for real numbers will be given, motivated by ideas from statistical mechanics in general and work of Knauf and Fiala and Kleban in particular. Critical for this classification of real numbers will be the Diophantine properties of continued fraction expansions. Underneath this classification is a new partition function on the space of infinite sequences of zeros and ones.

The Orbit Problem consists of determining, given a linear transformation $A$ on $Q^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$.

We will investigate this problem with a different point of view: is it possible to synthesise suitable invariants, that is, subsets of $Q^d$ that contain $x$ but not $y$. Such invariants provide natural certificates for negative instances of the Orbit Problem. We will show that semialgebraic invariants exist in all reasonable cases. A more recent (yet unpublished) result is that existence of semilinear invariants is decidable.

This is a joint work with Nathanaël Fijalkow, Joël Ouaknine, Amaury Pouly and James Worrell, published in STACS 2017.

Formal models for the computation of problems, say circuits, automata, Turing machines, can be naturally extended to compute word-to-word functions. But abstracting from the computation model, what does it mean to “lift” a language class to functions? We propose to address that question in a first step, developing a robust theory that incidentally revolves around the (topological) notion of continuity. In language-theoretic terms, a word-to-word function is V-continuous, for a class of languages V, if it preserves membership in V by inverse image.

In a second step, we focus on transducers, i.e., automata with letter output. We study the problem of deciding whether a given transducer realizes a V-continuous function, for some classical classes V (e.g., aperiodic languages, group languages, piecewise-testable, …).

If time allows, we will also see when there exists a correlation between the transducer structure (i.e., its transition monoid), and its computing a continuous function.

Joint work with Olivier Carton, Andreas Krebs, Michael Ludwig, Charles Paperman.

We are interested in 2-dimensional cellular automata and more precisely in the recognition of langages in small time. The time complexity we consider is called real-time and is rather classic for the study of cellular automata. It consists of the smallest amount of time needed to read the whole imput. It has been shown that this set of langages depend on the neighborhood of the automaton. For example the two most used neighborhoods (Moore and von Neumann ones) are different with respect to this complexity. Our study deals with more generic sets of neighborhoods, round and diamond neighborhoods. We prove that all diamond neighborhoods can recognize the same langages in real time and that the round neighborhoods can recognize stricly less than the diamond ones.

Several notions of computability have been defined before every one agreed that Turing Machines are the good model of computation, a statement raised to the widely accepted Church-Turing Thesis. However, since then, lots of stronger computability notions have been defined and studied, for the sake of math and because it gives us new insight on some already existing fields.

In this talk, we will see two ways to extend usual computability: by defining a more powerful model, or in a more set theoretic fashion. The first method is used to define Infinite Time Turing Machine, a model where Turing Machines are allowed to compute throught infinite time (that is, throught the ordinals instead of the integers). It has a lot of links with admissibility theory. The second method is used to define alpha-recursion, where alpha is any admissible ordinal. It is an abstract and very general definition of computation. Even if it has a very set-theoretic basis, it reflects the idea of computation and contains the notions of Turing Machine and Infinite Time Turing Machines computabilities. It also includes Higher Computability.

By investigating which properties on the extensions are needed to lift theorems to the new setting, we are able to isolate the important properties of the classical case. We also apply these generalized recursion theories to define randomness, in the same way that we did in the classical case: a string is said to be random if it has no exceptionnal properties, in a computable sense. Our new definition of computation then gives use new definition of randomness.

(No prior knowledge on set theory is assumed.)

In this talk I will give a gentle introduction to symbolic dynamics and motivate an open question in this field: which are the structures where can we construct aperiodic tilings using local rules. I will then introduce the notion of simulation of an effective dynamical system and show how these results can be used to produce aperiodic tilings in extremely complicated structures. We end the talk by presenting a novel simulation theorem which allows to show the existence of such tilings in the Grigorchuk group.

We investigate different notions of recognizability for a free monoid morphism $\sigma: A^* \to B^*$. Full recognizability occurs when each (aperiodic) two-sided sequence over $B$ admits at most one tiling with words $\sigma(a)$, $a \in A$. This is stronger than the classical notion of recognizability of a substitution $\sigma$, where the tiling must be compatible with the language of the substitution. We show that if $A$ is a two-letter alphabet, or if the incidence matrix of $\sigma$ has rank $|A|$, or if $\sigma$ is permutative, then $\sigma$ is fully recognizable. Next we investigate the classical notion of recognizability and improve earlier results of Mossé (1992) and Bezuglyi, Kwiatkowski and Medynets (2009), by showing that any substitution is recognizable for aperiodic points in its substitutive shift. Finally we define (eventual) recognizability for sequences of morphisms which define an $S$-adic shift. We prove that a sequence of morphisms on alphabets of bounded size, such that compositions of consecutive morphisms are growing on all letters, is eventually recognizable for aperiodic points. We provide examples of eventually recognizable, but not recognizable, sequences of morphisms, and sequences of morphisms which are not eventually recognizable. As an application, for a recognizable sequence of morphisms, we obtain an almost everywhere bijective correspondence between the $S$-adic shift it generates and the measurable Bratteli-Vershik dynamical system that it defines.

This is joint work with Valérie Berthé, Jörg Thuswaldner and Reem Yassawi.

An automatic presentation (also called an FA-presentation) is a description of a relational structure using regular languages. The concept an FA-presentation arose in computer science, to fulfil a need to extend finite model theory to infinite structures. Informally, an FA-presentation consists of a regular language of abstract representatives for the elements of the structure, such that each relation (of arity $n$, say) can be recognized by a synchronous $n$-tape automaton. An FA-presentation is “unary” if the language of representatives is over a 1-letter alphabet.

In this talk, I will introduce and survey automatic presentations, with particular attention to connections with decidability and logic. I will then discuss work with Nik Ruskuc (Univ. of St Andrews, UK) and Richard Thomas (Univ. of Leicester, UK) on algebraic and combinatorial structures that admit automatic presentations or unary automatic presentations. The main focus will be on results that characterize the structures of some type (for example, groups, trees, or partially ordered sets) that admit automatic presentations.

Il y a 50 ans, Cerny a posé une conjecture combinatoire sur les automates, qui n'est toujours pas résolue. Un automate est dit synchronisé quand il existe un mot u et un état p tel que depuis n'importe quel état, si on lit u on arrive en p. Sa conjecture est que si l'automate synchronisé possède n états, alors il existe un tel u de longueur au plus (n-1)2. Dans cet exposé, nous nous intéresserons à la version probabiliste de la conjecture de Cerny : on montrera qu'un automate aléatoire est non seulement synchronisé (résultat déjà prouvé par Berlinkov), mais qu'en plus la conjecture de Cerny est vraie avec forte probabilité.

On s'intéresse au parallèle entre 2 problèmes sur des modèles distincts d'automates. D'une part, les automates de Mealy (transducteurs lettre à lettre complets) qui produisent des semi-groupes engendrés par les transformations sur les mots infinis associées aux états. En 2013, Gillibert a montré que le problème de la finitude de ces semi-groupes était indécidable, en revanche la question est ouverte dans le cas où l'automate de Mealy produit un groupe. D'autre part, les automates cellulaires unidirectionnels pour lesquels la question de la décidabilité de la périodicité est ouverte. On peut montrer l'équivalence de ces problèmes. On fera un pas vers une preuve d'indécidabilité en montrant qu'il est possible de simuler du calcul Turing dans un automate cellulaire unidirectionnel réversible, rendant ainsi des problèmes de prédiction indécidables ainsi que la question de la périodicité partant d'une configuration donnée finie.

I will present the equivalence between a class of asynchronous distributed automata and a small fragment of least fixpoint logic, when restricted to finite directed graphs. More specifically, the considered logic is (a variant of) the fragment of the modal μ-calculus that allows least fixpoints but forbids greatest fixpoints. The corresponding automaton model uses a network of identical finite-state machines that communicate in an asynchronous manner and whose state diagram must be acyclic except for self-loops. As a by-product, the connection with logic also entails that the expressive power of those machines is independent of whether or not messages can be lost.

Given an integer base $b>1$, a set of integers is represented in base $b$ by a language over $\{0,1,\dots,b-1\}$. The set is said $b$-recognisable if its representation is a regular language. It is known that eventually periodic sets are $b$-recognisable in every base $b$, and Cobham's theorem imply the converse: no other set is $b$-recognisable in every base $b$.

We are interested in deciding whether a $b$-recognisable set of integers (given as a finite automaton) is eventually periodic. Honkala showed in 1986 that this problem is decidable and recent developments give efficient decision algorithms. However, they only work when the integers are written with the least significant digit first.

In this work, we consider here the natural order of digits (Most Significant Digit First) and give a quasi-linear algorithm to solve the problem in this case.

No knowledge in arithmetic complexity will be assumed.

We still don't know an explicit polynomial that requires non-commutative circuits of size at least superpolynomial. However, the context of non commutativity seems to be convenient to get such lower bound because the rigidity of the non-commutativity implies a lot of constraints about the ways to compute. It is in this context that Nisan, in 1991, provides an exponential lower bound against the non commutative Algebraic Branching Programs computing the permanent, the very first one in arithmetic complexity. We show that this result can be naturally seen as a particular case of a theorem about circuits with unique parse tree, and show some extensions to get closer to lower bounds for general NC circuits.

Two joint works: with Guillaume Malod and Sylvain Perifel; with Nutan Limaye and Srikanth Srinivasan.

In the first part of the talk I will recall the duality approach to language recognition. To start with, I will explain the following simple fact. The elements of the syntactic monoid of a regular language $L$ over a finite alphabet $A$ are in one to one correspondence with the atoms of the finite sub-Boolean algebra of $P(A^*)$ generated by the quotients of $L$. This correspondence can be seen as an instance of Stone duality for Boolean algebras, and has lead to a topological notion of recognition for non-regular languages, the so called Boolean spaces with internal monoids.

A fundamental tool in studying the connection between algebraic recognisers, say classes of monoids, and fragments of logics on words is the availability of constructions on monoids which mirror the action of quantifiers, such as block products or other kinds of semidirect products. In the second part of the talk I will discuss generalisations of these techniques beyond the case of regular languages and present a general recipe for obtaining constructions on the topological recognisers introduced above that correspond to operations on languages possibly specified by transducers.

This talk is based on joint work with Mai Gehrke and Luca Reggio.

A subset of natural numbers is called an IP-set if it contains an infinite increasing sequence of numbers and all its finite sums. In the talk we show how certain families of uniformly recurrent words can be used to generate IP-sets, as well as sets possessing some related additive properties.

Schema mappings are a fundamental concept in data integration and exchange, and they have been thoroughly studied in different data models. For graph data, however, mappings have been studied in a very restricted context that, unlike real-life graph databases, completely disregards the data they store. Our main goal is to understand query answering under graph schema mappings - in particular, in exchange and integration of graph data - for graph databases that mix graph structure with data. We show that adding data querying alters the picture in a very significant way.

As the model, we use data graphs: a theoretical abstraction of property graphs employed by graph database implementations. We start by showing a very strong negative result: using the simplest form of nontrivial navigation in mappings makes answering even simple queries that mix navigation and data undecidable. This result suggests that for the purposes of integration and exchange, schema mappings ought to exclude recursively defined navigation over target data. For such mappings and analogs of regular path queries that take data into account, query answering becomes decidable, although intractable. To restore tractability without imposing further restrictions on queries, we propose a new approach based on the use of null values that resemble usual nulls of relational DBMSs, as opposed to marked nulls one typically uses in integration and exchange tasks. If one moves away from path queries and considers more complex patterns, query answering becomes undecidable again, even for the simplest possible mappings.

I will discuss a notion of equivalence between two probabilistic systems introduced by Larsen and Skou in 89 called probabilistic bisimulation.

In particular, I will look at logical characterizations for this notion: the goal is to describe a logic such that two systems are bisimilar if and only if they satisfy the same formulas. This question goes all the way back to Hennessey and Millner for non probabilistic transition systems.

I will develop topological tools and give very general logical characterization results for probabilistic simulation and bisimulation.

Let $(X,T)$ be a one-dimensional invertible subshift. The symmetry group of $(X,T)$ is the group of all shift-commuting homeomorphisms $X$. In the larger reversing symmetry group of $(X,T)$, we also consider homeomorphisms $\Phi$ of $X$ where $\Phi \circ T= T^{-1}\circ \Phi$, also called lip conjugacies. We define a generalisation of the reversing symmetry group for higher dimensional shifts, and we find this extended symmetry group for two prototypical higher dimensional shifts, namely the chair substitution shift and the Ledrappier shift. Joint work with M. Baake and J.A.G Roberts.
–––––
French version: Les automorphismes généralisés des sous shifts.
Soit $(X,\mathbb Z^d)$ un soushift inversible. Nous définissons le groupe des automorphismes généralisés: c'est le normalisateur du groupe engendré par le shift dans le groupe d'homéomorphismes de $X$. Nous trouvons les automorphismes généralisés de deux shifts prototyiques: le pavage de la chaise et le soushift Ledrappier. En collaboration avec M. Baake et J.A.G Roberts.

The evaluation of queries is a central problem in database management systems. Given a query q and a database D the evaluation of q over D consists in computing the set q(D) of all answers to q on D. An interesting case is when the query is boolean (aka the model checking problem, where the answer to the query is either a “yes” or a “no”). Even for boolean query, the problem of computing the answer (with input q and D) is already PSpace-complete. For non-boolean queries, the size of the output can blow up to |D|^r, where r is the arity of q. It is therefore not always realistic to compute the entire set of solutions. Moreover, the time needed to construct the set might not reflect the difficulty of the task.

In this talk we will discuss query enumeration, that is outputting the solutions one by one. Two parameters enter in play, the delay and the preprocessing time. The delay is the maximal time between two consecutive output and the preprocessing time is the time needed to produce the first solution. We will investigate cases where the delay is constant (does not depend on the size of the database) and the preprocessing is linear (in the size of the database) i.e. constant delay enumeration after linear preprocessing. This is not always possible as this implies a linear model-checking. We will therefore add restriction to the classes of databases and/or queries such as bounded degree databases, tree-like structures, conjunctive queries…

The entropy of a language is a measure of its complexity and a well-studied dynamical invariant. I consider two related questions: for a given class of languages, can this parameter be computed, and what values can it take?

In 1D tilings (subshifts) of finite type, we have known how to compute the entropy for 30 years, and the method gives an algebraic characterisation of possible values. In higher dimension, a surprise came in 2007: not only is the entropy not computable in general, but any upper-semi-computable real number appears as entropy - a weak computational condition. Since then new works have shown that entropy becomes computable again with aditionnal mixing hypotheses. We do not know yet where the border between computable and uncomputable lies.

In this talk, I will explore the case of general subshifts (not of finite type) in any dimension, hoping to shed some light on the finite type case. I relate the computational difficulty of computing the entropy to the difficulty of deciding if a word belongs to the language. I exhibit a threshold in the mixing rate where the difficulty of the problem jumps suddenly, the very phenomenon that is expected in the finite type case.

This is a joint work with Silvère Gangloff and Cristobal Rojas.

Joint work with Zoltán Ésik University of Szeged, Hungary

We equip the collection of labeled posets (partially ordered sets), abbreviated l.p., with different operations: series product (concatenation of l.p), parallel product (disjoint union of posets), omega-power (concatenation of an omega sequence of the same poset) and omega-product (concatenation of an omega sequence of possibly different posets, which has therefore infinite arity). We select four subsets of these operations and show that in each case the equational theory is axiomatizable. We characterize the free algebras in the corresponding varieties, both algebraically as classes which are closed under the above operations as well as combinatorially as classes of partially ordered subsets. We also study the decidability issues when the question makes sense.

Nous munissons la collection des posets étiquetés (ensembles partiellement), en abrégé p.e., de différentes opérations: lproduit série (concaténation de p.e.), produit parallèle (union disjointe de p.e.), omega puissance (concaténation d'une omega suite du même p.e.) et omega produit (concaténation d'une omega suite de p.e., éventuellement différents, donc d'arité infinie. Nous distinguons quatre sous-ensembles parmi les opérations ci-dessus et nous montrons que dans chaque cas la théorie équationnelle est axiomatisable. Nous caractérisons les algèbres libres dans les variétiés correspondante aussi bien algébriquement en tant classes d'algèbres fermées pour les opérations ci-dessus et combinatoriquement en tant que classes de structures ordonnées. Nous étudions aussi les problèmes de décidabilité quand ils ont un sens.

In a one-counter automaton (OCA), one can produce a letter from some finite alphabet, increment and decrement the counter by one, or compare it with constants up to some threshold. It is well-known that universality and language inclusion for OCAs are undecidable. In this paper, we consider OCAs with counter observability: Whenever the automaton produces a letter, it outputs the current counter value along with it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are PSPACE-complete, thus no harder than the corresponding problems for finite automata. In fact, by establishing a link with visibly one-counter automata, we show that OCAs with counter observability are effectively determinizable and closed under all boolean operations.

In formal language theory, several different models characterize regular languages, such as finite automata, congruences of finite index, or monadic second-order logic (MSO). Moreover, several fragments of MSO have effective characterizations based on algebraic properties, the most famous example being the Schützenberger-McNaughton and Papert theorem linking first-order logic with aperiodic congruences. When we consider transducers instead of automata, such characterizations are much more challenging, because many of the properties of regular languages do not generalize to regular word functions. In this paper we consider functions that are definable by one-way transducers (rational functions). We show that the canonical bimachine of Reutenauer and Schützenberger preserves certain algebraic properties of rational functions, similar to the syntactic congruence for languages. In particular, we give an effective characterization of functions that can be defined by an aperiodic one-way transducer.

Program:

• (09h20 - 09h30) Opening
• (09h30 - 10h00) Serge Grigorieff : “Algorithmic randomness and uniform distribution modulo one”
• (10h00 - 10h30) Stéphane Demri : “Reasoning about data repetitions with counter systems”
• (10h30 - 11h00) Coffee Break
• (11h00 - 11h30) Michel Habib : “A nice graph problem coming from biology: the study of read networks”
• (11h30 - 12h00) Delia Kesner : “Completeness of Call-by-Need (A fresh view)”
• (12h00 - 12h30) Pierre Vial : “Infinite Intersection Types as Sequences: a New Answer to Klop's Problem”
• (12h30 - 14h00) Lunch (Buffon Restaurant - 17 rue Hélène Brion - Paris 13ème)
• (14h00 - 14h30) Verónica Becher : “Finite-state independence and normal sequences”
• (14h30 - 15h00) Brigitte Vallée : “Towards the random generation of arithmetical objects”
• (15h00 - 15h30) Valérie Berthé : “Dynamical systems and their trajectories”
• (15h30 - 16h00) Coffee Break
• (16h00 - 16h30) Nicolás Alvarez : “Incompressible sequences on subshifts of finite type”
• (16h30 - 17h00) Eugene Asarin : “Entropy Games”
• (17h00 - 18h00) Discussion about the future of LIA INFINIS

More details are available here.

Representations of braids as isotopy classes of laminations of punctured disks are related with a family of normal forms, which we call relaxation normal forms. Roughly speaking, every braid is identified with a picture on a punctured disk, and reducing step-by-step the complexity of this picture amounts to choosing a relaxation normal form of the braid.

We will study the right relaxation normal form, which belongs to this family of normal forms. We will show that it is regular, and that it is synchronously bi-automatic if and only if the braid group has 3 punctures or less.

A successful idea in the area of verification is to consider finite-state abstractions of infinite-state systems. A prominent example is the fact that many language classes satisfy a Parikh's theorem, i.e. for each language, there exists a finite automaton that accepts the same language up to the order of letters. Hence, provided that the abstraction preserves pertinent properties, this allows us to work with finite-state systems, which are much easier to handle.

While Parikh-style abstractions have been studied very intensely over the last decades, recent years have seen an increasing interest in abstractions based on the subword ordering. Examples include the set of (non necessarily contiguous) subwords of members of a language (the downward closure), or their superwords (the upward closure). Whereas it is well-known that these closures are regular for any language, it is often not obvious how to compute them. Another type of subword based abstractions are piecewise testable separators. Here, a separators acts as an abstraction of a pair of languages.

This talk will present approaches to computing closures, deciding separability by piecewise testable languages, and a (perhaps surprising) connection between these problems. If time permits, complexity issues will be discussed as well.

In this talk, we study a model computing relations over finite words, generalising one- and two-way transducers. The model, called two-way two-tape automaton, consists in a finite-state machine with two read-only tapes, each one with a reading head able to go both ways. We first emphasize its relation with 4-way automata, which recognize sets of two-dimensional arrays of letters called picture languages; such correspondence provides a proof of the undecidability of the model, and an example separating determinism and non-determinism. We then describe several techniques which, applied to our model, establish (non-)closure properties of the recognizable relations. Finally, the main result presented in this talk is that alternating two-way two-tape automata are not closed under complementation. The proof is a refinement of one of J. Kari for picture languages.

Joint work with Olivier Carton and Olivier Serre.

We study the classical problem of conjunctive query evaluation. This problem admits multiple formulations and has been studied in numerous contexts; for example, it is a formulation of the constraint satisfaction problem, as well as the problem of deciding if there is a homomorphism from one relational structure to another (which transparently generalizes the graph homomorphism problem).

We here restrict the problem according to the set of permissible queries; the particular formulation we work with is the relational homomorphism problem over a class of structures A, wherein each instance must be a pair of structures such that the first structure is an element of A. We present a comprehensive complexity classification of these problems, which strongly links graph-theoretic properties of A to the complexity of the corresponding homomorphism problem. In particular, we define a binary relation on graph classes and completely describe the resulting hierarchy given by this relation. This binary relation is defined in terms of a notion which we call graph deconstruction and which is a variant of the well-known notion of tree decomposition. We then use this graph hierarchy to infer a complexity hierarchy of homomorphism problems which is comprehensive up to a computationally very weak notion of reduction, namely, a parameterized form of quantifier-free reductions. We obtain a significantly refined complexity classification of left-hand side restricted homomorphism problems, as well as a unifying, modular, and conceptually clean treatment of existing complexity classifications, such as the classifications by Grohe-Schwentick-Segoufin (STOC 2001) and Grohe (FOCS 2003, JACM 2007).

After presenting this new advance, we will compare this line of research with another that aims to classify the complexity of the homomorphism problem where the second (target) structure is fixed, and that is currently being studied using universal-algebraic methods. We will also make some remarks on two intriguing variants, injective homomorphism (also called embedding) and surjective homomorphism.

This talk is mostly based on joint work with Moritz Müller that appeared in CSL-LICS ’14. In theory, the talk will be presented in a self-contained fashion, and will not assume prior knowledge of any of the studied notions.

9h30-9h45 welcome

9h45 Svetlana Puzynina 10h15 Sebastian Schoener 10h30 Célia Borlido 11h Thibault Godin 11h45 Benjamin Hellouin 12h15 Thomas Garrity

14h Olivier Carton 14h30 Sylvain Lombardy (LaBRI)– Démonstration du logiciel Vaucuson-R 15h30 Pablo Rotondo

Word equations are combinatorial equalities between strings of symbols, variables and functions, which can be used to model problems in a wide range of domains. While some complexity results for the solving of specific classes of equations are known, currently there does not exist any equation solver publicly available. Recently, we have proposed the implementation of such a solver based on Boolean satisfiability that leverages existing SAT solvers for this purpose. In this paper, we propose a new representation of equations on words having fixed length, by using an enriched graph data structure. We discuss the implementation as well as experimental results obtained on a sample of equations.

We consider deterministic automata which accept vectors of d integers for a fixed positive integer d. A deterministic automaton is then a finite representation of the sets of vectors it accepts. Many operations are particularly efficient with this representation, such as intersection of sets, testing whether two sets are equal or deciding whethersuch an automaton accepts a Presburger-definable set, that is a FO[+,<]-definable set over integers. We consider a similar problem for less expressive logics such as FO[<,0,moda] or \FO[+1,0,mod], where mod is the class of modular relations.

We state that it is decidable in time O(nlog(n)) whether a set of vectors accepted by a given finite deterministic automaton can be defined in the less expressive logic. The case of dimension 1 was already proven by Marsault and Sakarovitch. If the first algorithms gives a positive answer, the second one computes in time O(n^{3}log(n)) an existential formula in this logic that defines the same set. This improves the 2EXP time algorithm that can be easily obtained by combining the results of Leroux and Choffrut.

In this talk, it is intended to: -Introduce automata reading vectors of integers, -Present the logic FO[<,0,mod] over integers -Introduce classical tools relating automata to numbers. -Give an idea of how they can be applied to the above-mentionned problem.

We present in this work an alternative solution to perfect-information stochastic parity games. Instead of using the framework of μ-calculus, which hides completely the algorithmic aspect, we solve it by induction on the number of absorbing states.

We study an extension of FO^2[<], first-order logic interpreted in finite words in which only two variables are used. We adjoin to this language two-variable atomic formulas that say, 'the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables.

We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We also give an effective algebraic characterization of the properties expressible in this logic. This enables us to prove, among many other things, that our new logic has strictly less expressive power than full first-order logic FO[<].

This is joint work with Andreas Krebs, Kamal Lodaya, and Paritosh Pandya, and will be presented at LICS2016.

This PhD is about two natural extensions of Finite Automata: the 2-way FA (2FA) and the 2-way transducers (2T).

The 2FA are computably equivalent to FA, even in their nondeterministic (2NFA) variant. However, in the Descriptional Complexity area, some questions remain. Raised by Sakoda and Sipser in 1978, the question of the cost of the simulation of 2NFA by 2DFA is still open. In this manuscript I give an answer in a restricted case in which the nondeterministic choices of the 2NFA may occur at the border of the input only (2ONFA). I show that every 2ONFA can be simulated by a 2DFA of subexponential (but superpolynomial) size. Under the assumptions L=NL, this cost is reduced to the polynomial level. Moreover, I prove that the complementation, and the simulation by a halting 2ONFA is polynomial.

Classical transducers (1-way) are well-known and admit nice characterizations (rational relations, logic). But their 2-way variant (2T) is still unknown, especially the nondeterministic case. In this area, my manuscript gives a new contribution: a algebraic characterization of the relations accepted by 2NT when both the input and output alphabets are unary. It can be reformulated as follows: each unary 2NT is equivalent to a sweeping (and even rotating) 2T. I also show that the assumptions made on the size of the alphabets are required.

The study of word relations, as algebraic object, and their transitive closure is another subject considered in my phd. When the relation belongs to some low level class, we are able to set the complexity of its transitive closure. This quickly becomes uncomputable when higher classes are considered.

Weighted automata (WA) extend finite-state automata defining functions from the set of words to a semiring S. Recently, cost register automata (CRA) have been introduced as an alternative model to describe any function realised by a WA by means of a deterministic machine.

Regarding unambiguous WA over a group G, they can equivalently be described by a CRA whose registers take their values in G, and are updated by operations of the form X:=Y.c, with c in G and X,Y registers.

In this talk, I will give a characterisation of unambiguous weighted automata which are equivalent to cost register automata using at most k registers, for a given k. To this end, I will generalise two notions originally introduced by Choffrut for finite-state transducers: a twinning property and a bounded variation property, here parametrised by an integer k and that characterise WA/functions computing by a CRA using at most k registers.

This is a joint work with Pierre-Alain Reynier and Jean-Marc Talbot.

Matrices and matrix products play a crucial role in a representation and analysis of various computational processes. Unfortunately, many simply formulated and elementary problems for matrices are inherently difficult to solve even in dimension two, and most of these problems become undecidable in general starting from dimension three or four. Let us given a finite set of square matrices (known as a generator) which is forming a multiplicative semigroup S. The classical computational problems for matrix semigroups are:

• Membership (Decide whether a given matrix M belong to a semigroup S) and special cases such as: Identity (i.e if M is the identity matrix) and Mortality (i.e if M is the zero matrix) problems
• Vector reachability (Decide for a given vectors u and v whether exist a matrix M in S such that Mu=v)
• Scalar reachability (Decide for a given vectors u, v and a scalar L whether exist a matrix M in S such that uMv=L)
• Freeness (Decide whether every matrix product in S is unique, i.e. whether it is a code)

The undecidability proofs in matrix semigroups are mainly based on various techniques and methods for embedding universal computations into matrix products. The case of dimension two is the most intriguing since there is some evidence that if these problems are undecidable, then this cannot be proved using any previously known constructions. Due to a severe lack of methods and techniques the status of decision problems for 2×2 matrices (like membership, vector reachability, freeness) is remaining to be a long standing open problem. More recently, a new approach of translating numerical problems of 2×2 integer matrices into variety of combinatorial and computational problems on words and automata over group alphabet and studying their transformations as specific rewriting systems have led to a few results on decidability and complexity for some subclasses.

We introduce Sturmian colorings of regular trees, which are colorings of minimal unbounded factor complexity. Then, we classify Sturmian colorings into two families, namely cyclic and acyclic ones. We characterize acyclic Sturmian colorings in a way analogous to continued faction algorithm of Sturmian words. As for cyclic Sturmian colorings, we show that the coloring is a countable union of a periodic coloring, possibly union with a regular subtree colored with one color.

This is joint work with Seonhee Lim.

Une tuile de Wang est un carré dont les bords sont colorés. Étant donné un ensemble fini de tuiles de Wang, on cherche à savoir s'il est possible de paver le plan discret tout entier avec ces tuiles, en mettant une tuile par case de sorte que deux tuiles adjacentes aient la même couleur sur le bord qu'elles partagent. On s'intéresse plus particulièrement aux jeux de tuiles apériodiques, ceux pour lesquels un pavage existe, mais où il est impossible de paver le plan périodiquement. Ces jeux de tuiles sont une des briques de base de la majorité des résultats en dynamique symbolique multidimensionnelle.

Le premier jeu de tuiles apériodique trouvé par Berger avait 20426 tuiles, et le nombre de tuiles nécessaire a baissé progressivement jusqu'à ce que Culik obtienne en 1996 un jeu de 13 tuiles en utilisant une méthode due à Kari.

Avec Michael Rao, nous avons trouvé avec l'aide de plusieurs ordinateurs un jeu apériodique de 11 tuiles. Ce nombre est optimal : il n'existe pas de jeu apériodique de moins de 11 tuiles. Une des principales difficultés de cette recherche guidée par ordinateur est que nous cherchons une aiguille dans une botte de foin indécidable : il n'existe pas d'algorithme qui décide si un jeu de tuiles est apériodique.

Après une brève introduction au problème, je présenterai l'ensemble de 11 tuiles, ainsi que les techniques de théorie des automates et de systèmes de transitions qui ont permis de prouver (a) qu'il est apériodique, et (b) que c'est le plus petit.

An infinite language L determines an infinite word α if every string in L is a prefix of α. If L is regular, it is known that α must be ultimately periodic; conversely, every ultimately periodic word is determined by some regular language. We investigate other classes of languages to see what infinite words they determine, focusing on languages recognized by various kinds of automata.

Next, we consider prediction of infinite words by automata. In the classic problem of sequence prediction, a predictor receives a sequence of values from an emitter and tries to guess the next value before it appears. The predictor masters the emitter if there is a point after which all of the predictor's guesses are correct. We study the case in which the predictor is an automaton and the emitted values are drawn from a finite set; i.e., the emitted sequence is an infinite word.

The automata we consider are finite automata, pushdown automata, stack automata (a generalization of pushdown automata), and multihead finite automata, and we relate them to purely periodic words, ultimately periodic words, and multilinear words.

Two intimately related new classes of games are introduced and studied: entropy games (EGs) and matrix multiplication games (MMGs). An EG is played on a finite arena by two-and-a-half players: Despot, Tribune and the non-deterministic People. Despot wants to make the set of possible People’s behaviors as small as possible, while Tribune wants to make it as large as possible. An MMG is played by two players that alternately write matrices from some predefined finite sets. One wants to maximize the growth rate of the product, and the other to minimize it. We show that in general MMGs are undecidable in quite a strong sense. On the positive side, EGs correspond to a subclass of MMGs, and we prove that such MMGs and EGs are determined, and that the optimal strategies are simple. The complexity of solving such games is in NP ∩ coNP.

Joint work with Julien Cervelle, Aldric Degorre, Cătălin Dima, Florian Horn, and Victor Kozyakin.