Nathanaël Fijalkow

Hugo Gimbert
email: hugo.gimbert@labri.fr

Edon Kelmendi
email: edon.kelmendi@labri.fr

Youssouf Oualhadj
email: youssouf.oualhadj@lacl.fr

Ë L Nathana

Hugo Fijalkow

Edon Gimbert

AND Youssouf Kelmendi

Oualhadj

Deciding the value 1 problem for probabilistic leaktight automata

Keywords: 1998 ACM Subject Classification: Probabilistic computation Probabilistic automata, Value 1 problem, Algebraic Techniques in Automata Theory

Introduction

Probabilistic automata. Rabin invented a very simple yet powerful model of probabilistic machine called probabilistic automata, which, quoting Rabin, "are a generalization of finite deterministic automata" [START_REF] Michael | Probabilistic automata[END_REF]. A probabilistic automaton has a finite set of states and reads input words from a finite alphabet. The computation starts from the initial state and consists in reading the input word sequentially; the state is updated according to transition probabilities determined by the current state and the input letter. The probability to accept a finite input word is the probability that the computation ends in one of the final states.

Probabilistic automata, and more generally partially observable Markov decision processes and stochastic games, are a widely studied model of probabilistic machines used in many fields like software verification [START_REF] Baier | Probabilistic ω-automata[END_REF][START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF], image processing [START_REF] Culik | Digital images and formal languages[END_REF], computational biology [START_REF] Durbin | Biological Sequence Analysis: Probabilistic Models of Proteins and Nucleic Acids[END_REF] and speech processing [START_REF] Mohri | Finite-state transducers in language and speech processing[END_REF]. As a consequence, it is crucial to understand which decision problems are algorithmically tractable for probabilistic automata. From a language-theoretic perspective, several algorithmic properties of probabilistic automata are known: while language emptiness is undecidable [Paz71, Ber74, GO10], functional equivalence is decidable [START_REF] Paul | On the definition of a family of automata[END_REF][START_REF] Tzeng | A polynomial-time algorithm for the equivalence of probabilistic automata[END_REF] as well as other properties [START_REF] Cortes | On the computation of the relative entropy of probabilistic automata[END_REF].

Our initial motivation for this work comes from control and game theory: we aim at solving algorithmic questions about partially observable Markov decision processes and stochastic games. For this reason, we consider probabilistic automata as machines controlled by a blind controller, who is in charge of choosing the sequence of input letters in order to maximize the acceptance probability. While in a fully observable Markov decision process the controller can observe the current state of the process to choose adequately the next input letter, a blind controller does not observe anything and its choice depends only on the number of letters already chosen. In other words, the strategy of a blind controller is an input word of the automaton.

The value of a probabilistic automaton. With this game-theoretic interpretation in mind, we define the value of a probabilistic automaton as the supremum acceptance probability over all input words, and we would like to compute this value. Unfortunately, as a consequence of Paz undecidability result, the value of an automaton is not computable in general. However, the following decision problem was conjectured by Bertoni [START_REF] Bertoni | The solution of problems relative to probabilistic automata in the frame of the formal languages theory[END_REF] to be decidable:

Value 1 problem: Given a probabilistic automaton, does it have value 1? In other words are there input words whose acceptance probability is arbitrarily close to 1?

Recently, the second and fourth authors of the present paper proved that the value 1 problem is undecidable [START_REF] Gimbert | Probabilistic automata on finite words: Decidable and undecidable problems[END_REF].

Our result. We introduce a new class of probabilistic automata, called leaktight automata, for which the value 1 problem is decidable. This subclass strictly subsumes all known subclasses of probabilistic automata sharing this decidability property and has good closure properties. Our algorithm to decide the value 1 problem computes in polynomial space a finite monoid whose elements are directed graphs and checks whether it contains a certain type of elements that are value 1 witnesses. Related works. Introducing subclasses of probabilistic automata to cope with undecidability results has been a fruitful and lively topic recently. We discuss some of them here.

The first subclass which was introduced specifically to decide the value 1 problem are the ♯-acyclic automata [START_REF] Gimbert | Probabilistic automata on finite words: Decidable and undecidable problems[END_REF]. Later on, Chatterjee and Tracol [START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF] introduced structurally simple automata, which are probabilistic automata satisfying a structural property (related to the decomposition-separation theorem from probability theory), and proved that the value 1 problem is decidable for structurally simple automata. At the same time, a subset of the authors introduced leaktight automata, and proved a similar result. As we shall see, both ♯-acyclic and structurally simple automata are leaktight, hence our results extend both [START_REF] Gimbert | Probabilistic automata on finite words: Decidable and undecidable problems[END_REF] and [START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF].

Quite recently, Chadha, Sistla and Viswanathan introduced the subclass of hierarchical automata [START_REF] Chadha | Power of randomization in automata on infinite strings[END_REF], and showed that over infinite words, they recognize exactly the class of ω-regular languages. As we shall see, hierarchical automata are leaktight, hence as a consequence of our result, the value 1 problem is decidable for hierarchical automata.

Proof techniques. Our proof techniques totally depart from the ones used in [START_REF] Chadha | Power of randomization in automata on infinite strings[END_REF][START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF][START_REF] Gimbert | Probabilistic automata on finite words: Decidable and undecidable problems[END_REF]. We make use of algebraic techniques and in particular Simon's factorization forest theorem, which was used successfully to prove the decidability of the boundedness problem for distance automata [START_REF] Simon | On semigroups of matrices over the tropical semiring[END_REF], and extended models as desert automata and Bautomata [START_REF] Daniel | Distance desert automata and the star height problem[END_REF][START_REF] Colcombet | The theory of stabilisation monoids and regular cost functions[END_REF] Outline. Basic definitions are given in Section 1. In Section 2, we introduce the Markov monoid and the Markov monoid algorithm for the value 1 problem; since the problem is in general undecidable, the algorithm is incomplete: a positive answer implies that the automaton has value 1, but a negative answer gives no guarantee.

In Section 3, we define the class of leaktight automata and show that the leaktight property is a sufficient condition for this algorithm to be complete; in particular, this implies that the value 1 problem is decidable for leaktight automata.

In Section 4, we show that the Markov monoid algorithm runs in polynomial space, and obtain as a corollary that the value 1 problem for leaktight automata is PSPACE-complete. Furthermore, we extend the Markov monoid algorithm to check at the same time whether an automaton is leaktight and whether in such case it has value 1.

In Section 5, we further investigate the class of leaktight automata: we provide examples of leaktight automata and show that all subclasses of probabilistic automata whose value 1 problem is known to be decidable are leaktight.

In Section 6, we give a general theorem allowing to extend the decidability results from finite words to infinite words.

1. Definitions 1.1. Probabilistic automata. We fix A a finite alphabet. A (finite) word u is a (possibly empty) sequence of letters u = a 0 a 1 • • • a n-1 , the set of finite words is denoted by A * . For i ≤ j we denote by u[i, j] the subword a i • • • a j-1 , and

u <p = u[0, p] = a 0 a 1 • • • a p-1 .
Let Q be a finite set of states. A probability distribution over Q is a function δ : Q → [0, 1] such that q∈Q δ(q) = 1; we often see δ as a row vector of size |Q|. We denote by 1 3 • q + 2 3 • q ′ the distribution that picks q with probability 1 3 and q ′ with probability 2 3 , and by q the trivial distribution picking q with probability 1. For a subset R of states, the uniform distribution over R picks each state in R with probability 1 |R| . The support of a distribution δ is the set of states picked with positive probability, i.e. Supp(δ) = {q ∈ Q | δ(q) > 0}.

Finally, the set of probability distributions over Q is D(Q).

Definition 1.1 (Probabilistic automaton). A tuple A = (Q, q 0 , ∆, F ) represents a probabilistic automaton, where Q is a finite set of states, q 0 ∈ Q is the initial state, ∆ defines the transitions and F ⊆ Q is the set of accepting states.

The transitions of a probabilistic automaton are given by a function ∆ : Q×A → D(Q), where ∆(q, a) is the probability distribution obtained by reading the letter a from the state q. The function ∆ induces the function ∆

′ : D(Q) × A → D(Q), where ∆ ′ (δ, a) = q∈Q δ(q) • ∆(q, a). Going further, ∆ naturally extends to ∆ * : D(Q) × A * → D(Q) by induction: for a letter a ∈ A, we set ∆ * (δ, a) = ∆ ′ (δ, a)
, and for an input word u = av, we set ∆ * (δ, u) = ∆ * (∆ ′ (δ, a), v). Intuitively, ∆ * (δ, u) is the probability distribution obtained by reading the word u starting at the initial probability distribution δ. From now on, we will make no difference between ∆, ∆ ′ and ∆ * , and denote the three of them by ∆.

We denote by P A (s u -→ t) the probability to go from state s to state t reading u on the automaton A, i.e. ∆(s, u)(t). Then P A (s u -→ T ) is defined as t∈T P A (s u -→ t). Finally, the acceptance probability of a word u ∈ A * by A is P A (q 0 u -→ F ), which we denote by P A (u). For computational purposes, we assume that each value is a rational number given by two integers in binary decomposition. (1.1) 1.2. The value 1 problem. We are interested in the following decision problem:

Problem 1.3 (Value 1 Problem). Given a probabilistic automaton A, decide whether val(A) = 1.

The value 1 problem can be reformulated using the notion of isolated cut-point introduced by 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.

0 L1 L2 R1 R2 a b, 1 2 a, 1 -x b a, x a, b b, 1 2 a, x b a, 1 -x a, b
Figure 1: This automaton has value 1 if and only if x > 1 2 .

The automaton depicted on figure 1 has value 1 if and only if x > 1 2 (a similar example appears in [START_REF] Baier | Probabilistic ω-automata[END_REF]). The input alphabet is A = {a, b}, the initial state is the central state 0 and the unique final state is L 2 .

We describe the behaviour of this automaton. 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 val(A) = 1 2 . However, if x > 1 2 then we show that A has value 1. We have:

P A (0 ba n --→ L 1 ) = 1 2 • x n and P A (0 ba n --→ R 1 ) = 1 2 • (1 -x) n
We fix an integer N and analyse the action of reading (ba n ) N • b: 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 • x n , losing (that is, remaining in R 2 ) with probability q n = 1 2 • (1 -x) n
, or going to the next round (that is, reaching 0) with probability 1 -(p n + q n ). 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 ((ba n ) N • b) = N k=1 (1 -(p n + q n )) k-1 • p n = p n • 1-(1-(pn+qn)) N 1-(1-(pn+qn)) = 1 1+ qn pn • 1 -(1 -(p n + q n )) N
We now set N = 2 n . A simple calculation shows that the sequence ((1-(p n +q n )) 2 n ) n∈N converges to 0 as n goes to infinity. Furthermore, if x > 1 2 then 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 ((ba n ) 2 n • b) = 1.
This example witnesses two surprising 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 ((ba n ) 2 n •b) n∈N witnessing the value 1 involves two convergence speeds: indeed, the words a n b are repeated an exponential number of times, namely 2 n . One can show that repeating only n times does not lead to words accepted with arbitrarily high probability.

1.3. Recurrent states and idempotent words. We fix A a probabilistic automaton, and define two main notions: recurrent states and idempotent words.

Definition 1.4 (Induced Markov chain). Let u be a finite word, it induces a Markov chain M A,u whose state space is Q and transition matrix M A,u is defined by:

M A,u (s, t) = P A (s u -→ t).
We rely on the classical notion of recurrent states in Markov chains.

Definition 1.5 (Recurrent state). A state s is u-recurrent if it is recurrent in M A,u .
A finite word u is idempotent if reading once or twice the word u does not change qualitatively the transition probabilities.

Definition 1.6 (Idempotent word). A Markov chain is idempotent if its transition matrix M satisfies that for all states s, t:

M (s, t) > 0 ⇐⇒ M 2 (s, t) > 0. A finite word u is idempotent if M A,u is idempotent.
In the case of idempotent words, recurrence of a state is easily characterized, relying on simple graph-theoretical arguments: Lemma 1.7. Let u be an idempotent word. A state s is u-recurrent if and only if for all states t we have:

M A,u (s, t) > 0 =⇒ M A,u (t, s) > 0.
2. An (incomplete) algorithm for the value 1 problem

In this section, we present an algebraic algorithm for the value 1 problem, called the Markov monoid algorithm. Since the problem is undecidable, this algorithm does not solve the problem on all instances; we will show that it is correct, i.e. if it answers that an automaton has value 1, then the automaton does have value 1, but not complete, i.e. the converse does not hold. In the next section, we shall show that this algorithm is complete for the class of leaktight automata.

2.1. The Markov monoid algorithm. Our algorithm for the value 1 problem computes iteratively a set G of directed graphs called limit-words. Each limit-word is meant to represent the asymptotic effect of a sequence of input words, and some particular limitwords can witness that the automaton has value 1.

Definition 2.1 (Limit-word). A limit-word is a function u : Q 2 → {0, 1}, such that for all states s, there exists a state t such that u(s, t) = 1.

In proofs and examples, we will adopt either of the two equivalent views for limit-words: graphs over the set Q or square matrices over Q × Q.

We now explain the algorithm in detail. For the remainder of this section, we fix A a probabilistic automaton. Initially, G only contains those limit-words a that are induced by input letters a ∈ A : ∀s, t ∈ Q, (a(s, t) = 1 ⇐⇒ P A (s a -→ t) > 0), plus the limit-word 1 which is induced by the empty word:

∀s, t ∈ Q, (1(s, t) = 1 ⇐⇒ s = t).
The algorithm repeatedly adds new limit-words to G. There are two ways for that: concatenating two limit-words or iterating an idempotent limit-word.

ALGORITHM 1: The Markov monoid algorithm.

Data: A probabilistic automaton. G ← {a | a ∈ A} ∪ {1}. repeat if there is u, v ∈ G such that u • v / ∈ G then add u • v to G end if there is u ∈ G such that u is idempotent and u ♯ /
∈ G then add u ♯ to G end until there is nothing to add ; if there is a value 1 witness in G then return true; else return false; end Concatenation of two limit-words The concatenation of two limit-words u and v is the limit-word u • v such that:

(u • v)(s, t) = 1 ⇐⇒ ∃q ∈ Q, u(s, q) = 1 and v(q, t) = 1.
In other words, concatenation corresponds to the multiplication of matrices with coefficients in the boolean semiring ({0, 1}, ∨, ∧). Intuitively, the concatenation of two limit-words corresponds to the concatenation of two sequences (u n ) n∈N and (v n ) n∈N of input words into the sequence (u n • v n ) n∈N .

We say that a limit-word u is idempotent if u•u = u. The following lemma gives simple properties of idempotent limit-words.

Lemma 2.2. For all limit-words u:

• the limit-word u |Q|! is idempotent,

• if u is idempotent, then for all states r ∈ Q, there exists a state r ′ ∈ Q such that u(r, r ′ ) = 1 and r ′ is u-recurrent.

The proof is omitted and relies on simple graph-theoretical arguments.

Iteration of an idempotent limit-word The iteration u ♯ of a limit-word u is only defined when u is idempotent. It relies on the notion of u-recurrent state.

Definition 2.3 (u-recurrence). Let u be an idempotent limit-word. A state s is u-recurrent if for all states t, we have:

u(s, t) = 1 =⇒ u(t, s) = 1.
Note that this echoes Lemma 1.7. The iterated limit-word u ♯ removes from u any edge that does not lead to a recurrent state:

u ♯ (s, t) = 1 ⇐⇒ u(s, t) = 1 and t is u-recurrent.
Intuitively, if a limit-word u represents a sequence (u n ) n∈N then its iteration u ♯ represents the sequence u

f (n) n n∈N
for some increasing function f : N → N.

2.2. The Markov monoid and value 1 witnesses. The set of limit-words G computed by Algorithm 1 is called the Markov monoid.

Definition 2.4 (Markov monoid). The Markov monoid associated with A is the smallest set of limit-words containing {a | a ∈ A}∪{1} and closed under concatenation and iteration.

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

Definition 2.5 (Reification). A sequence (u n ) n∈N of words reifies a limit-word u if for all states s, t, (P A (s un -→ t)) n∈N converges and:

u(s, t) = 1 ⇐⇒ lim n P A (s un -→ t) > 0.
(2.1)

Note that if (u n ) n∈N reifies u, then any subsequence of (u n ) n∈N also does. We will use this simple observation several times. Definition 2.6 (Consistency). A set of limit-words G is consistent with A if for every limit-word u ∈ G, there exists a sequence of input words (u n ) n∈N which reifies u. Definition 2.7 (Completeness). A set of limit-words G is complete for A if for each sequence of input words (u n ) n∈N , there exists u ∈ G such that for all states s, t ∈ Q:

lim sup n P A (s un -→ t) = 0 =⇒ u(s, t) = 0.
(2.2)

Limit-words are useful to decide the value 1 problem because some of these are witnesses that the automaton has value 1.

Definition 2.8 (Value 1 witness).

A value 1 witness is a limit-word u such that for all states t: u(q 0 , t) = 1 =⇒ t ∈ F, (2.3) where q 0 is the initial state of the automaton.

Thanks to value 1 witnesses, the answer to the value 1 problem can be read in a consistent and complete set of limit-words: Lemma 2.9 (A criterion for value 1). If G is consistent with A and complete for A, then A has value 1 if and only if G contains a value 1 witness.

Specifically:

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

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

Proof. We prove the first item. Assume that G is consistent with A and contains a value 1 witness u. Since G is consistent, there exists a sequence (u n ) n∈N reifying u. It follows from (2.1) and (2.3) that for t / ∈ F , we have lim n P A (q 0 un -→ t) = 0. Thus lim n P A (u n ) = t∈F lim n P A (q 0 un -→ t) = 1, so A has value 1. We now prove the second item. Assume that G is complete for A and that A has value 1. Then there exists a sequence of words (u n ) n∈N such that lim n P A (u n ) = 1, i.e. lim n t∈F P A (q 0 un -→ t) = 1. Since for all n ∈ N, we have q∈Q P A (q 0 un -→ q) = 1, then for all t / ∈ F , lim sup n P A (q 0 un -→ t) = 0. Since G is complete, there exists a limit-word u such that (2.2) holds. Then u is a value 1 witness: let t ∈ Q such that u(q 0 , t) = 1, then according to (2.2), lim sup n P A (q 0 un -→ t) > 0, hence t ∈ F .

Correctness of the Markov monoid algorithm.

Theorem 2.10. The Markov monoid associated with A is consistent.

This implies that if the Markov monoid algorithm outputs "true", then for sure the input automaton has value 1. This positive result holds for every automaton (leaktight or not).

To prove Theorem 2.10, recall that the Markov monoid is the smallest set of limitwords containing {a | a ∈ A} ∪ {1} and closed under concatenation and iteration, hence it suffices to prove that the initial elements form a consistent set, and the closure under the two operations.

First, a is reified by the constant sequence (a) n∈N , and 1 by the constant sequence (ε) n∈N . We state the closure under the two operations in the following proposition: Proposition 2.11. Let (u n ) n∈N and (v n ) n∈N be two sequences that reify the limit-words u and v respectively. Then:

(1) the sequence of words

(u n • v n ) n∈N reifies u • v, (2)
if u is idempotent, then there exists an increasing function f : N → N such that for all increasing functions g :

N → N satisfying g ≥ f , the sequence u n g(n) n∈N reifies the limit-word u ♯ .
The statement about iteration is stronger than required: the existence of f such that (u n f (n) ) n∈N reifying the limit-word u ♯ is enough to prove Theorem 2.10. However, we will use this stronger result later on (in Section 5.4).

Proof.

(1) Let w n = u n • v n . Then (w n ) n∈N reifies u • v, since:

P A (s wn --→ t) = r∈Q P A (s un -→ r) • P A (r vn -→ t).
(2) Consider the Markov chain M with state space Q and transition matrix M defined by M (s, t) = lim n P A (s un -→ t). Since (u n ) n∈N reifies u, we have u(s, t) = 1 if and only if M (s, t) > 0. First observe that since u is idempotent, the Markov chain M is aperiodic. According to standard results about finite Markov chains, this implies that the sequence of matrices (M k ) k∈N has a limit which we denote by M ∞ , satisfying the following:

∀s, t ∈ Q, M ∞ (s, t) > 0 =⇒ t is recurrent in M.
(2.4)

By definition the sequence of matrices (M A,un ) n∈N converges to M . Since the matrix product operation is continuous, for every

k ∈ N, M k A,un n∈N converges to M k . So for every k ≥ 1, there exists N k ∈ N such that for all p ≥ N k , ||M k -M k A,up || ∞ ≤ 1 k . We define f : N → N by induction, so that f (k) is the maximum of f (k -1) + 1 and of N k , ensuring that f is increasing. Then for any increasing function g : N → N satisfying g ≥ f , the sequence of matrices M n A,u g(n) n∈N converges to M ∞ . We prove that u n g(n) n∈N reifies u ♯ : u ♯ (s, t) = 1 ⇐⇒ u(s, t) = 1 and t is u-recurrent ⇐⇒ M (s, t) > 0 and t is recurrent in M ⇐⇒ M ∞ (s, t) > 0 ⇐⇒ lim n P A (s u n g(n) ---→ t) > 0,
where the first equivalence is by definition of the iteration, the second holds because (u n ) n∈N reifies u, the third by definition of M ∞ , and the fourth because

M A,u n g(n) n∈N converges to M ∞ .
This concludes the proof.

Note that completeness is not true in general; for instance, one can show that the Markov monoid of the automaton represented in figure 1 is not complete. The next section gives a sufficient condition for completeness: the leaktight property.

Decidability of the value 1 problem for leaktight automata

In this section we establish our main result:

Theorem 3.1. The value 1 problem is decidable for leaktight automata.

The definition of leaktight automata is given in the next subsection. For now (in this section), we are only interested in decidability issues; we will actually prove in Section 4 that the value 1 problem is PSPACE-complete for leaktight automata.

Note that as observed in the literature [BBG12, CSV13, Fij14], the value 1 problem for probabilistic automata over finite words is equivalent to the emptiness problem for probabilistic Büchi automata with positive semantics, hence we obtain the following corollary:

Corollary 3.2. The emptiness problem is decidable for probabilistic Büchi leaktight automata with positive semantics.

The following theorem proves that the Markov monoid of a leaktight automaton is complete; since it is always consistent, by Lemma 2.9, the Markov monoid algorithm solves the value 1 problem for leaktight automata.

Theorem 3.3. If a probabilistic automaton is leaktight then its Markov monoid is complete.

The remainder of this section is devoted to the proof of Theorem 3.3. We first define the leaktight property, and extend the Markov monoid. This extended version allows to state an algebraic characterization of the leaktight property. Then, the technical core of the proof relies on a subtle algebraic argument based on the existence of ♯-factorization trees of bounded height [START_REF] Simon | Factorization forests of finite height[END_REF][START_REF] Simon | On semigroups of matrices over the tropical semiring[END_REF][START_REF] Colcombet | The theory of stabilisation monoids and regular cost functions[END_REF][START_REF] Toruńczyk | Languages of profinite words and the limitedness problem[END_REF].

3.1. Leaks. The undecidability of the value 1 problem comes from the necessity to compare parallel convergence rates in order to track down vanishing probabilities. Comparing two convergence rates may require to compare the decimals of the rates up to an arbitrary precision, which in turn can encode a Post correspondence problem, hence the undecidability.

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.

L1 L2 0 b a b a a, b a a n • b L1 L2 0 ε Figure 2: (a n • b) n∈N is a leak from L 1 to L 2 .
Such leaks occur in the automaton depicted in the left hand side of figure 2 with the input sequence (a n b) n∈N . As n grows large, the probability to reach L 2 from L 1 while reading the input word a n b vanishes, thus the sets {L 1 } and {L 2 } 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 2 shows the asymptotic behaviour of reading (a n b) n∈N . Since the automaton in figure 1 contains two symmetric parts identical to figure 2, 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.

An automaton without leak is called a leaktight automaton. In this section we prove that the value 1 problem is decidable when restricted to the subclass of leaktight automata.

The formal definition of a leak is as follows:

Definition 3.4 (Leak). Let (u n ) n∈N be a sequence of idempotent words. Assume that the sequence of matrices P A (u n ) converges to a limit M , that this limit is idempotent and denote M the assocaited Markov chain. The sequence (u n ) n∈N is a leak if there exist r, q ∈ Q such that the following three conditions hold:

(1) r and q are recurrent in M, (2) lim n P A (r un -→ q) = 0, (3) for all n ∈ N, P A (r un -→ q) > 0.

Definition 3.5 (Leaktight automata). A probabilistic automaton is leaktight if it has no leak.

Several examples of leaktight automata are given in Section 5.

3.2.

The extended Markov monoid. The existence of leaks can be decided by a slight extension of the Markov monoid algorithm which keeps track of strictly positive transition probabilities.

Definition 3.6 (Extended limit-word). An extended limit-word is a couple (u, u + ) of two limit-words, such that for all s, t ∈ Q, we have u(s, t) = 1 =⇒ u + (s, t) = 1.

As for limit-words, extended limit-words can be seen either as graphs over the set Q, or couples of square matrices over Q × Q. Such a graph has two different kind of edges: an edge (s, t) is "normal" if u(s, t) = 1, and is a +-edge if u(s, t) = 0 but u + (s, t) = 1.

We define the concatenation and iteration operations for extended limit-words. The concatenation of two extended limit-words (u, u + ) and (v, v + ) is the component-wise concatenation, i.e. (u • v, u + • v + ). The iteration of an extended limit-word (u, u + ) is only defined when it is idempotent (i.e. component-wise idempotent), by (u, u + ) ♯ = (u ♯ , u + ). Definition 3.7 (Extended Markov monoid). The extended Markov monoid is the smallest set of extended limit-words containing {(a, a) | a ∈ A} ∪ {(1, 1)} and closed under concatenation and iteration.

Note that if (u, u + ) is in the extended Markov monoid, then u is in the Markov monoid. The essential difference between the Markov monoid and its extended version is that the extension keeps track of those edges that are deleted by successive iteration operations. This serves two purposes: first, to characterize the leaktight property in algebraic terms, and second, to prove Theorem 3.3.

We state a consistency result for the extended Markov monoid, extending Theorem 2.10. The proofs of both these results are similar and given only once.

Lemma 3.8. For each (u, u + ) in the extended Markov monoid, there exists a sequence (u n ) n∈N such that for all states s, t ∈ Q, (P A (s un -→ t)) n∈N converges and:

u(s, t) = 1 ⇐⇒ lim n P A (s un -→ t) > 0, (3.1) for all n ∈ N, u + (s, t) = 1 ⇐⇒ P A (s un -→ t) > 0 . (3.2) 3.3. Leak witnesses.
Definition 3.9 (Leak witness). An idempotent extended limit-word (u, u + ) is a leak witness if there exist r, q ∈ Q such that the following three conditions hold:

(1) r and q are u-recurrent, (2) u(r, q) = 0, (3) u + (r, q) = 1.

Lemma 3.10. If a probabilistic automaton is leaktight, then its extended Markov monoid does not contain any leak witness.

Proof. Suppose that there is a leak witness (u, u + ) in the extended Markov monoid: u and u + are idempotent and there exists r, q ∈ Q such that r and q are u-recurrent, u(r, q) = 0 and u + (r, q) = 1. We prove that there exists a leak. Thanks to Lemma 3.8, there exists a sequence (u n ) n∈N satisfying (3.1) and (3.2). Note that since u + is idempotent, (3.2) implies that for all n ∈ N, u n is idempotent.

Consider the Markov chain M with state space Q and transition matrix M defined by M (s, t) = lim n P A (s un -→ t). M is idempotent since u is idempotent and thanks to (3.1). We show that (u n ) n∈N is a leak. There are three conditions to be met. First, r and q are recurrent in M: this follows from (3.1) and the fact that r and q are u-recurrent. Second, lim n P A (r un -→ q) = 0: this follows from (3.1) and the fact that u(r, q) = 0. Third, for all n ∈ N, P A (r un -→ q) > 0: this follows from (3.2) and the fact that u + (r, q) = 1.

As we will show in the next section, the converse of Lemma 3.10 is also true, which gives an algebraic characterization of the leaktight property using the extended Markov monoid. However, the proof of the converse implication is more involved and requires the lower bound lemma (Lemma 3.15), which is the object of the next subsection.

3.4. Stabilization monoids and ♯-factorization trees. We now introduce the technical material required to state and prove the lower bound lemma. The key notions here are stabilization monoids and ♯-factorization trees.

Factorization trees for monoids have been introduced by Simon [START_REF] Simon | Factorization forests of finite height[END_REF]. Roughly speaking, Simon's factorization theorem states that given a morphism φ : A * → M from the set of finite words over A to a finite monoid M , the following holds: for all words u, the computation of φ(u) can be factorized 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 an iteration operation ♯ for monoids over the tropical semiring (N ∪ {∞}, min, +). Then Kirsten extended this technique to desert automata and the nested distance desert automata [START_REF] Daniel | Distance desert automata and the star height problem[END_REF]. After him, Colcombet generalized this approach by defining stabilization monoids [START_REF] Colcombet | The theory of stabilisation monoids and regular cost functions[END_REF], which are monoids equipped with an iteration operation, and proved the existence of ♯-factorization trees of bounded depth. The formal definition is as follows:

Definition 3.11 (Stabilization monoid). A stabilization monoid (M, •, ♯) is a finite monoid (M, •) equipped with an iteration operation ♯ : E(M ) → E(M )
, where E(M ) is the set of idempotents of M , such that:

(a • b) ♯ • a = a • (b • a) ♯ for a • b ∈ E(M ) and b • a ∈ E(M ), (3.3) (e ♯ ) ♯ = e ♯ for e ∈ E(M ), (3.4) e ♯ • e = e ♯ for e ∈ E(M ). (3.5)
Lemma 3.12. The extended Markov monoid is a stabilization monoid.

Proof. To start with, the extended Markov monoid is a monoid for the concatenation: 1 is the neutral element, and the concatenation is associative. Now, let us prove the three properties required for the iteration operation ♯.

Proof of (3.3). Let (u, u + ), (v, v + ) such that (u • v, u + • v + ) and (v • u, v + • u + ) are idempotent. By definition ((u, u + ) • (v, v + )) ♯ •(u, u + ) is equal to (u • v) ♯ • u, u + • v + • u + , and (u, u + ) • ((v, v + ) • (u, u + )) ♯ to u • (v • u) ♯ , u + • v + • u + . Let s, t ∈ Q, we have the following equivalence: (u • v) ♯ • u (s, t) = 1 if and only if: there exists r, q ∈ Q, u(s, r) = 1 ∧ v(r, q) = 1 ∧ u(q, t) = 1 ∧ q is (u • v)-recurrent, (3.6) and similarly, u • (v • u) ♯ (s, t) = 1 if and only if: there exists r, q ∈ Q, u(s, r) = 1 ∧ v(r, q) = 1 ∧ u(q, t) = 1 ∧ t is (v • u)-recurrent. (3.7)
We show that (3.6) and (3.7) are equivalent. Assume (3.6), and prove that t is (v and (3.7) is proved. Conversely, assume (3.7), and prove that q is (u • v)recurrent. Note that from v(r, q) = 1, u(q, t) = 1 and the fact that Proof of (3.4). This boils down to proving (u ♯ ) ♯ = u ♯ . This is clear from the definition of u ♯ , since the notions of u-recurrence and u ♯ -recurrence coincide.

• u)- recurrent. Let p ∈ Q such that (v • u)(t, p) = 1. Since v is a limit-word, there exists ℓ ∈ Q such that v(p, ℓ) = 1. Observe that u(q, t) = 1, (v • u)(t, p) = 1 and v(p, ℓ) = 1, so (u • v) 2 (q, ℓ) = 1. As u • v is idempotent, this implies (u • v)(q, ℓ) = 1. Since q is (u • v)- recurrent, we have (u • v)(ℓ, q) = 1. Altogether, v(p, ℓ) = 1, (u • v)(ℓ, q) = 1 and u(q, t) = 1 imply that (v • u) 2 (p, t) = 1. As v • u is idempotent, this implies (v • u)(p, t) = 1, so t is (v • u)-recurrent,
t is (v • u)-recurrent, we obtain that (v • u)(t, r) = 1. Let p ∈ Q such that (u • v)(q, p) = 1. Since u is a limit-word, there exists ℓ ∈ Q such that u(p, ℓ) = 1. Observe that v(r, q) = 1, (u • v)(q, p) = 1 and u(p, ℓ) = 1, so (v • u) 2 (r, ℓ) = 1, and with (v • u)(t, r) = 1 this implies (v • u) 3 (t, ℓ) = 1. As v • u is idempotent, this implies (v • u)(t, ℓ) = 1. Since t is (v • u)-recurrent, we have (v • u)(ℓ, t) = 1. Altogether, u(p, ℓ) = 1, (v • u)(ℓ, t) = 1, (v • u)(t, r) = 1 and v(r, q) = 1 imply that (u • v) 3 (p, q) = 1. As u • v is idempotent, this implies (u • v)(p, q) = 1, so q is (u • v)-recurrent,
Proof of (3.5). This boils down to proving u ♯ • u = u ♯ . It follows from the observation that if r ∈ Q is u-recurrent and u(r, t) = 1, then t is u-recurrent (under the assumption that u is idempotent). Definition 3.13. Let A be a finite alphabet, (M, •, ♯) a stabilization monoid and φ : A * → M a morphism into the submonoid (M, •). A ♯-factorization tree of a word u ∈ A * is a finite unranked ordered tree, whose nodes have labels in A * × M and such that:

i) the root is labelled by (u, u), for some u ∈ M , ii) every internal node with two children (called concatenation nodes) labelled by (u 1 , u 1 ) and (u 2 , u 2 ) is labelled by (u 1 • u 2 , u 1 • u 2 ), iii) every internal node with three or more children (called iteration nodes) is labelled by (u 1 . . . u n , e ♯ ) for some e ∈ E(M ), and its children are labelled by (u 1 , e), . . . , (u n , e). iv) every leaf is labelled by (a, a) where a is a letter, or (ε, 1).

Note that in a factorization tree, the second label is not always the image of the first component under φ; indeed, it is an element of the stabilization monoid (M, •, ♯) whereas the image of a finite word under φ is an element of the submonoid (M, •). However, the projection of second label into this submonoid (which consists in ignoring the operation ♯) 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 generalized 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 3.14. Let A be a finite alphabet, (M, •, ♯) a stabilization monoid and φ : A * → M a morphism into the submonoid (M, •). Every word u ∈ A * has a ♯-factorization tree whose depth is less than 3 • |M |.

3.5. The lower bound lemma. We are ready to state and prove the lower bound lemma, which is the central argument in the proof of completeness of leaktight Markov monoids.

Lemma 3.15 (Lower bound lemma). Let A be a probabilistic automaton whose extended Markov monoid contains no leak witness. Let p min the smallest non-zero transition probability of A. Then for all words u ∈ A * , there exists (u, u + ) in the extended Markov monoid such that, for all states s, t:

u + (s, t) = 1 ⇐⇒ P A (s u -→ t) > 0, (3.8) u(s, t) = 1 =⇒ P A (s u -→ t) ≥ p 2 3 |Q| 2 +1
min .

(3.9)

Proof. Consider a finite word u ∈ A * ; by Theorem 3.14 applied to the extended Markov monoid G + associated with A (which is a stabilization monoid thanks to Lemma 3.12) and the morphism φ : A → M defined by φ(a) = (a, a), there exists a ♯-factorization tree of depth at most 3 • |G + |, whose root is labelled by (u, (u, u + )) for some extended limit-word (u, u + ).

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 (u, (u, u + )) of this tree at depth h, for all states s, t:

u + (s, t) = 1 ⇐⇒ P A (s u -→ t) > 0, (3.10) u(s, t) = 1 =⇒ P A (s u -→ t) ≥ p 2 h min . (3.11)
The case h = 0 is for leaves. Here, either u is a letter a and u = u + = a, or u is the empty word ε and u = u + = 1. Then both (3.10) and (3.11) hold.

Assume h > 0, there are two cases.

First case: a concatenation node labelled by (u, (u, u + )) with two children labelled by (u 1 , (u 1 , u +,1 )) and (u 2 , (u 2 , u +,2 )). By definition

u = u 1 • u 2 , u = u 1 • u 2 and u + = u +,1 • u +,2 .
We first prove that (3.10) holds. Indeed, for s, t ∈ Q, u + (s, t) = 1 if and only if there exists r ∈ Q such that u +,1 (s, r) = 1 and u +,2 (r, t) = 1. On the other side, since:

P A (s u -→ t) = r∈Q P A (s u 1 -→ r) • P A (r u 2 -→ t), then P A (s u -→ t) > 0 if and only if there exists r ∈ Q such that P A (s u 1 -→ r) • P A (r u 2 -→ t) > 0, which is equivalent to P A (s u 1 -→ r) > 0 and P A (r u 2 -→ t) > 0.
We conclude with the induction hypothesis.

Now we prove that (3.11) holds. Let s, t ∈ Q such that u(s, t) = 1. Then there exists r ∈ Q such that u 1 (s, r) = 1 and u 2 (r, t) = 1. So:

P A (s u -→ t) ≥ P A (s u 1 -→ r) • P A (r u 2 -→ t) ≥ p 2 h min • p 2 h min = p 2 h+1
min , where the second inequality is by induction hypothesis. This completes the proof of (3.11).

Second case: an iteration node labelled by (u, (u ♯ , u + )) with k sons labelled by (u 1 , (u, u + )), . . . , (u k , (u, u + )). By definition, u = u 1 • • • u k , and (u, u + ) is idempotent.

The proof that (3.10) holds is similar to the concatenation node case. Now we prove that (3.11) holds. Let s, t ∈ Q such that u ♯ (s, t) = 1. Since k ≥ 3:

P A (s u -→ t) ≥ P A (s u 1 -→ t) • q∈Q P A (t u 2 •••u k-1 ------→ q) • P A (q u k -→ t).
(3.12)

To establish (3.11) we prove that:

P A (s u 1 -→ t) ≥ p 2 h min , (3.13)
for all q ∈ Q, P A (t

u 2 •••u k-1 ------→ q) > 0 =⇒ P A (q u k -→ t) ≥ p 2 h min . (3.14)
We prove (3.13). Since u ♯ (s, t) = 1, by definition u(s, t) = 1 and t is u-recurrent. The induction hypothesis for the node (u 1 , (u, u + )) implies that P A (s

u 1 -→ t) ≥ p 2 h
min , i.e. (3.13). Now we prove (3.14). For that we use the hypothesis that (u, u + ) is not a leak witness. Let q ∈ Q such that P A (t

u 2 •••u k-1
------→ q) > 0. By induction hypothesis for each child, (3.10) implies that u k-2 + (t, q) = 1. Since u + is idempotent, u + (t, q) = 1. We argue that u(q, t) = 1. Let ℓ ∈ Q a u-recurrent state such that u(q, ℓ) = 1. Then u + (t, ℓ) = 1, and t, ℓ are urecurrent. Since (u, u + ) is not a leak witness, it follows that u(t, ℓ) = 1, which implies that u(ℓ, t) = 1 since t is u-recurrent. Together with u(q, ℓ) = 1, this implies u(q, t) = 1. Thus, by induction hypothesis and according to (3.11), P A (q

u k -→ t) ≥ p 2 h
min , so (3.14) holds. Now, putting (3.12), (3.13) and (3.14) altogether:

P A (s u -→ t) ≥ P A (s u 1 -→ t) • q∈Q P A (t u 2 •••u k-1 ------→ q) • P A (q u k -→ t) ≥ p 2 h min • q∈Q P A (t u 2 •••u k-1 ------→ q) • p 2 h min = p 2 h+1 min ,
where the last equality holds because q∈Q P A (t

u 2 •••u k-1
------→ q) = 1. This completes the proof of (3.11).

To conclude, note that G + has less than 3 |Q| 2 elements.

3.6. Completeness of the Markov monoid algorithm for leaktight automata. In this subsection we rely on the lower bound lemma (Lemma 3.15) to prove Theorem 3.3. Let A be a leaktight automaton. By Lemma 3.10, its extended Markov monoid does not contain any leak witness, hence Lemma 3.15 applies. We prove the completeness of the Markov monoid associated with A. Let (u n ) n∈N be a sequence of finite words. By Lemma 3.15, for each word u n there exists (u n , u +,n ) in the extended Markov monoid such that for all states s, t:

u n (s, t) = 1 =⇒ P A (s un -→ t) ≥ p 2 3 |Q| 2 +1 min .
Since the set of limit-words is finite, there exists N ∈ N such that {n ∈ N | u N = u n } is infinite. To complete the proof, we prove that u N satisfies, for all states s, t:

lim sup P A (s un -→ t) = 0 =⇒ u N (s, t) = 0.
Assume lim sup P A (s un -→ t) = 0, then lim sup P A (s un -→ t) < p 2 3 |Q| 2 +1 min for n sufficiently large. Since u N = u n for infinitely many n ∈ N, this implies u N (s, t) = 0, which completes the proof of Theorem 3.3.

Properties of leaktight automata

In this section, we extend the algorithm presented in Section 2, and investigate its running complexity. The extended algorithm has two features: first, it checks at the same time whether an automaton is leaktight and whether it contains a value 1 witness, second, it runs in polynomial space.

We present an algebraic characterization of the leaktight property based on the extended Markov monoid, allowing the extended algorithm to check the leaktight property. For the complexity, one needs a deeper understanding of the Markov monoid; in this section, we will show a linear bound on the ♯-height, allowing to compute the extended Markov monoid in polynomial space. As a corollary, we obtain that the value 1 problem for leaktight automata is PSPACE-complete. 4.1. Characterization of the leaktight property. In this subsection, we show the converse of Lemma 3.10, which implies the following theorem, characterizing the leaktight property in algebraic terms.

Theorem 4.1. An automaton A is leaktight if and only if its extended Markov monoid does not contain any leak witness.

Lemma 3.15 is instrumental in the proof of this lemma.

Proof. We prove that if the extended Markov monoid of an automaton A does not contain any leak witness, then A is leaktight. The converse was proved in Lemma 3.10.

Assume A has a leak (u n ) n∈N , we show that its extended Markov monoid contains a leak witness. Consider the Markov chain M with state space Q and transition matrix M defined by M (s, t) = lim n P A (s un -→ t). By assumption M is idempotent. By definition of a leak: r and q are recurrent in M, (4.1)

M (r, q) = 0, (4.2) for all n ∈ N, P A (r un -→ q) > 0. (4.3)
Assume towards contradiction that the extended Markov monoid does not contain any leak witness, then Lemma 3.15 applies. For each word u n , there exists (u n , u +,n ) in the extended Markov monoid such that for all states s, t:

u +,n (s, t) = 1 ⇐⇒ P A (s un -→ t) > 0, (4.4) u n (s, t) = 1 =⇒ P A (s un -→ t) ≥ p 2 3 |Q| 2 +1 min . (4.5)
Since the extended Markov monoid is finite, there exists N ∈ N such that for infinitely many n ∈ N, we have (u N , u +,N ) = (u n , u +,n ). Note that since each u n is idempotent, (4.4) implies that each u +,n is idempotent as well.

Let (v, v + ) = (u N , u +,N ) |Q|! . The power |Q|! ensures that u |Q|! N is idempotent, by Lemma 2.2. Since u +,N is idempotent, v + = u +,N . Also, since v is idempotent, there exists r ′ and q ′ which are v-recurrent, such that v(r, r ′ ) = 1 and v(q, q ′ ) = 1, again thanks to Lemma 2.2. Now, we prove that (v, v + ) is a leak witness:

r ′ and q ′ are v-recurrent, (4.6) v(r ′ , q ′ ) = 0, (4.7) v + (r ′ , q ′ ) = 1. (4.8) Let η = p 2 3 |Q| 2 +1
min and K = |Q|!. Observe that for all states s, t, we have v(s, t) = 1 =⇒ M (s, t) > 0:

v(s, t) = 1 =⇒ u K N (s, t) = 1 (by definition of v) =⇒ u K n (s, t) = 1 for infinitely many n (by definition of N ) =⇒ P A (s u K n --→ t) ≥ η K for infinitely many n (by (4.5)) =⇒ lim n P A (s u K n --→ t) ≥ η K =⇒ M K (s, t) > 0 (by definition of M ) =⇒ M (s, t) > 0 (since M is idempotent).
First, (4.6) is by definition of r ′ and q ′ . We prove (4.7). Towards contradiction, assume that v(r ′ , q ′ ) = 1. Then M (r ′ , q ′ ) > 0, so together with M (r, r ′ ) > 0 (which follows from v(r, r ′ ) = 1) this implies M 2 (r, q ′ ) > 0, so M (r, q ′ ) > 0 as M is idempotent. Since M (q, q ′ ) > 0 (which follows from v(q, q ′ ) = 1) and q is recurrent in M , we have M (q ′ , q) > 0. This implies M 2 (r, q) > 0, and M (r, q) > 0 because M is idempotent, which contradicts (4.2).

We prove (4.8). Thanks to (4.3) and (4.4), we have u +,N (r, q) = 1, i.e. v + (r, q) = 1. Since M (r, r ′ ) > 0 and r is recurrent in M , we have M (r ′ , r) > 0, so (4.4) implies that u +,N (r ′ , r) = 1, i.e. v + (r ′ , r) = 1. Similarly, M (q, q ′ ) > 0, so (4.4) implies that u +,N (q, q ′ ) = 1, i.e. v + (q, q ′ ) = 1. The three equalities v + (r ′ , r) = 1, v + (r, q) = 1 and v + (q, q ′ ) = 1 imply v 3 + (r ′ , q ′ ) = 1, and since v + is idempotent v + (r ′ , q ′ ) = 1. It follows that (v, v + ) is a leak witness, which completes the proof.

The immediate corollary of Theorem 4.1 is that checking whether an automaton is leaktight can be done by computing the extended Markov monoid and looking for leak witnesses, hence it is decidable. 4.2. The extended Markov monoid algorithm. Algorithm 2 computes the extended Markov monoid, and looks for value 1 witnesses, which in the extended Markov monoid is an extended limit-word (u, u + ) such that u is a value 1 witness (in the Markov monoid). If there is a value 1 witness, then the automaton has value 1, even if it is not leaktight, thanks to Theorem 2.10. Otherwise, the algorithm looks for a leak witness; if there is no leak witness, then the automaton is leaktight thanks to Theorem 4.1, and it does not have value 1 thanks to Theorem 3.3. In case there is a leak witness, the automaton is not leaktight, and nothing can be said.

ALGORITHM 2: The extended Markov monoid algorithm. Data: A probabilistic automaton.

G + ← {(a, a) | a ∈ A} ∪ {(1, 1)}. repeat if there is (u, u + ), (v, v + ) ∈ G + such that (u • v, u + • v + ) / ∈ G + then add (u • v, u + • v + ) to G + end if there is (u, u + ) ∈ G + such that (u, u + ) is idempotent and (u ♯ , u + ) / ∈ G + then add (u ♯ , u + ) to G + end
until there is nothing to add ; if there is a value 1 witness in G + then return true; else if there is no leak witness in G + then return false; else return fail: the automaton is not leaktight; end end 4.3. Parallel composition and PSPACE-hardness. The objective of this subsection is to prove 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. Proposition 4.2. Deterministic automata are leaktight.

Proof. For all limit-words u ∈ {a | a ∈ A} ∪ {1}, for all states s, there exists a unique state t such that u(s, t) = 1. In particular, each recurrence class is formed of only one state with a self-loop. This property is preserved by concatenation, and implies that the iteration operation is trivial, i.e. u ♯ = u. Consequently, for all extended limit-words (u, u + ) in the extended Markov monoid, we have u = u + , which implies that there are no leak witnesses.

Definition 4.3 (Parallel composition). Consider two probabilistic automata, denoted

A = (Q A , q A 0 , ∆ A , F A ) and B = (Q B , q B 0 , ∆ B , F B ).
We assume that Q A and Q B are disjoint. The parallel composition of A and B is:

A || B = (Q A ⊎ Q B , δ 0 , ∆ , F A ∪ F B ),
where δ 0 = 1 2 • q A 0 + 1 2 • q B 0 , and:

∆(q, a) = ∆ A (q, a) if q ∈ Q A , ∆ B (q, a) if q ∈ Q B .
By definition, for u ∈ A * , we have P A||B (u) = 1 2 • P A (u) + 1 2 • P B (u). Note that in this definition, we allowed an initial probability distribution rather than only one initial state. This could be avoided by adding a new initial state that leads to each previous initial state with probability half, but we do it here for technical convenience in the proof of the following proposition.

) ∈ G A||B + , if u(s, t) = 1, then either s, t ∈ Q A or s, t ∈ Q B ,
and similarly for u + . Relying on this, we map (u, u

+ ) ∈ G A||B + to ((u, u + )[A] , (u, u + )[B]
), where (u, u + )[A] is the restriction to A and similarly for B. An easy induction on (u, u + ) shows that this map is an embedding into G A + × G B + . Consequently, the extended Markov monoid of the parallel composition contains a leak witness if and only if one of the extended Markov monoid contains a leak witness. 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 4.5. 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 [START_REF] Kozen | Lower bounds for natural proof systems[END_REF].

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 Proposition 4.2 and Proposition 4.4. 4.4. Bounding the ♯-height in the 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 iterations, since each iteration adds a new extended limit-word in the monoid and there are at most 3 |Q| 2 different limit-words. This gives an EXPTIME upper bound.

A better complexity can be achieved by looking for a value 1 witness or a leak witness in a non-deterministic way. The algorithm guesses the witness by its decomposition into concatenations and iterations. The key observation, made by Kirsten [START_REF] Daniel | Distance desert automata and the star height problem[END_REF] in the context of distance desert automata, is that the ♯-height, that is the number of nested applications of the iteration operation, can be restricted to at most |Q|.

Note that when dealing with ♯-height, it suffices to consider limit-words instead of extended limit-words, as by definition the second component of an extended limit-word does not contain any ♯.

Formally, we define the ♯-hierarchy inside the Markov monoid as follows:

S 0 = {a | a ∈ A} ∪ {1} , S p+1 = S p ∪ {u ♯ | u ∈ E(S p )} ,
where T is the set of limit-words obtained as concatenation of limit-words in T .

Definition 4.6 (♯-height of a limit-word). The ♯-height of a limit-word u is the minimal p such that u ∈ S p .

Theorem 4.7. Every limit-word has ♯-height at most |Q|, i.e. the ♯-hierarchy collapses at level |Q|.

In the following, we adapt 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 Markov monoid, and to show the following:

• the quantity is bounded above by |Q|.

• the quantity strictly decreases when iterating an unstable limit-word (i.e. if u ♯ = u),

• the quantity does not increase when concatenating. Let u be an idempotent limit-word, we define ∼ u the relation on Q by s ∼ u t if u(s, t) = 1 and u(t, s) = 1. Clearly, ∼ u is symmetric, and since u is idempotent, ∼ u is transitive. If for some state s there exists a state t such that s ∼ u t, then s ∼ u s since u is idempotent. Consequently, the restriction of ∼ u to the set

Z u = {s ∈ Q | s ∼ u s}
is reflexive, i.e. ∼ u is an equivalence relation on Z u . From now on by equivalence class of ∼ u we mean an equivalence class of ∼ u on Z u . We denote by [s] u the equivalence class of s, and by Cl(u) the set of equivalence classes of ∼ u . The quantity associated with u is |Cl(u)|, the number of equivalence classes of ∼ u , that is the number of non-trivial connected components in the underlying graph of u. Note that |Cl(u)| ≤ |Q|.

Here are two useful observations. Lemma 4.8.

• Let u, v be two limit-words and s, t, r ∈ Q. Then (u • v)(s, t) ≥ u(s, r) • v(r, t).

• Let u be an idempotent limit-word and s, t ∈ Q. There exists r ∈ Q such that u(s, t) = u(s, r) • u(r, r) • u(r, t).

Proof. The first claim is clear and follows from the equality:

(u • v)(s, t) = r∈Q u(s, r) • v(r, t).
Consider now the second claim. For all states r ∈ Q, since u is idempotent we have:

u(s, t) = u 3 (s, t) = p,q∈Q u(s, p) • u(p, q) • u(q, t) ≥ u(s, r) • u(r, r) • u(r, t).
Since u is idempotent, we have u = u n+2 , so there exist s = r 0 , . . . , r n+2 = t such that u(s, t) = u(r 0 , r 1 ) • • • u(r n+1 , r n+2 ). By a counting argument, there exist i, j such that 1 ≤ i < j ≤ (n + 1) and r i = r j , denote it by r. We have:

u(s, r) = u i (s, r) ≥ u(r 0 , r 1 ) • • • u(r i-1 , r i ), u(r, r) = u j-i (r, r) ≥ u(r i , r i+1 ) • • • u(r j-1 , r j ), u(r, t) = u n+2-j (r, t) ≥ u(r j , r j+1 ) • • • u(r n+1 , r n+2 ). Hence, u(s, r) • u(r, r) • u(r, t) ≥ u(r 0 , r 1 ) • • • u(r n+1 , r n+2 ) = u(s, t)
, and the second claim follows.

a(t, p) • v(p, s) = 1, and b(s, t) = (v • b)(s, t) ≥ v(s, q) • b(q, t) = 1. To sum up, a(t, s) • v(s, s) • b(s, t) = 1, and hence, β([s] v ) = [t] u .
The following lemma wraps up the previous two lemma. For technical convenience, we set S -1 = ∅. Lemma 4.11. Let u be an idempotent limit-word and p ≥ 0.

If u ∈ S p \ S p-1 , then |Cl(u)| ≤ |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 u be an idempotent limit-word such that u ∈ S p+1 \ S p . By definition, The bound is almost tight, as shown in figure 3. The only value 1 witness of this automaton is ( automaton is leaktight, so the extended Markov monoid algorithm will find the value 1 witness and correctly answers that it has value 1.

u = v 1 • • • v k where for all i, either v i ∈ S p or v i = u ♯ i for u i ∈ S p and v i / ∈ S p . If for all i, v i ∈ S p , then u = v 1 • • • v k ∈ S p , which is a contradiction. Consequently, there exists i such that v i = u ♯ i for u i ∈ S p and v i / ∈ S p . Since u i ∈ S p and v i = u ♯ i / ∈ S p , we have u ♯ i = u i . Towards contradiction, assume u i ∈ S p-1 , then p ≥ 1, and this implies u ♯ i ∈ S p , which is a contradiction. Hence, u i ∈ S p \ S p-1 . By induction, we have |Cl(u i )| ≤ |Q| -p. Since u ♯ i = u i , by Lemma 4.9 we have |Cl(u ♯ i )| < |Cl(u i )|. Since u ≤ J u ♯ i ,
• • • ((a ♯ 0 a 1 ) ♯ a 2 ) ♯ a 3 ) ♯ • • • a n-1 ) ♯ , whose ♯-height is |Q| -2. Note that this 0 1 2 n -1 n ⊥ a 0 , 1 2 (a i ) i≥0 (a i ) i≤0 (a i ) i≤1 (a i ) i≤n-2 (a i ) i≥0 a 0 , 1 2 a 1 , 1 2 a 1 , 1 2 a 2 , 1 2 a 2 , 1 2 a n-1 , 1 2 a n-1 , 1 2 (a i ) i≥1 (a i ) i≥2 (a i ) i≥3 (a i ) i≥n . .

4.5.

Finding witnesses in the Markov monoid. In the subsection, we will prove the following complexity result.

Proposition 4.12. 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 3.3, checking whether a leaktight automaton has value 1 boils down to finding a value 1 witness in the Markov monoid. Similarly, following Theorem 4.1, checking whether an automaton is not leaktight boils down to finding a leak witness in the extended Markov monoid. Note that in both cases, checking whether a given limit-word or extended limit-word 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. For the sake of readability, we here only deal with the Markov monoid, but similar ideas apply to the extended Markov monoid.

We describe an algorithm to guess a witness in the Markov monoid. The key property given by Theorem 4.7 is that we can restrict ourselves to at most |Q| nested iteration operations.

As the corresponding property was proved by 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 limit-words, of depth at most 2 • |Q| + 1, as follows:

• a leaf is labelled either by a for a ∈ A or by 1,

• an internal node can be a concatenation node, then it is labelled by

u = v 1 • • • v k for k ≤ 2 |Q| 2
and has k children, labelled by v 1 , . . . , v k , • an internal node can be an iteration node, then it is labelled by u ♯ and has one child labelled u. 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 limit-word obtained by concatenating all the left siblings of this node. From a node, the algorithm guesses a limit-word, and whether it will be a leaf, a concatenation node or an iteration 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 concatenating 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 limit-words at most, so it runs in polynomial space.

Examples and subclasses of leaktight automata

In this section, we investigate further the class of leaktight automata, by giving examples of leaktight automata, exhibiting subclasses, and showing closure properties. In particular, we prove that hierarchical automata, ♯-acylic automata and simple automata are all strict subclasses of leaktight automata. (Actually, since ♯-acylic automata are already a subclass of simple automata, we do not consider them.) This implies that our decidability result extends the decidability results from [START_REF] Gimbert | Probabilistic automata on finite words: Decidable and undecidable problems[END_REF][START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF]. 4 is leaktight. As we shall see, it is not hierarchical, nor simple, hence it witnesses that leaktight automata are not subsumed by hierarchical or simple automata. Its extended Markov monoid is depicted on the righthand side. Each of the four directed graphs represents an extended limit-word (u, u + ): if u(s, t) = 1, then (s, t) is an edge, and if u(s, t) = 0 but u + (s, t) = 1, then (s, t) is marked with +.

Two basic examples. The automaton on figure

The initial state of the automaton is state 0, and the unique final state is state 1. This automaton has value 1 and this can be checked using the extended Markov monoid: the two value 1 witnesses are a ♯ and b • a ♯ . The automaton on figure 5 is leaktight. The initial state of the automaton is state 0, and the unique final state is state F . The Markov monoid has too many elements to be represented here. This automaton does not have value 1. 5.2. Some closure properties. In this subsection, we show some closure properties: synchronised product and composition with a deterministic transducer. As for Proposition 4.4, the automata constructions reflect in algebraic constructions, allowing to use the characterization with leak witnesses given by Theorem 4.1.

In this subsection, we will omit initial and final states, as we are only interested in preserving the leaktight property, which does not depend on it.

Definition 5.1 (Synchronised product). Let A = (Q A , ∆ A ) and B = (Q B , ∆ B ) be two probabilistic automata.

A synchronised product of A and B is:

A × B = (Q A × Q B , ∆),
where ∆(q, a) = (∆ A (q, a), ∆ B (q, a)).

Proposition 5.2. The leaktight property is stable by synchronized product.

Proof. The extended Markov monoid G A×B + of the synchronized product embeds into the direct product G A + × G B + of the extended Markov monoids of each automaton. Let (u, u + ) be an extended limit-word in G A×B + . Define u A (s, t) = 1 if there exists s ′ , t ′ ∈ Q B such that u((s, s ′ ), (t, t ′ )) = 1, and similarly for u +,A , u B and u +,B . We have the following equivalence:

u((s, s ′ ), (t, t ′ )) = 1 ⇐⇒ u A (s, t) = 1 ∧ u B (s ′ , t ′ ) = 1,
and similarly for u + .

Relying on this, we map (u, u + ) ∈ G A×B + to ((u A , u +,A ) , (u B , u +,B )). An easy induction shows that this map is an embedding into G A + × G B + . Consequently, the extended Markov monoid of the synchronised product contains a leak witness if and only if one of the extended Markov monoid contains a leak witness.

The last closure property we prove will be useful in the next section. Definition 5.3 (Composition with a deterministic transducer). Let A = (Q A , ∆ A ) be a probabilistic automaton, and M = (Q M , Q A , ∆ M ) a deterministic transducer over A, i.e.

∆ M : Q M × Q A → Q M .
The composition of A by M is:

A ⊗ M = (Q A × Q M , ∆),
where ∆(q, p, a) = (∆ A (q, a), ∆ M (p, q)).

Proposition 5.4. The leaktight property is stable by composition with a deterministic transducer.

Proof. Following the same reasoning as in 4.2, one can show that the extended Markov monoids for A and for A ⊗ M are isomorphic.

5.3. Leaktight automata strictly contain hierarchical automata. The class of hierarchical automata has been defined in [START_REF] Chadha | Power of randomization in automata on infinite strings[END_REF], where it was proved that they are recognize exactly the class of ω-regular languages. The states Q of a hierarchical automaton are sorted according to levels such that for each letter, at most one successor is at the same level and all others are at higher levels.

Formally, there exists a mapping rank : Q → N such that for all a ∈ A, for all states s, t such that P A (s a -→ t) > 0, we have rank(s) ≤ rank(t). Furthermore, if P A (s a -→ t) > 0 and P A (s a -→ t ′ ) > 0 but rank(s) = rank(t) = rank(t ′ ), then t = t ′ . Proposition 5.5. Every hierarchical automata is leaktight.

Proof. We prove by induction that for every extended limit-word (u, u + ) in the extended Markov monoid of a hierarchical automaton, for every states s, t, t ′ :

u + (s, t) = 1 =⇒ rank(s) ≤ rank(t),
(5.1)

u + (s, t) = 1 ∧ u + (s, t ′ ) = 1 ∧ rank(s) = rank(t) = rank(t ′ ) =⇒ t = t ′ , (5.2) u(s, t) = 1 =⇒ rank(s) ≤ rank(t), (5.3) u(s, t) = 1 ∧ u(s, t ′ ) = 1 ∧ rank(s) = rank(t) = rank(t ′ ) =⇒ t = t ′ .
(5.4)

Note that (5.1) and (5.2) imply (5.3) and (5.4), since u(s, t) = 1 implies u + (s, t) = 1. The key property following from (5.2) and (5.3) is that the recurrence classes of u and of u + are singletons. This is trivial for (1, 1). The case of (a, a) is the definition of hierarchical automata. The induction step for concatenation is routinely checked, and trivial for the iteration.

We now prove that the extended Markov monoid of a hierarchical automaton does not contain any leak witness. We prove a slightly stronger statement; for every extended limitword (u, u + ) in the extended Markov monoid of a hierarchical automaton, for all states q, r:

u + (r, q) = 1 ∧ r is u-recurrent =⇒ u(r, q) = 1.
(5.5) This is clear for (1, 1) and for (a, a). Concatenation. Let (u, u + ) and (v, v + ) be two extended limit-words satisfying (5.5). Consider two states r, q such that (u + • v + )(r, q) = 1 and r is (u • v)-recurrent.

Since r is (u•v)-recurrent, the recurrence class of r for (u•v) is r itself, so (u•v)(r, r) = 1 and (u • v)(r, p) = 1 implies p = r. Let t be a state such that u(r, t) = 1 and v(t, r) = 1. Thanks to (5.3), rank(t) = rank(r).

We argue that u(r, p) = 1 implies p = t. Indeed, let p be a state such that u(r, p) = 1. There exists a state p ′ such that v(p, p ′ ) = 1, so in particular (u • v)(r, p ′ ) = 1, so p ′ = r. By (5.3), rank(r) ≤ rank(p) ≤ rank(r), so they are equal. By (5.4), since u(r, t) = 1, u(r, p) = 1 and rank(r) = rank(t) = rank(p), we have p = t. It follows that the state t is u-recurrent: by Lemma 2.2, there exists a state p such that u(r, p) = 1 and p is u-recurrent. The above remark implies that p = t.

We argue that v(t, p) = 1 implies p = r. Indeed, let p be a state such that v(t, p) = 1. We have (u • v)(r, p) = 1, so p = r. It follows that the state r is v-recurrent: by Lemma 2.2, there exists a state p such that v(t, p) = 1 and p is u-recurrent. The above remark implies that p = r.

Since (u + • v + )(r, q) = 1, there exists s ∈ Q such that u + (r, s) = 1 and v + (s, q) = 1. By induction hypothesis for (u, u + ), since u + (r, s) = 1 and r is u-recurrent, we have u(r, s) = 1. 5.4.2. The presence of a leak implies the presence of a non-simplicity witness. Now we show that the presence of a leak witness implies the presence of a non-simplicity witness.

Proposition 5.14. If the extended Markov monoid of a probabilistic automaton contains a leak witness, then it also contains a non-simplicity witness.

In the following proof, we will make use of the notion of ♯-height for an extended limitword. The ♯-height of a limit-word was defined in Section 4.6, the ♯-height of an extended limit-word (u, u + ) is the ♯-height of u.

Proof. Let A be a probabilistic automaton whose extended Markov monoid contains a leak witness. Consider the subset C of extended limit-words (u, u + ) in the extended Markov monoid such that there exist states r, t satisfying:

(1

) (u, u + ) is idempotent, (2) r is u-recurrent, (3) u(r, t) = 0, (4) u + (r, t) = 1.
Note that C is non-empty since every leak witness is in C. Consider an element (z, z + ) in C of minimal ♯-height and let r, t ∈ Q such that r is z-recurrent, z(r, t) = 0 and z + (r, t) = 1. In particular, we have z = z + , so in any decomposition of (z, z + ) into concatenation and iteration there must be at least one iteration. Consequently, z = uv ♯ w for some u, v, w, and uvw has a strictly smaller ♯-height than z.

Let R be the z-recurrence class of r, and T the set of v-transient states. We argue that the following holds: there exist r ′ ∈ R and t ′ ∈ T such that uv(r ′ , t ′ ) = 1.

(5.11)

Assume towards contradiction that (5.11) does not hold, i.e. for all r ′ ∈ R and t ′ ∈ T , we have uv(r ′ , t ′ ) = 0, then we prove that (uvw, z + ) |G + |! is in C, contradicting the minimality of (z, z + ) as it has strictly smaller ♯-height.

First observe that for all states q we have uv(r ′ , q) = uv ♯ (r ′ , q), which implies that for all r ′ ∈ R and state q, we have: uvw(r ′ , q) = uv ♯ w(r ′ , q) = z(r ′ , q).

(5.12)

We check that (uvw, z + ) |G + |! is in C, with the states r, t as witnesses:

(1) (uvw, z + ) |G + |! is idempotent, this follows from Lemma 2.2.

(2) r is (uvw

) |G + |! -recurrent. Indeed, let q ∈ Q such that (uvw) |G + |! (r, q) = 1. It follows that (uv ♯ w) |G + |! (r, q) = 1, but (uv ♯ w) |G + |! = z |G + |! = z, so z(r, q) = 1.
Since r is zrecurrent, we have z(q, r) = 1 and q ∈ R, so (5.12) implies that z(q, r) = uvw(q, r), thus uvw(q, r) = 1. Also, z(r, r) = uvw(r, r), so uvw(r, r) = 1, and altogether (uvw

) |G + |! (q, r) = 1. (3) (uvw) |G + |! (r, t) = 0. Indeed, assume towards contradiction that (uvw) |G + |! (r, t) = 1.
Then there exist q 0 , q 1 , . . . , q |G + |! such that q 0 = r, for i ∈ {0, . . . , |G + |! -1} we have uvw(q i , q i+1 ) = 1 and q |G + |! = t. We prove by induction on i ∈ {0, . . . , |G + |!-1} that q i is in R and that z(q i , q i+1 ) = 1. Assume q i is in R, then by (5.12), uvw(q i , q i+1 ) = z(q i , q i+1 ), so z(q i , q i+1 ) = 1. But q i is in R, which is a recurrence class for z, so q i+1 is in R as well, concluding the induction. Thus, we have z |G + |! (r, t) = 1, and since z is idempotent z(r, t) = 1, a contradiction. (4) z |G + |! + (r, t) = 1. It follows from the fact the z + is idempotent, and that z + (r, t) = 1.

We reached a contradiction, since (uvw, z + ) |G + |! has a strictly smaller ♯-height than (z, z + ). It follows from (5.11) that (u, v, w) is a non-simplicity witness for the states r ′ and t ′ , concluding the proof.

The proof of Theorem 5.9 is now a simple combination of Proposition 5.11 and Proposition 5.14. The inclusion is strict: figure 4 provides an example of a leaktight automaton which is not simple.

Probabilistic ω-automata

In this section, we relate the value 1 problem for probabilistic automata over finite words and over infinite words, as introduced and studied in [START_REF] Baier | Probabilistic ω-automata[END_REF]. We state a general theorem, showing the equivalence of the value 1 problem for automata over finite words and the value 1 problem for automata over infinite words with the parity condition. This theorem allows to extend the decidability results from finite words to infinite ones.

For the definitions of probabilistic automata over infinite words, we refer to [START_REF] Baier | Probabilistic ω-automata[END_REF]. For the sake of readability, we introduce two notations in this section. First, we denote by P A,w (E) the probability of the measurable event E when reading the infinite word w on A. Second, we denote by P δ A (u) the probability that the finite word u is accepted by A with δ as initial distribution. Note that in our definition, probabilistic automata have a unique initial state; however here we need to deal with automata having general initial distributions, so we sometimes consider the more general tuples A = (Q, δ, ∆, F ) where δ is the initial probability distribution. Theorem 6.1. Let A = (Q, δ 0 , ∆, c) be a probabilistic parity automaton where c : Q → N is a priority function. Consider the deterministic transducer M over A, which keeps track of the minimal priority seen: M = (c(Q), Q A , ∆ M ) where ∆ M (q, c) = min(c, c(q)).

The automaton A over infinite words has value 1 if and only if there exists R ⊆ Q, such that the two following probabilistic automata over finite words have value 1:

• The automaton A(R) with R as set of final states;

• The automaton A ⊗ M with the uniform distribution over R c = {(q, c(q)) | q ∈ R} as initial distribution and {(q, e) | q ∈ R and e even} as set of final states.

Before giving the proof, we need two lemma.

Lemma 6.2. Let A = (Q, δ, ∆, F ) be a probabilistic automaton, u a word and ε > 0

. Let µ = min{δ(q) | q ∈ Supp(δ)}. If P δ A (u) ≥ 1 -ε • µ, then for all q ∈ Supp(δ), P q A (u) ≥ 1 -ε. Proof. P δ A (u) = q∈Supp(δ) δ(q) • P q A (u) ≥ 1 -ε • µ.
Let q ∈ Supp(δ), since the probabilities are bounded by 1:

δ(q) • P q A (u) + p∈Supp(δ), p =q δ(p) 1-δ(q) ≥ 1 -ε • µ.
Hence:

P q A (u) ≥ 1 -ε • µ δ(q) ≥ 1 -ε.
argument, at the expense of considering a subsequence of (w n ) n∈N , we can assume that (δ n ) n∈N converges to a distribution δ, whose support is denoted by R. We now prove that A(R) as well as A ⊗ M have value 1.

The automaton A(R). Let ε > 0. Since (δ n ) n∈N converges to δ, for n large enough, we have ||δ n -δ|| ∞ ≤ ε 2•|R| . We fix n large enough; since (δ n φn(k) ) k∈N converges to δ n , for k large enough, we have ||δ n φn(k)δ n || ∞ ≤ ε 2•|R| . We fix such a large k, altogether this implies ||δ n φn(k) -δ|| ∞ ≤ ε |R| . Now consider u the prefix of w n until position φ n (k). We have:

P A(R) (u) = q∈R δ n φn(k) (q) ≥ q∈R δ(q) - ε |R| = 1 -ε.
It follows that A(R) has value 1.

The automaton A ⊗ M. Let ν = min{δ(q) | q ∈ Supp(δ)}, clearly 0 < ν < 1. Since (δ n ) n∈N converges to δ, we can assume that for all n ≥ 0, ||δ n -δ|| ∞ ≤ ν 4 , considering the sequence (w n ) n∈N from some index on. For each n, the sequence (δ n φn(k) ) k∈N converges to δ n , so again by considering the sequence from some index on, we can assume that for all k ≥ 0, ||δ n φn(k)δ n || ∞ ≤ ν 4 , hence ||δ n φn(k) -δ|| ∞ ≤ ν 2 . As a result, for all q ∈ R, we have δ n φn(k) (q) ≥ ν 2 > 0, so R = Supp(δ) ⊆ Supp(δ n ) ⊆ Supp(δ n φn(k) ).

Let ε > 0, and n such that Here again, k ′ depends on d; however with the same reasoning as above, we can assume that k ′ is uniform over all even colors d. Altogether, this implies: Let v be the infix of w n between the positions φ n (k) and φ n (k ′ ). The distribution δ n φn(k) is over the set of states Q; we embed it as δ over the set of states Q × c(Q), setting δ(q, c(q)) = δ n φn(k) (q) and 0 otherwise. By construction of v, we have P δ A⊗M (v) = P A,wn (Parity(c, k, k ′ )) ≥ 1ε • ν 2 . However, the initial distribution of A ⊗ M is uniform over R c . We apply Lemma 6.2; by construction µ ≥ ν 2 , so P δ A⊗M (v) ≥ 1-ε•µ. It follows that for all q ∈ Supp(δ n φn(0) ), P q,c(q) A⊗M (v) ≥ 1ε. Since R ⊆ Supp(δ n φn(k) ), we have P A⊗M (v) ≥ 1ε, hence A ⊗ M has value 1.

We now prove the right-to-left direction. Let R such that both A(R) and A ⊗ M have value 1. Let ε > 0, consider the sequence (ε k ) k≥0 given by Lemma 6.4.

Since A(R) has value 1, there exists u such that P A(R) (u) ≥ ε 0 . We show the existence of a sequence w 1 , w 2 , . . . of words such that for all k ≥ 0:

P A(R) (u • w 1 • w 2 • . . . • w k ) ≥ p≤k ε p and P δ ′ k A⊗M (w k+1 ) ≥ ε k+1 ,
where δ k is the distribution obtained by reading u • w 1 • w 2 • . . . • w k on A; the distribution δ k is over the set of states Q, we embed it as δ ′ k over the set of states Q × c(Q), setting δ ′ k (q, c(q)) = δ k (q) and 0 otherwise. We proceed inductively; assume w 1 , . . . , w k have been chosen. Note that by construction, q∈R δ k (q) ≥ p≤k ε p . However, the support of δ k is not included in R, so the first item of Corollary 6.3 does not apply. Then q∈Rc δ ′ k (q) ≥ p≤k ε p . Since A ⊗ M has value 1, thanks to the second item of Corollary 6.3, it has value at least p≤k ε p for δ ′ k as initial distribution. Together with 3., this implies that there exists w k+1 such that P δ ′ k A⊗M (w k+1 ) ≥ ε k+1 .

We have:

P A(R) (u • w 1 • w 2 • . . . • w k+1 ) ≥ P A(R) (u • w 1 • w 2 • . . . • w k ) • P δ k A(R) (w k+1 ) ≥ P A(R) (u • w 1 • w 2 • . . . • w k ) • P δ ′ k A⊗M (w k+1 ) ≥ p≤k ε p • ε k+1 =
p≤k+1 ε p , which concludes the inductive construction.

Let w = u • w 1 • w 2 • . . .. We evaluate P A,w (Parity(c)):

P A,w (Parity(c)) ≥ P A(R) (u)

• k≥0 P δ ′ k A⊗M (w k+1 ) ≥ ε 0 • k≥1 ε k = k≥0 ε k ≥ 1 -ε.
It follows that A has value 1 as a probabilistic parity automaton, which concludes the proof of Theorem 6.1.

Corollary 6.5. The value 1 problem for leaktight automata over infinite words with the parity condition is decidable and PSPACE-complete.

Indeed, observe that if A is leaktight, then by Proposition 5.4, so is A ⊗ M.

Acknowledgment

We thank Thomas Colcombet for having pointed us to the work of Leung and Simon, and the anonymous reviewers for their constructive comments.

Conclusion

We introduced a subclass of probabilistic automata, called leaktight automata, for which we proved that the value 1 problem is PSPACE-complete. This subclass generalizes all subclasses of probabilistic automata whose value 1 problem is known to be decidable. A challenging perspective is now to find subclasses of partially observable Markov decision processes where the value 1 problem is decidable (some preliminary results were given in [START_REF] Gimbert | Deciding the value 1 problem for sharp-acyclic partially observable markov decision processes[END_REF]), and to extend our results to the setting of partially observable stochastic games, which is even more challenging.

  Definition 1.2 (Value). The value of a probabilistic automaton A, denoted by val(A), is the supremum acceptance probability over all input words: val(A) = sup u∈A * P A (u).

  and (3.6) is proved. The property (3.3) follows.

Proposition 4. 4 .

 4 The leaktight property is stable by parallel composition. Proof. The extended Markov monoid G A||B + of the parallel composition embeds into the direct product G A + × G B + of the extended Markov monoids of each automaton. Note that for (u, u +

  by Lemma 4.10 we have |Cl(u)| ≤ |Cl(u ♯ i )|. Altogether, it follows |Cl(u)| ≤ |Q| -(p + 1). It follows from Lemma 4.11 that S |Q| = S |Q|+1 , i.e. the ♯-hierarchy collapses at level |Q|, proving Theorem 4.7.

Figure 3 :

 3 Figure 3: A leaktight automaton with value 1 and ♯-height |Q| -2.

Figure 4 :

 4 Figure 4: A leaktight automaton and its extended Markov monoid.

.

  Figure 5: A leaktight automaton which does not have value 1.

4 .

 4 P A,wn (Parity(c)) ≥ 1ε • ν 4 . Let Büchi(d) be the set of runs where the color d is reached infinitely often and by CoBüchi(< d) the set of runs where colors less than d are reached only finitely often. Observe that: Parity(c) = d even color Büchi(d) ∩ CoBüchi(< d).Let Safe(< d, k) be the set of runs where colors less than d are not reached anymore after the position φ n (k). Observe that:Büchi(d) ∩ CoBüchi(< d) ⊆ Büchi(d) ∩ k≥0 Safe(< d, k), so: P A,wn (Büchi(d) ∩ CoBüchi(< d)) ≤ P A,wn   Büchi(d) ∩ k≥0 Safe(< d, k)   .Since the sequence Büchi(d) ∩ (Safe(< d, k)) k≥0 is increasing with respect to set inclusion, for some k we have:P A,wn (Büchi(d) ∩ Safe(< d, k)) ≥ P A,wn (Büchi(d) ∩ CoBüchi(< d))ε • νNote that here, k depends on d; however, since if it holds for k then it holds for any bigger k and that there are finitely many even colors d, we can assume that k is uniform over all even colors d. Now, let Reach(d, k, k ′ ) be the set of runs where the color d is reached between the positions φ n (k) and φ n (k ′ ). Observe that:Büchi(d) ∩ Safe(< d, k) ⊆ k ′ >k Reach(d, k, k ′ ) ∩ Safe(< d, k), so: P A,wn (Büchi(d) ∩ Safe(< d, k)) ≤ P A,wn k ′ >k Reach(d, k, k ′ ) ∩ Safe(< d, k) .Since the sequence (Reach(d, k, k ′ ) ∩ Safe(< d, k)) k ′ >k is increasing with respect to set inclusion, for some k ′ we have: P A,wn (Reach(d, k, k ′ ) ∩ Safe(< d, k)) ≥ P A,wn (Büchi(d) ∩ Safe(< d, k))ε • ν 4 .

P

  A,wn (Reach(d, k, k ′ ) ∩ Safe(< d, k)) ≥ P A,wn (Büchi(d) ∩ CoBüchi(< d))ε • ν 2 ,and summing these equalities for each even color d:P A,wn (Parity(c, k, k ′ )) ≥ d even color P A,wn (Reach(d, k, k ′ ) ∩ Safe(< d, k)) ≥ P A,wn (Parity(c))ε • ν2 , where Parity(c, k, k ′ ) is the set of runs where the minimal color seen between the positions φ n (k) and φ n (k ′ ) is even.

This project was supported by the french ANR project "Stoch-MC" as well as "LaBEX CPU" of Université de Bordeaux.

The following lemma shows that the quantity |Cl(u)| strictly decreases when iterating an unstable limit-word (i.e. if u ♯ = u). Lemma 4.9. Let u be an idempotent limit-word.

Cl(u ♯ ) ⊆ Cl(u), (4.9)

if u = u ♯ , then Cl(u ♯ ) = Cl(u).

(4.10)

Proof. We prove (4.9). Let s ∈ Z u ♯ ; by definition we have s ∼ u ♯ s. We show that [s]

In other words, the equivalence classes for u ♯ are also equivalence classes for u, so Cl(u ♯ ) ⊆ Cl(u).

We prove (4.10). Assume u = u ♯ ; let s, t such that u(s, t) = 1 and u ♯ (s, t) = 0. By Lemma 4.8, there exists r such that u(s, t) = u(s, r) • u(r, r) • u(r, t), so u(r, r) = 1. Towards contradiction, assume u ♯ (r, r) = 1. It follows that:

The following lemma shows that the quantity |Cl(u)| 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, see [START_REF] Lallement | Semigroups and Combinatorial Applications[END_REF][START_REF] Howie | Fundamentals of semigroup theory[END_REF], or [START_REF] Colcombet | Green's relations and their use in automata theory[END_REF] for its applications to automata theory).

Define u ≤ J v if there exist a, b such that a • v • b = u, and uJ v, i.e. u and v are in the same J -class, if u ≤ J v and v ≤ J u. We construct a partial surjective mapping β : Cl(v) → Cl(u), which depends on the choice of a and b. For all states s ∈ Z v and t ∈ Z u satisfying a(t, s)

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 ′ ∈ Z v and t, t ′ ∈ Z u , and assume a(t, s)

To show that β is well defined, we have to show that if

We show that β is surjective. Let t ∈ Z u . We exhibit some s such that β(

The case of iteration is easy.

The inclusion is strict, an example is given by figure 4.

5.4. Leaktight automata strictly contain simple automata. The class of simple automata has been defined in [START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF], where it was proved that the value 1 problem is decidable for a subset of this class (namely, for structurally simple automata). In the following we show that the class of simple automata is strictly contained in the class of leaktight automata.

We fix A a probabilistic automaton.

Definition 5.6 (Jets). A jet is a sequence

Definition 5.7 (Simple process [START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF]). Let w ∈ A ω be an infinite word. The process induced by w from the state p is simple if there exists λ > 0 and two jets

for all k ∈ N and all q ∈ A k , P A (p

Definition 5.8 (Simple automata [START_REF] Chatterjee | Decidable problems for probabilistic automata on infinite words[END_REF]). A is simple if for every infinite word w and every state p the process induced by w from p is simple.

Theorem 5.9. Every simple automaton is leaktight.

The remainder of this subsection is devoted to the proof of Theorem 5.9. The proof is divided into two parts: first, we define non-simplicity witnesses, which are elements of the Markov monoid that witnesses the non-simplicity of an automaton, and second we show that if the Markov monoid of an automaton contains a leak, then it also contains a non-simplicity witness.

Non-simplicity witness.

Definition 5.10 (Non-simplicity witness). A triple (u, v, w) of elements of the Markov monoid is a non-simplicity witness if there exist states r, t such that:

(1)

Proposition 5.11. If the Markov monoid of a probabilistic automaton contains a nonsimplicity witness, then it is not simple.

To prove Proposition 5.11, we rely on the following two lemmata:

Lemma 5.12. Let u be an idempotent element of the Markov monoid, r be a state urecurrent, and (u n ) n∈N a sequence of words that reifies u. Then there exists a constant γ > 0 and a strictly increasing map h : N → N such that for all n ∈ N, we have:

Proof. Since the sequence of words (u n ) n∈N reifies the limit-word u, for all states s, t, P A (s un -→ t) converges and:

(5.6)

Thanks to (5.6), there exists an increasing map h : N → N such that the following two conditions hold, for all states s, t and for all n ∈ N:

(5.8) We now use (5.7) and (5.8) to prove the desired result, for γ

. We first bound the quantity P A (r wn --→ Q \ R). Note that for q ∈ R and t a state, the following holds: if u(q, t) = 1 then t ∈ R, i.e. R is not left while following transitions consistent with u. It follows that the probability to leave R from r while reading w n is smaller than

, which is smaller than 1 2 by (5.7). Thus P A (r

2 . Now, since r is u-recurrent, and u is idempotent, for all q ∈ R we have u(q, r) = 1, so using (5.8) we get that P A (q u h(n-1) -----→ r) ≥ λ. It follows that P A (r wn --→ r) ≥ λ 2 , which concludes. Lemma 5.13. Let w ∈ A ω be an infinite word. If there exist states p, s, t, (i n ) n∈N , (j n ) n∈N and γ > 0 such that:

(1) for all n ∈ N, P A (p

(2) for all n ∈ N, i n < j n and P A (s

then the process induced by w from p is not simple.

Proof. Assume towards contradiction that w induces a simple process from p with bound λ. We first argue that for infinitely many n ∈ N, we have s ∈ A in and t ∈ B jn . Indeed, if this is not the case, then for n ∈ N large enough either s / ∈ A in or t / ∈ B jn , so either for infinitely many n ∈ N we have s / ∈ A in , or for infinitely many n ∈ N we have t / ∈ B jn . The first case is contradicted by (1), the second case by (3).

Let n ∈ N such that s ∈ A in and t ∈ B jn , since P A (s w[in,jn] -----→ t) > 0, along a path from s to t there is a transition from the jet A to the jet B. Formally, there exists k n such that i n ≤ k n < j n and the k n th transition goes from q kn ∈ A kn to q kn+1 ∈ B kn+1 . This transition is a one-step transition in the automaton A; denote by p min the minimal nonzero probabilistic transition in A, we have P A (q kn w[kn,kn+1] -------→ q kn+1 ) ≥ p min . Now, consider P A (p w ≤kn ---→ q kn+1 ); since q kn ∈ A kn , we have P A (p w <kn ---→ q kn ) ≥ λ, so P A (p w ≤kn ---→ q kn+1 ) ≥ λ • p min . But for infinitely many n ∈ N, q kn+1 ∈ B kn+1 , contradicting lim n→∞ P A (p w<n ---→ B n ) = 0. Now we are ready to prove Proposition 5.11.

Proof. Let (u, v, w) be a non-simplicity witness, and r, t ∈ Q such that r is uv ♯ w-recurrent, uv(r, t) = 1 and t is v-transient. Let (u n ) n∈N , (v n ) n∈N , (w n ) n∈N be sequences of words which reify u, v, w respectively.

Thanks to Proposition 2.11, there exists a strictly increasing map f :

By assumption uv(r, t) = 1, so there exists N k ∈ N such that for all n ≥ N k , P A (r

, so it reifies uv ♯ w as well. By definition of the function g, we have: for all n ∈ N, P A (r

--------→ t) > 0.

(5.9)

We apply Lemma 5.12 to the limit-word uv ♯ w, the state r and the sequence of words

) n∈N , and obtain h a strictly increasing map and a constant γ > 0. Define the new sequence of words (z n

) n∈N . We have: for all n ∈ N, P A (r

(5.10)

Let z = z 0 z 1 • • • . We argue that the conditions of Lemma 5.13 are met:

(1) for all n ∈ N, P A (r

The item (1) is (5.10), the item (2) follows from (5.9), so we consider (3). First, note that (x n ) n∈N reifies uv ♯ . Indeed, we first argue that (v n f (g(n)) ) n∈N reifies v ♯ : it follows from Proposition 2.11, since f • g : N → N is a strictly increasing map satisfying f • g ≥ f , and that (v n f (n) ) n∈N reifies v ♯ . Now, (v

) n∈N , so it reifies v ♯ as well, and it follows that (x n ) n∈N reifies uv ♯ . Second, let q ∈ Q, since t is v-transient, uv ♯ (q, t) = 0. Since (x n ) n∈N reifies uv ♯ , we have lim n→∞ P A (q xn -→ t) = 0. Now,

and for each term in the sum, the second factor converges to zero, so lim n→∞ P A (r

Thus Lemma 5.13 applies, and z induces a non-simple process from p, so A is not simple. Corollary 6.3. Let A = (Q, δ, ∆, F ) be a probabilistic automaton. If A has value 1, then:

• For all distributions δ ′ such that Supp(δ ′ ) ⊆ Supp(δ), it has value 1 with δ ′ as initial distribution.

• For all distributions δ ′ such that q∈Supp(δ) δ ′ (q) ≥ θ, it has value at least θ with δ ′ as initial distribution.

Proof. Assume A has value 1. Let ε > 0, then there exists a word u such that P A (u) ≥ 1ε • µ. Thanks to Lemma 6.2, this implies that for all q ∈ Supp(δ), we have P q A (u) ≥ 1ε. Now for δ ′ :

For the first item, note that if Supp(δ ′ ) ⊆ Supp(δ), then q∈Supp(δ) δ ′ (q) = 1, so P δ ′ A (u) ≥ 1ε, so A has value 1 with δ ′ as initial distribution.

The second item follows from the last inequality, implying P δ ′ A (u) ≥ θ • (1ε), so A has value at least θ with δ ′ as initial distribution. Lemma 6.4. For all ε > 0, there exists a sequence (ε k ) k≥0 satisfying:

(1) For all k ≥ 0, we have 0 < ε k < 1;

(2) k≥0 ε k ≥ 1ε;

(3) For all k ≥ 0, we have p≤k ε p > ε k+1 .

Proof. Define ν k = 1 -1 2 2 k , which clearly satisfies 1. It also satisfies 3.:

The inequality p≤k ν p > ν k+1 is equivalent to:

which is easily proved by induction, since (2 2 k+1 -1) 2 < 2 2 k+2 -1. The infinite product k≥0 ν k has a value ν ≈ 0.350184, in particular 0 < ν < 1. Let ε > 0, then for λ = ln(1-ε) ln(ν) , which satisfies λ > 0, the sequence (ν λ k ) k∈N satisfies the three conditions.

We are now fully equipped for the proof of Theorem 6.1

We begin with the left-to-right direction. Let (w n ) n∈N be a sequence of infinite words such that P A,wn (Parity(c)) converges to 1. For each n, denote by (δ n k ) k∈N the sequence of distributions assumed by A when reading w n . Since there are finitely many possible supports, there exists a subsequence where all distributions have the same support. Since [0, 1] Q is a compact space, we can extract from this subsequence another one, denoted by (δ n φn(k) ) k∈N , which converges to a distribution denoted by δ n . By the same compactness