I started my PhD in September 2012, jointly supervised by Thomas Colcombet in Paris 7 and Mikołaj Bojańczyk in Warsaw.

I defended on October 16th 2015, in Paris, at Université Paris 7 Denis Diderot.

I got the PhD diploma in both Paris and Warsaw, and my PhD dissertation got distinguished by the University of Warsaw.

There are four different ways to get into it:

Title

Committee

Summary


This thesis is a contribution to the study of quantitative models of automata, and more specifically of automata with counters and probabilistic automata. They have been independently studied for decades, leading to deep theoretical insights of practical value.
We investigate here two seemingly unrelated questions, the first about finite-memory determinacy for boundedness games, and the second about the value 1 problem for probabilistic automata. Some of the results are obtained by transferring techniques and ideas from one model to the other, revealing some connections between them.

The first part of this document investigates finite-memory determinacy for boundedness games, which is motivated by, and belongs to, a research program launched ten years ago by Bojanczyk and Colcombet, aiming at understanding boundedness logics; the so-called MSO + U and cost-MSO. These two logics induce two related models of games with counters, for which we show both positive and negative results about their finite-memory determinacy.
The main motivation for this investigation is the LoCo conjecture, stated by Colcombet and Loeding in 2010, and shown to imply the decidability of cost-MSO over infinite trees, which is the main open problem of this research program. We show that unfortunately the LoCo conjecture does not hold. On the positive side, we show a weaker statement: the LoCo conjecture holds for all thin tree arenas.

The second part of this document is about the value 1 problem for probabilistic automata. The starting point is the undecidability of this problem, which was proved in 2010 by Gimbert and Oualhadj. The aim of the results presented here is to understand to what extent is the value 1 problem undecidable, by constructing an algorithm that partially solves it and arguing that it is in some sense optimal.
The first step is the construction of the Markov Monoid algorithm, inspired by the notion of stabilisation monoids as introduced by Colcombet in the study of cost-MSO. We first prove that it is correct for a subclass of probabilistic automata that we define, called leaktight automata, relying on the notion of factorisation trees as developed by Imre Simon. We then show that all subclasses for which the value 1 problem was shown to be decidable are leaktight, implying that this algorithm is so far the best known algorithm.
The second step aims at better understanding the Markov Monoid algorithm, using a new framework that we introduce, called the prostochastic theory. The prostochastic theory is a topological approach for probabilistic automata inspired by the profinite theory as developed by Almeida, Pin, Weil and others for classical automata, and used by Torunczyk for the study of MSO + U. In this context, the value 1 problem reformulates at an emptiness problem, providing theoretical foundations for reasoning about the Markov Monoid algorithm. Our main result is to give a characterisation of the Markov Monoid algorithm using the prostochastic theory. It says that the Markov Monoid algorithm captures exactly all polynomial behaviours; the undecidability result shows that combining polynomial and exponential behaviours leads to undecidability. The combination of these two results supports the claim that the Markov Monoid algorithm is optimal.