I will present a hierarchy of fast-growing complexity classes and show its suitability for completeness statements of many non elementary problems, which occur naturally in logic, combinatorics, formal language, verification, etc., with complexities ranging from simple towers of exponentials to Ackermannian and beyond.

I plan to skim over the following topics:

1. subrecursive hierarchies: these are functions and classes that allow to define rapidly-growing functions by recursion over ordinal indices,¡/li¿
2. length function theorems for well-quasi-orders, which are the key combinatorial statements for the upper bounds of most of the non-elementary problems I will mention,¡/li¿
3. the definition of fast-growing complexity classes and some easy properties.

The recent results will be taken from work together with S. Abriola, D. Figueira, S. Figueira, C. Haase, S. Haddad, and Ph. Schnoebelen.

Linear recurrence sequences (such as the Fibonacci numbers) permeate a vast number of areas of mathematics and computer science (in particular: program termination and probabilistic verification), and also have many applications in other fields such as economics, theoretical biology, and statistical physics. In this talk, I will focus on three fundamental decision problems for linear recurrence sequences, namely the Skolem Problem (does the sequence have a zero?), the Positivity Problem (are all terms of the sequence positive?), and the Ultimate Positivity Problem (are all but finitely many terms of the sequence positive?).

This is joint work with James Worrell.

Green’s relations form a fundamental tool in the analysis of the structure of semigroups and monoids, in particular for the finite ones. Understanding Green’s relations can give remarkable intuitions concerning these objects, and as a consequence for understanding the structure of regular languages of words (finite or infinite). In particular, this description generalizes the understanding of automata through their decomposition into strongly connected components that is used in many proofs.

During this talk, I will present some of the key results concerning Green’s relations, emphasizing on how one can think about regular languages using them. I will also show how these can be used for deriving non-trivial automata related results (such as McNaughton’s determinization result, Schützenberger’s characterization of star-free languages, Simon’s factorization forest theorem, … though unfortunately I will not have time do to all these).

The counting ability of weak formalisms (e.g. determining the number of 1’s in a string of length N) is of interest as a measure of their expressive power, and also resorts to complexity theoretic motivations : the more we can count the closer we get to real computing power. The question was investigated in several papers in complexity theory and in weak arithmetic a long time ago. In each case, the considered formalism (constant-depth circuits, MSO with addition or first-order bounded arithmetic) was shown to be able to count up to a polylogarithmic number. An essential part of the proofs is the construction of a 1–1 mapping from a small subset of {0,…,N - 1} into a small initial segment. In each case the expressibility of this mapping depends on some strong and non-constructive argument (group theoretic device or prime number theorem).

In this talk we will evocate these different methods and present a completely elementary (and constructive) approach to reprove uniformly all these results (based on an old paper with M. More and C. Lautemann). We will also review why some of these results cannot be extended.

Machine learning guys do things like linear regression, neural networks and support vector machines. Logic guys do relational structures, formulas, automata and such stuff. These two type of guys hardly ever meet to work together. So few logic guys know that neural networks are sometimes considered with only binary weights and signals, which makes them exactly circuits. And few machine learning guys know quantitative logics good enough to recognize thier standard neural network in a formula. In this talk, I will define very basic concepts used in machine learning in a way that exposes their logic counterparts. I will then argue that such relationship can be beneficial for both fields - providing theorems and deeper understanding to machine learning and practically relevant questions and experimental results to logic.

What do you do if a computational object (e.g., a document, a program trace) fails a specification? An obvious approach is to perform a repair: modify the object minimally to get something that satisfies the constraints. This approach has been extensively investigated in the database community for relational integrity constraints, and in the AI community for propositional logics. Different modification operators have been considered on the basis of the application scenarios. For instance, a repair of an XML document usually consists of applying to the underlying tree structure a certain number of editing operations such as relabelings, deletions, and insertions of nodes. In this talk I will survey some results related to the worst-case cost of repairing documents between regular specifications. Precisely, I will focus on the number of edits that are needed to get from a document (i.e., a word or a tree) that satisfies a source specification (i.e., a regular language S) to some document that satisfies a target specification (i.e., a regular language T). As this number may well be unbounded, I will consider the problem of determining those pairs of languages (S,T) such that one can get from any word/tree in S to a word/tree in T using a finite, uniformly bounded number of editing operations. I will give effective characterizations of these pairs when S and T are given by finite state automata (word case) or stepwise tree automata (tree case), and derive some complexity bounds for the corresponding problems. Time permitting, I will also talk about the normalized repair cost; more specifically, about the problem of computing the worst-case repair cost between two languages S and T normalized by the length of the input word.

The presentation is based on joint works with Michael Benedikt, Cristian Riveros, Sławek Staworko, and Pierre Bourhis.

I am going to present a brand-new (about a week old) proof of the classic theorem of I. Simon showing the equivalence of piecewise testability of regular languages and J-triviality of the syntactic monoid. Mikolaj Bojanczyk and I found this proof while contemplating recent results, discovered independently by Czerwinski-Martens-Masopust and by van Rooijen-Zeitoun, which show that one can determine in polynomial time in the size of NFAs recognizing L and M, whether or not L and M can be separated by a piecewise testable language. (In particular, if M is the complement of L, this gives an efficient algorithm for determining if a given language is piecewise testable.) After giving the proof of Simon’s Theorem, I will explain this more general result.

Tree walking automata were introduced during the 70s as a model for describing regular languages of trees [AU77]. The run of such an automaton, instead of being a tree as for standard tree automata, form a path in the input tree. At each step of the run, the (unique) head of the automato is located in some node, and based on the current configuration of the tree and the current state of the automaton goes to one of the children of the current node, or go to the parent of the current node, and changes of states. Iterating this process, the automaton walks a path in the tree, possibly ending accepting the input tree. Tree walking automata are easy to show to define regular languages of finite trees.

In this talk, we will cover several subjects related to tree walking automata, including, the separation properties (deterministic tree walking automata are strictly weaker than non-deterministic ones [BC06], which in turn are strictly weaker than regular languages [BC08]) and closure properties (under complementation in particular [MSS06]). We will also present the models of pebble automata and relate it to first-order logic with transitive closure [EH99]. We will conclude with the separation of this logic from monadic logic over finite trees [BSSS06,BS10].

I will give a survey on my recent work with Bruno Courcelle concerning the expressive power of monadic second-order logic on certain graph classes. In particular, I will present our work on the transduction hierarchy, a classification of graph classes according to their encoding power with respect to transductions. I will also give an overview on more recent work on the definability of linear orderings on certain classes of graphs. Here we aim at simple combinatorial characterisations of whether such an ordering is definable or not.

In this talk I will prove that it is not possible to define a choice function in monadic second-order logic (MSO) over the infinite binary tree. Such a choice function would be given by a formula that has one free set variable and one free element variable, and for each non-empty set of nodes the formula becomes true for exactly one element from this set. This result has first been obtained by Gurevich and Shelah in 1983 using set theoretic methods. The proof presented in this talk is (in my opinion) much simpler, and is completely based on automata theoretic arguments.

A consequence of this result is that MSO-definable relations of infinite trees cannot be uniformized in MSO (where a uniformization of a binary relation is a function that is a subset of the relation and has the same domain as the relation). One can also use the result to show that there are nondeterministic automata on infinite trees that are not equivalent to an unambiguous automaton, i.e., an automaton that has at most one accepting run for each input.

To uniformize a binary relation means to find a partial function whose graph lies in the relation and whose domain coincides with that of the relation. Said differently it consists of selecting a unique image for each element of the domain. Depending on the class of relations, it is possible or not to uniformize the relations by functions in the same class.

I will not give a survey, rather talk of what I know of the topic, which is mainly binary rational relations over finite and infinite words and some connected problems.

In this talk, we will present the classical construction of Safra, which transforms non-deterministic Büchi automata to deterministic Rabin automata. We will adopt the point of view of modern presentations of this result (in particular of Schewe), and cover the lower bound results.

First, I will talk about Defender’s Forcing, a technique introduced by Jancar and Srba that is used for proving lower bounds in bisimilarity checking of infinite state systems, i.e. the problem, given two infinite state systems, to decide whether they are bisimilar. I plan to apply this simple but powerful technique to some classes of infinite state systems for which simple representations exist, such as for prefix-recognisable graphs, Petri Nets or PA processes.

Second, I will recall two classical results from complexity theory (i) PSPACE is serializable meaning roughly that for determining whether a word lies in a fixed PSPACE language one only needs to check if the yield (the leaf string) of the computation tree of an NP machine lies in a fixed regular language (ii) Converting a natural number in binary to its Chinese remainder representation is in NCˆ1. I plan to use these results for proving lower bounds for reachability problems and model checking problems for one-counter automata and timed automata, respectively.