Compteurs et Aléas en Théorie des Automates
Nathanaël Fijalkow · HAL (Le Centre pour la Communication Scientifique Directe) · 2015
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 similarities 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 Bojańczyk 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, which we call uniform and non-uniform boundedness games. We first consider non-uniform boundedness games, which appear in the study of MSO + U, and present results aiming at characterising the memory requirements of a given condition, first for special cases of boundedness conditions, and then for general conditions under topological assumptions. We then consider uniform boundedness games, which appear in the study of cost-MSO. In 2010, Colcombet and Löding stated a conjecture about finite-memory determinacy for such games, that we call the LoCo conjecture. They proved that this conjecture implies 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 decidable, 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 Toruńczyk 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.