Mikołaj Bojańczyk

Thomas Colcombet

Antonin Kučera

Wolfgang Thomas

Nathalie Bertrand

Anuj Dawar

Damian Niwiński

Jean-Éric Pin

Paweł Urzyczyn

my coauthors, colleagues, family members and friends

Introduction 1 The origins

In the beginning was logic. A perfect match between automata and logics was discovered, leading to the notion of regularity. Automata theory expanded, and further investigations led to new theoretical tools; games is one of them. Among the various natural extensions of automata theory, adding quantitative aspects is a prominent one. We put a focus on one such quantitative aspect, namely boundedness questions. In this section, we discuss these three concepts: regularity, games, and quantitative extensions.

1.1 The Notion of Regularity in Automata Theory

The Ubiquity of Games

A milestone in the development of automata theory is Church's problem [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis[END_REF], also known as the circuit synthesis problem. The main conceptual novelty is due to McNaughton [START_REF] Mcnaughton | Finite-state infinite games[END_REF], who advocated setting this problem in the context of games. This idea is been picked up by Landweber, leading to what is today known as the Büchi-Landweber theorem [START_REF] Büchi | Definability in the Monadic Second-Order Theory of Successor[END_REF].

An instance of Church's problem is given by a specification, described for instance by a logical formula, and asks for the construction of a system satisfying this specification. The idea of McNaughton is to cast this as a game, in which two players have antagonistic goals. The game is played over a graph, called an arena, which represents the system; the first player, we call her Eve, represents the controller of the system, and her opponent, we call him Adam, represents the environment. The specification gives rise to a winning condition that Eve tries to ensure. Thus, the Church problem is equivalent to determining whether Eve has a winning strategy in the game, and to construct such a winning strategy.

In other words, an important conceptual contribution of McNaughton is to advocate the use of games as algorithmic back-ends to solve computational problems, such as Church's problem.

A second observation motivates the study of games for its applications to automata theory, this time not as an algorithmic back-end but as a theoretical tool. Indeed, studying the existence and shape of winning strategies gives a deep combinatorial insight into automata-theoretic problems.

The first achievement in this direction is the long list of simplifications of the complex and celebrated Rabin's Theorem [START_REF] Michael | Decidability of Second-Order Theories and Automata on Infinite Trees[END_REF], stating the decidability of monadic second-order logic over infinite trees.

The use of determinacy for automata constructions was first noticed by Büchi [START_REF] Büchi | Using Determinancy of Games to Eliminate Quantifiers[END_REF]; Gurevich and Harrington [START_REF] Gurevich | Trees, Automata, and Games[END_REF] went further by proving finite-state determinacy, that they called "forgetful determinacy". Emerson and Jutla found a strong relation between the parity conditions and the modal µ-calculus, allowing to a give a simple proof of the positionality of parity games [EJ88; EJ91]. Muller and Schupp gave a conceptually different proof of this result, which in particular gives a new proof of the determinisation for automata over infinite words [START_REF] Muller | Alternating Automata on Infinite Trees[END_REF][START_REF] Muller | Simulating Alternating Tree Automata by Nondeterministic Automata: New Results and New Proofs of the Theorems of Rabin, McNaughton and Safra[END_REF].

An important contribution of these works is to pinpoint the use of positional determinacy of parity games in the proof of Rabin's theorem. This result states the existence of positional winning strategies: if there exists a winning strategy, then there exists a very simple one, namely a positional winning strategy. We say that parity conditions are positionally determined; this type of results, called positionality results, or more generally finite-memory determinacy results, is central in many automata-theoretic constructions that came later, for instance for the equivalence between two-way and one-way automata [START_REF] Vardi | Reasoning about The Past with Two-Way Automata[END_REF], or for solving pushdown games [START_REF] Walukiewicz | Pushdown Processes: Games and Model-Checking[END_REF].

Boundedness Questions

The central object in automata theory is languages, i.e. qualitative properties: a structure (a word, a tree) is either in the language, or not. In order to extend the toolbox to a quantitative setting, different attempts have been made, to give automata the ability -for instance -to count or to randomise.

A general and widely studied approach is given by weighted automata as defined by Schützenberger [START_REF] Schützenberger | On the Definition of a Family of Automata[END_REF]. In this framework fits a number of important classes of quantitative models of automata, such as probabilistic automata (introduced independently by Rabin [START_REF] Michael | Probabilistic Automata[END_REF]) and distance automata.

The literature on quantitative extensions of automata theory is vast and still growing; We will now focus on one branch of this research area, specifically boundedness questions.

About ten years ago, Bojańczyk introduced the logic MSO `U [START_REF] Bojańczyk | A Bounding Quantifier[END_REF], to capture boundedness questions. A typical example of a boundedness question is: given a regular language L Ď ta, bu ˚, does there exist a bound N such that all words from L contain at most N occurrences of a?

The motivations for studying boundedness questions gets back to the 80s, when Hashiguchi, and then later Leung, Simon and Kirsten solved the star-height problem by reducing it to boundedness questions [START_REF] Hashiguchi | Improved Limitedness Theorems on Finite Automata with Distance Functions[END_REF][START_REF] Simon | On Semigroups of Matrices over the Tropical Semiring[END_REF][START_REF] Leung | Limitedness Theorem on Finite Automata with Distance Functions: An Algebraic Proof[END_REF][START_REF] Daniel | Distance Desert Automata and the Star-Height Problem[END_REF].

Over the last ten years, a lot of results have been obtained about the logic MSO `U and its close parent cost-MSO, introduced as part of the theory of regular cost functions by Colcombet [Col09;[START_REF] Colcombet | Regular Cost Functions, Part I: Logic and Algebra over Words[END_REF].

The results of this line of work come in two flavours: the first is reducing various problems to boundedness questions, and the second is obtaining decidability results for boundedness questions as formulated by variants of the logics MSO `U and cost-MSO.

For the first point, many problems have been reduced to boundedness questions. The first example is the star-height problem over words [Has90; Sim94; Leu91; Kir05] and over trees [START_REF] Colcombet | The Nesting-Depth of Disjunctive µ-Calculus for Tree Languages and the Limitedness Problem[END_REF]. A year later, Kirsten solved the finite substitution problem [START_REF] Daniel | A Burnside Approach to the Finite Substitution Problem[END_REF]. When Bojańczyk introduced MSO `U, one of his motivation was for solving the finite satisfiability of the modal µ-calculus with backward modalities. Recently, the boundedness question for fixed points of monadic formulae over finite and infinite words and trees have been cast as boundedness problems by Blumensath, Otto and Weyer [START_REF] Blumensath | Decidability Results for the Boundedness Problem[END_REF]. Last but not least, the most important problem that has been reduced is to a boundedness problem is to decide the Mostowski hierarchy for infinite trees [START_REF] Colcombet | The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata[END_REF]. The decidability of this problem remains open, as the corresponding boundedness question, namely boundedness of B-parity automata over infinite trees, is not known to be decidable.

For the second point, we review some of the most important results. The first paper by Bojańczyk introduces MSO `U and solves a fragment over infinite trees, not closed under negations [START_REF] Bojańczyk | A Bounding Quantifier[END_REF]. Two years later, Bojańczyk and Colcombet show the decidability of a bigger fragment closed under negations, over infinite words [START_REF] Bojańczyk | Bounds in ω-Regularity[END_REF]. From there, two paths emerge: the study of the weak variant of MSO `U led by Bojańczyk on one side, and the theory of regular cost functions and cost-MSO led by Colcombet on the other.

The logic weak MSO `U has been shown decidable over infinite words [START_REF] Bojańczyk | Weak MSO with the Unbounding Quantifier[END_REF], infinite trees [START_REF] Bojańczyk | Weak MSO+U over Infinite Trees[END_REF], and even with path quantifiers [START_REF] Bojańczyk | Weak MSO+U with Path Quantifiers over Infinite Trees[END_REF]. Quite recently, the non weak version had a tragic end, when Bojańczyk, Toruńczyk and Parys proved the undecidability of MSO `U over infinite words [START_REF] Bojańczyk | The MSO+U theory of (N, <) is Undecidable[END_REF].

The theory of regular cost functions, built around the logic cost-MSO, has been successfully developed over finite words [START_REF] Colcombet | The Theory of Stabilisation Monoids and Regular Cost Functions[END_REF][START_REF] Colcombet | Regular Cost Functions, Part I: Logic and Algebra over Words[END_REF] and finite trees [START_REF] Colcombet | Regular Cost Functions over Finite Trees[END_REF], yielding notions of regular expressions, automata, monoids and logics that all have the same expressive power, and that extend the standard notions. This led to decidability results for boundedness questions over finite words and trees.

Memory in Quantitative Games

The study of games in automata theory is motivated by two different objectives: the first is to use games as algorithmic back-ends, constructing powerful algorithms to determine the winner and synthesise winning strategies, the second is to use games as proof objects, proving the existence of positional or finite-memory winning strategies. They are often related; in the first chapter of this document, we will focus on the second objective, namely finite-memory determinacy issues, and study the class of quantitative games given by boundedness games. We discuss on this section these two lines of work: first, results characterising memory requirements, and second, the study of quantitative games. This leads us to the LoCo conjecture, which is the main motivation for the first chapter of this document.

Characterising Memory Requirements

Quantitative Games

There are two ways to make games quantitative:

• the first is to add quantitative features to the arenas, for instance randomised edges, inducing stochastic arenas,

• the second is to consider quantitative conditions, for which a play is not winning or losing, but is assigned a value, that one player tries to minimise or maximise.

For the first approach, we just mention one interesting example. Stochastic games were introduced by Shapley [START_REF] Shapley | Stochastic Games[END_REF]; Condon investigated the case of stochastic reachability games and proved several properties about them, in particular their positional determinacy [START_REF] Condon | The Complexity of Stochastic Games[END_REF]. Later, Zwick and Paterson considered mean-payoff and discounted games: the arenas are deterministic (they do not have randomised edges), but the conditions are quantitative, as they assign to a play the limit (or discounted limit) of the average weights along the play. Zwick and Paterson showed that both types of games are positionally determined, and used this result to reduce them to the stochastic games of Condon [START_REF] Zwick | The Complexity of Mean-Payoff Games on Graphs[END_REF]. This is an interesting example where one approach reduces to the other: considering quantitative conditions can be reduced to qualitative conditions over stochastic arenas.

The second approach, considering quantitative conditions, has been quite popular recently. We distinguish two aims: either the quantitative aspect is used to refine a qualitative specification, or the quantitative aspect is used to specify a quantitative behaviour, combined with an independent qualitative specification.

We give an example of the first aim. Linear temporal logic is a powerful formalism to express qualitative specifications; for instance, one can specify that a request is eventually granted. Three quantitative counterparts have been introduced to further specify the existence of a time bound between requests and their grants. The first are the finitary conditions introduced by Alur and Henzinger [START_REF] Alur | Finitary Fairness[END_REF], then parametric linear temporal logic, defined by Alur, Etessami, La Torre and Peled [START_REF] Alur | Parametric Temporal Logic for Model Measuring[END_REF], and its fragment prompt linear temporal logic, introduced by Kupferman and Vardi [START_REF] Kupferman | From Liveness to Promptness[END_REF]. In these three approaches, the quantitative aspect aims at giving a numerical account of "how well" is the specification satisfied.

Games with finitary conditions have been studied by Henzinger, Chatterjee and Horn, leading to surprisingly effective algorithms [START_REF] Chatterjee | Finitary Winning in omega-regular Games[END_REF]. The PhD thesis of Zimmermann studies games with parametric linear temporal logic conditions [START_REF] Zimmermann | Solving Infinite Games with Bounds[END_REF], both by proving finite-memory determinacy and by constructing algorithms to determine the winner.

There are several examples of conditions combining an independent qualitative aspect and a quantitative aspect in the literature. We mention for instance energy parity games [START_REF] Chatterjee | Energy Parity Games[END_REF] and mean-payoff parity games [START_REF] Chatterjee | Perfect-Information Stochastic Mean-Payoff Parity Games[END_REF]. In these two examples, the parity condition serves as an abstraction for a qualitative specification, and either the mean-payoff or the energy condition serves an abstraction for a quantitative specification.

The LoCo Conjecture

The theory of regular cost functions has been successfully developed for finite and infinite words, and for finite trees, leading to decidability results for the logic cost-MSO over these structures.

However, extending this theory to infinite trees in order to prove the decidability of the logic cost-MSO seems to be much harder. One motivation for this extension is a result of Colcombet and Löding, which reduces the index problem of the Mostowski hierarchy to the decidability of cost-MSO over infinite trees [START_REF] Colcombet | The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata[END_REF]. This problem is open for over forty years; the deterministic case was solved, and recently extended to the case of game automata [START_REF] Facchini | Rabin-Mostowski Index Problem: A Step beyond Deterministic Automata[END_REF]. The approach through regular cost functions allowed to solve the special case of weak definability for Büchi languages [START_REF] Colcombet | Deciding the weak definability of Büchi definable tree languages[END_REF].

Colcombet and Löding pointed out that the only missing point to obtain the decidability of cost-MSO over infinite trees is a finite-memory determinacy result for boundedness games. Boundedness games are quantitative games involving a finite set of counters; their conditions are conjunctions of a parity condition and a condition requiring that the counter values remain bounded along the play.

Colcombet and Löding conjectured that there exists a trade-off between the size of the memory and the bound achieved on the counters [START_REF] Colcombet | Fonctions Régulières de Coût[END_REF], which we call the LoCo conjecture.

So far, this conjecture resisted both proofs and refutations, and the only non-trivial positive case known is due to Vanden Boom [START_REF] Vanden | Weak Cost Monadic Logic over Infinite Trees[END_REF], which implied the decidability of the weak variant of cost-MSO over infinite trees, later generalised to quasi-weak cost-MSO in [START_REF] Blumensath | Two-Way Cost Automata and Cost Logics over Infinite Trees[END_REF]. Unfortunately, quasi-weak cost-MSO is strictly weaker than cost-MSO, and this leaves open the question whether cost-MSO is decidable.

The first chapter of this document, "Finite-memory Determinacy for Boundedness Games", investigates further the LoCo conjecture.

Probabilistic Automata

Probabilistic automata have been introduced by Rabin [START_REF] Michael | Probabilistic Automata[END_REF], as a very simple randomised computation model. It has been broadly studied for both its theoretical and practical values; in particular, it is used in various fields such as computational biology, linguistics and image processing.

In this section, we are interested in the algorithmic properties of probabilistic automata: given a probabilistic automaton, what can be said about its behaviour, in an effective way?

We first discuss some algorithmic questions that appeared in the seminal paper of Rabin. These are quantitative problems: they ask for the behaviours of a given probabilistic automaton, comparing the acceptance probabilities to numerical thresholds. This set of questions led to several developments over the last forty years, which unfortunately are almost all undecidability results, supporting the claim that quantitative problems for probabilistic automata are undecidable.

Hence we take a different path and discuss a recent work of Gimbert and Oualhadj, who considered a qualitative problem, the value 1 problem. The second chapter of this document continues this line of work, aiming at a better understanding of the value 1 problem.

Algorithmic Properties for Probabilistic Automata

The first result about algorithmic properties of probabilistic automata precedes the introduction of probabilistic automata. Indeed, while studying weighted automata, Schützenberger proved that the equivalence between two weighted automata is decidable, provided the underlying semiring is a field [START_REF] Schützenberger | On the Definition of a Family of Automata[END_REF]. This applies to probabilistic automata, as the underlying semiring is the reals with addition and multiplication. Later, a different polynomial time algorithm was given by Tzeng [START_REF] Tzeng | A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata[END_REF]. Recently, this problem has been further analysed, leading to very efficient randomised algorithms, with applications to software verification [KMOWW11; KMOWW12; KMOWW13].

When Rabin introduced probabilistic automata, he showed how they can be used to define languages: a probabilistic automaton defines the language consisting of the set of words accepted with probability at least one half. The threshold one half is not special, any rational threshold between 0 and 1 leads to an equivalent notion of probabilistic languages. This motivated the first algorithmic question:

(1) can we decide if a probabilistic language is empty, i.e. if there exists a word accepted with probability at least one half? Rabin first observed that probabilistic languages strictly subsume regular languages, and gave a sufficient condition for a probabilistic automaton to define a regular language, using the notion of isolated thresholds.

The threshold one half is said isolated if there exists an interval around it such that for all words, their probability to be accepted lie outside this interval. In other words, Rabin showed that if no complicated convergence phenomenon occurs around the threshold one half, then the language is regular. This motivated the second and third algorithmic questions:

(2) can we decide if a probabilistic automaton defines a regular language?

(3) can we decide if for a probabilistic automaton, the threshold one half is isolated, i.e. if there exists a sequence of words accepted with probability arbitrarily close to one half?

Undecidability of Quantitative Problems

The first question was answered by Paz: the emptiness problem for probabilistic languages is undecidable [START_REF] Paz | Introduction to Probabilistic Automata[END_REF].

This undecidability result says that asking to precisely compare to a threshold is too much to ask. A probabilistic automaton may exhibit complicated behaviours that happen very close to the threshold, and this implies the undecidability.

Bertoni answered the second question, using a similar reduction: the regularity problem is undecidable [START_REF] Bertoni | Mathematical Methods of the Theory of Stochastic Automata[END_REF].

The third question asks whether there is a convergence phenomenon towards the threshold, without trying to determine whether it goes beyond the threshold. Unfortunately, Bertoni showed that the isolation problem is also undecidable [START_REF] Bertoni | The Solution of Problems Relative to Probabilistic Automata in the Frame of the Formal Languages Theory[END_REF][START_REF] Bertoni | Some Recursive Unsolvable Problems Relating to Isolated Cutpoints in Probabilistic Automata[END_REF], answering the third question. This means that not only determining if a word exceeds the threshold is undecidable, but also determining whether it is approached at all is also undecidable.

A simpler question is the following bounded-error emptiness problem, which asks for the construction of an algorithm with the following behaviour; given a probabilistic automaton as input:

• if there exists a word accepted with probability at least two thirds, then accept,

• if all words are accepted with probability at most one third, then reject,

• in any other case, any answer is fine, including no answer at all. In this problem, there is no convergence phenomena involved: what happens between the thresholds one third and two thirds is not relevant. Condon and Lipton gave the coup de grâce: there exists no algorithm solving the bounded-error emptiness problem [START_REF] Condon | On the Complexity of Space Bounded Interactive Proofs (Extended Abstract)[END_REF].

We comment on the term quantitative problem: it refers here to the idea that the emptiness problem, the isolation problem and the bounded-error emptiness problem all involve numerical thresholds, like one half, one third or two thirds, and comparisons with these thresholds. A priori, an algorithm solving a quantitative problem needs to deal with numerical values, and maybe approximations of them, which may be intrinsically hard.

The bounded-error emptiness seems to be the "easiest" quantitative problem, and its undecidability hints at the sad conclusion that all quantitative problems for probabilistic automata are undecidable.

On the opposite, a qualitative problem does not involve any numerical thresholds. Following the above intuition, qualitative problems should be easier than quantitative problems.

The Value 1 Problem

Gimbert and Oualhadj considered in 2010 the following qualitative problem, which they called the value 1 problem: given a probabilistic automaton, does there exist a sequence of words accepted with probability arbitrarily close to 1? (Similar problems have been considered for stochastic games, see for instance [START_REF] De Alfaro | Concurrent Omega-Regular Games[END_REF], where it is called "limit winning".) Their first contribution was to prove that this problem is undecidable [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF].

There are several reasons that make this problem interesting and worth further investigations.

First of all, it is very simple, and asks about a convergence phenomenon in a qualitative way: it does not involve comparisons with any precise threshold other than 1. As such, it is a good stepping stone to construct partial algorithms to determine properties of probabilistic automata. Indeed, the undecidability proof involves probabilistic automata with a complex structure, leaving some hope that these behaviours are rare and that it is possible to construct algorithms that solve the value 1 problem in most cases.

As it turned out later, the value 1 problem appeared in a different context, as the emptiness of probabilistic Büchi automata with positive semantics [START_REF] Baier | Probabilistic ωautomata[END_REF]. The two problems are Turing-equivalent [START_REF] Chadha | Probabilistic Automata with Isolated Cut-Points[END_REF].

Besides proving that the value 1 problem is undecidable, Gimbert and Oualhadj also constructed a subclass of probabilistic automata, called 7-acyclic, and showed that the value 1 problem is decidable when restricted to this subclass.

This led to further developments, and in particular to the second chapter of this document, "The Value 1 Problem for Probabilistic Automata". This question has also been considered for more expressive models, such as probabilistic timed automata [START_REF] Bertrand | Deciding the Value 1 Problem for Reachability in 1-Clock Decision Stochastic Timed Automata[END_REF].

Last but not least, the value 1 problem can be cast as an (un)boundedness question for probabilistic automata; this informal observation is the missing link between the two chapters of this document. 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.

Chapter 1

Finite-memory Determinacy for Boundedness Games

This first chapter deals with boundedness games, which are games with counters equipped with conditions requiring that the values of the counters remain bounded. The problem we tackle here is the finite-memory determinacy for such games: "Does there exist finite-memory winning strategies for boundedness games?" This question comes in several variants, depending on the conditions and the structural properties of the underlying arenas. In 2010, Colcombet and Löding stated a conjecture, that we call the LoCo conjecture, asserting the existence of finite-memory strategies in uniform boundedness games, and proved that this conjecture implies the decidability of cost-MSO over infinite trees. This conjecture has been the main motivation for all the results presented in this chapter.

In Section 1, we define boundedness games, which can be uniform and non-uniform. The non-uniform variant originates from the study of MSO `U, and the uniform variant from the study of cost-MSO. We discuss further the relation between the two definitions: we show that for games played over pushdown arenas, both definitions are equivalent, a result obtained in collaboration with Krishnendu Chatterjee in [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF].

We define finite-memory strategies in Section 2, and state finite-memory determinacy questions for boundedness games. We present in this section two sets of results about these questions.

In the first set of results, we take as a starting point the finitary parity games studied by Chatterjee, Henzinger and Horn [START_REF] Chatterjee | Finitary Winning in omega-regular Games[END_REF], which are a special case of non-uniform boundedness games. We extend their results in two directions: first by considering the cost-parity games, which generalise at the same time parity games and finitary parity games, in collaboration with Martin Zimmermann [FZ12;[START_REF] Fijalkow | Cost-Parity and Cost-Streett Games[END_REF], and second by considering finitary parity games played over infinite arenas, in collaboration with Krishnendu Chatterjee in [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF].

The second set of results is a characterisation of the memory requirements for topologically closed conditions, obtained in collaboration with Thomas Colcombet and Florian Horn [START_REF] Colcombet | Playing Safe[END_REF]. This allows to obtain tight memory bounds for several conditions, and in particular applies to a special case of uniform boundedness conditions.

We state the LoCo conjecture in Section 3. We show that it implies the equivalence between alternating and non-deterministic B-parity automata, as introduced in the theory of regular cost functions by Colcombet [Col09;[START_REF] Colcombet | Regular Cost Functions, Part I: Logic and Algebra over Words[END_REF]. A closer analysis at how the LoCo conjecture is used to prove this result allows to state a refined LoCo conjecture taking into account the structural properties of the arenas.

In Section 4, we give a state of the art on this conjecture and show new examples. We then explain how the slicing technique developed by Vanden Boom in [START_REF] Vanden | Weak Cost Monadic Logic over Infinite Trees[END_REF] to prove a special case of the LoCo conjecture allowed to obtain a positionality for stochastic games, which was the main contribution of [START_REF] Fijalkow | Emptiness Of Alternating Tree Automata Using Games With Imperfect Information[END_REF], in collaboration with Sophie Pinchinat and Olivier Serre.

In Section 5, we show that the LoCo conjecture does not hold, by constructing a counter example. The counter example is defined over a sequence of finite arenas, and is extended to show that non-uniform boundedness games are not finite-memory determined. On the positive side, we show in Section 6 that the LoCo conjecture holds for games played over thin tree arenas. The proof involves structural decompositions of thin tree and word arenas.

Both the counter example and the case of thin tree arenas are joint work with Florian Horn, Denis Kuperberg and Michał Skrzypczak [START_REF] Fijalkow | Trading Bounds for Memory in Games with Counters[END_REF].

We conclude in Section 7.

Boundedness Games

This section gives the definitions used throughout this chapter. We define games in Subsection 1.1, and boundedness conditions in Subsection 1.2.

As we will see, a fine point in this definition is whether the bound on these counters is uniform over all plays, as in the study of cost-MSO, or non-uniform, as it is the case for MSO `U. We discuss this further in Subsection 1.3.

We then report on our first contribution in Subsection 1.4, which an equivalence result between the uniform and non-uniform variants for games played over pushdown arenas, obtained in collaboration with Krishnendu Chatterjee and published in [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF].

Games

The model of games we consider is closely connected to the study of automata. Most of our definitions are standard, and taken from the book [START_REF]Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF].

The games are played by two players, Eve and Adam, over potentially infinite graphs called arenas.

Definition 1 (Arena)

An arena G is given by a directed graph pV, Eq whose vertex set is divided into vertices controlled by Eve (V E ) and vertices controlled by Adam (V A ), and a colouring function c : E Ñ A, where A is a finite alphabet.

The colouring function c : E Ñ A will be used by the winning condition. Note that sometimes, the colouring function is c : V Ñ A. When the arena is given without the colouring function, we talk about the underlying graph.

In Figure 1 we present a finite arena. The vertices controlled by Eve are drawn as circles, the vertices controlled by Adam are drawn as squares.

For the following definitions, fix an arena G. A token is initially placed on a given initial vertex v 0 , and the player who controls this vertex pushes the token along an edge, reaching a new vertex; the player who controls this new vertex takes over, and this interaction goes on forever, describing an infinite path Figure 1: A finite arena (without any colouring function). called a play. We assume that the arenas contain no dead ends: for every vertex v P V , there exists at least one edge pv, v 1 q P E.

Definition 2 (Play)

A play is a finite or infinite path, seen as a sequence of edges.

Plays are typically denoted π. Note that plays are sequences of edges, but sometimes it is technically convenient to consider only the induced sequences of vertices. As a convention, a play denoted π " e 0 ¨e1 ¨¨¨is a sequence of edges, and a play denoted π " v 0 ¨v1 ¨¨¨is a sequence of vertices.

Definition 3 (Strategy)

A strategy for Eve is a mapping σ :

E ˚¨V E Ñ E.
A strategy takes as input the history played so far and the current vertex, and outputs the next edge. We say that a play π " e 0 ¨e1 . . . is consistent with σ if e n`1 " σpe 0 ¨¨¨e n ¨vn q for every n with v n P V E .

From now on, the definitions that we give of winning conditions and games are qualitative, i.e. a play is either won or lost by Eve. In the next subsection, we will define quantitative winning conditions and games.

Informally speaking, a winning condition (or simply: condition) is a set of plays. The plays in the condition are called the winning plays for Eve, the other plays are winning for Adam. A strategy is winning for a condition, or ensures this condition, if all plays consistent with the strategy belong to the condition. The formal definition is slightly more complicated, in order to reason about conditions abstractly.

Definition 4 (Winning condition)

A condition over an alphabet A is a subset W Ď A ω .

Given an arena G and a condition W , we define the following set of plays:

tπ " e 0 ¨e1 ¨¨¨| cpe 0 q ¨cpe 1 q ¨¨¨P W u, to be the set of winning plays for Eve.

Although conditions are not formally sets of plays, we will often abuse notations and say that a play π " e 0 ¨e1 ¨¨¨satisfies a condition W Ď A ω , meaning that cpe 0 q cpe 1 q ¨¨¨P W .

Definition 5 (Game)

A game is given by an arena G and a condition W . Such a game is denoted pG, W q.

For a game pG, W q, we denote Win E pG, W q the winning region of Eve, i.e. the set of vertices from which Eve has a winning strategy. When G is clear from the context, we write Win E pW q.

All these definitions can be transposed for Adam. A strategy for Adam is usually denoted τ , and Win A pG, W q is the winning region of Adam.

Note that Win E pG, W q X Win A pG, W q " H. If Win E pG, W q Y Win A pG, W q " V , we say that the game is determined: from any vertex, either Eve has a winning strategy, or Adam has a winning strategy. All the games we will consider in this document are determined, as we will only consider Borel conditions [START_REF] Martin | Borel determinacy[END_REF]. When stating results about general conditions, we will always (implicitly) assume that the condition is Borel, to use the fact that the underlying games are determined.

We now define the classical ω-regular conditions.

Definition 6 (ω-regular condition)

• The parity condition with d `1 colors is defined over the alphabet A " t0, . . . , du, by: Parity " tc 0 ¨c1 ¨c2 ¨¨¨| maxpinftc i | i P Nuq is evenu, in words, it requires that the maximum color seen infinitely often is even.

• The Büchi condition is the special case of the parity condition over the alphabet A " t1, 2u, denoted Büchi.

• The CoBüchi condition is the special case of the parity condition over the alphabet A " t0, 1u, denoted CoBüchi.

• The reachability condition is defined over the alphabet A " t0, 1u, by:

Reach " tc 0 ¨c1 ¨c2 ¨¨¨| Di P N, c i " 1u.

• The safety condition is defined over the alphabet A " t0, 1u, by: Safe " tc 0 ¨c1 ¨c2 ¨¨¨| @i P N, c i " 0u.

As a convention, the colouring function of the parity condition is denoted Ω : V Ñ t0, . . . , du. We will sometimes use partial colouring functions for the parity condition; what matters is that every infinite play contains infinitely many coloured vertices, which will always be the case.

For a Büchi condition, we define F " tv P V | cpvq " 2u, and call F the set of Büchi vertices; the Büchi condition requires to see F infinitely many times. Similarly, for a CoBüchi condition, we define F " tv P V | cpvq " 1u, and call F the set of CoBüchi vertices; the Büchi condition requires to see F finitely many times.

For both reachability and safety conditions, we define F " tv P V | cpvq " 1u. The reachability condition requires to see F at least once, and the safety condition never to see F at all.

Boundedness Games

We now introduce counters and the boundedness conditions, which are quantitative conditions, i.e. functions f : A ω Ñ N Y t8u.

Definition 7 (B and B-parity conditions)

The quantitative B condition with k counters is defined over the alphabet A " tε, i, ru k . The counters take integer values, initialized at 0. The actions are:

• increment by 1, denoted i,

• reset to 0, denoted r,

• leave unchanged, denoted ε.

The function B :

A ω Ñ N Y t8u assigns to a sequence s the supremum of the values of all counters along the sequence.

The quantitative B-parity condition with d `1 colors and k counters is defined over the alphabet A " t0, . . . , du ˆtε, i, ru k . The function B X Parity : A ω Ñ N Y t8u assigns to a sequence s " pc 0 , a 0 q ¨pc 1 , a 1 q ¨pc 2 , a 2 q ¨¨¨:

# 8 if c 1 ¨c2 ¨¨¨R Parity Bpa 0 ¨a1 ¨a2 ¨¨¨q otherwise.
A quantitative condition f : A ω Ñ N Y t8u gives rise to two conditions:

• the uniform condition W pN q " ts P A ω | f psq ď N u,
• the non-uniform condition W " ts P A ω | f psq ă 8u.

We say that the condition W pN q is uniform, because a strategy ensuring this condition ensures the same bound N for all plays. On the opposite, the condition W is non-uniform, because a strategy ensuring this condition ensures a different bound for each play.

The two conditions induced by the quantitative B-parity conditions are denoted BpN q X Parity (uniform) and B X Parity (non-uniform).

We consider particular cases of B-parity conditions, as for instance B-Büchi conditions or B-CoBüchi conditions. In the special case of B-reachability conditions, denoted B Until Reach, we assume that the game stops when it reaches F .

A colouring function for the B-parity condition is usually given by two functions Ω : V Ñ t0, . . . , du and c : E Ñ tε, i, ru k .

Definition 8 (Boundedness game)

The B-parity games are called boundedness games.

Boundedness games have been given a lot of different names: the uniform variants have been called cost-games, cost-parity games, B-parity games or B games, and the non-uniform variants ωB-games.

Uniform and Non-Uniform

We explain in this subsection the distinction between uniform and non-uniform bounds, which comes from the study of MSO `U and cost-MSO. We here define both logics over infinite trees, but the definition also applies to infinite words, and to finite or infinite trees for cost-MSO.

We fix an alphabet A. An A-labelled (complete binary) tree is a function t : t0, 1u The logic MSO `U was introduced by Bojańczyk in 2004 [START_REF] Bojańczyk | A Bounding Quantifier[END_REF]. It is an extension of MSO, with a B quantifier (we will define B rather than U, which is equivalent as they are dual); we assume the reader to be familiar with MSO, see for instance [START_REF]Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF].

Consider φpXq an MSO formula using a free second-order variable X, ranging over sets of nodes. We define the syntactic construction BpXq φpXq, whose semantics is as follows:

BpXq φpXq " DN P N, @X, φpXq ùñ |X| ď N . In words, the formula BpXq φpXq holds for a tree t if there exists a bound N P N such that if t satisfies φpXq, then X has size at most N .

A typical example is the formula BpXq " @x, y, z, x ă y ă z ^x P X ^z P X ùñ y P X ^@x, apxq.

Here the symbol ă is interpreted as the descendant relation in the tree, so x ă y holds if y is a descendant of x. This formula states that there exists a bound N , such that all connected sets X that contain only a's have size at most N . The semantics is Boolean: a tree t either satisfies or does not satisfy a given MSO `U formula. Hence the following decision problem:

Finite-memory Determinacy for Boundedness Games Problem 1 (Satisfiability of MSO `U)

Given an MSO `U formula φ, does there exist a tree t that satisfies φ? Note that a formula in MSO`U can using several nestings of this B quantifier, together with first-and second-order quantifications. Consider for instance a formula of the form @X, BpY q φpX, Y q. Unravelling the semantics, we obtain:

@X, DN P N, @Y, φpX, Y q ùñ |Y | ď N .
Here, if a tree t satisfies this formula, the bound N (a priori) depends on X: for every X, there exists a different N . This non-uniform behaviour makes the problem very hard.

Bojańczyk conjectured in 2004 that the satisfiability problem for MSO `U was decidable, even over infinite trees [START_REF] Bojańczyk | A Bounding Quantifier[END_REF]. Quite recently (February 2015), this conjecture has been disproved by Bojańczyk, Parys and Toruńczyk:

Theorem 1 (Undecidability of MSO `U over infinite words [START_REF] Bojańczyk | The MSO+U theory of (N, <) is Undecidable[END_REF])

The satisfiability problem for MSO `U over infinite words is undecidable.

The logic cost-MSO was introduced by Colcombet in 2009 [START_REF] Colcombet | The Theory of Stabilisation Monoids and Regular Cost Functions[END_REF]. It also extends MSO, with the syntactic construction |X| ď N.

The atomic formula |X| ď N can appear in different places in a cost-MSO formula, but always positively, i.e. under the scope of an even number of negations, and with the same variable N.

The semantics of a cost-MSO formula assigns a value in N Y t8u to a tree, which is the smallest N P N such that t satisfies φ where the variable N is substituted by the value N . So instead of defining a language, as MSO and MSO `U, a cost-MSO formula defines a function from the set of trees to N Y t8u.

The main decision problem for cost-MSO is the boundedness problem:

Problem 2 (Boundedness of cost-MSO)

Given a cost-MSO formula φ, does there exist N P N such that all trees t satisfy φ with the value N ? Unlike MSO `U, the same bound N applies to all trees. This uniform behaviour makes the problem easier. In particular, the undecidability result mentioned above does not imply anything for cost-MSO.

From Non-Uniform to Uniform for Pushdown Arenas

This subsection reports on a result obtained in collaboration with Krishnendu Chatterjee, published in [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF]. The aim is to understand when are the uniform and non-uniform B-parity conditions equivalent.

We have:

Bp0q X Parity Ď Bp1q X Parity Ď Bp2q X Parity Ď ¨¨¨Ď B X Parity.
Consider an arena G with the colouring function given as two functions Ω : V Ñ t0, . . . , du and c : E Ñ tε, i, ru k . Denoting Win E pN q for Win E pG, BpN q X Parityq and Win E for Win E pG, Bq X Parityq, it follows that:

Win E p0q Ď Win E p1q Ď Win E p2q Ď ¨¨¨Ď Win E .
Hence the question: does there exist N such that Win E pN q " Win E , i.e. does this hierarchy collapse?

We denote limBpN q the condition requiring that a suffix of the play satisfies the condition BpN q. The complement of limBpN q is closed under suffixes, which implies interesting properties for strategies ensuring this condition.

Lemma 1 (Winning regions of suffix-closed conditions are traps) Consider a game pG, W q where W is closed under suffixes: for π a finite play and π 1 an infinite play, if π ¨π1 P W , then π 1 P W .

Let σ be a winning strategy, then all plays consistent with σ remain in Win E pG, W q.

Proof. Assume towards contradiction that there exists a strategy σ ensuring W , and a play consistent with this strategy that at some point leaves Win E pG, W q, and reaches a vertex v P V zWin E pG, W q " Win A pG, W q. Denote by π this finite play. By definition, there exists a strategy τ of Adam that from v ensures that W is not satisfied. Consider the play from there consistent with both σ and τ , denote it π 1 . Since σ is winning, we have π ¨π1 P W , and since τ ensures the complement of W , we have π 1 R W , contradicting that W is closed under suffixes.

We first consider the case of finite arenas.

Theorem 2 (Collapse over finite arenas)

For all boundedness games played over a finite arena, for all initial vertices, the following are equivalent:

• Dσ strategy for Eve, @π plays, DN P N, π P BpN q X Parity,

• Dσ strategy for Eve, DN P N, @π plays, π P limBpN q X Parity.

Proof. We argue that the following two properties hold:

1. there exists N such that Win E pN q " Win E pN `1q " ¨¨¨,

for such N , we have Win

A pN q Ď Win A , hence Win E " Win E pN q.
The first property follows from the observation that pWin E pN qq nPN is a non-decreasing family of finite sets.

We now argue that the second property holds. Observe that limBpN qXParity is closed under prefixes, or equivalently its complement is closed under suffixes. From Win A pN q, Adam has a strategy τ N that ensures that either the parity condition is not satisfied, or that some counter value exceeds N . It follows from Lemma 1 that all plays consistent with this strategy remain in Win A pN q.

We construct a strategy from Win A pN q that ensures the complement of BXParity. The argument above yields a sequence of strategies pτ N 1 q N 1 ěN . The strategy simulates those strategies in turn, switching from the strategy τ N 1 to the strategy τ N 1 `1 if some counter value exceeds N 1 . Note that since each strategy τ N 1 ensures to remain in Win A pN 1 q " Win A pN q, the general strategy can indeed switch from one strategy to the next. It follows that Win A pN q Ď Win A , implying Win E " Win E pN q.

Remark 1. The above proof does not give a bound on N ; the sequence pWin E pN qq N PN is ultimately constant, but the index from which it is constant can be a priori arbitrarily large.

Indeed, it is not true that Win E pN q " Win E pN `1q implies that Win E pN `1q " Win E pN `2q, so this sequence might be constant (say, equal to the empty set) for N up to a very large value, and then contain all vertices for N larger than this value.

The main contribution of [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF] is to extend this collapse result to pushdown games. Such games are played over arenas that are induced by a pushdown process; they are in general infinite.

A pushdown process is a finite-state machine which features a stack: it is given by a finite set of control states Q, a stack alphabet Γ and a transition relation ∆. There is a special stack symbol denoted K which does not belong to Γ; we denote by Γ K the alphabet Γ Y tKu. A configuration is a pair pq, uKq (the top stack symbol is the leftmost symbol of u). There are three kinds of transitions in ∆:

• pp, a, pushpbq, qq: allowed if the top stack element is a P Γ K , the symbol b P Γ is pushed onto the stack.

• pp, poppaq, qq: allowed if the top stack element is a P Γ, the top stack symbol a is popped from the stack.

• pp, a, skip, qq: allowed if the top stack element is a P Γ K , the stack remains unchanged.

The symbol K is never pushed onto, nor popped from the stack.

Definition 9 (Pushdown graph)

A pushdown process and two subsets

Q E , Q A such that Q " Q E Z Q A induce
a pushdown graph, whose set of vertices is Q ˆΓ˚K , and set of edges is E induced by the transition relation ∆.

For instance, if pp, a, pushpbq, qq P ∆, then ppp, awKq, pq, bawKqq P E, for all words w in Γ ˚.

A colouring function for a pushdown arena is given by c : ∆ Ñ A, and naturally extended to c : E Ñ A.

Following our convention, a colouring function for the B-parity condition over a pushdown graph is given by two functions Ω : Q Ñ t0, . . . , du and c : ∆ Ñ tε, i, ru k .

We give an example of a game played over a pushdown arena in Figure 2. Example 1 (Stack as credit in a boundedness game played over a pushdown arena)

Figure 2 presents a B-Büchi game played over a pushdown arena where Eve wins for the non-uniform condition B, but for no uniform condition BpN q.

Let us first look at the two bottom states: in the left-hand state at the bottom, Adam can push as many b's as he wishes, and moves the token to the state to its right, where all those b's are popped one at a time, incrementing the counter each time. In other words, each visit of the two bottom states allows Adam to announce a number N and to increment the counter by N .

We now look at the states on the top line: the initial state is the leftmost one, where Adam can push an arbitrary number of a's. We see those a's as credits: from the central state, Adam can use one credit (i.e pop an a) to pay a visit to the two bottom states. When he runs out of credit, which will eventually happen, he moves the token to the rightmost state, where nothing happens anymore.

The following theorem is the main contribution of [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF]. It was called the "forgetful property", following the intuition that even if a configuration carries an unbounded amount of information (since the stack may be arbitrarily large), this information cannot be forever transmitted along a play. Indeed, to increase the counter values significantly, Adam has to use the stack, consuming or forgetting its original information.

Theorem 3 (Collapse over pushdown arenas)

For all boundedness games played over a pushdown arena, for all initial configurations, the following are equivalent:

• Dσ strategy for Eve, @π plays, DN P N, π P BpN q X Parity,

• Dσ strategy for Eve, DN P N, @π plays, π P limBpN q X Parity. This result is in some sense maximal: it is easy to construct an example of a game played over a higher order pushdown system of level 2, where the above equivalence does not hold.

The proof follows the same lines as for the case of finite arenas, except that for the case of pushdown arenas, the sequence pWin E pN qq N PN now consists of infinite sets of configurations. To prove that this sequence is ultimately constant, we show that these sets are regular of bounded size, relying on general results for pushdown games due to [START_REF] Serre | Note on Winning Positions on Pushdown Games with ωregular Conditions[END_REF][START_REF] Serre | Contribution à l'Étude des Jeux sur des Graphes de Processus à Pile[END_REF].

We will use alternating P-automata to recognize sets of configurations: an alternating P-automaton B for a given pushdown process is a classical alternating automaton over finite words: it has a finite set of control states S, a transition function δ : S ˆΓ Ñ B `pSq (the notation B `pSq denotes the set of positive boolean formulae over S) and a subset F of S of final states. We assume that the set of states S contains Q. A configuration pq, uKq is accepted by B if it is accepted with q P Q Ď S as initial state and the classical alternating semantics. A set of configurations is called regular if it is accepted by an alternating P-automaton. The size of an alternating P-automaton is its number of states.

Theorem 4 (Regularity of winning regions [START_REF] Serre | Contribution à l'Étude des Jeux sur des Graphes de Processus à Pile[END_REF]) For all prefix-independent winning conditions W Ď A for all games played over a pushdown arena, the set Win E pW q is a regular set of configurations recognized by an alternating P-automaton of size |Q|.

Relying on Theorem 4, it is easy to see that the sequence pWin E pN qq N PN is ultimately constant, so the proof of Theorem 2 can be repeated to prove Theorem 3.

As a corollary of the forgetful property, we obtain the following decidability result, relying on decidability results obtained in the theory of regular cost functions [START_REF] Blumensath | Two-Way Cost Automata and Cost Logics over Infinite Trees[END_REF].

Corollary 1 (Decidability of boundedness games played over pushdown arenas) Determining the winner in a non-uniform boundedness game played over a pushdown arena is decidable. Indeed, it is easy and classical to reduce the problem of determining the winner in a game played over a pushdown arena to the membership problem of a given regular tree by a corresponding two-way automaton [START_REF] Kupferman | An Automata-Theoretic Approach to Reasoning about Infinite-State Systems[END_REF]. This problem was shown decidable for two-way cost-automata in [START_REF] Blumensath | Two-Way Cost Automata and Cost Logics over Infinite Trees[END_REF].

Finite-Memory Determinacy

In this section, we define finite-memory strategies, and investigate finite-memory determinacy questions: roughly speaking, is it true that if Eve has a winning strategy, then she has a finite-memory winning strategy?

In Subsection 2.1 we introduce finite-and bounded-memory determinacy, and state four questions about finite-memory determinacy for boundedness games.

We then present some results we obtained in this direction. In Subsection 2.2, we discuss the results obtained in collaboration with Krishnendu Chatterjee, published in [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF], and with Martin Zimmermann, published in [START_REF] Fijalkow | Cost-Parity and Cost-Streett Games[END_REF][START_REF] Fijalkow | Cost-Parity and Cost-Streett Games[END_REF]. These results are about finite-memory determinacy for special classes of nonuniform boundedness games, and specifically extensions of finitary conditions. For the sake of keeping this document to a reasonable length, we do not detail the proofs, which can be found in the corresponding papers.

In Subsection 2.3, we report on results obtained in collaboration with Thomas Colcombet and Florian Horn, published in [START_REF] Colcombet | Playing Safe[END_REF]. In this work, we focus on topologically closed conditions, and give an exact characterisation of the memory requirements.

Finite-Memory Strategies

Definition 10 (Memory structure) A memory structure for the arena G consists of a set M of memory states, an initial memory state m 0 P M and an update function µ : M ˆE Ñ M .

The update function takes as input the current memory state and the chosen edge to compute the next memory state, in a deterministic way. It can be extended to a function µ : E ˚¨V Ñ M by defining µ ˚pvq " m 0 and µ ˚pπ ¨pv, v 1 qq " µpµ ˚pπ ¨vq, pv, v 1 qq.

A strategy using the memory structure M is induced by a next-move function σ : V E ˆM Ñ E, by σpπ ¨vq " σpv, µ ˚pπ ¨vqq. Note that we denote both the next-move function and the induced strategy σ. The size of such a strategy is the cardinal of M and denoted mempσq. A strategy is memoryless, or positional if M is a singleton: it only depends on the current vertex. Note that a memoryless strategy can be described as a function σ : V E Ñ E.

An arena G and a memory structure M for G induce the expanded graph G ˆM where the memory state is computed online: the vertex set is V ˆM , the edge set is E ˆµ, defined by: ppv, mq, pv 1 , m 1 qq P E 1 if pv, v 1 q P E and µpm, pv, v 1 qq " m 1 . There is a natural one-to-one correspondence between memoryless strategies in G ˆM and strategies in G using M as memory structure, and similarly between strategies in G ˆM using M 1 as memory structure and strategies in G using M ˆM1 as memory structure. We often implicitly reason in the expanded graph G ˆM when consider a strategy using M as memory structure.

Definition 11 (Positional and finite-memory determinacy) Consider a condition W Ď A ω .

• We say that W is positionally determined if the following holds: for all games with condition W , for all initial vertices, if Eve has a winning strategy, then she has a positional winning strategy.

• We say that W is finite-memory determined if the following holds: for all games with condition W , for all initial vertices, if Eve has a winning strategy, then she has a finite-memory winning strategy.

• We say that W is bounded-memory determined if the following holds: there exists a bound mem P N such that for all games with condition W , for all initial vertices, if Eve has a winning strategy, then she has a finite-memory winning strategy using mem memory states.

Note that here, we only consider the case of Eve, so the classical terminology talks about half -positionally determined conditions in this case, see for instance [START_REF] Gimbert | Jeux Positionnels[END_REF][START_REF] Kopczyński | Half-Positional Determinacy of Infinite Games[END_REF]. As we will be only interested in the case of Eve, we use "positionally determined" for "halfpositionally determined".

The following positionality result has far reaching consequences in automata theory.

Theorem 5 (Positionality of parity games [EJ88])

Parity games are positionally determined.

Problem 3 (Finite-and bounded-memory determinacy for boundedness games)

Are uniform and non-uniform boundedness games finite-memory determined? Bounded-memory determined?

We instantiate the definitions of finite-and bounded-memory determinacy for boundedness games.

For a boundedness game and v 0 an initial vertex, we denote valpv 0 q the smallest N such that Eve has a strategy ensuring BpN q X Parity.

(i) Bounded-memory determinacy for uniform boundedness games For all k, d P N, there exists mem P N such that for all boundedness games with k counters, d `1 colors and initial vertices v 0 , there exists a strategy using mem memory states ensuring Bpvalpv 0 qq X Parity.

(ii) Finite-memory determinacy for uniform boundedness games For all k, d P N, for all boundedness games with k counters, d `1 colors and initial vertices v 0 , there exists a strategy using finitely many memory states ensuring Bpvalpv 0 qq X Parity.

(iii) Bounded-memory determinacy for non-uniform boundedness games For all k, d P N, there exists mem P N such that for all boundedness games with k counters, d `1 colors and initial vertices, if Eve has a strategy ensuring B X Parity, then she has one using mem memory states.

(iv) Finite-memory determinacy for non-uniform boundedness games For all k, d P N, for all boundedness games with k counters, d `1 colors and initial vertices, if Eve has a strategy ensuring B X Parity, then she has one using finite memory.

We will answer those four questions:

• we show in Subsection 3.1 that (ii) holds and (i) does not hold,

• we show in Section 5 that (iii) and (iv) do not hold.

As we will see, the LoCo conjecture introduces another dimension to these questions: it allows distortion of the value, see Section 3.

Some results for Non-Uniform Boundedness Games

This subsection discusses the results obtained in collaboration with Krishnendu Chatterjee [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF] and Martin Zimmermann [FZ12;[START_REF] Fijalkow | Cost-Parity and Cost-Streett Games[END_REF].

Both papers are related to the finitary conditions, which have been introduced in verification by Alur and Henzinger [START_REF] Alur | Finitary Fairness[END_REF] as a strengthening of liveness conditions. Intuitively, a liveness condition requires that some event occurs eventually, its finitary counterpart strengthens this by requiring an overall bound on the waiting time.

We now define the finitary parity condition with d `1 colors over the alphabet A " t0, . . . , du. Given a sequence s " c 0 ¨c1 ¨¨¨and k P N, we define:

dist k psq " inftk 1 ´k | k 1 ě k, c k 1 is even and c k 1 ď c k u;
i.e dist k psq is the "waiting time" by means of number of transitions followed from the k th position before reaching a preferable color (that is, even and lower or equal than in the k th position). The finitary parity condition was defined as follows in [START_REF] Chatterjee | Finitary Winning in omega-regular Games[END_REF]:

FinParity " ts | lim sup k dist k psq ă 8u;
i.e, it requires that the supremum limit of the distance sequence is bounded.

The finitary parity condition can be seen up to encoding as a special case of the nonuniform B-parity condition. The specificity here is that the counters are used to quantify how well is the parity condition satisfied. This makes the situation very different from the general case of B-parity conditions, where the parity condition and the counters are completely independent.

Chatterjee, Henzinger and Horn introduced and studied games with finitary parity conditions [START_REF] Chatterjee | Finitary Winning in omega-regular Games[END_REF]. Their main result is that determining the winner in a finitary parity game can be achieved in cubic time, which should be contrasted with the situation for parity games, where determining the winner is not known to be doable in polynomial time. Furthermore, they showed that finitary parity games over finite arenas are, as parity games, positionally determined: Theorem 6 (Positionality of finitary parity games over finite arenas [START_REF] Chatterjee | Finitary Winning in omega-regular Games[END_REF]) Finitary parity games over finite arenas are positionally determined.

Inspired by these results, we introduced in collaboration with Martin Zimmermann a condition called cost-parity condition, generalizing both parity conditions and finitary parity conditions. We proved that the corresponding games, called parity games with costs, have the best expected properties, i.e. that they do not get worse than any of the two conditions they generalise:

Theorem 7 (Parity games with costs)

• Parity games with costs played over finite arenas are positionally determined.

• Given an algorithm that solves parity games played over finite arenas in time T pn, m, dq, there is an algorithm that solves parity games with costs played over finite arenas in time Opn ¨T pdn, dm, d `2qq, where n is the number of vertices, m is the number of edges and d the number of colors.

We refer to [START_REF] Fijalkow | Cost-Parity and Cost-Streett Games[END_REF] for the definitions and proofs.

The second generalization we considered was to extend the positionality result for finitary parity conditions to infinite arenas. Relying on different ideas and techniques to tackle infinite arenas, we proved the following result in collaboration with Krishnendu Chatterjee [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF]:

Theorem 8 (Bounded-memory determinacy of finitary parity games) Finitary parity games with d `1 colors are bounded-memory determined, with strategies using d{2 memory states.

We refer to [START_REF] Chatterjee | Infinite-state Games with Finitary Conditions[END_REF] for the proof. A natural question is whether this result can be extended to the general case of nonuniform boundedness games. The answer is no, as we will show in Section 5 that nonuniform boundedness games are not bounded-memory determined.

Memory for Topologically Closed Conditions

This subsection reports on some results obtained in collaboration with Thomas Colcombet and Florian Horn, published in [START_REF] Colcombet | Playing Safe[END_REF].

The initial observation is the following simple positionality result:

Fact 1 (Positionality of uniform B games with one counter)

Uniform B games with one counter are positionally determined, i.e. for all B games with one counter and initial vertices v 0 , Eve has a positional strategy ensuring Bpvalpv 0 qq.

Proof. Consider a B game pG, Bq with one counter, and a strategy σ ensuring Bpvalpv 0 qq. Denote N " valpv 0 q. Observe that the condition BpN q is closed under suffix, as defined in Lemma 1, hence all plays consistent with σ remain in Win E pG, BpN qq. For every vertex v P Win E pG, BpN qq, there exists a maximal value N pvq ď N such that σ ensures BpN q from v, starting with N pvq as counter value.

Informally speaking, this value N pvq is the worst-case scenario from v, so in this case the strategy σ has to produce its best move. Indeed, the strategy can play some nonoptimal moves as long as the counter value remains small, and start playing optimal moves when the situation gets dangerous, i.e. if the counter value gets closer to N . Looking at the move that σ prescribes from v with counter value N pvq guarantees the best outcome. Formally, this means that the strategy σ ensures that the chosen edge leads to a vertex v 1 with a counter value N 1 such that σ ensures BpN q from v 1 , starting with N 1 as counter value. Consequently, N 1 ď N pv 1 q.

We construct a positional strategy σ 1 ensuring BpN q by playing from v as σ would have played from v with counter value N pvq. The reasoning above ensures that this strategy ensures to remain forever in the winning region Win E pG, BpN qq, implying that the strategy σ 1 is winning.

Our objective is to generalise this reasoning. The key observation here is that the condition BpN q is topologically closed, as we will define now. We will show that the reasoning sketched above extends to all topologically closed conditions.

Problem 4 (Characterising memory requirement)

Given W Ď A ω , characterise the following quantity: mempW q " sup pG,W q game inf σ winning strategy mempσq.

In words, mempW q is the necessary and sufficient number of memory states for constructing a winning strategy in games with condition W . Equivalently:

• upper bound: for all games pG, W q, for all initial vertices, if Eve has a winning strategy, then she has a winning strategy using at most mempW q memory states,

• lower bound: there exists a game pG, W q and an initial vertex such that Eve has a winning strategy, but no winning strategy using less than mempW q memory states.

The quantity mempW q has been considered in two different works before. First, Dziembowski, Jurdziński and Walukiewicz characterised mempW q for all Muller conditions W , i.e. for Boolean combinations of the conditions "color c appears infinitely many times" [START_REF] Dziembowski | How Much Memory is Needed to Win Infinite Games?[END_REF].

In this subsection, we characterise mempW q for all conditions W that are closed (with respect to the Cantor topology over infinite words). We will use the following property as a definition: a condition W over an alphabet A is closed if, and only if, it is given by a subset P Ď A ˚of forbidden prefixes of colors, inducing the condition W " tc 0 ¨c1 ¨¨¨| @i P N, c 0 ¨c1 ¨¨¨c i R P u.

Note that closed conditions are incomparable with ω-regular conditions, so our results are incomparable with [START_REF] Dziembowski | How Much Memory is Needed to Win Infinite Games?[END_REF][START_REF] Kopczyński | Half-Positional Determinacy of Infinite Games[END_REF][START_REF] Kopczyński | Half-Positional Determinacy of Infinite Games[END_REF].

For the remainder of this section, we fix a closed condition W induced by P Ď A ˚.

Remark 2. We restrict ourselves to arenas with finite out-degree: for every vertex v P V , the set tv 1 | pv, v 1 q P Eu is finite. In particular, in the definition of mempW q, the supremum ranges over all arenas of finite out-degree. This assumption will be used only in the proof of Lemma 6, but we will show that the result fails without this assumption.

A First Upper Bound

We first give an upper bound on mempW q. Let w P A ˚, define its left quotient as:

w ´1W " ts P A ω | w ¨s P W u.

We denote RespW q the set of left quotients of W :

RespW q " tw ´1W | w P A ˚u.

We mention some special left quotients: the initial one, ε ´1W (equal to W ), and the empty one, obtained as w ´1W for any w P P . Recall that RespW q is finite if, and only if, W is regular, and in such case it can be used to describe the set of states of the minimal deterministic automaton recognizing W . This remark allows to reduce games with closed conditions W to safety games, and to use the following folklore result: Lemma 2 (Positionality of safety games) Safety games are positionally determined.

We will often use a slightly more general result in this chapter: Lemma 3 (Positionality of safety games, take 2) Consider a condition W Ď A, an arena G equipped with a colouring function c : E Ñ A ˆt0, 1u, i.e. by two colouring functions c A : E Ñ A and c S : E Ñ t0, 1u, and an initial vertex. This gives rise to the game pG, W X Safeq, where W uses the colouring function c A and Safe the colouring function c S .

If there exists a winning strategy in pG, W X Safeq using mem memory states, then there exists a winning strategy in pG, W q using mem memory states.

The following lemma reduces games with closed conditions to safety games, and constructs the most important tool in the proofs to follow: Lemma 4 (First upper bound) For all games pG, W q with a closed condition W , for all initial vertices, if Eve has a winning strategy, then she has a winning strategy using at most |RespW q| memory states.

Consequently, mempW q ď |RespW q| .

Proof. We construct a memory structure M, as follows: the set of memory states is RespW q, the initial memory state is W and the update function is µ, where µpw ´1W, aq " pw ¨aq ´1W . (It is easy to check that this is well defined, i.e. independent of the representant w chosen). At any point in the game, the memory state computed by M is the current left quotient.

Let G be an arena with a colouring function c : E Ñ A. We construct the expanded arena G ˆM equipped with the colouring function c 1 : E ˆRespW q Ñ t0, 1u defined by:

c 1 p_, w ´1W q " # 1 if w ´1W " H (equivalently, w P P ), 0 otherwise.
We equip G ˆM with the safety condition, giving rise to the game pG ˆM, Safeq. First observe that by construction, the plays in G ˆM are of the form pe 0 , cpe 0 q ´1W q pe 1 , cpe 0 ¨e1 q ´1W q ¨¨¨pe k , cpe 0 ¨e1 ¨¨¨e k q ´1W q, so by definition of c 1 a play is winning in pG ˆM, Safeq if, and only if, its projection (on the first component) is winning in pG, W q.

It follows that a winning strategy for Eve in pG, W q from v 0 induces a winning strategy in pG ˆM, Safeq from pv 0 , W q. Now, thanks to Lemma 2, since Eve wins in pG ˆM, Safeq, she has a positional winning strategy. This induces a winning strategy in pG, W q using M as memory structure, concluding the proof of Lemma 4.

The game pG ˆM, Safeq defined above will be an important tool in the proofs to follow. We will also rely on the following remark: assume we want to prove that a strategy σ is winning. Then it is enough to show that for all plays π consistent with σ, for all k, cpπ k q ´1W ‰ H, where π k is the prefix of π of length k. This simple observation follows from the definition of safety conditions.

A Tighter Upper Bound

The memory structure M is not optimal. A first remark is that the empty left quotient (which exists if W ‰ A ω ) can be removed from the memory states as the game is lost. From now on by "left quotient" we mean "non-empty left quotient of W ", and in particular RespW q denotes the set of non-empty left quotients.

The second remark is the following: let L 1 and L 2 two left quotients, such that L 1 Ď L 2 . With the same notations as above, consider a vertex v in the arena G. If Eve wins from pv, L 1 q in pG ˆM, Safeq, then she also wins from pv, L 2 q: indeed, she can play as she would have played from pv, L 1 q. Since this ensures from v that all plays are winning for L 1 , then a fortiori they are winning for L 2 .

This suggests to restrict the memory states only to minimally winning left quotients with respect to inclusion. Two issues arise:

• which left quotients are winning depends on the current vertex, so the semantics of a memory state can no longer be one left quotient, but rather a left quotient for each possible vertex,

• there may not exist minimally winning left quotients.

For the sake of presentation, we first show how to deal with the first issue, assuming the second issue does not appear. Specifically, in the following lemma, we assume that RespW q is finite (i.e. W is regular), implying the existence of minimally winning left quotients. We will later drop this assumption.

We define the width of a (partially) ordered set pE, ďq as the cardinal of the maximal antichain of E with respect to ď, i.e. the cardinal of the largest set of pairwise incomparable elements.

Lemma 5 (Upper bound in the regular case)

Assume that RespW q is finite. For all games pG, W q with a closed condition W , for all initial vertices, if Eve has a winning strategy, then she has a winning strategy using at most K memory states, where K is the width of pRespW q, Ďq.

Proof. We use the same notations as for the proof of Lemma 4, and construct a smaller memory structure together with a winning strategy using this memory structure. In this proof, by winning we mean winning in the game pG ˆM, Safeq.

Let K be the cardinal of the maximal antichain of left quotients of W . We construct the memory structure M ˚whose set of memory sates is t1, . . . , Ku initial memory state is 1 and update function is µ, and the next-move function σ inducing the strategy also denoted σ.

Let v be a vertex in G. We consider the set of minimal left quotients L such that pv, Lq is winning. (Here we use the finiteness of RespW q to guarantee the existence of such left quotients.) This is an antichain, so there are at most K of them, we denote them by L 1 pvq, . . . , L p pvq, for some p ď K. The key property is that for every left quotient L such that pv, Lq is winning, there exists i such that L i pvq Ď L. Furthermore, we choose L 1 pv 0 q such that L 1 pv 0 q Ď W . (Indeed, by assumption pv 0 , W q is winning.)

We define the update function: µpi, pv, v 1 qq is a j such that L j pv 1 q Ď L i pvq ¨cpv, v 1 q. Note that in general, such a j may not exist; it does exist if pv 1 , L i pvq ¨cpv, v 1 qq is winning, and we will prove that this will always be the case when playing the strategy σ.

We define the next-move function σ. Let v P V E , and consider pv, L i pvqq: since Eve wins from there, there exists an edge pv, v 1 q P E such that pv 1 , L i pvq ¨cpv, v 1 qq is winning. Define σpv, iq to be this v 1 .

We show that the strategy σ is winning. Consider a play π " pv 0 , v 1 q ¨pv 1 , v 2 q ¨¨c onsistent with σ, and i 0 ¨i1 ¨¨¨the sequence of memory states assumed along this play. Denote π k the prefix of π of length k, we prove that for all k, L i k pv k q Ď cpπ k q ´1W . Note that by definition, pv k , L i k pv k qq is winning, so L i k pv k q ‰ H, implying that cpπ k q ´1W ‰ H.

We proceed by induction. For k " 0, it follows from L 1 pv 0 q Ď W . Let k ą 0, the induction hypothesis is L i k´1 pv k´1 q Ď cpπ k´1 q ´1W . We distinguish two cases.

• Either v k´1 belongs to Eve, then by construction of σ we have that pv k , L i k´1 pv k´1 q cpv k´1 , v k qq is winning. It follows that the update function is well defined, and L i k pv k q Ď L i k´1 pv k´1 q ¨cpv k´1 , v k q, which together with the induction hypothesis implies

L i k pv k q Ď cpπ k q ´1W .
• Or v k´1 belongs to Adam. Since Adam cannot escape Win E pG ˆM, Safeq, we have that pv k , L i k´1 pv k´1 q ¨cpv k´1 , v k qq is winning, and the same reasoning concludes.

It follows that the strategy σ is winning, concluding the proof of Lemma 5.

We now get rid of the regularity assumption. This means that for a vertex v, there may not be a minimal left quotient L such that pv, Lq is winning. To get around this difficulty, the semantics of a memory state is a not anymore a left quotient for each vertex, but rather a decreasing sequence of left quotients for each vertex.

In the following proof of Lemma 6, we will use the assumption that the out-degree of every vertex is finite, i.e. for every vertex v P V , the set tv 1 | pv, v 1 q P Eu is finite.

Lemma 6 (Upper bound)

For all games pG, W q with a closed condition W over an arena with finite out-degree, for all initial vertices, if Eve has a winning strategy, then she has a winning strategy using at most K memory states, where K is the width of pRespW q, Ďq.

Consequently, mempW q is smaller than or equal to the width of pRespW q, Ďq.

Proof. We use the same notations as for the proof of Lemma 5, and construct a memory structure together with a winning strategy using this memory structure.

Let K be the cardinal of the maximal antichain of left quotients of W . We construct the memory structure M ˚whose set of memory states is t1, . . . , Ku initial memory state is 1 and update function is µ, and the next-move function σ inducing the strategy also denoted σ.

Let v be a vertex in G. We consider the set Winpvq of left quotients L such that pv, Lq is winning. We split Winpvq into maximal decreasing (finite or infinite) sequences of left quotients, denoted 1 pvq, . . . , p pvq, for some p ď K. Furthermore, we choose 1 pv 0 q such that W P 1 pv 0 q. (Indeed, by assumption pv 0 , W q is winning.)

We say that pv, q is winning if for all L P , we have that pv, Lq is winning. For a sequence of left quotients and a P A, we define ¨a component-wise. Note that even if is infinite, it may be that ¨a is finite.

We define the update function: µpi, pv, v 1 qq is a j as follows.

• If i pvq ¨cpv, v 1 q is finite, denote L ¨cpv, v 1 q its last element. Choose j such that L ¨cpv, v 1 q P j pv 1 q. Note that in general, such a j may not exist; it does exist if pv 1 , i pvq ¨cpv, v 1 qq is winning, and we will prove that this will always be the case when playing the strategy σ.

• If i pvq ¨cpv, v 1 q is infinite, then choose j such that j pv 1 q has an infinite intersection with i pvq ¨cpv, v 1 q. Such a j exists without any assumption.

We define the next-move function σ. Let v P V E , and consider pv, i pvqq. Let L P i pvq, Eve wins from pv, Lq, so there exists an edge pv, v 1 q P E such that pv 1 , L¨cpv, v 1 qq is winning, we say that pv, v 1 q P E is good for L. Since Winpv 1 q is upward closed, if pv, v 1 q P E is good for L, then it is good for every L 1 such that L Ď L 1 . We argue that there exists an edge pv, v 1 q P E that is good for all L P i pvq, i.e. such that pv 1 , i pvq ¨cpv, v 1 qq is winning; define µpv, iq to be this v 1 . There are two cases:

• Either i pvq is finite, denote L its last element. Since i pvq is decreasing, an edge good for L is good for all L 1 P i pvq.

• Or i pvq is infinite. The vertex v has finite degree, so there exists an edge which is good for infinitely many L P i pvq. Since i pvq is decreasing, it is good for all L 1 P i pvq.

We show that the strategy σ is winning. Consider a play π " pv 0 , v 1 q ¨pv 1 , v 2 q ¨¨c onsistent with σ, and i 0 ¨i1 ¨¨¨the sequence of memory states assumed along this play. Denote π k the prefix of π of length k, we prove that for all k, there exists L P i k pv k q such that L Ď cpπ k q ´1W . Note that by definition, pv k , i k pv k qq is winning, so cpπ k q ´1W ‰ H.

We proceed by induction. For k " 0, it follows from W P 1 pv 0 q. Let k ą 0, the induction hypothesis implies the existence of L P i k´1 pv k´1 q such that L Ď cpπ k´1 q ´1W . We distinguish two cases, and denote c k " cpv k´1 , v k q.

• Either v k´1 belongs to Eve, then by construction of σ we have that pv k , i k´1 pv k´1 q¨c k q is winning. It follows that the update function is well defined, and:

1. If i k´1 pv k´1 q ¨ck is finite, denote L 1 ¨ck its last element, we have L 1 ¨ck P i k pv k q.

Since L 1 ¨ck is the last element of i k´1 pv k´1 q ¨ck , it follows that L 1 Ď L. We have thus L 1 ¨ck Ď L ¨ck , so L 1 Ď cpπ k q ´1W , and

L 1 ¨ck P i k pv k q. 2. If i k´1 pv k´1 q¨c k is infinite, i k pv k q has an infinite intersection with i k´1 pv k´1 q¨c k . So there exists L 1 Ď L with L 1 P i k´1 pv k´1 q such that L 1 ¨ck is in this intersection. We have L 1 ¨ck P i k pv k q and L 1 Ď cpπ k q ´1W .
• Or v k´1 belongs to Adam. Since Adam cannot escape Win E pG ˆM, Safeq, we have that pv k , i k´1 pv k´1 q ¨ck q is winning, and the same reasoning concludes.

It follows that the strategy σ is winning, concluding the proof of Lemma 6.

A Matching Lower Bound For all closed conditions W , there exists a game pG, W q and an initial vertex such that Eve has a winning strategy, but no winning strategy using less than K memory states where K is the width of pRespW q, Ďq.

v 0 v ′ 0 v 1 v i v K w 1 w 2 w K-1 w K . . . u i,1 u i,2 u i,K-1 u i,K . . . . . . . . .
Consequently, mempW q is greater than or equal to the width of pRespW q, Ďq.

Proof. Consider tw ´1 1 W, . . . , w ´1 K W u an antichain of left quotients of W . For i ‰ j, there exists u i,j P A ω such that u i,j P w ´1 i W and u i,j R w ´1 j W . We describe the game, illustrated in Figure 3. A play consists in three steps:

1. From v 0 to v 1 0 : Adam chooses a word in tw 1 , . . . , w K u;

2. Eve chooses between K options;

3. say Eve chose the i th option, then Adam chooses between the K ´1 words u i,j for j ‰ i.

We first show that Eve has a winning strategy from v 0 , using K memory states. It consists in choosing the i th option whenever Adam chooses the word u i : whatever Adam chooses at the third step, w i ¨ui,j P W . We now show that there exists no winning strategy using less than K memory states. Indeed, such a strategy will not comply with the above strategy and for some i ‰ j, choose the j th option if Adam chooses w i . Then Adam wins by playing u i,j , since w i ¨ui,j R W .

Tight Bounds

Putting together upper and lower bounds, we proved the following result:

Theorem 9 (Memory for closed conditions) For all closed conditions W , mempW q is the width of pRespW q, Ďq.

Theorem 9 allows to uniformly derive memory requirements for different conditions, such as the BpN q-condition with one counter, which was the original motivation, but also the generalised reachability condition, that we introduced and studied in collaboration with Florian Horn [START_REF] Fijalkow | Les Jeux d'accessibilité généralisée[END_REF], and the energy condition, see [START_REF] Colcombet | Playing Safe[END_REF] for more details about these applications.

We conclude by giving an example showing that the result would fail without the finite out-degree assumption. Let A " ta, b, cu and W " ta n ¨bp ¨cω | n ď pu Y ta ω u Y a ˚¨b ω . It is a non-regular closed condition, called the outbidding condition. Figure 4 represents the partial order pRespW q, Ďq: the solid edges represent inclusions of left quotients, and the dashed edges figure the minimal (yet infinite) deterministic automaton recognizing W . Its width is 3: there are two incomparable infinite increasing sequences of left quotients, ppa n q ´1W q nPN and ppa n ¨bq ´1W q nPN , and c ´1W .

c ε a a 2 a 3 a 4 a 5 b ab a 2 b a 3 b a 4 b a 5 b • • • • • • c a a a a a
v 0 v ′ 0 v 1 v 2 v 3 v n
Hence thanks to Theorem 9, mempW q " 3. However, there exists an outbidding game where Eve wins but needs infinite memory for this. This does not contradict Theorem 9, as this game, represented in Figure 5, has a vertex of infinite out-degree. It goes as follows: first Adam picks a number n, and then Eve takes over: she has to pick a number p, higher than or equal to n. A strategy using finitely many memory states can only choose from finitely many options, hence cannot win against all strategies of Adam.

The LoCo Conjecture

In this section, we state the LoCo conjecture. We give a first statement of the conjecture in Subsection 3.1, and show what it implies in the theory of regular cost functions in Subsection 3.2. We then refine the conjecture by considering structural properties of the arenas in Subsection 3.3.

A First Statement of the Conjecture

The LoCo conjecture is a bounded-memory determinacy statement, that introduces a trade-off between memory and bounds:

Conjecture 1 (LoCo conjecture) For all k, d P N, there exists mem P N and α : N Ñ N such that for all boundedness games with k counters, d `1 colors and initial vertices v 0 , there exists a strategy σ using mem memory states ensuring Bpαpvalpv 0 qqq X Parity.

The function α is called a trade-off function: at the price of increasing the bound from valpv 0 q to αpvalpv 0 qq, one can use a bounded-memory strategy.

Note that we state the LoCo conjecture here only for Eve. Throughout this chapter, we will only consider strategies for Eve. As we will see in Subsection 3.2, this allows to prove the equivalence between alternating and non-deterministic B-parity automata over infinite trees. To obtain the corresponding equivalence for S-parity automata, and the decidability of cost-MSO over infinite trees, one needs to also prove the LoCo conjecture for Adam. We do not consider this here.

To get a better understanding of this conjecture, we make a series of observations. 1. We show the implications between the LoCo conjecture and finite-and boundedmemory determinacy for boundedness games, as illustrated in Figure 6.

2. We show that the uniform boundedness games are not bounded-memory determined.

3. We show that the non-uniform boundedness games are finite-memory determined. We start by the implications illustrated in Figure 6. Three of them are simple logical implications, so we focus on the last one, overlined "fixpoint".

Lemma 8 (Fixpoint)

Consider a prefix-independent condition W , i.e. closed under prefixes and suffixes: for π a finite play and π 1 an infinite play, π ¨π1 P W if, and only if, π 1 P W .

Assume that there exists mem P N such that for all games pG, W q, if Win E pG, W q is non-empty, then there exists a vertex v 0 such that Eve has a winning strategy from v 0 using mem memory states. Then W is bounded-memory determined.

Before proving this lemma, let us see how it helps to show the implication from Figure 6. Assume that the LoCo conjecture holds, we prove that non-uniform boundedness games are bounded-memory determined.

Let pG, B X Parityq be a non-uniform boundedness game. We show that the assumptions of Lemma 8 hold; first of all the condition B X Parity is prefix-independent. We argue that the following holds:

If Win E pG, B X Parityq is non-empty, then there exists N P N such that Win E pG, BpN q X Parityq is non-empty.

We show the contrapositive. Assume that for all N P N, Win E pG, BpN qXParityq is empty, it means that Adam has a strategy τ N ensuring the complement of BpN q X Parity: in a play consistent with τ N , either at some point some counter reaches value N `1, or the infinite play does not satisfy the parity condition. We construct a strategy τ for Adam that ensures the complement of B X Parity, implying that Win E pG, BpN q X Parityq is empty. The strategy τ simulates the strategies pτ N q N PN , starting from τ 1 and switching from τ N to τ N `1 if at some point some counter reaches value N `1.

Let v 0 P Win E pG, BpN q X Parityq, thanks to the LoCo conjecture (which we assume here holds), this yields a strategy ensuring BpαpN qq X Parity using mem memory states. A fortiori, this strategy ensures B X Parity.

It follows from Lemma 8 that under the assumption that the LoCo conjecture holds, the non-uniform condition B X Parity is bounded-memory determined. As we will see in Section 5, the LoCo conjecture does not hold.

We now prove Lemma 8. It is a rather classical technique, which was for instance heavily used in [Kop06; Kop09; CF13]. To prove it, we need the following lemma, which raises the question of uniformity for winning strategies. So far, all finite-memory determinacy statements were for a given initial vertex. A stronger finite-memory determinacy statement is obtained by asserting the existence of one strategy, which would be winning from all vertices of the winning region; such a strategy is called uniform. Note that this notion of uniformity is not related at all to the uniformity in boundedness games.

Lemma 9 (Uniform strategies) Consider a condition W closed under suffixes: for π a finite play and π 1 an infinite play, if π ¨π1 P W , then π 1 P W .

Let Y be a subset of vertices, and for all vertices v P Y , a strategy σ v using mem memory states winning from v. Then there exists a uniform strategy using mem memory states, winning from Y .

Proof. Without loss of generality, we assume that the strategies σ v use the same memory structure M. We construct a uniform strategy σ using the memory structure M, which is winning from all vertices of Y .

Consider ĺ a well order on V (the existence of such a well order is a consequence of the axiom of choice). For a vertex v P V and a memory state m P M , we define σpv, mq as σ v 0 pv, mq, where v 0 is the least element with respect to the well-order ĺ such that σ v 0 pv, mq is defined (i.e. there exists a play from pv 0 , m 0 q to pv, mq).

We argue that σ is winning. Consider a play consistent with σ from some vertex of Y . By definition, it is ultimately consistent with some strategy σ v , so a suffix of the play belongs to W . By closure under suffixes, this implies that the play itself belongs to W . ' ' ' %

X 0 " H Y 0 " " v P V ˇˇˇE ve has a winning strategy in G from v using mem memory states * X α`1 " X α Y Y α Y α`1 " " v P V ˇˇˇE ve has a winning strategy in GrV zX α`1 s from v using mem memory states * X β " Ť αăβ X α Y Y α Y β "
" v P V ˇˇˇE ve has a winning strategy in GrV zX β s from v using mem memory states * Here β denotes a limit ordinal, and GrXs is the arena induced by the subset of vertices X.

By assumption Ť α X α " Win E pG, W q. Thanks to Lemma 9, for every ordinal α there exists a strategy σ α using mem memory states which is winning from Y α . The same reasoning as in Lemma 1 shows that all plays consistent with σ α in GrV zX α s remain in Y α . However, this is not true anymore when considering plays consistent with σ α in G: a play can go from Y α to Y β for β ă α.

Consider the strategy σ which is the disjoint sum of the strategies σ α . It uses mem memory states. The above observation implies that all plays consistent with σ are ultimately consistent with one σ α , so a suffix of the play belongs to W . By closure under suffixes, this implies that the play itself belongs to W , and σ is winning from Win E pG, W q, which concludes.

We now show that the uniform boundedness games are not bounded-memory determined:

Lemma 10 (Uniform boundedness games are not bounded-memory determined) For all N P N, there exists a B-reachability game and an initial vertex v 0 such that:

• valpv 0 q " N , so Eve has a strategy ensuring BpN q Until Reach using N `1 memory states,

• no strategy using less than N `1 memory states ensures BpN q Until Reach.

v 0 v u N u N -1 . . . u 2 u 1 F i N i N r i N -1 i r i N -2 i N -2 r i i N -1 r
Figure 7: Eve needs N `1 memory states to ensure BpN q Until Reach, but has a positional strategy for Bp2N q Until Reach.

Proof. The game is represented in Figure 7. It involves one counter and the condition B Until Reach. Starting from v 0 , the game moves to v and sets the value of the counter to N . The objective of Eve is to take the edge to the right to F . However, this costs N increments, so if she wants the counter value to remain smaller than N she has to set its value to 0 before taking this edge. She has N options: for P t1, . . . , N u, the th option consists in going to u , involving the following actions:

• first, take N ´ increments,

• then, reset the counter,

• then, take ´1 increments, setting the value to ´1.

It follows that there is a strategy for Eve to ensure BpN q Until Reach, which consists in going successively through u N , u N ´1, and so on, until u 1 , and finally to F . Hence to ensure that the bound is always smaller than N , Eve needs N `1 memory states.

Observe that in Figure 7, if we consider the bound 2N rather than N , then Eve has a very simple strategy, which consists in going directly to F , using no memory at all. This is a simple example of a trade-off: to ensure the bound N , Eve needs N `1 memory states, but to ensure the worse bound 2N , she has a positional strategy.

We conclude by showing that the uniform boundedness games are finite-memory determined.

Lemma 11 (Finite-memory determinacy for uniform boundedness games) For all k P N, for all boundedness games with k counters and initial vertices v 0 , there exists a strategy σ ensuring Bpvalpv 0 qq X Parity using pvalpv 0 q `1q k memory states.

Proof. Denote N " valpv 0 q, and consider the memory structure M which keeps track of the counter values: the set of memory states is M " t0, . . . , N u k YtKu, the initial memory state 0 k , and the update function µ mimics the counter actions. If a counter value exceeds N , the memory state is updated to K. We construct the arena G ˆM equipped with the colouring function c : E ˆM Ñ t0, 1u defined by: cp_, mq "

# 1 if m " K, 0 otherwise.
The condition BpN q X Parity in G is equivalent to the condition Safe X Parity in G ˆM.

Since parity games are positionally determined and thanks to Lemma 3 (to handle the additional safety condition), there exists a positional winning strategy in pG ˆM, Safe X Parityq, which induces a winning strategy in pG, BpN q X Parityq using M as memory structure. Note that since this strategy is winning, it does not make use of the memory state K, so it uses pN `1q k memory states. This concludes.

Applications to the Theory of Regular Cost Functions

In this section, we show that the LoCo conjecture is the key property for proving that alternating and non-deterministic B-parity automata over infinite trees are equivalent.

We first recall the classical construction for alternating automata without counters, which from an alternating automaton constructs an equivalent non-deterministic automaton. This construction is due to Muller and Schupp [START_REF] Muller | Alternating Automata on Infinite Trees[END_REF][START_REF] Muller | Simulating Alternating Tree Automata by Nondeterministic Automata: New Results and New Proofs of the Theorems of Rabin, McNaughton and Safra[END_REF].

Then, we explain how to extend this construction to the case of alternating Bautomata, i.e. when adding counters. The LoCo conjecture was introduced to make this construction work.

Recall that a (complete binary) A-labelled tree is a function t : t0, 1u ˚Ñ A. A branch of t is an infinite word π P t0, 1u ω .

Definition 12 (Alternating automaton over infinite trees) An alternating (parity tree) automaton A is given by a finite set of states Q divided into existential states (Q E ) and universal state pQ A q, a transition function ∆ Ď QˆAˆQˆQ, an initial state q 0 and a colouring function Ω : Q Ñ t0, . . . , du.

We define the semantics of alternating automata using games. An alternating automaton A and an A-labelled tree t induce the parity game pG A,t , Parityq, that we define now, and we say that t is accepted by A if, and only if, Eve has a winning strategy in G A,t .

In the acceptance game pG A,t , Parityq, Eve is trying to prove that t is accepted, and Adam tries to disprove her. She is in charge of the existential states, and Adam in charge of the universal states. Together, they build a run of the automaton, which can be seen as a Q-labelled tree. In addition, Adam also chooses the directions; this corresponds to the fact that a run is accepting if all its branches are accepting. Here the acceptance condition is given by a parity condition.

Formally:

V " " V E " tpq, nq | q P Q E , n P t0, 1u ˚u V A " tpq, nq | q P Q A , n P t0, 1u ˚u Y tpq 0 , q 1 , nq | q 0 , q 1 P Q, n P t0, 1u ˚u E "
" pq, nq Ý Ñ pq 0 , q 1 , nq pq, tpnq, q 0 , q 1 q P ∆ pq 0 , q 1 , nq Ý Ñ pq , n ¨ q n P t0, 1u ˚, P t0, 1u Ωpq, nq " Ωpqq.

The definition of non-deterministic automata can be obtained as the special case of alternating automata where all states are existential. Note that in this case, the games semantics given above reduces to the following: a tree is accepted if there exists a run over this tree such that all branches of the run are accepting.

Theorem 10 (Alternating and non-deterministic automata [MS87; MS95]) For every alternating automaton, there exists an equivalent non-deterministic automaton, i.e. accepting the same set of trees.

We sketch the proof of this theorem. Since parity games are positionally determined, a tree t is accepted by A if, and only if, Eve has a positional winning strategy in G A,t . Observe that a positional strategy is a function σ : Q ˆt0, 1u ˚Ñ ∆, so it can be seen as a pQ ˆ∆q-labelled tree. We construct a non-deterministic automaton C that accepts pA ˆQ ˆ∆q-labelled trees; a tree pt, σq is accepted by C if, and only if, σ is a winning strategy in G A,t .

This set of infinite trees has a special property: it is branch-wise, i.e. it is the form tt | for all branches π, trπs P Lu, for some set L of infinite words, where trπs is the infinite word obtained by restricting the tree t to the branch π.

In the present case, the language L is ω-regular, so it recognized by some deterministic automaton over infinite words. This allows to construct C as a deterministic automaton over infinite trees.

Finally, we construct B as the projection of C on the second component: a tree t is accepted by B if, and only if, there exists a tree pt, σq accepted by C. The automaton B makes at every transition non-deterministic guesses about the second component σ.

To summarise, the key properties used in the above construction are:

• parity games are positionally determined,

• every ω-regular language is recognized by a deterministic automaton, allowing to construct a deterministic automaton for the branch-wise language over infinite trees.

We now consider B-parity automata, as introduced by Colcombet in the theory of regular cost functions [START_REF] Colcombet | The Theory of Stabilisation Monoids and Regular Cost Functions[END_REF][START_REF] Colcombet | Regular Cost Functions, Part I: Logic and Algebra over Words[END_REF]. An alternating B-parity automaton is an alternating automaton additionally equipped with a set of counters, which are manipulated through the colouring function c : ∆ Ñ tε, i, ru k .

The semantics of a B-parity automaton is given as before through an acceptance game; an alternating B-parity automaton A and a tree t induce the boundedness game pG A,t , B X Parityq, which is defined as before, extended with the colouring function c for the counters. It follows that A defines a function from the set of trees to N Y t8u: rAs ptq is the smallest N such that Eve wins has a strategy in G A,t ensuring BpN q X Parity.

Recall that the theory of regular cost functions aims at defining boundedness properties; hence functions f, g from the set of trees to N Y t8u are considered up to an equivalence relation, which only preserves boundedness properties:

f « g
if for all sets of trees X, f pXq is bounded ðñ gpXq is bounded.

Equivalently, f « g if there exists a non-decreasing function α : N Ñ N such that f ď αpgq and g ď αpf q.

We say that two B-parity automata A, B are equivalent if rAs « rBs.

Theorem 11 (The LoCo conjecture and alternating B-parity automata [START_REF] Colcombet | Fonctions Régulières de Coût[END_REF])

If the LoCo conjecture holds, then for every alternating B-parity automaton, there exists an equivalent non-deterministic B-parity automaton.

In [START_REF] Colcombet | Fonctions Régulières de Coût[END_REF], Colcombet explained how to extend the above construction to B-parity automata:

• the positionality of parity games is replaced by the LoCo conjecture,

• the determinisation over infinite words is replaced by history-deterministic automata.

Note that in this document we only consider the LoCo conjecture for Eve. A similar conjecture can be made for Adam, and a similar construction implies that alternating and non-deterministic S-parity automata are equivalent. Under the assumption that both results are true, this implies that for every cost-MSO formula, there exists an equivalent non-deterministic S-parity automaton, implying the decidability of the boundedness problem for cost-MSO. As shown in [START_REF] Colcombet | The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata[END_REF], this would imply the decidability of the Rabin-Mostowski hierarchy, a long-standing open problem in automata theory.

Refined Statement: Structural Properties of the Arenas

In the previous subsection, we showed the motivations for introducing the LoCo conjecture. A closer inspection reveals that the LoCo conjecture is not used for general arenas, but only for arenas underlying the acceptance game of a tree by an alternating automaton.

In this subsection, we refine the LoCo conjecture by taking this remark into account. First of all, the arenas underlying acceptance games are chronological:

Definition 13 (Chronological arena)

An arena is chronological if there exists a function r : V Ñ N which increases by one on every edge: for all pv, v 1 q P E, rpv 1 q " rpvq `1.

One can be even more precise. The arenas underlying acceptance games for alternating automata over infinite words are word arenas:

Definition 14 (Word arena)
An arena is a word arena of width W if it is chronological, and for all i P N, the set tv P V | rpvq " iu has cardinal at most W .

In the previous subsection, we defined complete labelled trees. We here consider partial unlabeled trees, which are given by T Ď t0, 1u ˚, where T is prefix-closed and non-empty.

A (finite or infinite) branch π is a word in t0, 1u ˚or t0, 1u ω . We say that π is a branch of the tree T if π Ď T (or every prefix of π belongs to T when π is infinite) and π is maximal satisfying this property.

Definition 15 (Thin tree [BIS13])

A tree is called thin if it has only countably many branches. Equivalently, a tree is thin if, and only if, there exists a ranking function rank associating a countable ordinal to every node, such that:

1. if n 1 is a child of n, then rankpn 1 q ď rankpnq, 2. the set of nodes having the same rank is either a single node or an infinite branch of the tree.

The arenas underlying acceptance games for alternating automata over infinite trees are tree arenas: Definition 16 (Tree and thin tree arena) An arena is a tree arena of width W if there exists a function R : V Ñ t0, 1u ˚such that:

1. for all n P t0, 1u ˚, the set tv P V | Rpvq " nu has cardinal at most W .

2. for all pv, v 1 q P E, we have Rpv 1 q " Rpvq ¨ for some P t0, 1u.

It is a thin tree arena if RpV q is a thin tree.

To avoid a possible confusion: in a tree arena, "vertices" refers to the arena and "nodes" to RpV q, so if the arena has width W , then a node is a bundle of at most W vertices.

Observe that in both word and tree arenas, the width corresponds to the size of the automaton. The following refined statement of the LoCo conjecture says that both the trade-off function and the number of memory states can depend on the width of the arena.

Conjecture 2 (LoCo conjecture over tree arenas) For all k, d, W P N, there exists mem P N and α : N Ñ N such that for all boundedness games with k counters, d `1 colors and initial vertex v 0 played over a tree arena of width W , there exists a strategy σ using mem memory states ensuring Bpαpvalpv 0 qqq X Parity.

Note that both functions mem and α depend on k, d and W . In Section 6, we will make this dependence explicit, by considering mem : N 2 Ñ N and α : N 4 Ñ N.

Examples

In this section, we consider special cases of the LoCo conjecture, and gather results from the literature, new results and simple examples.

We start with B games in Subsection 4.1. We then consider two restrictions that make the LoCo conjecture much simpler: finite arenas in Subsection 4.2, and temporal arenas in Subsection 4.3.

We continue with B-reachability games in Subsection 4.4, then B-Büchi games in Subsection 4.5. This case has been solved by Vanden Boom in [START_REF] Vanden | Weak Cost Monadic Logic over Infinite Trees[END_REF] using a slicing technique, and is crucial in the decidability proofs of both weak cost-MSO [START_REF] Vanden | Weak Cost Monadic Logic over Infinite Trees[END_REF] and quasi weak cost-MSO [START_REF] Blumensath | Two-Way Cost Automata and Cost Logics over Infinite Trees[END_REF].

The next step is B-CoBüchi games, considered in Subsection 4.6.

To conclude, we present in Subsection 4.7 a result obtained in collaboration with Sophie Pinchinat and Olivier Serre and published in [START_REF] Fijalkow | Emptiness Of Alternating Tree Automata Using Games With Imperfect Information[END_REF], where we used ideas from the slicing technique to obtain a positionality result for stochastic games over infinite arenas.

The B games

The case of B games, with only counters, is well understood:

Theorem 12 (The LoCo conjecture for B games [CL08a; Col13a]) For all B games with k counters and initial vertex v 0 , Eve has a strategy ensuring Bpk k ¨valpv 0 q 2k q using k! memory states. This result is obtained as the combination of two ideas:

• an adaptation of the Latest Appearance Record (LAR), reducing k counters into k hierarchical counters [START_REF] Colcombet | Fonctions Régulières de Coût[END_REF],

• a reduction from k hierarchical counter into one [START_REF] Colcombet | The Nesting-Depth of Disjunctive µ-Calculus for Tree Languages and the Limitedness Problem[END_REF],

The LAR construction implies a blow-up of k! memory states, and the bounds the value by k ¨valpv 0 q k . The second construction also implies a distortion of the value, from k ¨valpv 0 q k to k k ¨valpv 0 q 2k . The LAR construction extends to B-parity conditions mutatis mutandis, allowing to assume without loss of generality that the counters are hierarchical. The second construction also has a general flavour, and extends to many cases. This is why when considering examples and counter-examples, we usually have only one counter instead of k: the interactions between the counters are not where the difficulty lies. Indeed, the difficulty in understanding boundedness games is in the interactions between the counters and the parity condition.

The Boundedness Games over Finite Arenas

The case of boundedness games over finite arenas is the very special, as in this setting boundedness games are somehow equivalent to ω-regular games.

Theorem 13 (The LoCo conjecture for boundedness games over finite arenas) For all boundedness games with k counters played over a finite arena, Eve has a strategy ensuring Bpn ¨2k q X Parity with 2 k memory states, where n " |V |.

Furthermore, if valpv 0 q ă 8, then valpv 0 q ď n ¨2k .

We sketch the proof. The idea is to approximate the condition B by the following ω-regular condition: for every counter, if it is incremented infinitely many times, then it is reset infinitely many times. This is an over-approximation: if the condition B is satisfied, then the latter is satisfied as well. Furthermore, ω-regular games are bounded-memory determined; more specifically here, there exists a strategy using 2 k memory states, as the condition approximating B X Parity is a conjunction of a Streett condition with k pairs together with a parity condition. A simple pumping argument shows that this strategy also ensures Bpn ¨2k q X Parity.

Note that in this result, the trade-off function depends on the number of vertices in the arena. We will see in Section 5 that this cannot be improved, as the LoCo conjecture does not hold, even over finite arenas.

The same proof yields the following result for the non-uniform case:

Theorem 14 (Non-uniform boundedness games over finite arenas) Non-uniform boundedness games over finite arenas are bounded-memory determined.

The Temporal Boundedness Games

The case of temporal boundedness games is a folklore result in the regular cost function community. The temporal regular cost functions have been introduced in [START_REF] Colcombet | Regular Temporal Cost Functions[END_REF], and correspond to boundedness games where the counters can be incremented and reset, but not left unchanged.

Formally, in a temporal boundedness game the colouring function for the counter actions is c : E Ñ ti, ru k .

Theorem 15 (The LoCo conjecture for temporal boundedness games) For all temporal boundedness games played over a chronological arena, Eve has a strategy ensuring Bp2 ¨valpv 0 qq X Parity using 2 k memory states.

We sketch the proof. Let N " valpv 0 q. The idea is to approximate the condition BpN q by a safety condition; using the fact that the arena is chronological, we slice the arena every N steps, and compose the arena with a memory structure of size 2 k checking for each counter whether it has been reset in the current slice.

Consider the following ω-regular condition: each counter is reset in each slice, and the parity condition is satisfied. Observe that it is positionally determined, as a conjunction of a safety and a parity condition. A strategy ensuring BpN q X Parity also ensures this condition. Conversely, a strategy ensuring this condition ensures Bp2N q X Parity.

This idea of slicing does not extend to the general case where counters can be left unchanged. However, the slicing technique has a similar flavour, see Subsection 4.5.

The B-Reachability Games

v 0 v u N u N -1 . . . u 2 u 1 v ′ 0 v ′ u ′ N u ′ N -1 . . . u ′ 2 u ′ 1 F i N i N i N r i N -1 i r i N -2 i N -2 r i i N -1 r r i N -1 i r i N -2 i N -2 r i i N -1 r
Figure 8: Eve has a 2 memory states strategy ensuring Bp2N q Until Reach, but no positional strategy for this.

For all N P N, we construct a B-reachability game, which is a variant of the one presented in Figure 7 in Subsection 3.1. Recall that in the original game:

• valpv 0 q " N , so Eve has a strategy ensuring BpN q Until Reach using N `1 memory states,

• Eve has a positional strategy ensuring Bp2N q Until Reach, which consists in going directly to F .

The present game repeats the original game twice; it is represented in Figure 8. In this game, the positional strategy cannot be repeated, as it would ensure Bp3N q Until Reach. Hence a second memory state is necessary to reset the value. The wisest choice is then to pick the option u N {2 .

• valpv 0 q " N , so Eve has a strategy ensuring BpN q Until Reach using N `1 memory states,

• Eve has a strategy ensuring Bp2N q Until Reach using 2 memory states,

• no positional strategy ensures Bp2N q Until Reach.

The bound 3N can be deemed acceptable; a simple extension of this example consists in repeating K times the original game, yielding a game where:

• valpv 0 q " N , so Eve has a strategy ensuring BpN q Until Reach using N `1 memory states,

• Eve has a strategy ensuring Bp2N q Until Reach using 2 memory states,

• no positional strategy ensures BpK ¨N q Until Reach.

We can go further, and repeat the original game infinitely many time, yielding the B-Büchi game described in the next subsection.

The B-Büchi Games

We consider now the case of B-Büchi games. The LoCo conjecture holds for B-Büchi games over chronological arenas, and this is so far the best result known about the LoCo conjecture over chronological arenas.

We start with the game represented in Figure 9, which is a variant of Figure 7 in Subsection 3.1. In this game:

• Eve has a strategy ensuring BpN q X Büchi using N `1 memory states, which is the diligent strategy that goes through each option u N , . . . , u 1 in between each visit to a Büchi vertex,

• Eve has a strategy ensuring Bp2N q X Büchi using 2 memory states, which is the careless strategy that alternates between u N {2 and the Büchi vertex,

• no positional strategy ensures B X Büchi.

The following result uses an interesting slicing technique, which is reminiscent of the breakpoint construction of Miyano and Hayashi [START_REF] Miyano | Alternating Finite Automata on omega-Words[END_REF].

v u N u N -1 . . . u 2 u 1 F i N r i N -1 i r i N -2 i N -2 r i i N -1 r
Figure 9: Eve has a 2 memory states strategy ensuring Bp2N q X Büchi, but no positional strategy for B X Büchi.

Theorem 16 (The LoCo for B-Büchi games over chronological arenas [START_REF] Vanden | Weak Cost Monadic Logic over Infinite Trees[END_REF])

For all B-Büchi games over a chronological arena with k counter and initial vertices v 0 , Eve has a strategy ensuring Bpk k valpv 0 q 2k q X Büchi using 2k! memory states.

We illustrate the slicing technique on an example; the proof ideas will be slightly generalised later, in the proof of the LoCo conjecture for boundedness games over word arenas, to remove the least important color when it is odd, see Subsection 6.1.

v 0 . . . . . . u N uN-1 u 2 u 1 F v 1 . . . i N r i N -1 i r i N -1 i N -2 r i i N -1 r
Figure 10: Eve has a 2 memory states strategy ensuring BpN q X Büchi.

Consider the game represented in Figure 10, which is yet another variant of Figure 7 in Subsection 3.1. On a first approximation, it is just an unravelling of the game presented in Figure 9: Eve tries to see infinitely many times Büchi vertices, but each time she does so she has to pay N increments. To keep the counter value below the value N , she can use one of the N options u N , . . . , u 1 ; the th option is available to her only if the counter value is at most , and sets the value to ´1.

The new feature of this game is that when Eve chooses such an option, Adam can decide not to grant it, and instead to go directly to the Büchi vertex, without any action on the counter. Although this is fine for Eve as she visits a Büchi vertex, she has to take into account that the counter value has not been decremented.

As before, there is a diligent strategy ensuring BpN q X Büchi using N `1 memory states, and a simple strategy ensuring Bp2N q X Büchi using 2 memory states, which chooses either u N {2 or the Büchi vertex. More surprisingly so, there is a strategy ensuring BpN q X Büchi using 2 memory states, which is constructed by the slicing technique, and that we describe now.

Fix a strategy ensuring BpN q X Büchi, let us say the diligent one. The slicing decomposes the arena horizontally; the slices are chosen so that the strategy ensures to reach a Büchi vertex in each slice. In our case, the slices consist in N `1 consecutive steps, since the diligent strategy chooses in turn u N , u N ´1, ¨¨¨, u 1 , the Büchi vertex, and then starts over, so it visits a Büchi vertex every N `1 steps.

The slicing techniques constructs two positional strategies for playing in each slice:

• the first is the waiting strategy, that always plays u N ,

• the second is the active strategy, that plays u N , u N ´1, ¨¨¨, u 1 and the Büchi vertex. Note that since each slice contains N `1 steps, if the active strategy starts at the beginning of a slice, it will visit a Büchi vertex before the next slice.

The 2 memory states strategy constructed by the slicing technique alternates between the waiting and the active strategy, as follows:

• when reaching a new slice, it switches to the active strategy,

• if at some point Adam does not grant an action and imposes a visit to the Büchi vertex, then it switches to the waiting strategy until a new slice.

This strategy ensures BpN q X Büchi using 2 memory states.

The B-CoBüchi Games

The case of B-CoBüchi games is the first case for which we do not know whether the LoCo conjecture holds over chronological arenas, or even tree arenas. Here we give two examples:

• A B-CoBüchi game over a word arena where Eve has no bounded-memory strategy to ensure Bpvalpv 0 qq X CoBüchi,

• A B-CoBüchi game over a tree arena where Eve has no positional strategy to ensure B X CoBüchi.

In other words, the first example shows that a trade-off function is necessary for B-CoBüchi games over word arenas, and the second example shows that 2 memory states is necessary for B-CoBüchi games over tree arenas. We start with the game represented in Figure 11. In this game:

F . . . . . . u N uN-1 u 2 u 1 w 1 F ℓ 1 ℓ 2 i N i N v 1 v 2 . . . . . . . . . i N i N r i N -1 i r i N -1 i N -2 r i i N -1 r
Figure 11: Eve has a 2 memory states strategy ensuring Bp2N q X CoBüchipF q, but no strategy using less than N `1 memory states ensures BpN q X CoBüchipF q.

• valpv 0 q " N , so Eve has a strategy ensuring BpN q X CoBüchi using N `1 memory states,

• Eve has a positional strategy ensuring Bp2 ¨N q X CoBüchi,

• no strategy using less than N `1 memory states ensures BpN q X CoBüchi.

At a very high level, this game is again a variant of Figure 7 in Subsection 3.1: the counter value is initialized at N , and Eve has to go through the N options u N , u N ´1, . . . , u 1 to decrease its value one by one, until the value reaches 0 and she can pay N increments to go to the left, where nothing happens anymore.

The implementation of this idea is different, as it here uses a CoBüchi condition instead of the Büchi condition in the previous section. Note that although it has not been presented this way, one can construct a word arena simulating Figure 11, of constant width (namely, 5).

We now look at the following game, played over a tree arena. First, Adam chooses a value n and goes to the tree arena t n . The tree arena t n`1 is represented in Figure 12; it leads to t n . In the tree arena t 0 , the play stops. Although this is again not clear from the representation in Figure 12, one can construct a tree arena simulating Figure 12, of constant width (namely, 3).

For the sake of explanation, we refer to Figure 13, which is behaviourally equivalent to Figure 12. What happens between t n`1 and t n is pretty simple: Eve pays N increments. From u n , she can loop and reset the value, and proceeds to t n .

The reasonable strategy is of course to first reset, and then proceeds; this requires 2 memory states. A positional strategy would either reset forever, or never, in which case the counter value would grow unbounded.

To summarise:

• valpv 0 q " N , and Eve has a strategy ensuring BpN q X CoBüchi using 2 memory states, • no positional strategy ensures B X CoBüchi.

t n+1 F F F F F t n t n t n t n t n i N i N i N i N i N

Application of the Slicing Technique for Stochastic Games

In this subsection, we report on a result obtained in collaboration with Sophie Pinchinat and Olivier Serre and published in [START_REF] Fijalkow | Emptiness Of Alternating Tree Automata Using Games With Imperfect Information[END_REF]. Note that the paper [START_REF] Fijalkow | Emptiness Of Alternating Tree Automata Using Games With Imperfect Information[END_REF] actually deals with emptiness checking of alternating automata, and in particular introduces the class of alternating qualitative automata; the corollary of the positionality result that we present here is the decidability of the emptiness problem for alternating qualitative Büchi automata.

We do not develop this further, and focus on the positionality result, as it makes use of the slicing technique, discussed in Subsection 4.5.

Before stating the result, we define stochastic games:

Definition 17 (Stochastic game)

A stochastic arena is an arena whose vertex set is divided into three subsets: vertices controlled by Eve pV E q, vertices controlled by Adam pV A q, and random vertices pV R q. It additionally features a probabilistic transition ∆ : V R Ñ DpV q, where DpV q is the set of distributions over V (see Subsection 1.1 for the definition of distributions).

By convention, the set E of edges is such that for every v P V R and v 1 P V , we have pv, v 1 q P E if, and only if, ∆pvqpv 1 q ą 0.

A pair of strategies σ for Eve and τ for Adam induces a set of infinite plays, which is equipped with the appropriate probability measure. For a measurable event W , we denote P σ,τ pW q its probability.

A strategy σ for Eve is said almost-surely winning for the condition W if for all strategies τ of Adam, we have P σ,τ pW q " 1.

Note that we did not extend the definition of strategies to include randomized strategies, which are strategies σ : E ˚¨V E Ñ DpEq. Since here pure strategies are sufficient, i.e. strategies σ : E ˚¨V E Ñ E, we will consider only them.

Theorem 17 (Positionality for Stochastic Büchi Games with Almost-Sure Semantics) For all stochastic Büchi games played over a chronological arena with finite out-degree, for all initial vertices, if Eve has an almost-surely winning strategy, then she has a positional almost-surely winning strategy.

We will use the following result for finite arenas. We state it here in a rather weak form (with the chronological assumption), as it can be easily proved by a backward induction, whereas the proof for general finite arenas is more involved. We refer to [START_REF] Condon | The Complexity of Stochastic Games[END_REF] for the original proof, and to [START_REF] Kucera | Turn-Based Stochastic Games[END_REF] for a nice survey.

Lemma 12 (Positionality for Stochastic Reachability Games over Finite Arenas)

For all stochastic reachability games played over a chronological and finite arena, if for every vertex v 0 in a given subset X of vertices Eve has strategy ensuring to win with probability at least 1 2 from v 0 , then she has a uniform positional strategy ensuring to win with probability at least 1 2 from X.

We first sketch the proof. The main idea is to note that if Eve can ensure to reach a Büchi vertex with probability 1 from some initial vertex, then there exists a bound k such that she can ensure to reach a Büchi vertex with probability at least 1 2 within k steps against any strategy of Adam. This allows to "slice" the arena into infinitely many disjoint finite arenas: in each slice Eve plays to reach a Büchi vertex with probability at least 1 2 . Since each slice forms a finite subarena, Eve can use positional strategies there thanks to Lemma 12.

The resulting strategy consists in playing in turns the above positional strategies; since each slice gives a probability to reach a Büchi vertex of at least 1 2 before proceeding to the next, the probability to reach infinitely many Büchi vertices is 1.

Proof. We fix an initial vertex and an almost-surely winning strategy σ from there. Note that σ is almost-surely winning from all reachable vertices; from now on we restrict to such vertices.

We first claim that for every vertex v, there exists k P N such that for all strategies τ of Adam we have P σ,τ pV ďk ¨F ¨V ω q ě 1 2 from v, i.e. σ ensures to reach a Büchi vertex within k steps with probability at least 1 2 from v. Towards contradiction, assume that such a k does not exist. Hence, for each k there exists a strategy τ k such that P σ,τ k pV ďk ¨F ¨V ω q ă 1 2 . From the sequence pτ k q kPN we extract a strategy τ 8 that is consistent, for any k P N, with infinitely many τ h on its k first moves. Note that this is possible since the arena has finite out-degree.

Consider the pair of strategies σ and τ 8 . For k P N, there exists h ě k such that P σ,τ8 pV ďk ¨F ¨V ω q " P σ,τ h pV ďk ¨F ¨V ω q ď P σ,τ h pV ďh ¨F ¨V ω q ď 1 2 .

Since V ˚¨F ¨V ω " Ť kPN V ďk ¨F ¨V ω , and the sequence pV ďk ¨F ¨V ω q kPN is increasing for set inclusion, this implies that P σ,τ8 pV ˚¨F ¨V ω q " lim k P σ,τ8 pV ďk ¨F ¨V ω q ď 1 2 , which leads a contradiction with σ being almost-surely winning. This proves the claim.

For k ă k 1 , define G rk,k 1 s the arena induced by G restricted to vertices of rank in rk, k 1 s. Since G has finite out-degree, there are finitely many vertices of rank in rk, k 1 s, hence G rk,k 1 s is finite.

We define inductively a sequence of ranks pk i q iPN together with a sequence of strategies pσ rk i ,k i`1 r q iPN such that for all i P N, σ rk i ,k i`1 r is a positional strategy, defined on all vertices of rank rk i , k i`1 r, such that from all vertices of rank k i , for all strategies τ of Adam, we have P σ rk i ,k i`1 r ,τ pV ď ¨F ¨V ω q ě 1 2 , where " k i`1 ´ki . Set k 0 " 0. Assume the first i ranks and strategies are defined. For each vertex of rank k i , the above claim implies the existence of a bound; since there are finitely many such vertices, we can consider the maximum of those bounds, and denote it by k i`1 . By construction, from all vertices of rank k i , for all strategies τ of Adam, we have P σ rk i ,k i`1 r ,τ pV ď ¨F ¨V ω q ě 1 2 , where " k i`1 ´ki . In other words, Eve has a strategy in the reachability game played over the chronological and finite arena G rk i ,k i`1 s ensuring to win with probability at least 1 2 , so thanks to Lemma 12 there exists a uniform positional strategy ensuring to reach a Büchi vertex with probability at least 1 2 , denote it σ rk i ,k i`1 r . This concludes the inductive construction.

The arenas G rk i ,k i`1 s are called slices. Now define σ 8 as the disjoint union of the strategies σ rk i ,k i`1 r . This is a positional strategy; we argue that it is almost-surely winning. Indeed, since σ 8 ensures that going through any slice, a Büchi vertex will be visited with probability at least 1 2 , the Borel-Cantelli Lemma implies that infinitely many Büchi vertices will be visited with probability 1.

Counter Examples

In this section, we show that the LoCo conjecture does not hold, even for finite arenas. This is a joint work with Florian Horn, Denis Kuperberg and Michał Skrzypczak [START_REF] Fijalkow | Trading Bounds for Memory in Games with Counters[END_REF].

Theorem 18 (The LoCo conjecture does not hold) For all K, for all N , there exists a B-reachability game played over a finite arena with one counter and an initial vertex such that:

• there exists a 3 K memory states strategy ensuring BpKpK `3qq Until Reach,

• no K `1 memory states strategy ensures BpN q Until Reach.

We proceed in two steps. The first is an example giving a lower bound of 3 explained in Subsection 5.1, and the second is a nesting of this first example, given in Subsection 5.2.

We then show how to adapt the example to prove that non-uniform boundedness games are not finite-memory determined, in Subsection 5.3.

A first lower bound of 3

We start with a first lower bound of 3. The arena G 1 is represented in Figure 14. The condition is B Until Reach. In this game, Eve is torn between going to the right to reach F , which implies incrementing the counter, and going to the left, to reset the counter. The actions of Eve from the vertex u n are:

• increment, and go one step to the right, to v n´1 ,

• reset, and go two steps to the left, to v n`2 .

The actions of Adam from the vertex v n are:

• play, and go down to u n ,

• skip, and go to v n´1 . Formally (note that the colouring functions c : E Ñ tε, i, ru and c : V Ñ t0, 1u are definitely together with the graph here):

v 9 v 8 v 7 v 6 v 5 v 4 v 3 v 2 v 1 v 0 F u 9 u 8 u 7 u 6 u 5 u 4 u 3 u 2 u 1 u 0 i i i i i i i i i i r r r r r r r r
V " " V E " tu n | n P Nu Y tF u V A " tv n | n P Nu E " $ ' ' & ' ' % tv n`1 Ý Ñ v n | n P Nu Y tv n Ý Ñ u n | n P Nu Y tu n`1 i ÝÑ v n | n P Nu Y tu 0 i ÝÑ F u Y tu n r Ý Ý Ñ v n`2 | n P Nu Proposition 1 (A lower bound of 3)
In pG 1 , B Until Reachq:

• Eve has a 4 memory states strategy ensuring Bp3q Until Reach,

• Eve has a 3 memory states strategy ensuring Bp4q Until Reach,

• For all N , no 2 memory states strategy ensures BpN q Until Reach from v N .

Proof. The first item follows from Lemma 11. However, to illustrate the properties of the game G 1 we will provide a concrete strategy with 4 memory states that ensures Bp3q Until Reach. The memory states are i 1 , i 2 , i 3 and r, linearly ordered by i 1 ă i 2 ă i 3 ă r. With the memory states i 1 , i 2 and i 3 , the strategy chooses to increment, and updates its memory state to the next memory state. With the memory state r, the strategy chooses to reset, and updates its memory state to i 1 . This strategy satisfies a simple invariant: it always resets to the right of the previous reset, if any. We show how to save one memory state, at the price of increasing the bound by one: we construct a 3 memory states strategy ensuring Bp4q Until Reach. The idea, as represented in Figure 15, is to color every second vertex and to use this information to track progress. The 3 memory states are called i, j and r. The update is as follows: the memory state is unchanged in uncoloured (white) states, and switches from i and j and from j to r on gray states. The strategy is as follows: in the two memory states i and j, Eve chooses to increment, and in r she chooses to reset. As for the previous strategy, this strategy ensures that it always resets to the right of the previous reset, if any.

v 9 v 8 v 7 v 6 v 5 v 4 v 3 v 2 v 1 v 0 F u 9 u 8 u 7 u 6 u 5 u 4 u 3 u 2 u 1 u 0 i i i i i i i i i i r r r r r r r r
We now show that 2 memory states is not enough. Assume towards contradiction that there exists a 2 memory states strategy ensuring BpN q Until Reach from v 2N , for some N , using the memory structure M.

We first argue that without loss of generality we can assume that the strategy σ is normalized, i.e. satisfies the following three properties:

1. for all n ď 2N , there is at least one memory state that chooses increment from u n , 2. for all n ď 2N but at most N of them, there is at least one memory state that chooses reset from u n , 3. no play from pv 2N , m 0 q consistent with σ comes back to v 2N .

Indeed:

1. Assume towards contradiction that this is not the case, then there exists n such that Eve resets from u n with both memory states; Adam can loop around this u n , contradicting that σ ensures to reach F .

2. Assume towards contradiction that there are at least N `1 vertices u n from which Eve increments from u n with both memory states; Adam can force N `1 increments without a reset, contradicting that σ ensures BpN q.

3. For m and m 1 two memory states, we say that m ă m 1 if there exists a play from pv 2N , m 1 q consistent with σ which reaches pv 2N , mq. Since σ ensures to reach F , the graph induced by ă is acyclic. We can take as initial memory state from v 2N the smallest memory state which is smaller than or equal to m 0 .

We fix the strategy of Adam which skips if, and only if, both memory states of σ choose to increment. Consider the play from v 2N consistent with σ and this strategy of Adam. This means that for all vertices u n that are reached, there is one memory state that resets, and one that increments. Since σ ensures BpN q and there are at most N positions skipped, at some point Eve chooses to reset. From there two scenarios are possible:

• Either Eve keeps resetting until she reaches v 2N , contradicting that σ is normalized,

• Or she starts incrementing again, which means that she uses the same memory state than she did before the reset, implying that there is a loop, contradicting that σ ensures to reach F .

General lower bound

We now push the example above further. A first approach is to modify G 1 by increasing the length of the resets, going steps to the left rather than only 2. However, this does not give a better lower bound: there exists a 3 memory states strategy in this modified game that ensures twice the value, following the same ideas as presented above.

v 9 v 8 v 7 v 6 v 5 v 4 v 3 v 2 v 1 v 0 F u 1,9 u 1,8 u 1,7 u 1,6 u 1,5 u 1,4 u 1,3 u 1,2 u 1,1 u 1,0 u 2,10 u 2,8 u 2,6 u 2,4 u 2,2 u 2,0 i i i i i i i i i i i i i i i i r r r r r r r r r r r
Figure 16: The game with two levels.

We construct G K,N , a nesting of G 1 with K levels. Unlike G 1 , it is finite, as we only keep a long enough "suffix". In Figure 16, we represented the interaction between two levels. Roughly speaking, the two levels are independent, so we play both games at the same time. Those two games use different timelines. For instance, in Figure 16, the bottom level is based on p`1, ´2q (an increment goes one step to the right, a reset two steps to the left), and the top level is based on p`2, ´4q. This difference in timeline ensures that a strategy for Eve needs to take care somehow independently of each level, ensuring that the number of memory states depends on the number of levels.

To give the formal definition of G K,N , we need two functions, dpK, N q " pN `1q K´1 and npK `1, N q "

# 2N if K " 0, pN `1q K`1 `pN `1q ¨npK, N q otherwise.
We now define G K,N (note that the colouring functions c : E Ñ tε, i, ru and c : V Ñ t0, 1u are definitely together with the graph here):

V " " V E " tu p,n | p P t1, . . . , Ku, n P t0, . . . , npK, N quu Y tF u V A " tv n | n P t0, . . . , npK, N quu E " $ ' ' ' ' ' & ' ' ' ' ' % tv n`1 Ý Ñ v n | nu Y tv n Ý Ñ u p,n | p, nu Y tu p,n`dpp,N q i ÝÑ v n | p, nu Y tu p,0 i ÝÑ F | pu Y tu p,n r Ý Ý Ñ v n`pp`1q¨dpp,N q | p, nu Observe that G 1,N is the "suffix" of length np1, N q of G 1 , for all N .
Proposition 2 (General lower bound)

In pG K,N , B Until Reachq:

• Eve has a 3 K memory states strategy ensuring BpKpK `3qq Until Reach,

• No K `1 memory states strategy ensures BpN q Until Reach from v npK,N q .

Proof. We start by constructing a strategy with 3 K memory states ensuring BpKpK 3qq Until Reach. To this end, we construct for the p th level a strategy with 3 memory states ensuring Bp2pp `1qq Until Reach, using the same ideas as for G 1 , colouring every pp`1q¨dpp, N q vertices. Now we construct the general strategy by playing independently in each copy, except that when a reset is taken, all memory structures update to the (initial) memory state i. This way, it ensures that it always resets to the right of the previous reset, if any. It uses 3 K memory states, and ensures Bp ř K p"1 2 ¨pp `1qq Until Reach, i.e. BpKpK `3qq Until Reach.

We now show that K `1 memory states is not enough. We proceed by induction on K. The case K " 1 follows from Proposition 1.

Consider a strategy ensuring BpN q Until Reach from v npK`1,N q in G K`1,N , for some N , using the memory structure M. We will prove that it has at least K `2 memory states. To this end, we will show that it induces a strategy ensuring BpN q Until Reach in G K,N , which uses one less memory state. The induction hypothesis will conclude.

First of all, for the sake of readability we will use n K`1 " npK `1, N q, n K " npK, N q and d " dpK `1, N q.

Consider the N `1 plays, for k P t0, . . . , N u, where from v n K`1 ´k¨pn K `dq Adam skips n K times and then plays:

v n K`1 ´k¨pn K `dq skip Ý Ý Ñ v n K`1 ´k¨pn K `dq´n K play Ý Ý Ñ u K`1,n K`1 ´k¨pn K `dq´n K .
(Note that this is well defined because by definition, n K`1 ´pN `1q ¨pn K `dq " 0.) We argue that there exists k P t0, . . . , N u and a memory state m P M such that if σ starts the k th play with the memory state m, then σ resets in u K`1,n K`1 ´k¨pn K `dq´n K . Assume towards contradiction that this is not the case, then by concatenating all plays with the matching memory state we get a play starting from v n K`1 with the memory state m 0 , which is consistent with σ and contains N `1 increments without resets, contradicting that σ ensures BpN q.

Let k P t0, . . . , N u and m P M satisfying the above property: denote n " n K`1 ´k pn K `dq, in the play from pv n , mq where Adam skips n K times and then plays, leading to u K`1,n´n K , the strategy σ resets. Up to renaming, we can assume that the memory state assumed along this play is always the same, denoted m. Observe that resetting from u K`1,n´n K leads to the left of v n , since by definition pK `2q ¨d ě n K .

Consider the memory state assumed when starting from pv n K`1 , m 0 q, Adam skips until he reaches v n ; denote it m 0 as well, by assumption σ ensures BpN q Until Reach from pv n , m 0 q. Furthermore, without loss of generality we can assume that no play from pv n , m 0 q consistent with σ comes back to v n , following the same proof as for G 1 . This implies that no plays from pv n , m 0 q consistent with σ reach pv n 1 , mq for some n 1 P tn ´nK , . . . , nu, as from there Adam would lead to u K`1,n´n K where σ would reset, leading to the left of v n , from where Adam would lead to v n by skipping an appropriate number of times.

The strategy σ induces a strategy σ 1 using one less memory state, which ensures BpN q Until Reach 1 from v n , where F 1 " tv n 1 | n 1 ă n ´nK u. The strategy σ 1 can be seen as a strategy in G K,N from v n K , so the induction hypothesis concludes.

Corollary

Theorem 19 (Non-uniform boundedness games are not finite-memory determined)

There exists a B-Büchi game and an initial vertex such that:

• Eve has a strategy ensuring B X Büchi,

• no finite-memory strategy ensures B X Büchi.

Proof. We construct a B-Büchi game, relying on the arenas G K,N from Theorem 18. In this game:

• first, Adam chooses a value K, that will be fixed for the whole play,

• then the game proceeds by rounds (possibly infinitely many). In a round, Adam chooses a value N and the game continues in G K,N ; upon reaching F the round ends and the counter is reset.

The condition is B X Büchi; the Büchi condition is equivalent to playing infinitely many rounds.

We first show that Eve has a winning strategy. Thanks to Theorem 18 she has a strategy ensuring BpKpK `3qq Until Reach in G K,N ; note that the strategy is different for different values of N , but the bound is independent of N . Playing this strategy ensures B X Büchi.

We now show that there is no finite-memory winning strategy. Assume towards contradiction that there is such a winning strategy, using mem memory states. Consider the strategy of Adam which consists in first choosing K " mem, and then an unbounded sequence for N . Thanks to Theorem 18, the strategy in G K,N does not ensure BpN q Until Reach, so either F is never reached or the counter value exceeds N . It follows that either the Büchi condition is not satisfied, or the counter values are unbounded, leading to a contradiction.

Thin Trees

In this section, we prove that the LoCo conjecture holds for the special case of thin tree arenas. This is a joint work with Florian Horn, Denis Kuperberg and Michał Skrzypczak [START_REF] Fijalkow | Trading Bounds for Memory in Games with Counters[END_REF].

Theorem 20 (The LoCo conjecture for thin tree arenas) There exist two functions mem : N 2 Ñ N and α : N 4 Ñ N such that for all boundedness games with k counters and d `1 colors over thin tree arenas of width W , for all initial vertices v 0 , Eve has a strategy to ensure Bpk k ¨valpv 0 q 2k ¨αpd, k, W `2, valpv 0 qqq X Parity, with W ¨3k ¨2k! ¨mempd, kq memory states.

The functions α and mem are defined inductively. Since the proof will work by induction on the number of colors, removing the least important color, we define four functions:

• α 0 and mem 0 when the least important color is 0, so the set of colors is t0, . . . , du,

• α 1 and mem 1 when the least important color is 1, so the set of colors is t1, . . . , du:

α 0 pd, k, W, N q " α 1 pd ´1, k `1, 3W, W ¨pN `1q k q, α 1 pd, k, W, N q " # k k ¨N 2k if d " 2, α 0 pd, k, 2W, N q otherwise, mem 0 pd, kq " 2 ¨mem 1 pd ´1, k `1q, mem 1 pd, kq " # 2 ¨k! if d " 1, 2 ¨mem 0 pd, kq otherwise.
Define α " α 0 and mem " mem 0 . As an intermediate result, in Subsection 6.1 we will prove that the conjecture holds for the special case of word arenas.

Existence of a trade-off for word arenas

This subsection is devoted to proving the following result: Proposition 3 (The LoCo conjecture over word arenas) There exists two functions mem : N 2 Ñ N and α : N 4 Ñ N such that for all B-parity games over word arenas of width W with initial vertex v 0 , Eve has a strategy to ensure Bpαpd, W, k, valpv 0 qqq X Parity, with mempd, kq memory states.

We prove Proposition 3 by induction on the colors in the parity condition. Consider a B-parity game G. We examine two cases, depending whether the least important color (i.e the smallest) that appears is odd or even:

• if the set of colors is t1, . . . , du, then we construct a B-parity game G 1 using t2, . . . , du as colors,

• if the set of colors is t0, . . . , du, then we construct a B-parity game G 1 using t1, . . . , du as colors.

In both cases, we obtain from the induction hypothesis a winning strategy using few memory states in G 1 , which we use to construct a winning strategy using few memory states in G. The base case is given by Büchi conditions, and follows from Theorem 16. Let k be the number of counters, W the width of the word arena G, and v 0 the initial vertex. The ranking function is denoted r : V Ñ N, and the two colouring functions c : E Ñ tε, i, ru k and Ω : V Ñ t0, . . . , du (or t1, . . . , du). Denote N " valpv 0 q.

Removing the least important color: the odd case

The first case we consider is when the least important color is 1. The proof that follows is an extension of the slicing technique developed by Vanden Boom [START_REF] Vanden | Weak Cost Monadic Logic over Infinite Trees[END_REF] and illustrated in Subsection 4.5. Note that if 1 is the only color in the arena, then Eve cannot win and the result is true; we now assume that the color 2 also appears in the arena.

Let σ be a strategy ensuring BpN q X Parity from v 0 . Without loss of generality we restrict ourselves to vertices reachable with σ from v 0 . Consider a vertex v and T v the tree of plays consistent with σ. The strategy σ ensures the parity condition, so in particular every branch in T v contains a vertex of color greater than 1. We prune the tree T v by cutting paths when they first meet a vertex of color greater than 1. Since the arena has finite out-degree, so is T v and by König's Lemma the tree obtained is finite. Thus, to every vertex v, we can associate a rank r v such that the strategy σ ensures that all paths from v contain a vertex of color greater than 1 before reaching the rank r v .

For k ă k 1 , define G rk,k 1 s the arena induced by G restricted to vertices of rank in rk, k 1 s. Since G has finite out-degree, there are finitely many vertices of rank in rk, k 1 s, hence G rk,k 1 s is finite.

We define inductively a sequence of ranks pk i q iPN , such that for all i P N, the strategy σ ensures that from all vertices of rank k i , a vertex of color greater than 1 is seen before reaching the rank k i`1 . We first set k 0 " r v 0 . Assume k i has been defined, we define k i`1 as max vPV tr v | rpvq " k i u.

The arenas G rk i ,k i`1 s are called slices. Now we equip G with a memory structure M of size 3 which keeps track whether or not a vertex of color greater than 1 has been reached in the current slice. Formally, M has three memory states:

• the memory state @ 1 means that all vertices visited in the current slice have color 1,

• the memory state D ą1 means that some vertex visited in the current slice has color greater than 1,

• the memory state K means that a whole slice has been crossed visiting only vertices of color 1.

The initial state is @ 1 if Ωpv 0 q " 1, and D ą1 otherwise. The update function is defined as follows:

µpm, pv, v 1 qq " $ ' ' ' ' ' ' & ' ' ' ' ' ' % D ą1 if Ωpv 1 q ą 1, D ą1 if m " D ą1 and rpv 1 q R tk i | i P Nu, @ 1 if Ωpv 1 q " 1, m " @ 1 and rpv 1 q R tk i | i P Nu, @ 1 if Ωpv 1 q " 1 and rpv 1 q P tk i | i P Nu, K otherwise.
We construct the expanded arena G ˆM equipped with the colouring function given by the three colouring functions c 1 : E ˆM Ñ tε, i, ru k , Ω 1 : V ˆM Ñ t2, . . . , du and c S : V ˆM Ñ t0, 1u defined by: c 1 pe, _q " cpeq.

Ω 1 pv, _q " # Ωpvq if Ωpvq ‰ 1, 2 otherwise. c S p_, mq " # 1 if m " K, 0 otherwise.
We equip G ˆM with the condition B X Parity X Safe, where B uses the colouring function c, Parity uses the colouring function Ω 1 , and Safe uses the colouring function c S .

The correctness of the construction is stated in the following lemma:

Lemma 13 (Correctness of the construction)

1. There exists a strategy σ 1 in G ˆM ensuring BpN q X Parity X Safe.

2. Assume there exists a strategy σ 1 in G ˆM ensuring BpN 1 q X Parity X Safe using K memory states, then there exists a strategy σ in G ensuring BpN 1 q X Parity using 2K memory states.

Proof.

1. The strategy σ 1 that simulates σ, ignoring the memory structure M, ensures BpN qX Parity X Safe by construction.

2. Let σ 1 be a strategy in G ˆM ensuring BpN 1 q X Parity X Safe using M 1 as memory structure. This induces σ using M ˆM1 as memory structure. Since plays of σ and of σ 1 are in one-to-one correspondence, σ ensures BpN 1 q X Parity. Further, the safety condition satisfied by σ 1 ensures that infinitely often a vertex of color greater than 1 is seen (specifically, in each slices), so σ satisfies Parity.

Note that since σ is winning, it does not make use of the memory state K, so it uses only 2K memory states.

We conclude thanks to the induction hypothesis and Lemma 3 (to handle the additional safety condition).

Removing the least important color: the even case

The second case we consider is when the least important color is 0. We explain the intuition for the case of CoBüchi conditions, i.e if there are only colors 0 and 1. Recall that F " tv | Ωpvq " 1u. Define S 0 " A 0 " H, and for i ě 1:

"

S i`1 " tv P V | there exists σ that ensures not to visit F before A i from v, if at allu A i`1 " tv P V | there exists σ that ensures to reach S i`1 from vu.

We have Ť iPN S i " Win E pCoBüchiq. A winning strategy based on these sets has two aims: in S i it avoids F ("Safe" mode) and in A i it attracts to the next S i ("Attractor" mode). The key property is that since the arena is a word arena of width W where Eve can bound the counters by N , she only needs to alternate between modes a number of times bounded by a function of N and W . In other words, the sequence pY i q iPN stabilises after a number of steps bounded by a function of N and W . (A remote variant of this bounded-alternation fact can be found in [START_REF] Kupferman | Weak Alternating Automata are not that Weak[END_REF].) Hence the CoBüchi condition can be checked using a new counter and a Büchi condition, as follows.

There are two modes: "Safe" and "Attractor". The Büchi condition ensures that the "Safe" mode is visited infinitely often. In the "Safe" mode, only vertices of colors 0 are accepted; visiting a vertex of color 1 leads to the "Attractor" mode and increments the new counter. At any time, she can reset the mode to "Safe". The counter is never reset, so to ensure that it is bounded, Eve must change modes finitely often. Furthermore, the Büchi condition ensures that the final mode is "Safe", implying that the CoBüchi condition is satisfied.

For the more general case of parity conditions, the same idea is used, but as soon as a vertex of color greater than 1 is visited, then the counter is reset.

Define G 1 :

V 1 " # V 1 E " V E ˆtA, Su Y V V 1 A " V A ˆtA, Su.
The correctness of the construction is stated in the following lemma:

Lemma 15 (Correctness of the construction)

1. There exists a strategy σ 1 in G 1 that ensures BpW ¨pN `1q k q X Parity.

2. Assume there exists a strategy σ 1 in G 1 ensuring BpN 1 q X Parity using K memory states, then there exists a strategy σ in G ensuring BpN 1 qXParity using 2K memory states.

Proof.

1. Thanks to Lemma 11, there exists a strategy σ in G ensuring BpN q X Parity using a memory structure M of size pN `1q k . We construct a strategy σ 1 in G 1 simulating σ. We now explain when does σ 1 chooses to set the "Safe" mode.

We consider the arena G ˆM, it is a word arena of width W ¨pN `1q k , and restrict it to the moves prescribed by σ, obtaining the word arena G σ of width W ¨pN `1q k . Without loss of generality we restrict G σ to vertices reachable with σ from the initial vertex pv 0 , 0q. Consider a vertex v of color 0 or 1, and G v σ the word arena obtained by considering v as initial vertex and pruned by cutting paths when they first meet a vertex of color greater than 1. Since the strategy σ ensures that the parity condition is satisfied, every infinite path in G v σ contains finitely many vertices of color 1. Relying on Lemma 14 for the word arena G v σ and F the set of vertices of color 1, we associate to each vertex v 1 in G v σ a rank with respect to v, which is a number between 1 and 2W ¨pN `1q k , the minimal i such that v 1 P X i pG v σ q. Now consider a play consistent with σ, and a suffix of this play starting in a vertex v of color 0 or 1. By definition, from this position on, the rank (with respect to v) is non-increasing until a vertex of color greater than 1 is visited, if any. Furthermore, if the rank is even then no vertices of color 1 are visited, and the rank does not remain forever odd.

The strategy σ 1 in G 1 simulates σ, and at any point of a play remembers the first vertex v that has not been followed by a vertex of color greater than 1. As observed above, the rank with respect to v is non-increasing; the strategy σ 1 switches to the "Safe" mode when the rank goes from even to odd. By definition, the new counter is incremented only when the rank goes from odd to even, which happens at most W ¨pN `1q k times, and it is reset when a vertex of color greater than 1 is visited, so σ 1 ensure that it remains bounded by W ¨pN `1q k . Also, since σ ensures to bound the counter values by N , then so does σ 1 . For the parity condition, there are two cases. Consider a play consistent with σ 1 . Either from some point onwards the only colors seen are 0 and 1 (with respect to Ω), then the new counter is not reset after this point, but it is incremented only when the rank decreases from odd to even, which corresponds to switches of mode from "Safe" to "Attractor". Since this counter is bounded, the mode stabilises, which by definition of the ranks imply that the stabilised rank is odd, so the mode is "Safe", and from there on only vertices of color 0 (with respect to Ω) are visited, hence Parity is satisfied. Or infinitely many vertices of color greater than 1 are seen (with respect to Ω), but since they coincide for Ω and Ω 1 , the condition Parity is satisfied.

It follows that σ 1 ensures BpW ¨pN `1q k q X Parity.

2. Let σ 1 be a strategy in G 1 ensuring BpN 1 q X Parity using M 1 as memory structure of size K. We construct σ that simulates σ 1 ; to this end, we need a memory structure which simulates both M 1 and the mode alternation, of size 2K. By definition, plays of σ and plays of σ 1 are in one-to-one correspondence, so σ ensures BpN 1 q. For the parity condition, there are two cases. Consider a play consistent with σ 1 . Either from some point onwards the only colors seen are 0 and 1 (with respect to Ω), then the new counter is not reset after this point, but it is incremented each time the mode switches from "Safe" to "Attractor"; since this counter is bounded, the mode stabilises, and since the play in G 1 satisfies Parity, the stabilised mode is "Safe", implying that from there on only vertices of color 0 (with respect to Ω) are visited, hence satisfy Parity. Or infinitely many vertices of color greater than 1 are seen (with respect to Ω), but since they coincide for Ω and Ω 1 , the condition Parity is satisfied.

The induction hypothesis concludes.

Extending to thin tree arenas

In this subsection, we extend the results for word arenas to thin tree arenas, proving Theorem 20.

Consider a B-parity game G. Define N " valpv 0 q. Let R : V Ñ t0, 1u ˚witnessing that G is a thin tree arena. Let σ be a strategy ensuring BpN q X Parity from v 0 . We rely on the decomposition of the thin tree RpV q to locally replace σ by strategies using small memory given by Proposition 3.

It follows from Fact 15 that along a play, the rank is non-increasing and decreases only finitely many times. Since the parity condition is prefix-independent, if for each rank Eve plays a strategy ensuring the parity condition, then the resulting strategy ensures the parity condition; however, a closer attention to the counters is required.

We summarise counter actions as follows: let w P ptε, i, ru k q ˚, its summary sumpwq P tε, i, ru k is, for each counter, r if the counter is reset in w, i if the counter is incremented by not reset in w, and ε otherwise.

Fact 2 (Summary)

Consider w " w 1 w 2 ¨¨¨w n w 8 , where w 1 , . . . , w n P ptε, i, ru k q ˚and w 8 P ptε, i, ru k q ω . Denote u " sumpw 1 qsumpw 2 q ¨¨¨sumpw n qsumpw 8 q, then:

1. valpuq ď valpwq, 2. if for all i P t1, . . . , n, 8u we have valpw i q ď N 1 and valpuq ď N , then valpwq ď N ¨N 1 .

We define a B game G 1 , where the plays that remain in vertices of the same rank are summarised in one step. It has k counters. Let rankpV q denote the set of ranks (subset of the countable ordinals), and S the set of all strategies in G ensuring BpN q X Parity. We define the set of vertices of G 1 :

V 1 " " V 1 E " rankpV q ˆt1, . . . , W u ˆtε, i, ru k V 1
A " rankpV q ˆt1, . . . , W u ˆS

We explain how a couple pν, q P rankpV q ˆt1, . . . , W u uniquely determines a vertex in G.

First, the rank ν corresponds in R either to a node or to an infinite branch, in the second case we consider the first node in this branch. Second, the component identifies a vertex in this node. We say that pν, 1 , aq is an outcome of pµ, , σq if there exists a play from the vertex corresponding to pµ, q consistent with σ ending in the vertex corresponding to pν, 1 q whose summarised counter actions are a. We define the set of edges of G 1 , together with the counter actions c 1 : E 1 Ñ tε, i, ru k : 1 , aq is an outcome of pµ, , σqu.

E 1 " # tppν, , aq a Ý Ý Ñ pν, , σqq | , ν, σu tppµ, , σq ε Ý Ý Ñ pν, 1 , aqq | if pν,

Lemma 16 (Correctness of the construction)

1. There exists a strategy σ 1 in G 1 ensuring BpN q.

2. Assume there exists a strategy σ 1 in G 1 ensuring BpN 1 q using K memory states, then there exists a strategy σ in G ensuring BpN 1 ¨αpd, W `2, k, N qq X Parity using W ¨3k ¨K ¨mempd, kq memory states.

Proof.

1. We argue that the strategy σ induces a strategy σ 1 in G 1 ensuring BpN q. A play consistent with σ 1 is of the form u " sumpw 1 qsumpw 2 q ¨¨¨sumpw n qsumpw 8 q, where w " w 1 w 2 ¨¨¨w n w 8 is a play consistent with σ, following the notations of Fact 2. This fact, item 1., implies that valpuq ď valpwq, so valpuq ď N . Hence the strategy σ 1 ensures BpN q.

2. Assume there exists a strategy σ 1 in G 1 ensuring BpN 1 q and using a memory structure M of size K. We construct a strategy in G ensuring BpN 1 ¨αpd, W `2, k, N qqXParity using W ¨3k ¨K ¨mempd, kq memory states. The memory structure is the product of four memory structures:

• a memory structure that keeps track of the P t1, . . . , W u used when entering the current rank, of size W ,

• a memory structure that keeps track of the summary since entering the current rank, of size 3 k ,

• the memory structure M, of size K,

• a memory structure of size mempd, kq, which is used to simulate the strategies obtained from Proposition 3.

Consider ν P rankpV q that corresponds to an infinite branch of RpV q. For every P t1, . . . , W u and m P M , the strategy σ 1 picks a strategy σ 1 pν, , mq to play in this infinite branch, ensuring BpN q X Parity. When playing this strategy, two scenarios are possible: either the play stays forever in the infinite branch, or an outcome is selected and the game continues from there.

We define an arena G ν, obtained from G as follows: the set of vertices is the vertices belonging to the infinite branch corresponding to ν, and the initial vertex is the one corresponding to pν, q. We add two vertices, corresponding to the good and the bad outcomes; an outcome is good if it is consistent with σ 1 pν, , mq, and bad otherwise. It is a word arena of width W `2 with d `1 colors and k counters. The colouring function is given by three colouring functions: c 1 and Ω 1 induced by c and Ω, and c S which gives color 0 to all vertices, except the bad outcome coloured 1.

We equip G ν, with the condition BpN qXParityXSafe, where Safe uses the colouring function c S . The strategy σ 1 pν, , mq induces a winning strategy in this game; thanks to Proposition 3 (combined with Lemma 3 to handle the safety condition), there exists a strategy σpν, , mq ensuring Bpαpd, W `2, k, N qq X Parity X Safe using mempd, kq memory states.

The strategy σ simulates the strategies σpν, , mq in the corresponding parts of the game. Observe that this requires to keep track of both the value and the summary of the current rank, which is done by the memory structure.

We argue that σ ensures BpN 1 ¨αpd, W, k, N qq X Parity. A play consistent with this strategy is of the form w " w 1 w 2 ¨¨¨w n w 8 , where for all i P t1, . . . , n, 8u, we have valpw i q ď αpd, W `2, k, N q. Denote u " sumpw 1 qsumpw 2 q ¨¨¨sumpw n qsumpw 8 q, we have valpuq ď N 1 , since it corresponds to a play consistent with σ 1 . It follows from Fact 2, item 2., that valpwq ď N 1 ¨αpd, W `2, k, N q. Hence the strategy σ ensures BpN 1 ¨αpd, W `2, k, N qq X Parity and uses W ¨3k ¨K ¨mempd, kq memory states.

We conclude using Lemma 16. Thanks to Theorem 12, there exists a strategy σ 1 in G 1 ensuring Bpk k ¨N 2k q and using a memory structure M of size 2k!. It follows that there exists a strategy σ in G ensuring Bpk k ¨N 2k ¨αpd, W `2, k, N qq X Parityq using W ¨3k ¨2k! ¨mempd, kq memory states.

Conclusions

We recall some of the results of this chapter, presented under three angles, asking further questions:

• Characterisation of the memory requirements for a given condition. In Subsection 2.3, we characterised the memory requirement mempW q for all topologically closed conditions W . Roughly speaking, these conditions depend on prefixes of the plays, and specify what happens in the finite. A similar result is known for Muller conditions, by Dziembowski, Jurdziński and Walukiewicz [START_REF] Dziembowski | How Much Memory is Needed to Win Infinite Games?[END_REF]. The Muller conditions, at the opposite of topologically closed conditions, are the ω-regular conditions that specify only the infinite behaviours of plays. Hence the natural continuation and joint generalisation of these two results is to characterise mempW q for all ω-regular conditions W .

Kopczyński made a step in this direction, proving that the chromatic memory requirement is computable for all ω-regular conditions [Kop06; Kop09]. The chromatic memory requirement of a condition W is a priori different from mempW q, as it does not consider all strategies, but only chromatic strategies (which depend only the colors). Kopczyński conjectured that the two quantities coincide for ω-regular conditions.

• Finite-memory determinacy for non-uniform boundedness games over infinite arenas. We obtained two results: on the negative side, Section 5 shows that B-Büchi games are not finite-memory determined; on the positive side, Subsection 2.2 states that finitary parity games are bounded-memory determined. This leaves some space in between: for instance, are cost-parity games, as introduced in [FZ12; FZ14], bounded-memory determined? Can we characterise the boundedness conditions that are bounded-memory determined?

• The LoCo conjecture over tree arenas. We obtained two results: on the negative side, Section 5 shows that the LoCo conjecture does not hold, even over finite arenas; on the positive side, Section 6 shows that the LoCo conjecture holds for thin tree arenas. The negative result can be interpreted as the need for a better understanding of the structural properties of tree arenas. The positive result is a promising step towards this goal, as it strongly relies on the decomposition of thin trees.

The LoCo conjecture over tree arenas remains an appealing conjecture to tackle.

This second chapter deals with probabilistic automata over finite words, and focuses on a decision problem called the value 1 problem. This problem has been shown undecidable in 2010 by Hugo Gimbert and Youssouf Oualhadj [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]; the objective of this chapter is to answer the following question:

"To what extent is the value 1 problem decidable?"

To answer this question, we will construct an algorithm, called the Markov Monoid algorithm, prove that it is often correct, show that it is the most correct algorithm from the literature, and finally argue that it is in some sense optimal.

The basic definitions are given in Section 1. In particular, we define probabilistic languages and the value of a probabilistic automaton, state some of the most important undecidability results, and give a simple proof that the regularity problem is undecidable: given a probabilistic language, determine whether it is regular, obtained in collaboration with Michał Skrzypczak [START_REF] Fijalkow | Irregular Behaviours for Probabilistic Automata[END_REF].

Section 2 develops a profinite theory for probabilistic automata, called prostochastic theory. This gives a topological account of the value 1 problem, which naturally reformulates as an emptiness problem in this new framework. The material presented in this section is taken from [START_REF] Fijalkow | Characterisation of an Algebraic Algorithm for Probabilistic Automata[END_REF].

We introduce the Markov Monoid algorithm in Section 3, which is an algebraic algorithm meant to partially solve the value 1 problem. We use the prostochastic theory developed in the previous section to prove some properties of this algorithm, and in particular obtain a characterisation: the Markov Monoid algorithm determines, given a probabilistic automaton, whether it accepts a polynomial prostochastic word.

Section 4 shows that this algorithm indeed solves the value 1 problem for the subclass of leaktight automata, that we introduce, and further studies this subclass of probabilistic automata. In particular, we compare our subclass to the other subclasses introduced in the literature to partially solve the value 1 problem, and prove that the subclass of leaktight automata strictly contains all the other classes.

The results presented in these two sections originate from [START_REF] Fijalkow | Deciding the Value 1 Problem for Probabilistic Leaktight Automata[END_REF] (conference version), which is co-authored with Hugo Gimbert and Youssouf Oualhadj, and [START_REF] Fijalkow | Deciding the value 1 Problem for Probabilistic Leaktight Automata[END_REF] (journal version), with the same co-authors plus Edon Kelmendi.

The previous section shows that the Markov Monoid algorithm subsumes all previous algorithms. The natural question is of course: how far, and how long can this be pushed? To answer this question, we consider undecidability results in Section 5. We give two results.

The first one is the undecidability of the two-tier value 1 problem, which is a simpler variant of the value 1 problem. The reduction proving this result is similar to the one proving the undecidability of the value 1 problem by Gimbert and Oualhadj in [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF], but we give here a finer analysis, which exhibits the role of convergence speeds in the undecidability.

The second one is the undecidability of the numberless value 1 problems. This shows that the undecidability remains even when the numerical values of the transition probabilities are not specified, which was the topic of the paper [START_REF] Fijalkow | Two Recursively Inseparable Problems for Probabilistic Automata[END_REF] co-authored with Hugo Gimbert, Florian Horn and Youssouf Oualhadj.

The undecidability results we obtain for numberless problems are then applied to robustness problems. In a robustness problem, the input is a probabilistic automaton, subject to small perturbations of its probabilistic transitions. We show that unfortunately, the robustness variants of both the value 1 problem and the emptiness problem are undecidable. Section 6 gathers and relates the results obtained in the previous sections, to argue that the Markov Monoid algorithm is in some sense optimal. We then discuss perspectives and extensions.

Probabilistic Automata

This section is devoted to basic definitions: probabilistic automata in Subsection 1.1, probabilistic languages in Subsection 1.2, and the value of a probabilistic automaton in Subsection 1.3. We state some of the most important undecidability results in Subsection 1.4.

To make things a bit more concrete and interesting, we construct two examples:

• a universally non-regular probabilistic automaton,

• a probabilistic automaton which has value 1 or not, depending on the numerical values of the probabilistic transitions.

The first example is the key ingredient in the undecidability proof of the regularity problem, that we give in Subsection 1.5. The second example is the key ingredient in the undecidability proof of the (two-tier) value 1 problem, that we give in Subsection 5.1.

Probabilistic Automata

Let Q be a finite set of states. A distribution over Q is a function δ : Q Ñ r0, 1s such that ř qPQ δpqq " 1. We denote DpQq the set of distributions over Q, which we often consider as vectors indexed by Q. We denote by 1 3 ¨q `2 3 ¨q1 the distribution that picks q with probability 1 3 and q 1 with probability 2 3 , and by q the trivial distribution picking q with probability 1. For E Ď R, we denote M QˆQ pEq the set of (square) matrices indexed by Q over E. A matrix M P M QˆQ pRq is stochastic if each line is a distribution over Q; the restriction to stochastic matrices is denoted S QˆQ pEq. We denote I the identity matrix.

Definition 18 (Probabilistic automaton)

A probabilistic automaton A is given by a finite set of states Q, a transition function φ : A Ñ S QˆQ pQq, a distribution of initial states δ I P DpQq and a set of final states

F Ď Q.
This simple and natural definition was given by Rabin in [START_REF] Michael | Probabilistic Automata[END_REF]. Observe that it generalises the definition for classical deterministic automata, in which transitions functions are φ : A Ñ S QˆQ pt0, 1uq.

Sometimes, mostly for undecidability proofs, we restrict ourselves to probabilistic automata whose probabilistic transitions have values 0, 1 2 or 1, i.e. φ : A Ñ S QˆQ pt0, 1 2 , 1uq. Recall that a dyadic number is a number of the form a 2 b for a, b in N. For the same reasons, it is sometimes more convenient to use as initial distribution a unique state, which will then be denoted q 0 . We call the probabilistic automata satisfying both assumptions simple.

A transition function φ : A Ñ S QˆQ pQq naturally induces a morphism φ : A ˚Ñ S QˆQ pQq. We sometimes give φ as a function Q ˆA Ñ DpQq, which is equivalent. We denote P A ps w Ý Ñ tq the probability to go from state s to state t reading w on the automaton A, i.e. φpwqps, tq.

The acceptance probability of a word w P A ˚by A is δ I ¨φpwq ¨F , which we denote P A pwq. Note that here, we consider δ I as a row vector and F as a Boolean column vector over Q. It is equal to

ÿ sPQ ÿ tPF δ I psq ¨φpwqps, tq.
In words, it is the probability that a run starting from the initial distribution δ I ends in a final state (i.e. a state in F ). Throughout this chapter, we will only consider finite words. The situation for infinite words is addressed at the end of this chapter.

Probabilistic Languages

How does a probabilistic automaton define a language? The following threshold semantics was introduced by Rabin [Rab63]:

Definition 19 (Probabilistic language)

Let A be a probabilistic automaton and x P p0, 1q. This induces the probabilistic language L ąx pAq " tw P A ˚| P A pwq ą xu.

This simple definition initiated the study of the class of probabilistic languages. Since deterministic automata are a special case of probabilistic automata, this class contains the class of regular languages. To prove that this inclusion is strict, it would be enough to construct a probabilistic automaton C such that L ąx pCq is non-regular for some x. We prove a stronger result, constructing a probabilistic automaton such that for every number x in p0, 1q, the language L ąx pCq is non-regular. We will use this in Subsection 1.5.

In the original paper introducing probabilistic automata, Rabin [START_REF] Michael | Probabilistic Automata[END_REF] gave an example of a probabilistic automaton A such that L ąx pAq is non-regular, for all irrational numbers x. The automaton A computes the binary decomposition function denoted bin,

q 0 q 1 1, 1 2 0, 1 2 ♯ 1, 1 2 1 0 0, 1 2
Figure 17: A universally non-regular probabilistic automaton.

i.e. P A puq " binpuq, defined by binpa 1 ¨¨¨a n q " a 1 2 n `¨¨¨`a n 2 1 . We show that adding one letter and one transition to this probabilistic automaton makes it universally non-regular.

Example 2 (Universally non-regular probabilistic automaton)

The automaton C is represented in Figure 17. The alphabet is C " t0, 1, 7u. The only difference between the automaton A proposed by Rabin [START_REF] Michael | Probabilistic Automata[END_REF] and this one is the letter 7. As observed by Rabin, a simple induction shows that for u in t0, 1u ˚, we have P C puq " binpuq.

We show that for all numbers x in p0, 1q, the language L ąx pCq is non-regular. Let u, v in t0, 1u ˚, observe that P C pu ¨7 ¨vq " binpuq ¨binpvq.

Fix x in p0, 1q. For every u, v in t0, 1u ˚such that binpuq ă binpvq ă x, there exists w in t0, 1u ˚such that u ¨7 ¨w R L ąx pCq and v ¨7 ¨w P L ąx pCq; it suffices to choose w such that binpwq is in ´x binpvq , x binpuq ¯. It follows that the left quotients u ´1 ¨Ląx pCq and v ´1 ¨Ląx pCq are distinct, so L ąx pCq has an infinite number of pairwise distinct left quotients, hence it is not regular.

The Value of a Probabilistic Automaton

The notion of value for a probabilistic automaton comes from game theory.

Definition 20 (Value of a probabilistic automaton)

The value of a probabilistic automaton A, denoted valpAq, is the supremum over all words of their acceptance probability:

valpAq " sup wPA ˚PA pwq.
In this chapter, we will be interested in the following decision problem:

Problem 5 (Value 1 problem)
Given a probabilistic automaton A, determine whether valpAq " 1.

An equivalent formulation of the value 1 problem is as follows: given a probabilistic automaton A, is it true that for all ε ą 0, there exists a word w such that P A pwq ě 1 ´ε? In other words, is there a sequence of words pu n q nPN such that lim n P A pu n q " 1?

The value 1 problem can also be reformulated using the notion of isolated cut-point introduced by Michael O. Rabin in his seminal paper [START_REF] Michael | Probabilistic Automata[END_REF]: an automaton has value 1 if, and only if, the cut-point 1 is not isolated.

Yet another formulation of the value 1 problem is by considering probabilistic automata over infinite words, as studied in [BG05; BBG12; BBG08; BBG09]: the value 1 problem is Turing-equivalent to the emptiness problem for probabilistic Büchi automata with probable semantics.

A first (very simple) reduction has been given in [START_REF] Baier | Probabilistic ωautomata[END_REF]: from a probabilistic automaton A over finite words, one can construct a probabilistic Büchi automaton A 1 of linear size, such that valpAq " 1 if, and only if, A 1 is non-empty for the probable semantics. The converse reduction is more involved, and follows from [START_REF] Chadha | Probabilistic Automata with Isolated Cut-Points[END_REF], but here the constructed automaton is of exponential size.

0 L 1 L 2 R 1 R 2 a b, 1 2 a, 1 -x b a, x a, b b, 1 2 a, x b a, 1 -x a, b
Figure 18: A probabilistic automaton which has value 1 if, and only if, x ą 1 2 .

Example 3 (Convergence speeds and the value 1 problem)

We construct a probabilistic automaton, depicted on Figure 18, such that the answer to the value 1 problem depends quantitatively on the transition probabilities. This example was introduced in [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]. It has value 1 if, and only if, x ą 1 2 . The input alphabet is A " ta, bu, the initial state is the central state 0 and the unique final state is L 2 .

We describe its behaviour. After reading one b, the distribution is uniform over L 1 , R 1 . To reach L 2 , one needs to read a b from the state L 1 , but on the right-hand side this leads to the non-accepting absorbing state R 2 . In order to maximize the probability to reach L 2 , one tries to "tip the scales" to the left. If x ď 1 2 , there is no hope to achieve this: reading a letter a gives more chance to stay in R 1 than in L 1 thus all words are accepted with probability at most 1 2 , and valpAq " 1 2 . However, if x ą 1 2 then we show that A has value 1.

We have:

P A p0 ba n Ý Ý Ñ L 1 q " 1 2 ¨xn and P A p0 ba n Ý Ý Ñ R 1 q " 1 2 ¨p1 ´xq n .
We fix an integer N and analyse the action of reading pba n q N : there are N "rounds", each of them corresponding to reading ba n from 0. In a round, there are three outcomes: winning (that is, remaining in L 1 ) with probability p n " 1 2 ¨xn , losing (that is, remaining in R 2 ) with probability q n " 1 2 ¨p1 ´xq n , or going to the next round (that is, reaching 0) with probability 1 ´pp n `qn q. If a round is won or lost, then the next b leads to an accepting or rejecting sink; otherwise it goes on to the next round, for N rounds. Hence:

P A ppba n q N q " ř N ´1 k"1 p1 ´pp n `qn qq k´1 ¨pn " p n ¨1´p1´ppn`qnqq N ´1 1´p1´ppn`qnqq " 1 1`q n pn ¨`1 ´p1 ´pp n `qn qq N ´1W
e now set N " 2 n and assume x ą 1 2 . A simple calculation shows that the sequence pp1 ´pp n `qn qq 2 n ´1q nPN converges to 0 as n goes to infinity. Furthermore, 1´x

x ă 1, so qn pn " `1´x

x ˘n converges to 0 as n goes to infinity. It follows that the acceptance probability converges to 1 as n goes to infinity. Consequently:

lim n P A ppba n q 2 n q " 1.
This example witnesses two interesting phenomena:

• the value is discontinuous with respect to the transition probabilities, as for x " 1 2 the value is 1 2 , and for x ą 1 2 the value is 1; • the sequence of words ppba n q 2 n q nPN witnessing the value 1 involves two convergence "speeds": indeed, the words a n b are repeated an exponential number of times, namely 2 n . We will call such sequences two-tier sequences in Subsection 5.1. One can show that repeating only n times does not lead to words accepted with arbitrarily high probability.

Undecidability Results

The first and most natural problem for probabilistic automata is the emptiness problem for probabilistic languages.

Problem 6 (Emptiness problem)

Given a probabilistic automaton A, determine whether L ą 1 2 pAq is empty, i.e. whether there exists a word w such that P A pwq ą 1 2 .

Note that it is equivalent to asking whether valpAq ą 1 2 . Unfortunately:

Theorem 21 (Undecidability of the emptiness problem [START_REF] Paz | Introduction to Probabilistic Automata[END_REF])

The emptiness problem is undecidable for simple probabilistic automata.

A nice and simple undecidability proof was given by Gimbert and Oualhadj in [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]. This negative result says that the value cannot be computed precisely. One can still try to approximate it. Unfortunately, a second result shows that this is not possible either:

Theorem 22 (Inapproximability of the value [CL89])

There exists no algorithm with the following behaviour. Given a probabilistic automaton A:

• if valpAq ą 2
3 , then the algorithm answers "YES", • if valpAq ă 1 3 , then the algorithm answers "NO", • otherwise, the algorithm can do anything, including not terminating.

An interpretation of this result is that the value cannot be approximated, even up to a constant. In [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF], Gimbert and Oualhadj introduced the value 1 problem. It is a priori simpler, as it does not ask to compare the value to a given threshold. Unfortunately:

Theorem 23 (Undecidability of the value 1 problem [GO10])

The value 1 problem is undecidable for simple probabilistic automata. This result is the starting point of this chapter, which aims at understanding to what extent is the value 1 problem decidable.

Note that in Subsection 5.1, we revisit the undecidability proof of [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF], and obtain a stronger undecidability result, for the two-tier value 1 problem.

Undecidability of the Regularity Problem

Problem 7 (Regularity problem) Given a probabilistic automaton A, determine whether L ą 1 2 pAq is regular.

We give here a very simple proof, obtained in collaboration with Michał Skrzypczak [START_REF] Fijalkow | Irregular Behaviours for Probabilistic Automata[END_REF]. This result was known [START_REF] Bertoni | Mathematical Methods of the Theory of Stochastic Automata[END_REF].

Theorem 24 (Undecidability of the regularity problem)

The regularity problem is undecidable for simple probabilistic automata.

Roughly speaking, the idea is to use the universally non-regular automaton given in Example 2 to "amplify" an irregular behaviour.

Proof. We construct a reduction from the emptiness problem to the regularity problem. Let A be a probabilistic automaton over the alphabet A. We construct a probabilistic automaton B such that:

L ą 1
2 pAq is empty if, and only if, L ą 1 2 pBq is regular.

The automaton B is over the alphabet B " A Z C where C " t0, 1, 7u, and uses the automaton C from Section 1.2. It is obtained as the sequential composition of A and C: it starts in A and from every final state of A moves by 7 to the initial state of C. The initial state of B is the initial state of A, the only final state of B is the final state of C.

For u P A ˚and v P C ˚, we have P B pu ¨7 ¨vq " P A puq ¨PC pvq. A word which is not in A ˚¨7 ¨C˚h as no accepting run, so is accepted with probability 0.

• Assume that L ą 1 2 pAq is empty. Thanks to the above observation we have that L ą 1 2 pBq is empty, so in particular it is regular.

• Conversely, assume that L ą 1 2 pAq is non-empty. Let u be a word such that P A puq ą 1 2 . Observe that L ą 1 2 pBq X pu ¨7 ¨Cq ˚" u ¨7 ¨Ląx pCq, where x " 1 2¨P A puq is in p0, 1q. By construction of C, the language L ąx pCq is non-regular, implying that L ą 1 2 pBq is also non-regular.

"Every morphism φ : A ˚Ñ S QˆQ pRq extends uniquely to a continuous morphism p φ : PA ˚Ñ S QˆQ pRq."

Here, by " p φ extends φ" we mean φ " p φ ˝ι. We give two statements about PA ˚, the first will be weaker but enough for our purposes in this paper, and the second more precise, and justifying the name "free prostochastic monoid". The reason for giving two statements is that the first avoids a number of technical points that will not play any further role, so the reader interested in the applications to the Markov Monoid algorithm may skip this second statement.

Theorem 25 (Existence of the free prostochastic monoid -weaker statement)

For every finite alphabet A, there exists a compact monoid PA ˚and a continuous injective morphism ι : A ˚Ñ PA ˚such that every morphism φ : A ˚Ñ S QˆQ pRq extends uniquely to a continuous morphism p φ : PA ˚Ñ S QˆQ pRq.

We construct PA ˚and ι. Consider X " ś φ:A ˚ÑS QˆQ pRq S QˆQ pRq, the product of S QˆQ pRq, with one copy for each morphism φ : A ˚Ñ S QˆQ pRq. An element m of X is denoted pmpφqq φ:A ˚ÑS QˆQ pRq .

We define the product norm on X by ||m|| " supt||mpφq|| | φ : A ˚Ñ S QˆQ pRqu, inducing the product topology on X, implying thanks to Tychonoff's theorem that the monoid X is compact.

Consider the map ι : A Ñ X defined by ιpaq " pφpaqq φ:AÑP , it induces a continuous injective morphism ι : A ˚Ñ X. To simplify notations, we sometimes assume that A Ď X and denote a for ιpaq.

Denote PA ˚" A ˚, the closure of A ˚Ď X. Note that it is a compact monoid: the compactness follows from the fact that it is closed in X.

By definition, an element u of PA ˚, called a prostochastic word, is obtained as the limit in PA ˚of a sequence u of finite words. In this case we write lim u " u and say that u induces u.

Note that by definition of the product topology on X, a sequence of finite words u converges in X if, and only if, for every morphism φ : A ˚Ñ S QˆQ pRq, the sequence of stochastic matrices φpuq converges.

We say that two converging sequences of finite words u and v are equivalent if they induce the same prostochastic word, i.e. if lim u " lim v. Observe that two converging sequences of finite words u and v are equivalent if, and only if, for every morphism φ : A ˚Ñ S QˆQ pRq, we have lim φpuq " lim φpvq.

Proof. We prove that PA ˚satisfies the universal property. Consider a morphism φ : A ˚Ñ S QˆQ pRq, and define p φ : PA ˚Ñ S QˆQ pRq by p φpuq " lim φpuq, where u is some sequence of finite words inducing u. This is well defined and extends φ. Indeed, consider two equivalent sequences of finite words u and v inducing u. By definition, for all ψ : A ˚Ñ S QˆQ pRq, we have lim ψpuq " lim ψpvq, so in particular for φ this implies lim φpuq " lim φpvq, and p φ is well defined. Both continuity and uniqueness are clear. We prove that p φ is a morphism. Consider D " tpu, vq P PA ˚ˆP A ˚| p φpu ¨vq " p φpuq ¨p φpvqu.

To prove that p φ is a morphism, we prove that D " PA ˚ˆP A ˚. First of all, A ˚ˆA ˚Ď D. Since A ˚ˆA ˚is dense in PA ˚ˆP A ˚, it suffices to show that D is closed. This follows from the continuity of both product functions in PA ˚and in S QˆQ pRq as well as of p φ.

We give a second, stronger statement about PA ˚, which in particular justifies the name "free prostochastic monoid".

From now on, by "monoid" we mean "compact topological monoids". Note that compact also includes Hausdorff: distinct points have disjoint neighbourhoods. The term topological means that the product function is continuous:

" P ˆP Ñ P ps, tq Þ Ñ s ¨t
A monoid is profinite if any two elements can be distinguished by a morphism into a finite monoid, i.e. by a finite automaton. (Formally speaking, this is the definition of residually finite monoids, which coincide with profinite monoids for compact monoids, see [START_REF] Almeida | Profinite Semigroups and Applications[END_REF].)

To define prostochastic monoids, we use a stronger distinguishing feature, namely probabilistic automata. Probabilistic automata correspond to stochastic matrices over the rationals; here we use stochastic matrices over the reals, since S QˆQ pRq is compact, while S QˆQ pQq is not.

Definition 21 (Prostochastic monoid)

A monoid P is prostochastic if for every elements s ‰ t in P, there exists a continuous morphism ψ : P Ñ S QˆQ pRq such that ψpsq ‰ ψptq.

There are much more prostochastic monoids than profinite monoids. Indeed, S QˆQ pRq is prostochastic, but not profinite in general.

The following theorem extends Theorem 25. The statement is the same as in the profinite theory, replacing "profinite monoid" by "prostochastic monoid".

Theorem 26 (Existence of the free prostochastic monoid -stronger statement) For every finite alphabet A, 1. There exists a prostochastic monoid PA ˚and a continuous injective morphism ι :

A ˚Ñ PA ˚such that every morphism φ : A ˚Ñ P, where P is a prostochastic monoid, extends uniquely to a continuous morphism p φ : PA ˚Ñ P.

2. All prostochastic monoids satisfying this universal property are homeomorphic.

The unique prostochastic monoid satisfying the universal property stated in item 1. is called the free prostochastic monoid, and denoted PA ˚.

Proof. We prove that PA ˚satisfies the stronger universal property, along the same lines as for the weaker one. Consider a morphism φ : A ˚Ñ P, and define p φ : PA ˚Ñ P by p φpuq " lim φpuq, where u is some sequence of finite words inducing u.

To see that this is well defined, we use the fact that P is prostochastic. Consider two equivalent sequences of finite words u and v inducing u. Consider a continuous morphism ψ : P Ñ S QˆQ pRq, the composition ψ ˝φ is a continuous morphism from A ˚to S QˆQ pRq, so since u and v are equivalent it follows that limpψ ˝φqpuq " limpψ ˝φqpvq, i.e. lim ψpφpuqq " lim ψpφpvqq. Since ψ is continuous, this implies ψplim φpuqq " ψplim φpvqq. We proved that for all continuous morphisms ψ : P Ñ S QˆQ pRq, we have ψplim φpuqq " ψplim φpvqq; since P is prostochastic, it follows that lim φpuq " lim φpvq, and p φ is well defined.

Clearly p φ extends φ. Both continuity and uniqueness are clear. We prove that p φ is a morphism. Consider D " tpu, vq P PA ˚ˆP A ˚| p φpu ¨vq " p φpuq ¨p φpvqu.

To prove that p φ is a morphism, we prove that D " PA ˚ˆP A ˚. First of all, A ˚ˆA ˚Ď D. Since A ˚ˆA ˚is dense in PA ˚ˆP A ˚, it suffices to show that D is closed. This follows from the continuity of both product functions in PA ˚and in P as well as of p φ.

We prove that PA ˚is prostochastic. Let u ‰ v in PA ˚. Consider two sequences of finite words u and v inducing respectively u and v, there exists a morphism φ : A ˚Ñ S QˆQ pRq such that lim φpuq ‰ lim φpvq. Thanks to the universal property proved in the first point, this induces a continuous morphism p φ : PA ˚Ñ S QˆQ pRq such that p φpuq ‰ p φpvq, finishing the proof.

We now prove that there is a unique prostochastic monoid satisfying the universal property, up to homeomorphism. Let P 1 and P 2 two prostochastic monoids satisfying the universal property, together with two continuous injective morphisms ι 1 : A ˚Ñ P 1 and ι 2 : A ˚Ñ P 2 . Thanks to the universal property, ι 1 and ι 2 are extended to continuous morphisms p ι 1 : P 2 Ñ P 1 and p ι 2 : P 1 Ñ P 2 , and p ι 1 ˝ι2 " ι 1 and p ι 2 ˝ι1 " ι 2 . This implies that p ι 1 ˝p ι 2 ˝ι1 " ι 1 ; thanks to the universal property again, there exists a unique continuous morphism θ such that θ ˝ι1 " ι 1 , and since both p ι 1 ˝p ι 2 and the identity morphism on P 1 satisfy this equality, it follows that they are equal. Similarly, p ι 2 ˝p ι 1 is equal to the identity morphism on P 2 . It follows that p ι 1 and p ι 2 are mutually inverse homeomorphisms between P 1 and P 2 .

Remark 3. The free prostochastic monoid PA ˚contains the free profinite monoid x A ˚.

To see this, we start by recalling the definition of x A ˚, which is the set of converging sequences up to equivalence, where:

• a sequence of finite words u is converging if for every deterministic automaton A, the sequence is either ultimately accepted by A or ultimately rejected by A, i.e. there exists N P N such that either for all n ě N , the word u n is accepted by A, or for all n ě N , the word u n is rejected by A,

• two sequences of finite words u and v are equivalent if for every deterministic automaton A, either both sequences are ultimately accepted by A, or both sequences are ultimately rejected by A.

Clearly:

• if a sequence of finite words is converging with respect to PA ˚, then it is converging with respect to x A ˚, as deterministic automata form a subclass of probabilistic automata,

• if two sequences of finite words are equivalent with respect to PA ˚, then they are equivalent with respect to x A ˚.

Every profinite word induces at least one prostochastic word: by compactness of PA ˚, every sequence of finite words u contains a converging subsequence with respect to PA ˚.

This defines an injection from x A ˚into PA ˚. In particular, this implies that PA ˚is uncountable.

Reformulation of the Value 1 Problem

The aim of this subsection is to reformulate the value 1 problem, which talks about sequences of finite words, into an emptiness problem over prostochastic words.

Definition 22 (Prostochastic language of a probabilistic automaton)

Let A be a probabilistic automaton. The prostochastic language of A is:

LpAq " tu | p φpuqpq 0 , F q " 1u.
We say that A accepts a prostochastic word u if u P LpAq.

Theorem 27 (Reformulation of the value 1 problem)

Let A be a probabilistic automaton. The following are equivalent:

• valpAq " 1,
• LpAq is non-empty.

Proof. Assume valpAq " 1, then there exists a sequence of words u such that lim P A puq " 1. We see u as a sequence of prostochastic words. By compactness of PA ˚it contains a converging subsequence. The prostochastic word induced by this subsequence belongs to LpAq.

Conversely, let u in LpAq, i.e. such that p φpuqpq 0 , F q " 1. Consider a sequence of finite words u inducing u. By definition, we have lim φpuqpq 0 , F q " 1, i.e. lim P A puq " 1, implying that valpAq " 1.

Fast and Polynomial Prostochastic Words

We show in this subsection how to construct non-trivial prostochastic words. To this end, we need to better understand convergence speeds phenomena: different limit behaviours can occur, depending on how fast the underlying Markov chains converge.

We define a limit operator ω. Consider the function f : N Ñ N defined by f pnq " k!, where k is maximal such that k! ď n. The function f grows linearly: roughly, f pnq " n. The choice of n is arbitrary; one could replace n by any polynomial, or even by any subexponential function, see Remark 4.

The operator ω takes as input a sequence of finite words, and outputs a sequence of finite words. Formally, let u be a sequence of finite words, define:

u ω " pu f pnq n q nPN .
It is not true in general that if u converges, then u ω converges. We will show that a sufficient condition is that u is fast.

We say that a sequence pM n q nPN converges exponentially fast to M if there exists a constant C ą 1 such that for all n large enough, we have ||M n ´M || ď C ´n.

Definition 23 (Fast sequence)

A sequence of finite words u is fast if it converges (we denote u the prostochastic word it induces), and for every morphism φ : A ˚Ñ S QˆQ pRq, the sequence pφpu n qq nPN converges exponentially fast.

A prostochastic word is fast if it is induced by some fast sequence. We denote by PA f the set of fast prostochastic words. Note that a priori, not all prostochastic words are induced by some fast sequence.

We first prove that PA f is a submonoid of PA ˚.

Lemma 17 (The concatenation of two fast sequences is fast) Let u, v be two fast sequences. The sequence u ¨v " pu n ¨vn q nPN is fast.

Proof. Consider a morphism φ : A ˚Ñ S QˆQ pRq and n P N.

||φpu n ¨vn q ´p φpu ¨vq|| " ||φpu n q ¨φpv n q ´p φpuq ¨p φpvq|| " ||φpu n q ¨pφpv n q ´p φpvqq ´pp φpuq ´φpu n qq ¨p φpvq|| ď ||φpu n q|| ¨||φpv n q ´p φpvq|| `|| p φpuq ´φpu n q|| ¨|| p φpvq|| " ||φpv n q ´p φpvq|| `|| p φpuq ´φpu n q||.

Since u and v are fast, the previous inequality implies that u ¨v is fast.

Let u and v be two fast prostochastic words, thanks to Lemma 17, the prostochastic word u ¨v is fast.

The remainder of this subsection is devoted to proving that ω is an operator PA f Ñ PA f . We start by a few definitions. As a convention, M denotes a matrix in S QˆQ pRq, and m a Boolean matrix.

Definition 24 (Idempotent Boolean matrix, recurrent and transient state)

Consider a matrix M P S QˆQ pRq, its Boolean projection πpM q is the Boolean matrix such that πpM qps, tq " 1 if M ps, tq ą 0, and πpM qps, tq " 0 otherwise.

Let m be a Boolean matrix. It is idempotent if m ¨m " m. Assume m is idempotent. We say that:

• the state s P Q is m-recurrent if for all t P Q, if mps, tq " 1, then mpt, sq " 1,
• the m-recurrent states s, t P Q belong to the same recurrence class if mps, tq " 1,

• the state s P Q is m-transient if it is not m-recurrent.
The main technical tool is the following theorem, stating the exponentially fast convergence of the powers of a stochastic matrix.

Theorem 28 (Powers of a stochastic matrix) Let M P S QˆQ pRq. Denote P " M |Q| . Then the sequence pP n q nPN converges exponentially fast to a matrix M ω , satisfying:

πpM ω qps, tq " # 1 if πpP qps, tq " 1 and t is πpP q-recurrent, 0 otherwise.
The proof of Theorem 28 is given in Subsection 2.4.

Lemma 18 (Limit operator for fast sequences)

Let u, v be two equivalent fast sequences, inducing the fast prostochastic word u. Then the sequences u ω and v ω are fast and equivalent, inducing the fast prostochastic word denoted u ω .

Furthermore, for every φ : A Ñ S QˆQ pRq, we have p φpu ω q " p φpuq ω .

Proof. Let φ : A Ñ S QˆQ pRq.

Observe that the sequence p p φpuq f pnq q nPN is a subsequence of p p φpuq |Q|¨n q nPN , so Theorem 28 implies that it converges exponentially fast to p φpuq ω . It follows that there exists a constant C 1 ą 1 such that for all n large enough, we have || p φpuq f pnq ´p φpuq ω || ď C ´f pnq 1 . We proceed in two steps, using the following inequality, which holds for every n:

||φpu f pnq n q ´p φpuq ω || ď ||φpu n q f pnq ´p φpuq f pnq || `|| p φpuq f pnq ´p φpuq ω ||.
For the left part, we rely on the following equality, where x and y may not commute:

x N ´yN " N ´1 ÿ k"0
x N ´k´1 ¨px ´yq ¨yk .

Let N " f pnq, this gives:

||φpu n q N ´p φpuq N || " || N ´1 ÿ k"0 φpu n q N ´k´1 ¨pφpu n q ´p φpuqq ¨p φpuq k || ď N ´1 ÿ k"0 ||φpu n q N ´k´1 || ¨||φpu n q ´p φpuq|| ¨|| p φpuq k || ď N ´1 ÿ k"0 ||φpu n q|| N ´k´1 looooooomooooooon "1
¨||φpu n q ´p φpuq|| ¨|| p φpuq|| k looomooon "1

" N ¨||φpu n q ´p φpuq||.

Since u is fast, there exists a constant C 2 ą 1 such that ||φpu n q´p φpuq|| ď C ´n 2 . Altogether, we have

||φpu f pnq n q ´p φpuq ω || ď f pnq ¨C´n 2 `C´fpnq 1 .
To conclude, observe that for all n large enough, we have n logpnq ď f pnq ď n. It follows that the sequence u ω is fast, and that φpu ω q converges to p φpuq ω .

Furthermore, since u and v are equivalent, we have lim φpuq " lim φpvq, i.e. p φpuq " p φpvq, so p φpuq ω " p φpvq ω , i.e. lim φpu ω q " lim φpv ω q, This implies that u ω and v ω are equivalent.

We can now define polynomial prostochastic words. First, ω-expressions are described by the following grammar:

E ÝÑ a | E ¨E | E ω .
We define an interpretation ¨of ω-expressions into fast prostochastic words:

• a is prostochastic word induced by the constant sequence of the one letter word a,

• E 1 ¨E2 " E 1 ¨E2 , • E ω " E ω .
Definition 25 (Polynomial prostochastic word)

The set of polynomial prostochastic words is tE | E is an ω-expressionu.

Remark 4. Why the term polynomial? Consider an ω-expression E, say pa ω bq ω , and the prostochastic word pa ω bq ω , which is induced by the sequence of finite words ppa f pnq bq f pnq q nPN . Roughly speaking f pnq " n, so this sequence represents a polynomial behaviour. Furthermore, the proofs above yield the following robustness property: all converging sequences of finite words ppa gpnq bq hpnq q nPN , where g, h : N Ñ N are subexponential functions, are equivalent, so they induce the same polynomial prostochastic word pa ω bq ω . We say that a function g : N Ñ N is subexponential if for all constants C ą 1 we have lim n gpnq ¨C´n " 0; all polynomial functions are subexponential.

This justifies the terminology; we say that the polynomial prostochastic words represent all polynomial behaviours.

Powers of a Stochastic Matrix

In this subsection, we prove Theorem 28. Let M P S QˆQ pRq, consider P " M |Q| . It is easy to see that πpP q is idempotent. We decompose P as illustrated in Figure 19, by indexing states in the following way:

• first, πpP q-transient states,

• then, πpP q-recurrent states, grouped by recurrence class. In this decomposition, we have the following properties:

                                                    Q R 0 J J 1 J 2 . . .
• for all m-transient states s P Q, we have ř t m-transient Qps, tq ă 1, so ||Q|| ă 1,

• the matrices J i are irreducible: for all states s, t P Q corresponding to the same J i , we have J i ps, tq ą 0.

The power P n of P is represented in Figure 20. This decomposition allows to treat separately the three blocks:

1. the block Q n : thanks to the observation above ||Q|| ă 1, which combined with ||Q n || ď ||Q|| n implies that pQ n q nPN converges to 0 exponentially fast, 2. the block

ř n´1 k"0 Q k ¨R ¨Jn´1´k ,
3. the block J n : it is handled by Lemma 19.

We first focus on item 3., and show that the sequence pJ n q nPN converges exponentially fast. Each block J i is handled separately by the following lemma.

                                                    Q n n-1 k=0 Q k • R • J n-1-k 0 J n J n 1 J n 2 . . . J n r 0 0 Figure 20: Decomposition of P n .
Lemma 19 (Powers of an irreducible stochastic matrix)

Let J P S QˆQ pRq irreducible: for all states s, t P Q, we have Jps, tq ą 0. Then the sequence pJ n q nPN converges exponentially fast to a matrix J 8 . Furthermore, J 8 is irreducible.

This lemma is a classical result from Markov chain theory, sometimes called "the Convergence Theorem"; see for instance [START_REF] Levin | Markov Chains and Mixing Times[END_REF].

We now consider item 2., and show that the sequence p ř n´1 k"0 Q k ¨R ¨Jn´1´k q nPN converges exponentially fast. Observe that since ||Q|| ă 1, the matrix I ´Q is invertible; denote N " pI ´Qq ´1, it is equal to ř kě0 Q k . Denote J 8 " lim n J n , which exists thanks to Lemma 19.

We have:

|| n´1 ÿ k"0 Q k ¨R ¨Jn´1´k ´N ¨R ¨J8 || " || n´1 ÿ k"0 " Q k ¨R ¨`J n´1´k ´J8 ˘`Q k ¨R ¨J8 ‰ ´N ¨R ¨J8 || " || n´1 ÿ k"0 Q k ¨R ¨`J n´1´k ´J8 ˘`˜n ´1 ÿ k"0 Q k ´N ¸¨R ¨J8 || ď || n´1 ÿ k"0 Q k ¨R ¨`J n´1´k ´J8 ˘|| `|| ˜n´1 ÿ k"0 Q k ´N ¸¨R ¨J8 ||.

The Markov Monoid Algorithm

In this section, we introduce the Markov Monoid algorithm, which first appeared in [START_REF] Fijalkow | Deciding the Value 1 Problem for Probabilistic Leaktight Automata[END_REF], in collaboration with Hugo Gimbert and Youssouf Oualhadj.

The definition of the algorithm is given in Subsection 3.1, and an example in Subsection 3.2. Informally speaking, the Markov Monoid algorithm abstracts the behaviour of a probabilistic automaton by a finite stabilisation monoid called the Markov Monoid. We define two properties in Subsection 3.3.

• consistency, which states that all behaviours predicted by the Markov Monoid correspond to behaviours of the probabilistic automaton,

• completeness, which states that all behaviours of the probabilistic automaton correspond to behaviours of the Markov Monoid.

We show that the consistency property holds, without any further assumption, for all probabilistic automata, in Subsection 3.4. This gives a characterisation of the Markov Monoid algorithm, which is the main result of [START_REF] Fijalkow | Characterisation of an Algebraic Algorithm for Probabilistic Automata[END_REF].

The combination of both consistency and completeness would imply that the Markov Monoid algorithm solves the value 1 problem; since this problem is undecidable, the completeness fails in general. We discuss this further in Subsection 3.5.

The Algorithm

Consider A a probabilistic automaton, the Markov Monoid algorithm consists in computing, through a saturation process, the Markov Monoid of A.

It is a monoid of Boolean matrices: all numerical values are projected away to Boolean values. So instead of considering M P S QˆQ pRq, we are interested in πpM q. Hence to define the Markov Monoid, one can consider the underlying non-deterministic automaton πpAq instead of the probabilistic automaton A.

The Markov Monoid of πpAq contains the transition monoid of πpAq, which is the monoid generated by tπpφpaqq | a P Au and closed under (Boolean matrix) products. Informally speaking, the transition monoid accounts for the Boolean action of every finite word. Formally, for a word w P A ˚, the element xwy of the transition monoid of πpAq satisfies the following: xwyps, tq " 1 if, and only if, there exists a run from s to t reading w on πpAq.

The Markov Monoid generalises the transition monoid by introducing a new operator, the stabilisation. On the intuitive level first: let M P S QˆQ pRq, it can be interpreted as a Markov chain; its Boolean projection πpM q gives the structural properties of this Markov chain. The stabilisation πpM q 7 accounts for lim n M n , i.e. the behaviour of the Markov chain M in the limit. The formal definition of the stabilisation operator is as follows:

Definition 26 (Stabilisation)
Let m be a Boolean idempotent matrix. The stabilisation of m is denoted m 7 and defined by:

m 7 ps, tq " # 1 if mps, tq " 1 and t is m-recurrent, 0 otherwise.
The definition of the stabilisation matches the intuition that in the Markov chain lim n M n , the probability to be in non-recurrent states converges to 0.

Definition 27 (Markov Monoid)

The Markov Monoid of A is the smallest set of Boolean matrices containing tπpφpaqq | a P Au and closed under product and stabilisation of idempotents. if there is m, m 1 P M such that m ¨m1 R M then add m ¨m1 to M end if there is m P M such that m is idempotent and m 7 R M then add m 7 to M end until there is nothing to add ; if there is a value 1 witness in M then return YES; else return NO; end

In proofs and examples, we will often see Boolean matrices as graphs over the set Q; such a graph has an edge between two states s, t P Q if mps, tq " 1.

The Boolean matrices m handled by the Markov Monoid algorithm have a special property: for all states s P Q, there exists a state t P Q such that mps, tq " 1. From now on, we only consider Boolean matrices having this property.

On an intuitive level, a Boolean matrix in the Markov Monoid reflects the asymptotic effect of a sequence of finite words.

The Markov Monoid algorithm, detailed in Algorithm 1 computes the Markov Monoid, and looks for value 1 witnesses: Definition 28 (Value 1 witness) A Boolean matrix m is a value 1 witness if: for all states s, t P Q, if δ I psq ą 0 and mps, tq " 1, then t P F . The Markov Monoid algorithm answers "YES" if there exists a value 1 witness in the Markov Monoid, and "NO" otherwise.

For proof purposes, we give an equivalent presentation of the Markov Monoid through ω-expressions. Given a probabilistic automaton A, we define an interpretation x¨y of ω-expressions into Boolean matrices:

• xay is πpφpaqq, • xE 1 ¨E2 y is xE 1 y ¨xE 2 y,
• xE ω y is xEy 7 , only defined if xEy is idempotent.

Then the Markov Monoid of A is txEy | E an ω-expressionu.

An Example

We apply the Markov Monoid algorithm on an example. As explained, the Markov Monoid does not take into account the numerical values of the probabilistic transition, so as input we can consider the underlying non-deterministic automaton of a probabilistic automaton. This is what we do in Figure 21: the non-deterministic automaton is represented at the top.

We do not represent here all elements of its Markov Monoid; the tool ACME computed it [START_REF] Fijalkow | ACME: Automata with Counters, Monoids and Equivalence[END_REF], it contains 42 elements. We chose to represent here only 5 elements:

• The first two correspond to the letters a and b.

• The third one is xa ω y, its represents the behaviour of pa n q nPN . Indeed, when reading a from the state 0, two events happen with positive probability: looping around the state 0 and going to state 1. So, reading the word a n from 0 gives a probability to remain in the state 0 converging to 0 when n goes to infinity. Formally, this is reflected by the fact that the state 0 is not xay-recurrent.

• The fourth one is xa ω ¨by, it illustrates the concatenation between xa ω y and xby. Note that it is not a value 1 witness: from the only initial state 0, we have xa ω ¨byp0, 0q " 1, and 0 is not final.

• The fifth one is xpa ω ¨bq ω y, it illustrates that stabilisation can be nested. Observe that it is a value 1 witness. This matches the calculation showing that lim n P A ppa n ¨bq n q " 1, implying that A has value 1.

0 1 F ⊥ a a a, b b a b b a 0 1 F ⊥ b 0 1 F ⊥ a ω 0 1 F ⊥ a ω • b 0 1 F ⊥ (a ω • b) ω 0 1 F ⊥

Properties

Two key properties, consistency and completeness, state that the Markov monoid reflect exactly every possible asymptotic effect of a sequence of words.

Definition 29 (Reification)

A sequence pu n q nPN of words reifies a Boolean matrix m if for all states s, t P Q, the sequence pP A ps Note that if pu n q nPN reifies m, then any subsequence of pu n q nPN also does. We will use this simple observation several times.

Definition 30 (Consistency and completeness)

A set of Boolean matrices M is:

• consistent with A if for every Boolean matrix m P M, there exists a sequence of words pu n q nPN which reifies m.

• complete for A if for every sequence of words pu n q nPN , there exists m P M such that for all states s, t P Q: lim sup n P A ps un Ý Ñ tq " 0 ùñ mps, tq " 0.

Thanks to value 1 witnesses, the answer to the value 1 problem can be read in a consistent and complete set of Boolean matrices: Lemma 20 (A criterion for value 1)

If M is consistent with A and complete for A, then A has value 1 if, and only if, M contains a value 1 witness. Specifically:

• If M is consistent with A and contains a value 1 witness, then A has value 1,

• If M is complete for A and A has value 1, then A contains a value 1 witness.

Proof. We prove the first item. Assume that M is consistent with A and contains a value 1 witness m. Since M is consistent, there exists a sequence pu n q nPN reifying m. It follows that for s P Q and t R F , we have lim n δ I psq ¨PA ps un Ý Ñ tq " 0. Since for all n P N, we have ř sPQ ř tPQ δ I psq ¨PA ps un Ý Ñ tq " 1, this implies lim n P A pu n q " ř sPQ ř tPF lim n δ I psq PA ps un Ý Ñ tq " 1, so A has value 1. We now prove the second item. Assume that M is complete for A and that A has value 1. Then there exists a sequence of words pu n q nPN such that lim n P A pu n q " 1, i.e. Then m is a value 1 witness: let s P Q such that δ I psq ą 0 and t P Q such that mps, tq " 1, then lim sup n P A ps un Ý Ñ tq ą 0, hence t P F .

Consistency

The aim of this section is to prove that the Markov Monoid algorithm is consistent, i.e. that for every probabilistic automaton A, the Markov Monoid of A is consistent with A.

Fix a probabilistic automaton A. Unravelling the definitions, this amounts to associate to every ω-expression E, inducing the element xEy of the Markov Monoid, a sequence of words that reifies xEy. We show here that any sequence of finite words inducing the polynomial prostochastic word E reifies xEy.

It follows that for every ω-expression E, the element xEy of the Markov Monoid of A is a value 1 witness if, and only if, the polynomial prostochastic word E is accepted by A. This implies the following characterisation of the Markov Monoid algorithm:

Theorem 29 (Consistency and characterisation of the Markov Monoid algorithm) For every probabilistic automaton A, the Markov Monoid of A is consistent with A.

The Markov Monoid algorithm answers "YES" on input A if, and only if, there exists a polynomial prostochastic word accepted by A.

A direct corollary of the consistency is the absence of false negatives: Consequently, for every probabilistic automaton A:

• any sequence inducing the polynomial prostochastic word E reifies xEy,

• the element xEy of the Markov Monoid is a value 1 witness if, and only if, the polynomial prostochastic word E is accepted by A.

Proof. We prove the first part of Proposition 4 by induction on the ω-expression E, which essentially amounts to gather the results from Section 2.

The base case is a P A, clear.

The product case: let E " E 1 ¨E2 , and φ : A Ñ S QˆQ pRq.

We prove that πp p φpEqq " xEy. By definition E " E 1 ¨E2 , so p φpEq " p φpE 1 q ¨p φpE 2 q because p φ is a morphism, and πp p φpEqq " πp p φpE 1 qq ¨πp p φpE 2 qq. Also by definition, we have xEy " xE 1 y ¨xE 2 y, so the conclusion follows from the induction hypothesis.

The iteration case: let E " F ω , and φ : A Ñ S QˆQ pRq.

We prove that πp p φpEqq " xEy. By definition, E " F ω , so p φpEq " p φpF ω q, which is equal to p φpF q ω thanks to Lemma 18. Now, πp p φpF q ω q " πp p φpF qq 7 thanks to Theorem 28. By induction hypothesis, πp p φpF qq " xF y, which concludes.

Consider a sequence u inducing the polynomial prostochastic word E. Thanks to the first item, πp p φpEqq " xEy, so πplim φpuqq " xEy, which means that u reifies E. Assume that xEy is a value 1 witness, i.e. for all states s, t P Q, if δ I psq ą 0 and xEyps, tq " 1, then t P F . Then if δ I psq ą 0 and t R F , we have lim φpuqps, tq " 0. Since for all s P Q, we have ř tPQ lim φpuqps, tq " 1, it follows that if δ I psq ą 0, we have ř tPF lim φpuqps, tq " 1. Since ř sPQ δ I psq " 1, this implies ř sPQ δ I psq ř tPF lim φpuqps, tq " 1, i.e. lim P A puq " 1, so the polynomial prostochastic word E induced by u is accepted by A.

Conversely, assume that the polynomial prostochastic word E is accepted by A. Since it is induced by u, it follows that δ I ¨lim φpuq¨F " 1. Consider two states s, t P Q such that δ I psq ą 0 and xEyps, tq " 1. It follows that πplim φpuqqps, tq " 1, so lim φpuqps, tq ą 0. The combination of δ I psq ą 0, lim φpuqps, tq ą 0 and δ I ¨lim φpuq ¨F " 1 implies that t P F , hence xEy is a value 1 witness.

No Completeness

In this subsection, we explain why the Markov Monoid algorithm cannot be complete:

• we asserted in Lemma 20 that if the Markov Monoid algorithm is consistent and complete, then it is correct, i.e. solves the value 1 problem,

• we asserted in Theorem 29 that the Markov Monoid algorithm is consistent,

• the value 1 problem has been shown to be undecidable in [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF] (we will revisit the undecidability proof in Subsection 5.1).

The logical implication of these three statements is that the Markov Monoid algorithm is not complete.

A concrete example of a probabilistic automaton A for which the Markov Monoid is not complete is given by Example 3 from Subsection 1.3. We make three observations about the Markov Monoid of A.

• We showed that A has value 1 if, and only if, x ą 1 2 . Since the Markov Monoid does not depend on the numerical values of the probabilistic transitions, and in particular on x, it cannot detect this, thus it is not complete.

• The Markov Monoid of A does not contain any value 1 witness. Indeed, the underlying non-deterministic automaton consists of two symmetric parts, left and right.

Nothing distinguishes those two parts, except for the numerical values of the probabilistic transitions. It follows that all elements m of the Markov Monoid of A are also symmetric, and in particular, mp0, L 2 q " mp0, R 2 q, implying that m is not a value 1 witness.

• The sequence of words witnessing that A has value 1 for x ą 1 2 is ppba n q 2 n q nPN . This sequence is not fast, and induces no polynomial prostochastic words. We will call in Subsection 5.1 such a sequence a two-tier sequence, and show that such sequences are enough to imply the undecidability of the value 1 problem.

Leaktight Automata

In this section, we define the class of leaktight automata, which was introduced in [START_REF] Fijalkow | Deciding the Value 1 Problem for Probabilistic Leaktight Automata[END_REF] with Hugo Gimbert and Youssouf Oualhadj.

The main result of [START_REF] Fijalkow | Deciding the Value 1 Problem for Probabilistic Leaktight Automata[END_REF] is that the value 1 problem is decidable and PSPACEcomplete for leaktight automata. More specifically, the class of leaktight automata is defined by a structural property on the Markov Monoid, which implies that the Markov Monoid algorithm is complete for this class.

We define the extended Markov Monoid algorithm in Subsection 4.1, and the class of leaktight automata in Subsection 4.2, where we prove that the extended Markov Monoid algorithm solves the value 1 problem for leaktight automata. In Subsection 4.3, we show that this problem is actually PSPACE-complete.

In the journal version [START_REF] Fijalkow | Deciding the value 1 Problem for Probabilistic Leaktight Automata[END_REF], which features Edon Kelmendi as a third co-author, we investigate the properties of the class of leaktight automata. In particular, we show that the class of leaktight automata strictly contains hierarchical, 7-acyclic and simple automata, implying that it is the largest class of probabilistic automata for which the value 1 problem is known to be decidable. We report on these results in Subsection 4.4.

The Extended Markov Monoid Algorithm

The undecidability of the value 1 problem comes from the necessity to track down vanishing probabilities. One of the phenomena that makes tracking vanishing probabilities difficult are leaks. A leak occurs in an automaton when a sequence of words turns a set of states C Ď Q into a recurrence class C on the long run, but on the short run, some of the probability of the recurrence class is "leaking" to a different recurrence class.

Such leaks occur in the automaton depicted in the left hand side of Figure 22 with the sequence of words pa n bq nPN . As n grows large, the probability to reach L 2 from L 1 while reading the word a n b vanishes, thus the sets tL 1 u and tL 2 u are two different recurrence classes on the long run (i.e. asymptotically), however on the short run remains a small yet positive probability to reach L 2 from L 1 .

The right hand side of Figure 22 shows the asymptotic behaviour of pa n bq nPN .

The automaton in Example 3 from Subsection 1.3 contains two symmetric parts identical to Figure 22, it features one leak on the left hand side and another in the right hand side. As a consequence, the real asymptotic behaviour is complex and depends on the compared speeds of these leaks.

To formalize the notion of leak, we will extend the Markov Monoid, and consider matrices over a three valued semiring, denoted B ε , instead of the Boolean semiring. The three values are the two Boolean values 0 and 1, plus a third value ε. The operations _ and ^are defined by:

_ 0 ε 1 0 0 ε 1 ε ε ε 1 1 1 1 1 ^0 ε 1 0 0 0 0 ε 0 ε ε 1 0 ε 1
The matrices over B ε are called extended Boolean matrices, and usually denoted m. As for Boolean matrices, an extended Boolean matrix m can be seen as graphs over the set Q; such a graph has two different kinds of edges, an edge ps, tq is "normal" if mps, tq " 1, and a ε-edge if mps, tq " ε.

On an intuitive level, the value ε is used for vanishing probabilities. The semiring structure of B ε induces a monoid structure for M QˆQ pB ε q. The notion of m-recurrent states is defined as for the Boolean case: a state q P Q is m-recurrent if for all states t P Q, if mps, tq " 1, then mpt, sq " 1. We define the stabilisation operator as follows:

Definition 31 (Stabilisation)
Let m be an extended Boolean idempotent matrix. The stabilisation of m is denoted m 7 and defined by:

m 7 ps, tq " $ ' ' ' & ' ' ' % 1 if mps, tq " 1 and t is m-recurrent, ε if mps, tq " 1 and t is m-transient, ε if mps, tq " ε, 0 otherwise. Definition 32 (Extended Markov Monoid)
The extended Markov Monoid of A is the smallest set of extended Boolean matrices containing tπpφpaqq | a P Au and closed under product and stabilisation of idempotents.

Note that initially, the extended Boolean matrices only contain values 0 or 1; the value ε is introduced by the stabilisation operator.

As for the Markov Monoid, for every m in the extended Markov Monoid of a probabilistic automaton, for all states s P Q, there exists a state t P Q such that mps, tq " 1.

From now on, we only consider extended Boolean matrices having this property. This will be crucial in the proof of Lemma 22.

Definition 33 (Value 1 witness) An extended Boolean matrix m is a value 1 witness if: for all states s, t P Q, if δ I psq ą 0 and mps, tq " 1, then t P F . Algorithm 2 computes the extended Markov monoid, and looks for value 1 witnesses. If there is a value 1 witness, then the algorithm answers "YES": indeed, in such case the automaton has value 1. Otherwise, the algorithm looks for leaks1 :

• if there are no leaks, then algorithm answers "NO"; indeed, the automaton is leaktight, and it does not have value 1 thanks to Theorem 30,

• if there is a leak, the algorithm answers "FAIL"; indeed, the automaton is not leaktight, and nothing can be said.

Recall that the Markov Monoid of A is txEy | E an ω-expressionu. Similarly, the extended Markov Monoid of A is txEy ε | E an ω-expressionu, where x¨y ε is defined using multiplication and stabilisation in B ε .

Lemma 21 (Relation between the extended and the classical Markov Monoid)

For every ω-expression E, the Boolean matrix xEy is obtained from the extended Boolean matrix xEy ε by replacing ε by 0 in all entries.

In particular, xEy is a value 1 witness if, and only if, xEy ε is a value 1 witness.

This lemma is easily proved by induction on ω-expressions. It follows that both algorithms give the same answer. Consequently, if the extended Markov Monoid algorithm answers "YES" on input A, then A has value 1.

We extend the definition of completeness for the extended Markov Monoid algorithm.

2. mps, tq " ε.

Definition 36 (Leaktight automata)

A probabilistic automaton A is leaktight if its extended Markov Monoid does not contain any leak.

We establish our main result:

Theorem 30 (Completeness for leaktight automata) For every probabilistic leaktight automaton A, the extended Markov Monoid of A is complete for A.

Consequently, the extended Markov Monoid algorithm is correct for leaktight automata, implying that the value 1 problem is decidable for leaktight automata.

The remainder of this section is devoted to the proof of Theorem 30. The technical core of the proof relies on an algebraic argument based on the existence of 7-factorisation trees of bounded height.

Factorisation trees for monoids have been introduced by Simon [START_REF] Simon | Factorization Forests of Finite Height[END_REF]. Roughly speaking, Simon's factorisation theorem states that given a morphism φ : A ˚Ñ M from the set of finite words over A into a finite monoid M , the following holds: for all words u, the computation of φpuq can be factorised in a tree whose depth is bounded independently of the length of the word.

Simon later developed the notion of decomposition trees to solve the limitedness problem for distance automata [START_REF] Simon | On Semigroups of Matrices over the Tropical Semiring[END_REF]. To this end, he defined a stabilisation operator for monoids of matrices over the tropical semiring pN Y t8u, min, `q. Then Kirsten extended this technique to desert automata and nested distance desert automata [START_REF] Daniel | Distance Desert Automata and the Star-Height Problem[END_REF]. After him, Colcombet generalised this approach by defining stabilisation monoids [START_REF] Colcombet | The Theory of Stabilisation Monoids and Regular Cost Functions[END_REF][START_REF] Colcombet | Regular Cost Functions, Part I: Logic and Algebra over Words[END_REF], which are monoids equipped with a stabilisation operator, and proved the existence of 7-factorisation trees of bounded depth. The formal definition is as follows:

Definition 37 (Stabilisation monoid) A stabilisation monoid pM, ¨, 7q is a finite monoid pM, ¨q equipped with a stabilisation operator 7 : EpM q Ñ EpM q, where EpM q is the set of idempotents of M , such that: pm ¨m1 q 7 ¨m " m ¨pm 1 ¨mq 7 for m ¨m1 P EpM q and m 1 ¨m P EpM q, pm 7 q 7 " m 7 for m P EpM q, m 7 ¨m " m 7 for m P EpM q.

Lemma 22 (The Markov Monoid is a stabilisation monoid)

The extended Markov Monoid of a probabilistic automaton is a stabilisation monoid.

Proof. First of all, the extended Markov monoid is a monoid for the multiplication: the identity matrix I is the neutral element, and the multiplication is associative. Now, let us prove the three properties required for the stabilisation operator 7.

First property. Let m, m 1 such that m ¨m1 and m 1 ¨m are idempotent. Let s, t P Q, we have the following equivalence: `pm ¨m1 q 7 ¨m˘p s, tq " 1 if, and only if, there exist two states r, q P Q such that mps, rq " 1, m 1 pr, qq " 1, q is pm ¨m1 q-recurrent and mpq, tq " 1. Similarly, `m ¨pm 1 ¨mq 7 ˘ps, tq " 1 if, and only if, there exist two states r, q P Q such that mps, rq " 1, m 1 pr, qq " 1, mpq, tq " 1 and t is pm 1 ¨mq-recurrent.

We show that those two statements are equivalent. Assume that the first holds, and prove that t is pm 1 ¨mq-recurrent. Consider a state p P Q such that pm 1 ¨mqpt, pq " 1. There exists a state P Q such that m 1 pp, q " 1. Observe that mpq, tq " 1, pm 1 ¨mqpt, pq " 1 and m 1 pp, q " 1, so pm¨m 1 q 2 pq, q " 1. Since m¨m 1 is idempotent, this implies pm¨m 1 qpq, q " 1. Recall that q is pm ¨m1 q-recurrent, so pm ¨m1 qp , qq " 1. Altogether, m 1 pp, q " 1, pm ¨m1 qp , qq " 1 and mpq, tq " 1 imply that pm 1 ¨mq 2 pp, tq " 1. Since m 1 ¨m is idempotent, this implies pm 1 ¨mqpp, tq " 1, so t is pm 1 ¨mq-recurrent, and we proved that the first statement implies the second. The converse, showing that the second statement implies the first, is very similar and omitted.

Second property. The equality pm 7 q 7 " m 7 follows from the observation that the notions of m-recurrence and m 7 -recurrence coincide.

Third property. The equality m 7 ¨m " m 7 follows from the observation that given two states r, t P Q, if r is m-recurrent and mpr, tq " 1, then t is m-recurrent (under the assumption that m is idempotent).

Definition 38 (7-factorisation tree) Consider a stabilisation monoid pM, ¨, 7q and a monoid morphism ψ : A ˚Ñ M . A 7-factorisation tree of a word u P A ˚is a finite unranked ordered tree, whose nodes have labels in A ˚ˆM and such that: i) the root is labelled by pu, mq, for some m P M , ii) every internal node with two children (called multiplication nodes) labelled by pu 1 , m 1 q and pu 2 , m 2 q is labelled by pu 1 ¨u2 , m 1 ¨m2 q, iii) every internal node with three or more children (called stabilisation nodes) is labelled by pu 1 . . . u n , m 7 q for some m P EpM q, and its children are labelled by pu 1 , mq, . . . , pu n , mq.

iv) every leaf is labelled by pa, ψpaqq where a is a letter, or pε, ψpεqq.

Note that in a factorisation tree, the second label is not always the image of the first component under ψ; indeed, it is an element of the stabilisation monoid pM, ¨, 7q whereas the image of a finite word under ψ is an element of the monoid pM, ¨q. However, the Since the set of extended Boolean matrices is finite, there exists N P N such that tn P N | m N " m n u is infinite. To complete the proof, we prove that m N satisfies, for all states s, t P Q: lim sup P A ps un Ý Ñ tq " 0 ùñ m N ps, tq " 0. • the value 1 problem for leaktight automaton is PSPACE-hard,

Assume

• the extended Markov Monoid can be computed in polynomial space.

As a corollary, we obtain that the value 1 problem for leaktight automata is PSPACEcomplete.

PSPACE-hardness

We start with the PSPACE-hardness of the value 1 problem for leaktight automata. To this end, we give a reduction from the emptiness problem of n deterministic automata. To prove that the reduction indeed constructs leaktight automata, we need to show that deterministic automata are leaktight, and the closure under parallel composition.

Lemma 24 (Deterministic automata are leaktight) Deterministic automata are leaktight.

Proof. For every extended Boolean matrix m P tπpφpaqq | a P AuYtIu, for all states s P Q, there exists a unique state t P Q such that mps, tq " 1. In particular, each recurrence class is formed of only one state with a self-loop. This property is preserved by multiplication, and implies that the stabilisation operator is trivial, i.e. m 7 " m. Consequently, all extended Boolean matrices m in the extended Markov Monoid have entries 0 or 1, which implies that there are no leaks.

Definition 39 (Parallel composition)

Let A and B two probabilistic automata over the disjoint set of states Q A and Q B , with the same alphabet A.

The parallel composition A||B of A and B is the probabilistic automaton over the set of states

Q A Y Q B , whose initial distribution is δ I " 1 2 ¨δA I `1 2 ¨δB I , set of final states is F " F A Y F B , and transition function is φpq, aq " # φ A pq, aq if q P Q A , φ B pq, aq if q P Q B .
By definition, for u P A ˚, we have P A||B puq " to pmrAs, mrBsq, where mrAs is the restriction to Q A and similarly for B. An easy induction shows that this map is an embedding into M A ε ˆMB ε . Consequently, if none of the extended Markov Monoids of A and B contain a leak, then neither does the extended Markov Monoid of their parallel composition. Now that we proved that deterministic automata are leaktight, and the closure under parallel composition, the PSPACE-hardness of the value 1 problem for leaktight automata is easy.

Proposition 5 (PSPACE-hardness of the value 1 problem for leaktight automata)

The value 1 problem for leaktight automaton is PSPACE-hard.

Proof. We give a reduction from the following problem: given n deterministic automata over finite words, decide whether the intersection of the languages they accept is empty. This problem is PSPACE-hard.

The reduction is as follows: given n deterministic automata, we construct the parallel composition of the n automata, where each copy is reached with probability 1 n . This automaton has value 1 if, and only if, the intersection of the languages is not empty, and is leaktight by Lemma 24 and Lemma 25.

Bounding the 7-height in the extended Markov Monoid

We now consider the running complexity of the extended Markov Monoid algorithm. A naïve argument shows that it terminates in less than 3 |Q| 2 stabilisations, since each stabilisation adds a new extended Boolean matrix in the monoid and there are at most 3 |Q| 2 different Boolean matrices. This gives an EXPTIME upper bound.

A better complexity can be achieved by looking for a value 1 witness or a leak in a non-deterministic way. The algorithm guesses the witness by its decomposition into multiplications and stabilisations. The key observation, made by Daniel Kirsten [START_REF] Daniel | Distance Desert Automata and the Star-Height Problem[END_REF] in the context of distance desert automata, is that the 7-height, that is the number of nested applications of the stabilisation operator, can be restricted to at most |Q|.

We fix a probabilistic automaton A, and define the 7-hierarchy inside the extended Markov Monoid M ε of A as follows:

S 0 " tπpφpaqq | a P Au ˚, S p`1 " pS p Y tm 7 | m P EpS p quq ˚,
where T ˚is the set of extended Boolean matrices obtained as multiplications of extended Boolean matrices in T .

Clearly:

S 0 Ď S 1 Ď S 2 Ď ¨¨¨Ď M ε
Definition 40 (7-height of a Boolean matrix)

The 7-height of an extended Boolean matrix m P M ε is the minimal p P N such that m P S p .

Theorem 32 (Linear bound on the 7-height) Every extended Boolean matrix m P M ε has 7-height at most |Q|, i.e. S |Q|´1 " M ε . We say that the 7-hierarchy collapses at level |Q| ´1.

In the following, we adapt Daniel Kirsten's proof from [START_REF] Daniel | Distance Desert Automata and the Star-Height Problem[END_REF] to the setting of probabilistic automata. Roughly speaking, the proof consists in associating a quantity to each idempotent element of the extended Markov Monoid, and to show the following:

• the quantity is bounded above by |Q| and below by 1,

• the quantity strictly decreases when stabilising an unstable element (i.e. such that m 7 ‰ m),

• the quantity does not increase when concatenating.

Let m be an extended Boolean idempotent matrix, we define " m the relation over Q by s " m t if mps, tq " 1 and mpt, sq " 1. The relation " m is symmetric, and since m is idempotent, it is transitive. If for some state s P Q there exists a state t P Q such that s " m t, then s " m s since m is idempotent. Consequently, the restriction of " m to the set Z m " ts P Q | s " m su is reflexive, i.e. " m is an equivalence relation on Z m . From now on by equivalence class of " m we mean an equivalence class of " m on Z m . We denote by rss m the equivalence class of s, and by Clpmq the set of equivalence classes of " m . The quantity associated with m is |Clpmq|, the number of equivalence classes of " m , that is the number of non-trivial connected components in the underlying graph of m. Note that 1 ď |Clpmq| ď |Q|.

The following lemma gives two useful observations. We order the three values 0, ε and 1 by 0 ă ε ă 1. Observe that for m, m 1 two extended Boolean matrices and two states s, t P Q, we have: pm ¨m1 qps, tq " max rPQ minpmps, rq, m 1 pr, tqq.

Lemma 26 (Facts about multiplication)

• Let m, m 1 be two extended Boolean matrices and three states s, t, r P Q. Then pm ¨m1 qps, tq ě mps, rq ¨m1 pr, tq.

• Let m be an idempotent extended Boolean matrix and two states s, t P Q. Then there exists a state r P Q such that mps, tq " mps, rq ¨mpr, rq ¨mpr, tq.

Proof. The first item follows from the equality above. Consider now the second item. For all states r P Q, since m is idempotent we have: mps, tq " m 3 ps, tq " ÿ p,qPQ mps, pq ¨mpp, qq ¨mpq, tq ě mps, rq ¨mpr, rq ¨mpr, tq.

Since m is idempotent, we have m " m |Q|`2 , so there exist r 0 " s, . . . , r |Q|`2 " t such that mps, tq " mpr 0 , r 1 q ¨mpr 1 , r 2 q ¨¨¨mpr |Q|`1 , r |Q|`2 q. By a counting argument, there exist i, j such that 1 ď i ă j ď |Q| `1 and r i " r j , denote it by r. We have: mps, rq " m i ps, rq ě mpr 0 , r 1 q ¨¨¨mpr i´1 , r i q, mpr, rq " m j´i pr, rq ě mpr i , r i`1 q ¨¨¨mpr j´1 , r j q, mpr, tq " m |Q|`2´j pr, tq ě mpr j , r j`1 q ¨¨¨mpr |Q|`1 , r |Q|`2 q.

Hence, mps, rq ¨mpr, rq ¨mpr, tq ě mpr 0 , r 1 q ¨mpr 1 , r 2 q ¨¨¨mpr |Q|`1 , r |Q|`2 q " mps, tq, and the second item follows.

The following lemma shows that the quantity |Clpmq| strictly decreases when stabilising an unstable extended Boolean matrix.

Lemma 27 (|Clp¨q| decreases with stabilisation)

Let m be an extended Boolean idempotent matrix.

• Clpm 7 q Ď Clpmq,

• if m 7 ‰ m, then Clpm 7 q ‰ Clpmq.

Proof. We prove the first item. Let s P Z m 7 , we show that rss m 7 " rss m . For all states t P Q such that s " m 7 t, we have s " m t, so rss m 7 Ď rss m . Conversely, let t P rss m ; we have mps, tq " 1 and mpt, sq " 1. Since s " m 7 s, we have m 7 ps, sq " 1, so in particular s is m-recurrent. It follows from mps, tq " 1 that t is also m-recurrent, so m 7 ps, tq " 1, and similarly m 7 pt, sq " 1. Thus s " m 7 t, i.e. t P rss m 7 , which implies the equality Lemma 29 (|Clp¨q| decreases with the 7-height) Let m be an extended Boolean idempotent matrix and p ě 0. If m P S p zS p´1 , then |Clpmq| ď |Q| ´p.

Proof. We proceed by induction on p. For p " 0, the assertion is obvious. Let p ě 0, we show the claim for p `1. Let m be an extended Boolean idempotent matrix such that m P S p`1 zS p . By definition, m " m The bound is almost tight, as shown in Figure 23. The only value 1 witness of this automaton is p¨¨¨ppa 7 0 a 1 q 7 a 2 q 7 a 3 q 7 ¨¨¨a n´1 q 7 , whose 7-height is n " |Q| ´2. This automaton is leaktight, so the extended Markov Monoid algorithm will find the value 1 witness and correctly answers that it has value 1.

0 1 2 n -1 n ⊥ a 0 (a i ) i≤n-1 (a i ) i≤0 (a i ) i≤1 (a i ) i≤n-2 (a i ) i≥0 a 0 a 1 a 1 a 2 a 2 a n-1 a n-1 (a i ) i≥1 (a i ) i≥2 (a i ) i≥3
We derive from Theorem 32 the following complexity result, improving over the naïve approach to implement the extended Markov Monoid algorithm.

Theorem 33 (The extended Markov Monoid algorithm in polynomial space) There exists an algorithm which checks in polynomial space whether an automaton is leaktight and whether in such case it has value 1.

Following Theorem 30, checking whether a leaktight automaton has value 1 boils down to finding a value 1 witness in the extended Markov Monoid. Similarly, checking whether an automaton is not leaktight boils down to finding a leak in the extended Markov Monoid. Note that in both cases, checking whether a given extended Boolean matrix is a witness is easily done in polynomial time.

Since we aim at proving that those two tasks can be computed in PSPACE, which is closed under complementation, it suffices to show how to find a witness in the extended Markov Monoid.

We describe an algorithm to guess a witness in the extended Markov Monoid. The key property given by Theorem 32 is that we can restrict ourselves to at most |Q| nested stabilisations.

As the corresponding property was proved by Daniel Kirsten [START_REF] Daniel | Distance Desert Automata and the Star-Height Problem[END_REF] in the context of distance automata, also to obtain a PSPACE algorithm, the following algorithm is also an adaptation of [START_REF] Daniel | Distance Desert Automata and the Star-Height Problem[END_REF]. Rather than a formal proof, we here give an intuitive description of the algorithm.

A witness can be described as a tree whose nodes are labelled by extended Boolean matrices, of depth at most 2 ¨|Q| `1, as follows:

• a leaf is labelled either by πpφpaqq for a P A or by I,

• an internal node can be a multiplication node, then it is labelled by m " m 1 ¨¨¨m k for k ď 3 |Q| 2 and has k children, labelled by m 1 , . . . , m k ,

• an internal node can be a stabilisation node, then it is labelled by m 7 and has one child labelled m.

We describe an algorithm that guesses such a tree. It starts from the root, and travels over nodes in a depth-first way: from top to bottom (and up again) and from left to right. In a node, the algorithm stores the branch that leads to this node, and for each node in the branch the extended Boolean matrix obtained by multiplying all the left siblings of this node. From a node, the algorithm guesses an extended Boolean matrix, and whether it will be a leaf, a multiplication node or an stabilisation node. In the first case, it goes up and checks the consistency of this guess. In the two other cases, it updates the value of this node by multiplying the new guess with the previous value and goes down. Although the tree is of exponential size, in each step the algorithm only stores 2¨|Q|`1 extended Boolean matrices at most, so it runs in polynomial space.

Comparisons with the Other Classes

In this section, we report on the results obtained in the journal version [START_REF] Fijalkow | Deciding the value 1 Problem for Probabilistic Leaktight Automata[END_REF], in collaboration with Hugo Gimbert, Edon Kelmendi and Youssouf Oualhadj. In addition to the results of the conference version [START_REF] Fijalkow | Deciding the Value 1 Problem for Probabilistic Leaktight Automata[END_REF], the aim of this journal version is to compare the class of leaktight automata to other subclasses. Two subclasses of probabilistic automata were constructed in order to decide the value 1 problem on such instances. The first class was the 7-acyclic automata by Hugo Gimbert and Youssouf Oualhadj [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]. Later but concurrently, two different works have been published in the very same conference. The first one introduces simple automata and structurally simple automata, by Krishnendu Chatterjee and Mathieu Tracol [START_REF] Chatterjee | Decidable Problems for Probabilistic Automata on Infinite Words[END_REF], and the second is ours (in collaboration with Hugo Gimbert and Youssouf Oualhadj), introducing leaktight automata [START_REF] Fijalkow | Deciding the Value 1 Problem for Probabilistic Leaktight Automata[END_REF].

Although geared towards the same goal (deciding the value 1 problem), the two classes came from different perspectives. The paper of Krishnendu Chatterjee and Mathieu Tracol relies on a theorem from Probability Theory, called the jet decompositions of (infinite) Markov Chains. Ours relies on Simon's theorem and comes from Algebra.

Theorem 34 (Inclusion of the different subclasses)

The class of 7-acyclic, simple and structurally simple automata are all strictly included in the class of leaktight automata.

We do not give here more details, and refer to [START_REF] Fijalkow | Deciding the value 1 Problem for Probabilistic Leaktight Automata[END_REF] for both definitions and proofs. The content of Theorem 34 is made a bit more precise in Figure 24. Another subclass of probabilistic automata, called hierarchical automata, has been defined in [START_REF] Chadha | Power of Randomization in Automata on Infinite Strings[END_REF]. The main result is that hierarchical automata recognize exactly the class of ω-regular languages. Unfortunately, the emptiness problem, which is undecidable for the general class of probabilistic automata, is still undecidable for hierarchical automata.

Theorem 35 (Inclusion of the hierarchical automata)

The class of hierarchical automata is strictly included in the class of leaktight automata.

Consequently, the value 1 problem is decidable for hierarchical automata, and the emptiness problem is undecidable for leaktight automata.

Undecidability Results

In this section, we give three undecidability results:

• the first is the undecidability of the two-tier value 1 problem,

• the second is the undecidability of the numberless value 1 problems, as proved in [START_REF] Fijalkow | Two Recursively Inseparable Problems for Probabilistic Automata[END_REF].

• the third is the undecidability of the robustness variants of the value 1 and the emptiness problem.

These results aim at better understanding the limits of what can be done about the value 1 problem, i.e. to what extend is this problem undecidable.

The proof of the first result is different from the original proof from [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]. It shows that the undecidability appears when considering different convergence speeds.

The second result departs from the other undecidability results as it does not consider probabilistic automata, but their numberless counterparts, i.e. the underlying nondeterministic automata. In other words, this result shows that even abstracting away the numerical values of the probabilistic transitions does not lead to decidability.

We then introduce robustness problems, in which a probabilistic automaton is given, but its probabilistic transitions can be modified up to a small perturbation. A decision problem for probabilistic automaton induces a robustness variant, where perturbations are allowed. We obtain as a corollary of the undecidability of the numberless problems that robustness problems are also undecidable.

Undecidability of the Two-tier Value 1 Problem

In this subsection, we revisit the undecidability proof of the value 1 problem. The undecidability result, stated as Theorem 23 in Subsection 1.4, is due to Gimbert and Oualhadj [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]. We give here an a finer analysis of the reduction, which yields the undecidability of a simpler variant, called the two-tier value 1 problem. We will further discuss this undecidability result in Section 6.

Theorem 36 (Undecidability of the two-tier value 1 problem)

The following problem is undecidable: given a simple probabilistic automaton A, determine whether there exist two finite words u, v such that lim n P A ppu ¨vn q 2 n q " 1.

Note that the two-tier value 1 problem is a priori much easier than the value 1 problem, as it restricts the set of sequences of finite words to very simple sequences. We call such sequences two-tier, because they exhibit two different behaviours: the word v is repeated a linear number of times, namely n, while the word u ¨vn is repeated an exponential number of times, namely 2 n . The reduction uses the probabilistic automaton described in Example 3 from Subsection 1.3; the calculations made in the proof to follow and in this example are very similar.

p 0 q 0 , L A F q F q 0 , R A F ⊥ check, 1
Proof. We construct a reduction from the emptiness problem for simple probabilistic automata to the two-tier value 1 problem. Let A be a simple probabilistic automaton. We construct a simple probabilistic automaton B such that the following holds: L ą 1 2 pAq is non-empty if, and only if, there exist two finite words u, v such that lim n P B ppu ¨vn q 2 n q " 1.

Without loss of generality we assume that the initial state q 0 has no ingoing transitions. The alphabet of B is B " A Z tcheck, endu, its set of states is Q B " Q ˆtL, Ru Z tp 0 , K, q F u, its transition function is φ 1 , the only initial state is p 0 and the only final state simple observations we restrict ourselves to words of the form w " check ¨w1 ¨end ¨w2 ¨end ¨¨¨w n ¨end ¨w1 , with w i P A ˚and w 1 P B ˚. Since P A pw i q ď 1 2 for every i, it follows that in B, after reading the last letter end in w before w 1 , the probability to be in pq 0 , Lq is smaller or equal than the probability to be in pq 0 , Rq. This implies the claim. It follows that the value of B is not 1, and in particular for two finite words u, v, we have lim n P B ppu ¨vn q 2 n q ă 1.

Undecidability of the Numberless Value 1 Problems

In this subsection, we report on results obtained in collaboration with Hugo Gimbert, Florian Horn and Youssouf Oualhadj, published in [START_REF] Fijalkow | Two Recursively Inseparable Problems for Probabilistic Automata[END_REF].

The main contribution is an undecidability result for numberless probabilistic automata, which are probabilistic automata where the numerical values of the probabilistic transitions are not specified. The motivation for introducing this model was to obtain a decidable variant of the value 1 problem, as the undecidability proof seemed to strongly rely on numerical manipulations. The negative result presented here shows that these numerical manipulations can be encoded in the structure of the automaton.

Definition 41 (Numberless probabilistic automaton)

A numberless probabilistic automaton is given by a finite set of states Q, a numberless transition function T Ď Q ˆA ˆQ, an initial state q 0 P Q and a set of final states F Ď Q.

The numberless transition function T is an abstraction of transition functions. We say that a transition function φ : A Ñ S QˆQ pQq is consistent with T if for all letters a P A and states s, t P Q, we have φpaqps, tq ą 0 if, and only if, ps, a, tq P T .

A numberless probabilistic automaton M together with a transition function φ consistent with T defines a probabilistic automaton Mrφs. We say that Mrφs is an instance of M. Conversely, a probabilistic automaton A induces an underlying numberless probabilistic automaton rAs, where T is defined by pq, a, pq P T if φpaqpq, pq ą 0.

We consider two variants of the value 1 problem for numberless probabilistic automata:

Problem 8 (Numberless value 1 problem)

• The existential value 1 problem: given a numberless probabilistic automaton M, determine whether there exists φ such that valpMrφsq " 1.

• The universal value 1 problem: given a numberless probabilistic automaton M, determine whether for all φ, we have valpMrφsq " 1.

There exists a numberless probabilistic automaton M such that:

• there exists φ such that valpMrφsq " 1,

• there exists φ 1 such that valpMrφ 1 sq ă 1.

Indeed, an example is given by Example 3 from Subsection 1.3: we proved that for x ą 1 2 , it has value 1, but not for x ď 1 2 . The main contribution of [START_REF] Fijalkow | Two Recursively Inseparable Problems for Probabilistic Automata[END_REF] is the following undecidability result.

Theorem 37 (Recursive Inseparability of the numberless value 1 problems) There exists no algorithm with the following behaviour. Given a numberless probabilistic automaton M:

• if all instances have value 1, then the algorithm answers "YES",

• if no instance has value 1, then the algorithm answers "NO",

• otherwise, the algorithm can do anything, including not terminating.

The remainder of this subsection is devoted to proving this result. Note that it in particular implies that both the universal and the existential value 1 problems are undecidable.

Overall construction Proposition 6 (Construction)

There exists an effective construction which takes as input a simple probabilistic automaton A and constructs a numberless probabilistic automaton M such that valpAq " 1 ðñ @φ, valpMrφsq " 1 ðñ Dφ, valpMrφsq " 1.

We first explain how Proposition 6 implies Theorem 37. Assume towards contradiction that there exists an algorithm A as described in the statement of the theorem. We show using Proposition 6 that this would imply that the value 1 problem is decidable for probabilistic automata. Indeed, let A be a simple probabilistic automaton, applying the construction yields a numberless probabilistic automaton M such that valpAq " 1 ðñ @φ, valpMrφsq " 1 ðñ Dφ, valpMrφsq " 1.

In particular, either all instances of M have value 1, or no instance of M has value 1. So the algorithm A on input M terminates, and:

• if it answers "YES" then valpAq " 1,

• if it answers "NO" then valpAq ă 1, allowing to determine whether A has value 1 or not.

We now give a high level description of the construction; it follows two steps. The first step is to build from A a family of probabilistic automata B λ such that for all 0 ă λ ă 1:

• the transition function of B λ is φ λ : A Ñ S QˆQ pt0, λ, 1 ´λ, 1uq,

• valpB λ q " valpAq.

The second step is to build from the B λ 's a numberless probabilistic automaton M such that, for each probabilistic transition function φ, there exists λ such that Mrφs has value 1 if, and only if, B λ has value 1.

It follows that:

Dφ, valpMrφsq " 1 ùñ Dλ, valpB λ q " 1 ùñ valpAq " 1 ùñ @λ, valpB λ q " 1 ùñ @φ, valpMrφsq " 1.

The fair coin construction

Let A be a simple probabilistic automaton over the alphabet A. We construct a family of probabilistic automata B λ for 0 ă λ ă 1 over the alphabet B " A Y t7u, whose transition function is φ λ : A Ñ S QˆQ pt0, λ, 1 ´λ, 1uq.

The automaton B λ is a copy of A where every probabilistic transition of A is replaced by the gadget illustrated in Figure 26. The initial and final states are the same in A and in B λ .

The left hand side shows part of automaton A: a probabilistic transition from q reading a, leading to r or s each with probability half. The right hand side shows how this behaviour is simulated by B λ : the letter a leads to an intermediate state q a , from which we can read a new letter 7. Each time a pair of 7's is read, the automaton B λ goes to r with probability λ ¨p1 ´λq, goes to s with probability p1 ´λq ¨λ, and stays in q a with probability λ 2 `p1 ´λq 2 . Reading a letter other than 7 while the automata is still in one of the new states leads to a rejecting sink state K. Thus, the probability of going to r is equal to the probability of going to s, and we can make the probability of a simulation failure as low as we want by increasing the number of 7's between two successive letters from A. Let u be a word of A ˚. We denote by rus k the word of B ˚where each letter a P A of u is replaced by a ¨72k . Conversely, if w is a word of B ˚, we denote by w the word obtained from w by removing all occurrences of the letter 7.

Intuitively, a run of A on the word u is simulated by a run of B λ on the word rus k . Whenever there is a transition in A, B λ makes k attempts to simulate it through the gadget of Figure 26, and each attempt succeeds with probability p1 ´2λ ¨p1 ´λqq, so each transition fails with probability:

A λ,k " 1 ´p1 ´2λ ¨p1 ´λqq k .

Lemma 30 (Correctness of the fair coin construction)

The probabilistic automaton B λ satisfies, for all states q, r P Q and k P N:

1. for every letter a P A, we have P B λ pq Proof. We prove the first item. Denote φ A pq, aq " 1 2 ¨r `1 2 ¨s. First, we have P B λ pq

ras k Ý Ý Ñ rq " P B λ pq a 7 2k
Ý Ý Ñ rqq. Reading two letters 7 from q a is interpreted as a round, with three possible outcomes: reaching r with probability λp1 ´λq, reaching s with probability λp1 ´λq, or coming back to q a with probability 1 ´2 ¨λp1 ´λq. Then The second item follows from the first item by induction. The third item is by construction.

Proposition 7 (Fair coin construction) For all 0 ă λ ă 1, we have valpB λ q " valpAq.

Proof. Consider pu n q nPN a sequence of words in A ˚. Denote k n " maxp|u n |, nq and consider the sequence pw n q nPN defined by w n " ru n s kn . Thanks to the second item of Lemma 30, we have P B λ pw n q " A |un| λ,kn ¨PA pu n q.

The sequence ´A|un| λ,kn ¯nPN converges to 1, so lim n P B λ pw n q " lim n P A pu n q. Thus valpAq ď valpB λ q.

The third item of Lemma 30 implies that valpB λ q ď valpAq. apply(b, q)

Figure 27: Naive fusion of the probabilistic transitions.

The simulation construction

All the B λ 's induce the same numberless probabilistic automaton, that we denote by B. Observe that there are many other instances of B, as illustrated in Figure 26, the transitions from the states pq a , Lq and pq a , Rq to the state q a add up to 1, which is not true for all instances of B.

We construct a numberless probabilistic automaton M over an extended alphabet C whose instances simulate all the B λ 's, but only them. The idea is that the new numberless probabilistic automaton will only have one probabilistic transition. An instance of this probabilistic transition translates to a value for λ. Figure 27 describes a first attempt at this (notice that our convention is that a non-drawn transition means a loop, rather than a transition to a sink state).

In this automaton, that we call M 1 , a single shared probabilistic transition q R $ Ý Ñ λ ¨s0 `p1 ´λq ¨s1 is used for all probabilistic transitions. In order to make all the probabilistic transitions of B happen in q R , we use new letters to detect where the runs come from before the probabilistic transition, and where it should go afterwards.

For each letter b in B and state q in Q, we introduce two new letters checkpb, qq and applypb, qq. We also introduce a new letter next_transition. Reading a b in B corresponds to reading p b in M 1 , defined by: p b " checkpb, q 0 q ¨$ ¨applypb, q 0 q ¨¨¨checkpb, q n´1 q ¨$ ¨applypb, q n´1 q ¨next_transition, where tq 0 , q 1 , . . . , q n´1 u is the set of states of B. The function p _ extends to a morphism. There are two copies of the set of states, which are the light gray boxes on the left and on the right of Figure 27. We illustrate the action of checkpb, qq ¨$ ¨applypb, qq, which aims at simulating the transition from q reading b:

• the letter checkpb, qq leads from the left copy of q to q R

• the letter 7 leads to λ ¨s0 `p1 ´λq ¨s1 ,

• the letter applypb, qq leads from s 0 to the λ-valued successor of pq, bq in B λ , and from s 1 to the p1 ´λq-valued successor of pq, bq in B λ .

Note that reading checkpb, qq¨$¨applypb, qq leaves everything else unchanged, as the actions of the letters on the other states are just self-loops. Once the transitions from every state have been simulated, the new letter next_transition sends the run back to the left part. apply(b, q)

apply(b, q)

Figure 28: The numberless probabilistic automaton M.

We get for any word u P B ˚, P B λ puq " P B 1 λ pp uq. The problem with the automaton M 1 is that one can "cheat", either by not testing an unwelcome state, or by changing state and letter between a check and the subsequent apply. For instance, the word checkpb, qq ¨$ ¨applypa, pq does not correspond to any behaviour of B. We say that a word is fair if it is of the form p u for u P B ˚.

The idea is to simulate a word u in B ˚by pp u ¨next_wordq n , for a large n, where next_word is a new letter. Each time p u is read, the run of the new automaton is split in two parts: a proportion of the run is for the simulation itself, as described above, and the rest goes to a wait state, waiting for the next word. Once the word p u is read, the new letter next_word has the following effect:

• the proportion of the run that simulated u and is accepting goes to the initial state of the fairness checker D,

• the proportion of the run that simulated u and is not accepting goes to the nonaccepting sink state K,

• the proportion of the run that ended up in the wait state goes back to the initial state q 0 , for the next simulation.

The fairness checker D is a deterministic automaton recognizing the regular language tp u ¨next_word | u P B ˚u˚.

The resulting automaton, denoted M is described in Figure 28. The structure of the automaton of Figure 27 is still there, but it has been augmented with an extra layer of scrutiny: each time we use the probabilistic transition, there is now a positive probability p1 ´θq to go to a new wait state. The final state of D is the only final state in all of M. Following Figure 28, we denote Mrλ, θs an instance of M. The alphabet of M is denoted C.

Consider the action of reading pp u ¨next_wordq n . The probability to be in the fairness checker increases each time a letter next_word is read, by a proportion of the acceptance probability of p u. If at some point an unfair word is read, then the probability to remain in the fairness checker drops to 0, hence cheating is punished. A run can still cheat before the first next_word letter, but the benefits of doing so are limited: the probability that Mrλ, θs accepts a word at that point is at most θ (except if the empty word is accepting, but that case is trivial).

A more formal proof follows.

Lemma 31 (Correctness of the simulation construction)

1. Let u be a word of B ˚of length k and w a word of pCztnext_worduq ˚. We have P Mrλ,θs pp u ¨next_word ¨wq " θ k ¨PB λ puq ``1 ´θk ˘¨P Mrλ,θs pwq.

2. Let u be a word in B ˚of length k and ě 1. We have P Mrλ,θs ppp u ¨next_wordq q " p1 ´p1 ´θk q q ¨PB λ puq.

3. Let w be a word of pCztnext_worduq ˚and w 1 a word of C ˚. We have P Mrλ,θs pw ¨next_word ¨w1 q ď θ `p1 ´θq ¨PMrλ,θs pw 1 q.

4. Let w 1 , . . . , w k be k words of pCztnext_worduq ˚and w be the word w 1 next_word ¨¨¨w k ¨next_word. Then, for any 1 ď i ď k, if w i R x B ˚, we have P Mrλ,θs pwq ď P Mrλ,θs pw i ¨next_word ¨¨¨w k ¨next_wordq.

5. Let w be a word in C ˚such that P Mrλ,θs pwq ą θ. Then there exists a word u P B such that P B λ puq ě P Mrλ,θs pwq ´θ 1 ´θ .

Proof.

1. This follows from the observation that after reading p u ¨next_word, the distribution is p1 ´θk q ¨q0 `θk ¨PB λ puq ¨qD 0 `θk ¨p1 ´PB λ puqq ¨K.

2. This follows from the first item by induction on .

3. This follows from the observation that after reading w ¨next_word, the run is in one of the following three states: q 0 with probability at most 1 ´θ, q D 0 with probability at most θ, and K.

4. After reading w ăi " w 1 ¨next_word ¨¨¨w i´1 ¨next_word, the run is in one of the following three states: q 0 , q D 0 , and K. As w i R x B ˚, reading w i from q D 0 leads to K. Thus, P Mrλ,θs pwq " P Mrλ,θs pq 0 w ăi Ý Ý Ñ q 0 q ¨PMrλ,θs pw i ¨next_word ¨¨¨w k ¨next_wordq, which concludes. 5. Denote w " w 1 ¨next_word ¨¨¨w p ¨next_word with w 1 , . . . , w p P pCztnext_worduq ˚.

Thanks to the third item, p ą 1, and thank to the fourth item, we can assume without loss of generality that w 2 , . . . , w p belong to x B ˚. Let u 2 , . . . , u p be the words of B ˚such that w i " p u i . Denote w 1 " p u 1 ¨next_word ¨. . . ¨p u p ¨next_word, thanks to the third item we have P Mrλ,θs pwq ď θ `p1 ´θq ¨PMrλ,θs pw 1 q. It follows that P Mrλ,θs pw 1 q ě P Mrλ,θs pwq´θ 1´θ

. Denote w 2 " p u 2 ¨next_word ¨. . . ¨p u p ¨next_word. Without loss of generality, we assume that P Mrλ,θs pw 2 q ď P Mrλ,θs pw 1 q. Denote k the length of u 1 , thanks to the first item we have P Mrλ,θs pw 1 q " θ k ¨PB λ pu 1 q ``1 ´θk ˘¨P Mrλ,θs pw 2 q.

It follows that P B λ pu 1 q ě P Mrλ,θs pw 1 q, which concludes.

Proposition 8 (Simulation construction)

For all 0 ă λ ă 1 and 0 ă θ ă 1, we have valpB λ q " 1 if, and only if, valpMrλ, θsq " 1.

Proof. Let pu n q nPN a sequence of words in B ˚such that lim n P B λ pu n q " 1. Denote k n " maxp2 | u n |, nq and consider the sequence pw n q nPN defined by w n " px u n ¨next_wordq kn .

Thanks to the second item of Lemma 31, we have P Mrλ,θs pw n q " p1 ´p1 ´θ|un| q kn q ¨PB λ pu n q.

A closer look at the sequence pp1 ´θ|un| q kn q nPN shows that it converges to 0. It follows that lim n P Mrλ,θs pw n q " 1, so valpMrλ, θsq " 1.

Conversely, let pw n q nPN be a sequence of words in C ˚such that lim n P Mrλ,θs pw n q " 1. Without loss of generality we can assume that for all n P N, we have P Mrλ,θs pw n q ą 1 ´θw . It follows from the fifth item of Lemma 31 that there exists a sequence pu n q nPN of words in B ˚such that for all n P N, we have P B λ pu n q ě P Mrλ,θs pwnq´θ 1´θ

. Thus lim n P B λ pu n q " 1, so valpB λ q " 1.

Proposition 6 is a direct corollary of Proposition 7 and Proposition 8.

Undecidability of the Robustness Problems

In this subsection, we consider robustness problems: rather than giving as input a probabilistic automaton, we look at a probabilistic automaton up to small modifications of its probabilistic transitions. This question appears naturally in practice: the probabilistic transitions may not be known with absolute precision, and may be subject to small perturbations.

In his original paper, Rabin [START_REF] Michael | Probabilistic Automata[END_REF] considered the influence of small perturbations of the probabilistic transitions on the languages defined by the automaton. He showed that for the class of probabilistic automaton called actual automata, in which there is always a positive probability to go from any state to any other, the language is robust, i.e. is not affected by small perturbations. This result motivated our investigations of the robustness problems.

Here we prove the undecidability of three robustness problems, relying on the undecidability of the numberless problems.

Consider a probabilistic automaton A and ε ą 0. We say that the transition function φ 1 : A Ñ S QˆQ pQq is ε-close to A if for all letters a P A and states s, t P Q, we have:

• |φpaqps, tq ´φ1 paqps, tq| ă ε, and

• φpaqps, tq ą 0 if, and only if, φ 1 paqps, tq ą 0.

Problem 9 (Robustness problems)

• The existential robustness value 1 problem: given a probabilistic automaton A and ε ą 0, determine whether there exists φ 1 which is ε-close to A such that valpArφ 1 sq " 1.

• The universal robustness value 1 problem: given a probabilistic automaton A and ε ą 0, determine whether for all φ 1 which are ε-close to A we have valpArφ 1 sq " 1.

• The universal robustness emptiness problem: given a probabilistic automaton A and ε ą 0, determine whether for all φ 1 which are ε-close to A we have valpArφ 1 sq ě 1 2 .

The existential robustness emptiness problem is missing from this definition; indeed, it is trivial, and reduces to a simple reachability question.

The undecidability of the numberless value 1 problems easily imply the undecidability of the three robustness problems:

Theorem 38 (Undecidability of the robustness problems)

The three robustness problems are undecidable. Proof. The undecidability of both robustness value 1 problems is obtained using Proposition 6, using the same reasoning as given there to prove Theorem 37.

To show that the universal robustness emptiness problem is undecidable, we construct a reduction from the universal robustness value 1 problem.

For the sake of explanation, we give a reduction from the universal numberless value 1 problem to the universal numberless emptiness problem, and later explain how this induces a similar reduction for robustness problems instead of numberless problems.

Let M be a numberless probabilistic automaton. We construct M 1 a numberless probabilistic automaton such that: @φ M , valpMrφ M sq " 1 ðñ @φ M 1 , valpM 1 rφ M 1 sq ě 1 2 .

The reduction is illustrated in Figure 29. Let a, b two new letters (not in A). The automaton M 1 contains a copy of M, and four new states: p 0 , p 1 , p 2 and a sink state K. The state p 0 is initial, and leads non-deterministically to p 1 or p 2 with an ε-transition. The state p 1 leads to the initial state of M with a and to K with b, and vice-versa for p 2 . Observe that a transition function φ 1 M for M 1 is given by a transition function φ M for M and a value x for the ε-transition from p 0 . Also, remark that for w P A ˚and φ 1 M extending φ M , we have P M 1 rφ M 1 s pa ¨wq " x ¨PMrφ M s pwq and P M 1 rφ M 1 s pb ¨wq " p1 ´xq ¨PMrφ M s pwq.

We prove the equivalence:

• Assume that for all φ M , we have valpMrφ M sq " 1. Fix φ M , and consider x, inducing φ M 1 . Let ε ą 0, there exists a word w such that P Mrφ M s pwq ě 1 ´ε. If x ě 1 2 , then P M 1 rφ M 1 s pa ¨wq ě 1´ε 2 , and if x ă 1 2 then P M 1 rφ M 1 s pb ¨wq ě 1´ε 2 . In both cases there exists a word accepted with probability at least 1´ε 2 , so valpM 1 rφ M 1 sq ě 1 2 . • Assume that for all φ M 1 , we have valpM 1 rφ 1 M sq ě 1 2 . Let φ M , and denote by φ 1 M its extension with x " 1 2 . Let ε ą 0, there exists a word w such that P M 1 rφ M 1 s pwq ě 1 2 ´ε. Consider w 1 the word obtained from w by removing its first letter, then P Mrφ M s pw 1 q ě 1 ´2 ¨ε. It follows that valpMrφ M sq " 1.

This proves the correctness of the reduction. To obtain a reduction for robustness problems, we follow the same construction and set x to be 1 2 . The same proof as above concludes.

numerical values for the probabilistic transitions. We give a construction that takes as input a probabilistic automaton A, and outputs a numberless probabilistic automaton C such that the following are equivalent:

• A has value 1,

• there exists an instance of C that has value 1,

• all instances of C have value 1.

Consequently, the numerical values attached to C do not matter, and whether C has value 1 or not does not depend on them. Besides the undecidability result that follows, this also shows that abstracting away the numerical values, as the Markov Monoid does, does not make the problem easier.

We now discuss the undecidability of the two-tier value 1 problem, proved in Subsection 5.1. A two-tier sequence of finite words is a sequence of the form ppu ¨vn q 2 n q nPN , for u, v two finite words. Intuitively, they combine two different behaviours. The first is linear, it consists in repeating n times the word v. The second is exponential, it consists in repeating 2 n times the word u ¨vn . Our interpretation is that the undecidability of the value 1 problem arises when polynomial and exponential behaviours are combined. Since the Markov Monoid captures exactly all polynomial behaviours, it is in this sense optimal.

Perspectives

This chapter focuses on the value 1 loomoon p1q problem for probabilistic automata looooooooooooomooooooooooooon p2q over finite words looooomooooon examples and inspiration to go forward. The experiments on ACME have been reported in [START_REF] Fijalkow | ACME: Automata with Counters, Monoids and Equivalence[END_REF], co-authored with Denis Kuperberg. We pushed this further, and more specifically faster; together with Hugo Gimbert, Edon Kelmendi and Denis Kuperberg, we created the tool ACME ``with the same purpose as ACME, but faster by several orders of magnitude.

Conclusion

What is the relation between the two chapters, i.e. between finite-memory determinacy for boundedness games and the value 1 problem for probabilistic automata?

The short answer is "none". We give a more constructive answer, arguing that a contribution of this document is to show that some techniques used in one context can be used in the other.

A first very rough approximation is that both chapters are about quantitative extensions of automata theory, the first automata with counters and the second probabilistic automata. A second closer inspection reveals that the two chapters are technically unrelated; the definitions, notions, theorems and results are completely independent. However, one can see the influence of the first over the second at a higher level. Indeed, we developed here tools for probabilistic automata and expand on ideas that have successfully been applied to automata with (and also without) counters.

The first example is the algebraic notion of stabilisation monoids, which has been introduced by Colcombet in the theory of regular cost functions [START_REF] Colcombet | The Theory of Stabilisation Monoids and Regular Cost Functions[END_REF], together with its analysis using Green's relations [START_REF] Daniel | Distance Desert Automata and the Star-Height Problem[END_REF][START_REF] Colcombet | Green's Relations and Their Use in Automata Theory[END_REF].

The introduction of the Markov Monoid algorithm was motivated by defining a stabilisation monoid for probabilistic automata.

The second example is the algebraic and combinatorial notion of factorisation forests of bounded height, which has been introduced by Simon in the study of distance automata, and later developed by Colcombet and Toruńczyk for similar purposes [START_REF] Simon | On Semigroups of Matrices over the Tropical Semiring[END_REF][START_REF] Colcombet | Factorization Forests for Infinite Words and Applications to Countable Scattered Linear Orderings[END_REF][START_REF] Toruńczyk | Languages of Profinite Words and the Limitedness Problem[END_REF].

The class of leaktight automata, and more specifically the proof that the Markov Monoid is complete for leaktight automata, is based on the notion of factorisation forests.

The third example is the topological notion of profinite words for regular languages and regular cost functions [START_REF] Pin | Profinite Methods in Automata Theory[END_REF][START_REF] Toruńczyk | Languages of Profinite Words and the Limitedness Problem[END_REF].

The prostochastic theory for probabilistic automata is an extension of the profinite theory for classical automata. The idea of using a profinite theory for probabilistic automata was inspired (although technically unrelated) by the treatment of MSO `U using profinite techniques by Toruńczyk.

Figure 2 :

 2 Figure 2: A B-Büchi game over a pushdown arena where Eve wins the non-uniform condition but no uniform ones.

Figure 3 :

 3 Figure 3: The lower bound.

Figure 4 :

 4 Figure 4: The outbidding condition: more b's than a's.

Figure 5 :

 5 Figure 5: An outbidding game with infinite out-degree where Eve needs infinite memory to win.

  Figure 6: Implications.

Figure 12 :r

 12 Figure 12: Eve has a 2 memory states strategy ensuring BpN qXCoBüchi, but no positional strategy ensures B X CoBüchi.

Figure 14 :

 14 Figure 14: Part of the game pG 1 , B Until Reachq, where Eve needs 3 memory states.

Figure 15 :

 15 Figure 15: Illustration of the 3 memory states strategy in G 1 .

J r 0 0 Figure 19 :

 019 Figure 19: Decomposition of P .

ALGORITHM 1 :

 1 The Markov Monoid algorithm. Data: A probabilistic automaton. M Ð tπpφpaqq | a P Au Y tIu. repeat

Figure 21 :

 21 Figure 21: A non-deterministic automaton and part of its Markov Monoid.

unÝÑ

  tqq nPN converges and: mps, tq " 1 ðñ lim n P A ps un Ý Ñ tq ą 0.

lim n ř sPQ ř tPF δ I psq ¨PA ps un Ý Ñ tq " 1 .

 1 Since for all n P N, we have ř sPQ ř tPQ δ I psq PA ps un Ý Ñ tq " 1, then for s P Q such that δ I psq ą 0 and t R F , it implies that lim sup n P A ps un Ý Ñ tq " 0. Since M is complete, there exists a Boolean matrix m P M such that for all states s, t P Q: lim sup n P A ps un Ý Ñ tq " 0 ùñ mps, tq " 0.

Corollary 2 (

 2 No false negatives for the Markov Monoid algorithm) If the Markov Monoid algorithm answers "YES" on input A, then A has value 1. Theorem 29 follows from the following proposition. Proposition 4 (Characterisation of the Markov Monoid algorithm) For every ω-expression E, for every φ : A Ñ S QˆQ pRq, we have πp p φpEqq " xEy.

Figure 22 :

 22 Figure 22: pa n ¨bq nPN is a leak from L 1 to L 2 .

  lim sup P A ps un Ý Ñ tq " 0, then P A ps un Ý Ñ tq ă p 2 3 |Q| 2 `1 minfor n sufficiently large. Since m N " m n for infinitely many n P N, this implies m N ps, tq ‰ 1, which completes the proof of Theorem 30.

4. 3

 3 Complexity of the Value 1 Problem for Leaktight Au- tomata In this section, we show two results:

Figure 23 :

 23 Figure 23: A leaktight automaton with value 1 and 7-height |Q| ´2.

Figure 24 :

 24 Figure 24: Inclusion of the different subclasses.

  Figure 25: Reduction.

Figure 26 :

 26 Figure 26: The fair coin gadget.

  ras k Ý Ý Ñ rq " A λ,k ¨PA pq a Ý Ñ rq,2. for all words u P A ˚, we have P B λ pqrus k Ý Ý Ñ rq " A |u| λ,k ¨PA pq u Ý Ñ rq,3. for all words w P B ˚, we have P B λ pq w Ý Ñ rq ď P A pq w Ý Ñ rq.

P B λ pq a 7 2k Ý

 2k ´λqq i´1 ¨λp1 ´λq " A λ,k 2 .

  Figure 29: Reduction.

  P b) ω P . (ba ω P ) ω P . (ab ωP ) ωP a ωP b . (a(ba) n ) 2 n . (ab n ) 2 n . (ba n ) 2 n

Figure 30 :

 30 Figure 30: Optimality of the Markov Monoid algorithm.

  p3q

.

  1 2 ¨PA puq `1 2 ¨PB puq. and two states s, t P Q A Y Q B , if mps, tq " 1, then either s, t P Q A or s, t P Q B . Relying on this, we map m P M

	Lemma 25 (Stability of the leaktight class by parallel composition)
	The class is leaktight automata is stable by parallel composition.
	A||B ε Proof. The extended Markov Monoid M direct product M A ε ˆMB ε of the extended Markov Monoids of each automaton. of the parallel composition embeds into the A||B ε Note that for m P M A||B ε

  1 1 ¨¨¨m 1 k where for all i, either m 1 i P S p or m 1 i " m 7 i for m i P S p and m 1 i R S p . If for all i, m 1 i P S p , then m " m 1 1 ¨¨¨m 1 k P S p , which is a contradiction. Consequently, there exists i such that m 1 i " m 7 i for m i P S p and m 1 i R S p . Since m i P S p and m 1 i " m 7 i R S p , we have m 7 i ‰ m i . Towards contradiction, assume m i P S p´1 , then p ě 1, and this implies m 7 i P S p , which is a contradiction. Hence, m i P S p zS p´1 . By induction, we have |Clpm i q| ď |Q| ´p. Since m 7 i ‰ m i , by Lemma 27 we have |Clpm 7 i q| ă |Clpm i q|. Since m ď J m 7 i , by Lemma 28 we have |Clpmq| ď |Clpm 7 i q|. Altogether, it follows |Clpmq| ď |Q| ´pp `1q. It follows from Lemma 29 that S |Q|´1 " S |Q| " M ε , i.e. the 7-hierarchy collapses at level |Q| ´1, proving Theorem 32.

Une synchyse est une phrase, rendue difficile à comprendre par l'inversion, ou parfois seulement le mélange, et c'est là qu'il faut de la créativité (comme en mathématiques me direz-vous), de certaines parties, simple.

Leaks are special elements of the extended Markov Monoid, see the definition of leaks and leaktight automata in Subsection 4.2.

Acknowledgments

Following [Que47], the same story (or part of it) is told several times, using different styles.

Here is the story:

We can now proceed to the proof of Lemma 8.

Proof. Consider a game pG, W q. We define the following sequences indexed by ordinals:

After each edge followed, Eve is left the choice to set the mode to S. The set of choice vertices is denoted V . We define E 1 together with c 1 : E Ñ tε, i, ru k`1 :

if pv, v 1 q P E, pv, Sq cpv,v 1 q,ε Ý ÝÝÝÝÝ Ñ pv 1 , Sq if pv, v 1 q P E and Ωpv 1 q " 0, pv, Sq cpv,v 1 q,i Ý ÝÝÝÝÝ Ñ pv 1 , Aq if pv, v 1 q P E and Ωpv 1 q " 1, pv, Sq cpv,v 1 q,r Ý ÝÝÝÝÝ Ñ pv 1 , Sq if pv, v 1 q P E and Ωpv 1 q ą 1, v ε Ý Ý Ñ pv, Aq and v ε Ý Ý Ñ pv, Sq Equip the arena G 1 with the colouring function Ω 1 defined by

if Ωpvq " 0 and m " S, Ωpvq otherwise.

Before stating and proving the equivalence between G and G 1 , we formalise the property mentioned above, that in word arenas Eve does not need to alternate an unbounded number of times between the modes "Safe" and "Attractor".

Lemma 14 (Bounded alternation in word arenas)

Let G be a word arena of width W , and a subset F of vertices such that every path in G contains finitely many vertices in F . Define the following sequence of subsets of vertices: X 0 " H, and for i ě 0:

"

v ˇˇˇa ll paths from v contain no vertices in F before the first vertex in X 2i , if any * , X 2i`2 " v ˇˇall paths from v are finite or lead to X 2i`1 ( .

We have X 0 Ď X 1 Ď X 2 Ď ¨¨¨, and X 2W covers the whole arena.

Proof. We first argue that the following property, denoted p:q, holds: "for all i ě 0, if X 2i does not cover the whole arena, then X 2i`1 zX 2i´1 contains an infinite path". (For technical convenience X ´1 " H.) Let v R X 2i . We consider G v where v is the initial vertex, and prune it by removing the vertices from X 2i´1 , as well as vertices which do not have an infinite path after removing X 2i´1 ; denote by G 1 v the arena we get. Note that for any u R X 2i , the vertex u belongs to G 1 v , so G 1 v contains an infinite path. We claim that there exists a vertex v 1 in G 1 v such that all paths from v 1 contain no vertices F . Indeed, assume towards contradiction that from every node in G 1 v , there exists a path to a vertex in F . Then there exists a path that visits infinitely many vertices in F , contradicting the assumption on G. Any infinite path from v 1 is included into X 2i`1 zX 2i´1 , hence the latter contains an infinite path. We conclude using p:q: assume towards contradiction that X 2W does not cover the whole arena. Then G contains W `1 pairwise disjoint paths, contradicting that it has width W .

Chapter 2

The Value 1 Problem for Probabilistic Automata

The Prostochastic Theory

In this section, we introduce the prostochastic theory, which is a profinite theory for probabilistic automata. We construct the free prostochastic monoid in Subsection 2.1.

The aim of this theory is to give a topological account of the value 1 problem; we will show in Subsection 2.2 that the value 1 problem naturally reformulates as an emptiness problem for prostochastic words.

In Subsection 2.3 we show how to construct non-trivial prostochastic words. We will use this material in Section 3 to prove some properties of the Markov Monoid algorithm. Subsection 2.4 is devoted to proving a technical result about powers of a stochastic matrix.

All the material presented here is taken from [START_REF] Fijalkow | Characterisation of an Algebraic Algorithm for Probabilistic Automata[END_REF].

The Free Prostochastic Monoid

We consider the norm || ¨|| defined on M QˆQ pRq by

The following classical properties will be useful:

Fact 3 (Topology of the stochastic matrices)

• For every matrix M P S QˆQ pRq, we have ||M || " 1,

• For every matrices M, M 1 P M QˆQ pRq, we have

• The monoid S QˆQ pRq is compact.

The purpose of the prostochastic theory is to construct a compact monoid PA ˚together with a continuous injective morphism ι : A ˚Ñ PA ˚, called the free prostochastic monoid, satisfying the following universal property:

We first consider the right term:

Thus, this term converges exponentially fast to 0.

We then consider the left term. Thanks to Lemma 19, there exists a constant C ą 1 such that for all p P N, we have

Thus, this term converges exponentially fast to 0. We proved that pP n q nPN converges exponentially fast to a matrix M ω . We conclude the proof of Theorem 28 by observing that: πpM ω qps, tq " # 1 if πpP qps, tq " 1 and t is πpP q-recurrent, 0 otherwise.

Assume first that πpM ω qps, tq " 1, i.e. M ω ps, tq ą 0. It already implies that t is πpP q-recurrent, looking at the decomposition of P n . Since M ω " lim n P n , it follows that for n large enough, we have P n ps, tq ą 0. The matrix πpP q is idempotent, so we have for all n P N the equality πpP n q " πpP q, implying that P ps, tq ą 0, i.e. πpP qps, tq " 1.

Conversely, assume that πpP qps, tq " 1 and t is πpP q-recurrent. Observe that for all n P N we have P n`1 ps, tq ě P ps, tq¨P n pt, tq. For n converging towards infinity, this implies M ω ps, tq ě P ps, tq ¨M ω pt, tq. Note that P ps, tq ą 0, and M ω pt, tq ą 0 since t is πpP qrecurrent and thanks to Lemma 19. It follows that M ω ps, tq ą 0, i.e. πpM ω qps, tq " 1.

ALGORITHM 2: The extended Markov Monoid algorithm. Data: A probabilistic automaton. A set of extended Boolean matrices M is complete for A if for each sequence of words pu n q nPN , there exists m P M such that for all states s, t P Q:

The same proof as for Lemma 20 shows that if M is complete for A and A has value 1, then A contains a value 1 witness. Together with the observation above, this implies that if M is complete for A, then the extended Markov Monoid algorithm correctly determines whether A has value 1.

Completeness for Leaktight Automata

In this subsection, we define leaktight automata, and show that the extended Markov Monoid algorithm is complete for leaktight automata.

Definition 35 (Leak)

An extended Boolean idempotent matrix m is a leak from the state s P Q to the state t P Q if:

1. s and t are m-recurrent, is indeed the image of the first component under ψ.

The following theorem was stated for the tropical semiring in [START_REF] Simon | On Semigroups of Matrices over the Tropical Semiring[END_REF], and generalised in [START_REF] Colcombet | The Theory of Stabilisation Monoids and Regular Cost Functions[END_REF]. A simple proof can be found in [START_REF] Toruńczyk | Languages of Profinite Words and the Limitedness Problem[END_REF].

Theorem 31 (Existence of 7-factorisation trees of bounded depth) Consider a stabilisation monoid pM, ¨, 7q and a monoid morphism ψ : A ˚Ñ M . Every word u P A ˚has a 7-factorisation tree whose depth is less than 3 ¨|M |.

In the proof of completeness of the extended Markov Monoid algorithm for leaktight automata, the following lemma, called the Lower bound lemma, is instrumental. It associates to every word a 7-factorisation tree of bounded depth and propagates bounds on the probabilities by induction on the levels of this tree.

Lemma 23 (Lower bound lemma)

Let A be a leaktight automaton, and p min the smallest non-zero transition probability of A. Then for all words u P A ˚, there exists m in the extended Markov monoid such that, for all states s, t P Q: mps, tq ‰ 0 ðñ

Proof. Consider a finite word u P A ˚; by Theorem 31 applied to the extended Markov Monoid M ε of A, which is a stabilisation monoid thanks to Lemma 22, and the morphism ψ : A Ñ M defined by ψpaq " πpφpaqq, there exists a 7-factorisation tree of depth at most 3 ¨|M ε |, whose root is labelled by pu, mq for some extended Boolean matrix m of M ε .

The depth of a node in this tree is defined in a bottom-up fashion: the leaves have depth zero, and a node has depth one plus the maximum of the depths of its children.

We prove by a bottom-up induction on h that for every node pu, mq of this tree at depth h, for all states s, t P Q:

mps, tq "

The case h " 0 is for leaves. Here, either u is a letter a and m " πpφpaqq, or u is the empty word ε and m " I. Then both (2.1) and (2.2) hold.

Assume h ą 0, there are two cases.

First case: a multiplication node labelled by pu, mq with two children labelled by pu 1 , m 1 q and pu 2 , m 2 q. By definition u " u 1 ¨u2 and m " m 1 ¨m2 .

We first prove that (2.1) holds. Indeed, for two states s, t P Q, we have pm 1 ¨m2 qps, tq ‰ 0 if, and only if, there exists a state r P Q such that m 1 ps, rq ‰ 0 and m 2 pr, tq ‰ 0. On the other side, since: Ý Ñ tq ą 0. We conclude with the induction hypothesis. Now we prove that (2.2) holds. Consider two states s, t P Q such that mps, tq " 1. Then there exists a state r P Q such that m 1 ps, rq " 1 and m 2 pr, tq " 1. So:

where the second inequality is by induction hypothesis. This completes the proof of (2.2).

Second case: a stabilisation node labelled by pu, m 7 q with k sons labelled by pu 1 , mq, . . . , pu k , mq. By definition, u " u 1 ¨¨¨u k , and m is idempotent.

The proof that (2.1) holds is similar to the concatenation node case. Now we prove that (2.2) holds. Consider two states s, t P Q such that m 7 ps, tq " 1. Since k ě 3:

To establish (2.2) we prove that P A ps

min and for all states q P Q, we have

min . Since m 7 ps, tq " 1, by definition mps, tq " 1 and t is m-recurrent. The induction hypothesis for the node pu 1 , mq implies that P A ps

min . For that we use the hypothesis that m is not a leak. By induction hypothesis for each child, (2.1) implies that m k´2 pt, qq ‰ 0. Since m is idempotent, mpt, qq ‰ 0. We argue that mpq, tq " 1. Let P Q an m-recurrent state such that mpq, q " 1. Then mpt, q ‰ 0, and t, are m-recurrent. Since m is not a leak, and in particular not a leak from t to , it follows that mpt, q " 1, which implies that mp , tq " 1 since t is m-recurrent. Together with mpq, q " 1, this implies mpq, tq " 1. Thus, by induction hypothesis and according to (2.2), P A pq

min . Now, putting all inequalities together:

where the last equality holds because

Ý ÝÝÝÝ Ñ qq " 1. This completes the proof of (2.2).

To conclude, note that M ε has less than 3 |Q| 2 elements.

Relying on the lower bound lemma (Lemma 23), we prove the completeness of the extended Markov monoid for leaktight automata.

Let A be a leaktight automaton, and pu n q nPN a sequence of finite words. By Lemma 23, for each word u n there exists an extended Boolean matrix m n in the extended Markov monoid such that for all states s, t P Q: m n ps, tq " 1 ùñ P A ps un Ý Ñ tq ě p 2 3 |Q| 2 `1 min . rss m 7 " rss m . In other words, the equivalence classes for m 7 are also equivalence classes for m, so Clpm 7 q Ď Clpmq.

We now prove the second item. Assume m ‰ m 7 ; it implies that there exist two states s, t P Q such that m 7 ps, tq " ε, mps, tq " 1 and t is m-transient. By Lemma 26, there exists r such that mps, tq " mps, rq ¨mpr, rq ¨mpr, tq, so mps, rq " mpr, rq " mpr, tq " 1. Note that r is m-transient, as mpr, tq " 1 would imply that t is m-recurrent. So m 7 pr, rq " ε. Thus, r P Z m but r R Z m 7 . Hence, there is a class rrs m in Clpmq, but there is no class rrs m 7 in Clpm 7 q.

The following lemma shows that the quantity |Clpmq| is common to all idempotents in the same J -class. The notion of J -class is a classical notion for the theory of monoids, derived from one of the four Green's relations called the J -preorder (for details about Green's relations and its applications to automata theory see [START_REF] Colcombet | Green's Relations and Their Use in Automata Theory[END_REF]).

Define m ď J m 1 if there exist two extended Boolean matrices n, n 1 such that n¨m 1 ¨n1 " m, and mJ m 1 , i.e. m and m 1 are in the same J -class, if m ď J m 1 and m 1 ď J m. Proof. Let n, n 1 be two extended Boolean idempotent matrices such that m ď J m 1 ; consider two extended Boolean matrices n, n 1 such that n ¨m1 ¨n1 " m. First, without loss of generality we assume that n ¨m1 " n and m 1 ¨n1 " n 1 . Indeed, if n or n 1 do not satisfy these conditions, then we consider n " n ¨m1 and n 1 " m 1 ¨n1 .

We construct a partial surjective mapping β : Clpm 1 q Ñ Clpmq, which depends on the choice of n and n 1 . For all states s P Z m 1 and t P Z m satisfying npt, sq ¨m1 ps, sq ¨n1 ps, tq " 1 we set βprss m 1 q " rts m . To complete the proof, we have to show that β is well defined and that β is indeed surjective.

We show that β is well defined. Let s, s 1 P Z m 1 and t, t 1 P Z m , and assume npt, sq m1 ps, sq ¨n1 ps, tq " 1 and npt 1 , s 1 q ¨m1 ps 1 , s 1 q ¨n1 ps 1 , t 1 q " 1. By definition βprss m 1 q " rts m and βprs 1 s m 1 q " rt 1 s m . To show that β is well defined, we have to show that if rss m 1 " rs 1 s m 1 , then rts m " rt 1 s m . Assume rss m 1 " rs 1 s m 1 , i.e., s " m 1 s 1 , so m 1 ps, s 1 q " 1. Since npt, sq ¨m1 ps, sq ¨n1 ps, tq " 1, we have npt, sq " n 1 ps, tq " 1. Similarly, npt 1 , s 1 q ¨m1 ps 1 , s 1 q n1 ps 1 , t 1 q " 1, so npt 1 , s 1 q " n 1 ps 1 , t 1 q " 1. Consequently, npt, sq ¨m1 ps, s 1 q ¨n1 ps 1 , t 1 q " 1, so mpt, t 1 q " pn ¨m1 ¨n1 qpt, t 1 q " 1. Symmetrically, npt 1 , s 1 q ¨m1 ps 1 , sq ¨n1 ps, tq " 1, so mpt 1 , tq " 1, implying t " m t 1 , i.e. rts m " rt 1 s m .

We show that β is surjective. Let t P Z m . We exhibit some state s P Q such that βprss m 1 q " rts m . Since mpt, tq " 1 and m " n ¨m1 ¨n1 , there exist two states p, q P Q such that npt, pq " m 1 pp, qq " n 1 pq, tq " 1. By Lemma 26, there exists a state s P Q such that m 1 pp, sq ¨m1 ps, sq ¨m1 ps, qq " m 1 pp, qq " 1, so m 1 pp, sq " m 1 ps, sq " m 1 ps, qq " 1, implying s P Z m 1 . We have npt, sq " pn ¨m1 qpt, sq ě npt, pq ¨m1 pp, sq " 1, and n 1 ps, tq " pm 1 ¨n1 qps, tq ě m 1 ps, qq ¨n1 pq, tq " 1. To sum up, npt, sq ¨m1 ps, sq ¨n1 ps, tq " 1, and hence, βprss m 1 q " rts m .

The following lemma wraps up the previous two lemma. For technical convenience, we set S ´1 " H. is q F . We describe φ 1 as a function φ

" 1 2 ¨pq 0 , Lq `1 2 ¨pq 0 , Rq φ 1 ppq, dq, aq " pφpq, aq, dq for a P A and d P tL, Ru φ 1 ppq 0 , Lq, checkq " q F φ 1 ppq, Lq, endq " q 0 if q P F φ 1 ppq, Lq, endq

where as a convention, if a transition is not defined, it leads to K.

Assume that there exists a finite word w such that P A pwq ą 1 2 , then we claim that lim n P B ppcheck ¨pw ¨endq n q 2 n q " 1. Denote x " P A pwq. We have

and

We fix an integer N and analyse the action of reading pcheck ¨pw ¨endq n q N : there are N "rounds", each of them corresponding to reading check ¨pw ¨endq n from p 0 . In a round, there are three outcomes: winning (that is, remaining in pq 0 , Lq) with probability p n " 1 2 ¨xn , losing (that is, remaining in pq 0 , Rq) with probability q n " 1 2 ¨p1 ´xq n , or going to the next round (that is, reaching p 0 ) with probability 1 ´pp n `qn q. If a round is won or lost, then the next check leads to an accepting or rejecting sink; otherwise it goes on to the next round, for N rounds. Hence:

e now set N " 2 n . A simple calculation shows that the sequence pp1 ´pp n qn qq N ´1q nPN converges to 0 as n goes to infinity. Furthermore, qn pn " p 1´x x q n , which converges to 0 as n goes to infinity since x ą 1 2 . It follows that the acceptance probability converges to 1 as n goes to infinity. Consequently:

Conversely, assume that for all finite words w, we have P A pwq ď 1 2 . We claim that every finite word in B ˚is accepted by B with probability at most 1 2 . First of all, using

Conclusions

At the end of the day, how did we answer the initial question: "to what extent is the value 1 problem decidable"? This section gathers the different elements of answers in Subsection 6.1, supporting the claim that the Markov Monoid algorithm is optimal. Subsection 6.2 opens perspectives for future research.

Optimality

The first observation is that probabilistic automata may exhibit complicated convergence phenomena with different convergence speeds, as witnessed by Example 3 from Subsection 1.3.

We construct in Section 3 an algebraic structure, extending the classical notion of transition monoid of a non-deterministic automaton, called the Markov Monoid. In addition to concatenation, the Markov Monoid additionally features a stabilisation operator, which accounts for some limit behaviours. This gives rise to an algorithm, called the Markov Monoid algorithm, which aims at partially solving the value 1 problem.

Using the prostochastic theory developed in Section 2, we give a characterisation of the Markov Monoid algorithm. Roughly speaking, it says that the Markov Monoid algorithm captures exactly all polynomial behaviours, which are described by polynomial prostochastic words.

We show in Section 4 that the Markov Monoid algorithm subsumes all previous known algorithms to solve the value 1. Indeed, we prove that it is correct for the subclass of leaktight automata, and that the class of leaktight automata strictly contains all subclasses for which the value 1 problem has been shown to be decidable. At this point, the Markov Monoid algorithm is the best algorithm so far. But can we go further? Section 5 gives two arguments supporting the claim that the Markov Monoid algorithm is in some sense optimal.

We first discuss the undecidability of the numberless value 1 problems, proved in Subsection 5.2. Since the Markov Monoid does not take into account the numerical values of the probabilistic transitions, it is natural to ask whether loosely specifying these numerical values makes the problem easier. To formalize this, we consider numberless probabilistic automata, which can be instantiated as probabilistic automata by specifying There are at least three natural follow-up questions:

(1) What about other values, such that 1 2 , i.e. the emptiness problem? (2) What about generalisations of probabilistic automata, such as partially observable Markov decision processes?

(3) What about infinite words, or trees?

The other natural and burning question is:

(4) What is the practical value of the Markov Monoid algorithm?

We discuss these four points further.

The emptiness problem. There are both positive and negative results:

• the emptiness problem is undecidable for acyclic probabilistic automata (only selfloops are allowed), which is a quite severe structural restriction,

• different subclasses of probabilistic automata have been defined for which this problem has been shown decidable. For instance, the class of one-level hierarchical automata have been introduced very recently in [START_REF] Chadha | Decidable and Expressive classes of Probabilistic Automata[END_REF], and shown to have a decidable emptiness problem while recognizing non-regular languages.

The general question we ask is:

"To what extent is the emptiness problem decidable?"

In particular, can we find an algorithm that is often correct? Can we quantify how often? Can we argue that it is optimal ? We hope that the prostochastic theory may help in answering these questions.

Several variants of the emptiness problem have been proposed. For instance, adding approximation may lead to decidable problems; a promising step was done in this direction recently in [START_REF] Manindra Agrawal | Approximate Verification of the Symbolic Dynamics of Markov Chains[END_REF].

Partially observable Markov decision processes. Extending subclasses of probabilistic automata to partially observable Markov decision processes to decide the value 1 problem has already started: this has been done for the class of 7-acyclic automata [START_REF] Gimbert | Deciding the Value 1 Problem for sharp-acyclic Partially Observable Markov Decision Processes[END_REF]. No extensions of the class of leaktight automata have been defined so far.

Beyond finite words. We investigated the setting of infinite words in [START_REF] Fijalkow | Deciding the value 1 Problem for Probabilistic Leaktight Automata[END_REF], and proved a generic result allowing to reduce the value 1 problem from infinite words to finite words. Note that this is different from the equivalence between the value 1 problem for finite words and the emptiness problem for probabilistic Büchi automata with positive semantics, as discussed in Subsection 1.3.

Defining probabilistic automata over infinite trees is not obvious. An interesting and well behaved definition was proved by Carayol, Haddad in Serre in [CHS11; CHS14], called qualitative automata. We extended the definition to alternating qualitative automata in [START_REF] Fijalkow | Emptiness Of Alternating Tree Automata Using Games With Imperfect Information[END_REF]. A lot of open questions remain about this class of languages over infinite trees.

Practical value of the Markov Monoid algorithm. Together with Denis Kuperberg, we implemented the Markov Monoid algorithm in the tool ACME, providing benchmarks,