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.