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.

The CoLiS project aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analyzing shell scripts. The data structure that is manipulated by these scripts, namely the file system tree, is a complex one.

We plan to use feature trees as an abstract representation of file system tree transformations. We thus investigate an extension of these feature trees that includes the update operation, which expresses that two trees are similar except in a particular subtree where there might have been changes.

We show that the first-order theory of this algebra is decidable via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers.

We present the first combinatorial scheme for counting labelled 4-regular planar graphs through a complete recursive decomposition. More precisely, we show that the exponential generating function of labelled 4-regular planar graphs can be computed effectively as the solution of a system of equations, from which the coefficients can be extracted. As a byproduct, we also enumerate labelled 3-connected 4-regular planar graphs, and simple 4-regular rooted maps. Finally, we discuss how to obtain asymptotic results.

This is based on joint works with Marc Noy (UPC) and Clément Réquile (TU Wien)

In a 2012 paper, Richard Statman exhibited an inference system, based on second order monadic logic and non-terminating rewrite rules, that exactly types all strongly normalizable lambda-terms. We show that this system can be simplified to first-order minimal logic with rewrite rules, along the Deduction Modulo Theory lines.

We show that our rewrite system is terminating and that the conversion rule respects weak versions of invertibility of the arrow and of quantifiers. This requires additional care, in particular in the treatment of the latter. Then we study proof reduction, and show that every typable proof term is strongly normalizable and vice-versa.

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

We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.