Arnaud Carayol
email: arnaud.carayol@univ-mlv.fr

Axel Haddad
email: axel.haddad@liafa.jussieu.fr

Liafa Ligm

Olivier Serre
email: olivier.serre@liafa.jussieu.fr

Qualitative Tree Languages

We study finite automata running over infinite binary trees and we relax the notion of accepting run by allowing a negligible set (in the sense of measure theory) of non-accepting branches. In this qualitative setting, a tree is accepted by the automaton if there exists a run over this tree in which almost every branch is accepting. This leads to a new class of tree languages, called the qualitative tree languages that enjoys many properties.

Then, we replace the existential quantification -a tree is accepted if there exists some accepting run over the input tree -by a probabilistic quantification -a tree is accepted if almost every run over the input tree is accepting. Together with the qualitative acceptance and the Büchi condition, we obtain a class of probabilistic tree automata with a decidable emptiness problem. To our knowledge, this is the first positive result for a class of probabilistic automaton over infinite trees.

I. INTRODUCTION

Finite automata on infinite trees were originally introduced by Rabin in [START_REF] Thomas | Languages, automata, and logic[END_REF] to prove the decidability of the monadic second order logic over the full binary tree as well as to solve the Church's synthesis problem [START_REF] Courcoubetis | Markov decision processes and regular events[END_REF]. Since then, automata on infinite trees and their variants have been intensively studied and found many applications, in particular in logic. Connections between automata on infinite trees and logic are discussed in the excellent surveys [START_REF] Vardi | Automata: from logics to algorithms[END_REF], [18].

Roughly speaking a tree automaton is a finite memory machine that takes as input an infinite node-labelled binary tree and processes it in a top-down fashion as follows. It starts at the root of the tree in its initial state, and picks (possibly nondeterministically) two successor states, one per son, according to the current control state, the letter at the current node and the transition relation. Then the computation proceeds in parallel from both sons, and so on. Hence a run of the automaton on an input tree is a labelling of this tree by control states of the automaton, that should satisfy the local constrains imposed by the transition relation. A branch in a run is accepting if the ω-word obtained by reading the states along the branch satisfies some acceptance condition (typically an ω-regular condition such as a Büchi or a parity condition). Finally, a tree is accepted by the automaton if there exists a run over this tree in which every branch is accepting. An ω-regular tree language is a tree language accepted by some tree automaton equipped with a parity condition. A fundamental result of Rabin is that ω-regular tree languages form a Boolean algebra [START_REF] Thomas | Languages, automata, and logic[END_REF]. The hard part in this proof is the complementation, and since the publication of this result in 1969, it has been a challenging problem to simplify the proof. A much simpler one was obtained in [START_REF] Muchnik | Mathematical metaphysics of randomness[END_REF] making use of two-player games on graphs. Beyond this result, the connection between automata and games is one of the main tool in automata theory (see e.g. [START_REF] Gurevich | Trees, automata, and games[END_REF]).

In this article, we consider variations of the classical model of tree automata over infinite trees. Theses variations involve probabilities and preserve the fruitful connection with game theory.

In the first part of this paper, we consider a relaxed notion of accepting run. While the usual definition requires that all branches satisfy the acceptance condition, we allow a negligible set (in the sense of measure theory) of non-accepting branches. In this qualitative setting, a tree is accepted by the automaton if there exists a run over this tree in which almost every branch is accepting. With the parity condition, this leads to a new class of tree languages, qualitative tree languages. We show that this class enjoys many desirable properties: closure under union and intersection (but not under complement), emptiness is decidable in polynomial time (note that no polynomial algorithm is known for the emptiness test of parity tree automata). We also prove that there exists a strong connection between automata accepting qualitative tree languages and Markov decision processes, which play here a similar role as two-player games for usual tree automata.

The idea of allowing a certain amount of rejecting branches in a run was already considered in [START_REF] Beauquier | Automata on infinite trees with path counting constraints[END_REF], where it was required that the number of accepting branches in a run belong to a specified set of cardinals Γ. In particular, they proved that if Γ consists of all cardinals greater than some γ, then one obtains a regular tree language. Qualitative tree languages as defined in this article are not captured by the work of [START_REF] Beauquier | Automata on infinite trees with path counting constraints[END_REF]. Indeed, they are incomparable with regular tree languages.

In the second part of this paper, we investigate probabilistic automata on infinite trees. Acceptance by an automaton is based on existential quantification: an input is accepted if there exists an accepting run over it. Probabilistic automata are an alternative way to define acceptance. On finite words they have been introduced by Rabin in [START_REF] Michael | Decidability of second-order theories and automata on infinite trees[END_REF]. Compared with the standard setting, the non-deterministic guesses are replaced by random choices. Hence the set of transitions is replaced by a probability distribution over the set of all transitions which induces a probability measure on the set of runs of the automaton. The acceptation is defined using a threshold 0 ă λ ă 1 on the probability of a run to be accepting. In contrast to the non-deterministic setting, the emptiness problem for probabilistic automata on finite words is undecidable [START_REF] Perrin | Infinite Words[END_REF].

This probabilistic model was recently extended to infinite words [START_REF] Baier | Recognizing omegaregular languages with probabilistic automata[END_REF]. In addition to the threshold acceptation, two additional acceptations were considered : almost-sure and positive which respectively corresponds to a probability 1 or ą 0 for a run to be accepting 1 . Surprisingly the class of languages defined by Büchi automata with the positive acceptation is closed under complement, which implies that it coincides with the class of languages defined by co-Büchi automata with the almost-sure acceptation 2 . The emptiness problem for Büchi automata with the almost-sure acceptation are decidable. However the emptiness problem for Büchi automata with the positive acceptation as well as for co-Büchi automata with the almost-sure acceptation are undecidable. Of course, emptiness is undecidable when considering a threshold condition. See [START_REF] Baier | On decision problems for probabilistic Büchi automata[END_REF] for more details on this topic.

We consider probabilistic automata on infinite trees which accept a tree if almost every run over the input tree is accepting. For the qualitative definition of accepting runs, we prove that there exists a strong connection with partial observation Markov decision processes. In particular, for the Büchi condition, these probabilistic automata on infinite trees enjoy a decidable emptiness problem. To our knowledge, this is the first positive result for a class of probabilistic automaton over infinite trees.

In the last part, we discuss alternative definitions for qualitative acceptance as well as acceptance by probabilistic automata.

II. DEFINITIONS A. Words and Trees

An alphabet A is a finite set of letters. In the sequel A denotes the set of finite words over A, and A ω the set of infinite words over A. The empty word is written ε; the length of a word u is denoted by |u|. Let u be a finite word and v be a (possibly infinite) word. Then u ¨v denotes the concatenation of u and v; the word u is a prefix of v, 1 In the finite word case, the almost-sure and positive acceptation are trivial as the set of runs for a given word is finite.

2 Indeed, let L be accepted by a Büchi automaton with the positive acceptation. As one can complement, there is a Büchi automaton with the positive acceptation A such that L is the language accepted by A. If one sees A as a co-Buchi automaton B (final states become the forbidden ones) with a almost-sure acceptation, B accepts a word iff A does not. Hence, B recognises the complement of L, namely L. denoted u Ď v, iff there exists a word w such that v " u ¨w. We denote by u Ă v the fact that u is a strict prefix of v (i.e. u Ď v and u " v). For some word u and some integer k ě 0, we denote by u k the word obtained by concatenating k copies of u (with the convention that u 0 " ε).

In this paper we consider full binary node-labelled trees. An A-labelled tree t is a mapping from t0, 1u ˚to A. In this context, an element u P t0, 1u ˚is called a node, and the node u ¨0 (resp. u ¨1) is the left son (resp. right son) of u. The node ε is called the root. We shall refer to |u| as the depth of u. The letter tpuq is called the label of u in t.

A branch is an infinite word π P t0, 1u ω . We write Br " t0, 1u ω for the set of all branches. A node u belongs to a branch π if u is a prefix of π. For an A-labelled tree t and a branch π " π 0 π 1 ¨¨¨we define the label of π as the ω-word tpπq " tpεqtpπ 0 qtpπ 0 π 1 qtpπ 0 π 1 π 2 q ¨¨¨. The cone going through a node u is the set Conepuq " u ¨t0, 1u ω . A sub-cone of a cone Conepuq is a cone Conepvq with u Ď v.

Given a tree t and a node u, the subtree of t rooted at u denoted trus is the tree defined by truspvq " tpu ¨vq. A tree t is said to be regular if it contains only finitely many different subtrees, i.e. the set ttrus | u P t0, 1u ˚u is finite.

Let F Br be the σ-algebra generated by the set of cones (i.e. the smallest set of subsets of t0, 1u ω containing the cones and closed under countable union and complementation). Let µ be the unique probability measure on F Br such that for all u P t0, 1u ˚, µpConepuqq " 2 ´|u| . The existence and unicity of µ are guaranteed by Carathéorody's extension theorem [START_REF] Bauer | Measure and Integration Theory[END_REF]. For all 0 ă p ă 1, a probability measure µ p is similarly defined by taking µ p pConepuqq " p |u|0 p1 ´pq |u|1 where |u| 0 and |u| 1 respectively designate the number of occurrences of 0 and 1 in u. In particular, the measure µ corresponds to µ 1{2 .

B. Tree Automata and Regular Tree Languages

A tree automaton A is a tuple xA, Q, q ini , ∆, Accy where A is the input alphabet, Q is the finite set of states, q ini P Q is the initial state, ∆ Ď Q ˆA ˆpQ ˆQq is the transition relation and Acc Ď Q ω is the acceptance condition. In the following, we use the notation q a Ñ pq 0 , q 1 q as a shorthand for pq, a, pq 0 , q 1 qq P ∆. An automaton is deterministic iff q a Ñ pq 0 , q 1 q and q a Ñ pq 1 0 , q 1 1 q implies q 0 " q 1 0 and q 1 1 " q 1

1 . An automaton is complete iff, for all q P Q and a P A there is at least one pair pq 0 , q 1 q P Q 2 such that q a Ñ pq 0 , q 1 q. Given an A-labelled tree t, a run of A over t is a Qlabelled tree ρ such that ' the root is labelled by the initial state, i.e. ρpεq " q ini ; ' for all nodes u, pρpuq, tpuq, ρpu ¨0q, ρpu ¨1qq P ∆. A branch π P t0, 1u ω is accepting in the run ρ iff ρpπq P Acc. A run ρ is accepting if all its branches are accepting. Finally, a tree t is accepted if there exists an accepting run of A over t. The set of all trees accepted by A is denoted LpAq.

We consider the following classical acceptance conditions:

' A reachability condition is given by a subset F Ď Q of final states by letting ReachpF q " Q ˚F Q ω , i.e. a branch is accepting if it contains a final state. ' A Büchi condition is given by a subset F Ď Q of final states by letting BuchipF q " pQ ˚F q ω , i.e. a branch is accepting if it contains infinitely many final states. ' A co-Büchi condition is given by a subset F Ď Q of forbidden states by letting coBuchipF q " Q ˚pQzF q ω , i.e. a branch is accepting it contains finitely many forbidden states. ' A parity condition is given by a colouring mapping Col : Q Ñ N by letting P arity " tq 0 q 1 q 2 ¨¨¨| lim infpColpq i qq i is evenu, i.e. a branch is accepting if the smallest colour appearing infinitely often is even. All these conditions are examples of ω-regular acceptance condition, i.e. Acc is regular set of ω-words [START_REF] Michael | Probabilistic automata[END_REF]. However, the parity condition is expressive enough to capture the general case of an arbitrary ω-regular condition. First, one considers a deterministic parity word automaton recognising Acc, and then takes the synchronised product of this automaton with the tree automaton. This leads to a parity tree automaton accepting the same language [START_REF] Michael | Probabilistic automata[END_REF].

When it is clear from the context, we may replace, in the description of A, Acc by F (for a reachability, Büchi or co-Büchi condition) or Col (for a parity condition), and we shall refer to the automaton as a reachability (resp. Büchi, co-Büchi, parity) tree automaton. A set L of trees is a regular language if there exists a parity tree automaton A such that L " LpAq. The class of regular tree languages is robust, as illustrated by the following statement. Theorem 1. [START_REF] Thomas | Languages, automata, and logic[END_REF], [START_REF] Grädel | Automata, Logics, and Infinite Games[END_REF] The class of regular tree languages is a Boolean algebra.

A regular tree languages is non-empty iff it contains a regular tree. Testing the emptiness of a regular tree language (defined by a given parity automaton) is in NP X co ´NP.

C. Markov Decision Process

1) Perfect information setting: A probability distribution over a countable set X is a mapping d : X Ñ r0, 1s such that ř xPX dpxq " 1. In the sequel we denote by DpXq the set of probability distributions over X.

An arena is a tuple G " xS, s ini , Σ, ζy where S is a countable set of states, s ini is an initial state, Σ is a finite set of actions and ζ : S ˆΣ Ñ DpSq is the transition (total) function.

A play in such an arena proceeds as follows. It starts in state s ini and Éloïse picks an action σ, and a successor state is chosen according to the probability distribution ζps ini , σq. Then Éloïse chooses a new action and the state is updated and so on forever. Hence a play is an infinite sequence s 0 s 1 s 2 ¨¨¨P S ω such that s 0 " s ini and for every i ě 0, there exists a σ P Σ with ζps i , σqps i`1 q ą 0. In the sequel we refer to a prefix of a play as a partial play and we denote by Plays the set of all plays.

A (pure) strategy 3 for Éloïse is a function ϕ : S ˚Ñ Σ assigning to every partial play an action. Of special interest are those strategies that does not require memory: a strategy ϕ is memoryless iff ϕpλ ¨sq " ϕpλ 1 ¨sq for all partial play λ, λ 1 and all states s (i.e. ϕ only depends on the current state). A play λ " s 0 s 1 s 2 ¨¨¨is consistent with a strategy ϕ if ζps i , ϕpv 0 ¨¨¨v i qqps i`1 q ą 0, for all i ě 0. Now, for any partial play λ, the cylinder for λ is the set Cylpλq " λS ω . Let F P be the σ-algebra generated by the set of cylinders. Then, pPlays, F P q is a measurable space.

A strategy ϕ induces a probability space over pPlays, F P q. Indeed, one defines a measure µ ϕ on cylinders and then uniquely extends it to a probability measure on F P using the Carathéodory's unique extension theorem. For this, we first define inductively µ ϕ on cylinders:

' as all plays start from s ini , we let µ ϕ pCylps ini qq " 1; ' for any partial play λ ending in some state s, we let µ ϕ pCylpλ ¨s1 qq " µ ϕ pCylpλqq ¨ζps, ϕpλqqps 1 q. We also denote by µ ϕ the unique extension of µ ϕ to a probability measure on F. Then pPlays, F P , µ ϕ q is a probability space.

An objective is a measurable set O Ď Plays: a play is winning if it belongs to O. A Markov decision process (MDP, aka one-and-half-player game) is a pair pG, Oq where G is an arena and O is an objective. In the sequel we should focus on ω-regular objectives (which are easily seen to be measurable), whose definitions are the same as for the acceptance condition on tree automata (the only difference is that we may have an infinite set of states).

A strategy ϕ is almost-surely winning if µ ϕ pOq " 1. If such a strategy exists, we say that Éloïse almost-surely wins G. The value of G is defined as ValpGq " sup ϕ µ ϕ pOq, and a strategy ϕ is optimal iff ValpGq " µ ϕ pOq.

When the set of actions Σ is reduced to one element, the MDP pG, Oq is called a Markov chain and we omit the unique action from all the definitions. The set of Plays is called the set of traces of the Markov chain and is denoted Traces. We write µ G the probability measure associated with the unique strategy. We say that the Markov chain almostsurely fulfils its objective if µ G pOq " 1.

MDPs over finite graphs enjoys many good properties.

Theorem 2.

[8], [START_REF] Church | Logic, arithmetic and automata[END_REF] Let G be an MDP over a finite arena with a parity objective. Then, one can decide in polynomial time whether Éloïse almost-surely wins. Moreover, Éloïse always has an optimal memoryless strategy.

2) Imperfect information setting: Now we consider the case where Éloïse has imperfect information about the current state. For this, we consider an equivalence relation " over S. We let rss " be the equivalence class of s for " and S{ " be the set of equivalence classes of " over S.

The intuitive meaning of " is that two states s 1 " s 2 cannot be distinguished by Éloïse. We easily extend " to partial plays: s 0 s 1 ¨¨¨s n " s 1 0 s 1 1 ¨¨¨s 1 n iff s i " s 1 i for all i " 0, ¨¨¨, n. If λ 1 " λ 2 Éloïse cannot distinguish λ 1 from λ 2 : therefore she should behave the same in both of them.

Hence, we should only consider so-called observationbased strategies. An observation-based (pure) strategy is a function ϕ : pS{ " q ˚Ñ Σ, i.e., to choose her next action, Éloïse considers the sequence of observations she got so far 4 . In particular, an observation-based strategy ϕ is such that ϕpλq " ϕpλ 1 q whenever λ " λ 1 . In this context, a memoryless strategy is a function from S{ " Ñ DpΣq, i.e. it only depend on the current equivalence class.

A partial observation Markov decision process (POMDP, aka one-and-half-player imperfect information game) is a triple pG, ", Oq where G is an arena, " is an equivalence relation over states and O is an objective. We say that Éloïse almost-surely wins G if she has an almost-surely winning observation-based strategy. Finally the value of G is defined as ValpGq " sup ϕ µ ϕ pOq where ϕ ranges over observationbased strategies; optimality is defined as previously.

The following decidability results are known for POMDP:

Theorem 3. [1]
In a POMDP with a Büchi objective, deciding whether Éloïse almost-surely wins is ExpTimecomplete. Moreover if Éloïse has an almost-surely winning strategy, she has an almost-surely winning strategy with finite memory. In a POMDP with a co-Büchi objective, it is undecidable whether Éloïse almost-surely wins.

Remark 1. The results in Theorem 2 and 3 do not depend on the encoding of probability distributions, as the only relevant information is which probabilities are non zero.

III. QUALITATIVE TREE LANGUAGES

A. Definition

In the classical definition, a run of a tree automaton A is accepting if all its branches satisfy the acceptance condition. In this article, we introduce a more relaxed notion of acceptation: a run is qualitatively accepting if almost every (in the sense of the measure µ) branch in it is accepting. More formally, consider a tree automaton A with an ωregular acceptance condition. A run ρ of A is qualitatively accepting if the set AccBrpρq " tπ P t0, 1u ω | ρpπq P Accu has measure 1, i.e. µpAccBrpρqq " 1. Note that, thanks to Proposition 1 below, the set AccBrpρq is indeed measurable. A tree t is qualitatively accepted if there exists a qualitatively accepting run of A over t and the set of all trees qualitatively accepted by A is denoted L Qual pAq. Finally, a qualitative tree language is a set L of trees such that there is a parity automaton A such that L Qual pAq " L. Proposition 1. Let A be a tree automaton equipped with an ω-regular acceptance condition, and let ρ be a run of A. Then the set AccBrpρq is measurable.

Example 1. Let L a be the language of ta, bu-labelled trees whose set of branches containing at least one a has measure 1. This language is recognised by the following reachability deterministic automaton A " xta, bu, tq ini , q f u, q ini , ∆, tq f uy where: ∆ " tq ini b Ñ pq ini , q ini q, q ini a Ñ pq f , q f q, q f a Ñ pq f , q f q, q f b Ñ pq ini , q ini qu. If one considers A as a Büchi automaton, the accepted language consists of those trees whose set of branches containing infinitely many a has measure 1.

Example 2. Let L 1 be the language of trees t such that in almost every branch, there is a node u labelled by a such that the subtree trus has only a on its leftmost branch. This language is recognised by the non-deterministic reachability automaton A " xA, Q, q w , ∆, tq acc uy with A " ta, bu, Q " tq w , q l , q acc , q rej u, and ∆ contains the following transitions: q w _ Ñ pq w , q w q, q w _ Ñ pq l , q acc q, q l a Ñ pq l , q acc q, q l b Ñ pq rej , q rej q, q acc _ Ñ pq acc , q acc q, q rej _ Ñ pq rej , q rej q (here _ is a shorthand for an arbitrary letter). Intuitively, the automaton can wait in state q w as long as it wants. It can at some node u use the second transition: this leads to accept (all branches in) the cone going through the right son, as well as those subtrees rooted at the right of the left-most branch going through u if this branch does not contain a node labelled b (note that the left-most branch going through u will be rejecting, but this does not affect the measure as there are only countably many such branches). If the leftmost branch going through u contains a b at node v then the cone of branches going through v is rejecting.

Remark 2. The choice of the measure µ though natural is arbitrary. Considering the measure µ p for some 0 ă p ă 1 2 would not affect the results obtained in this article (provided that definitions of the games are modified accordingly). However note that changing the measure does change the accepted language for a given automaton. For instance, consider the deterministic Büchi automaton A of Example 1 and the ta, bu-labeled tree such that for all u P t0, 1u ˚by tpuq " a if and only if µ p pConepuqq ą µpConepuqq.

A consequence of the proof of Kakutani's theorem in [START_REF] Paz | Introduction to probabilistic automata[END_REF] is that µ p pAccBrpρ 0 qq " 1 and µpAccBrpρ 0 qq " 0 where ρ 0 designates the unique run of A over t. Remark 3. A more general definition is to associate with any letter a in the alphabet a pair pp 0 a , p 1 a q P r0, 1s 2 with p 0 a p1 a " 1 and then to define the measure of a cone in a tree t by letting µpConepu 1 ¨¨¨u n qq " p u1 tpεq p u2 tpu1q . . . p un tpu1¨¨¨un´1q . Intuitively, the node label determines the respective weights of the left and right sons in the definition of the measure. In particular the measure µ p is the one obtained by letting pp 0 a , p 1 a q " pp, 1 ´pq for all letters a in the alphabet.

Again, with such a measure the results obtained in this article (provided that definitions of the games are modified accordingly) remains correct.

For the same reasons as for regular tree languages, the parity condition is expressive enough to capture any ωregular conditions: for any automaton A with an ω-regular acceptance condition, there exists a parity automaton B such that L Qual pAq " L Qual pBq. Thanks to the following proposition, we can only focus on complete automata. Proposition 2. For any tree automaton A with an ωregular acceptance condition, there exists a complete tree automaton B with the same acceptance condition and such that L Qual pAq " L Qual pBq.

Unsurprisingly determinism is a restriction.

Proposition 3. There is a qualitative tree language that cannot be qualitatively accepted by any deterministic automaton.

B. Pumping Lemma

Let t be a tree and u P t0, 1u ˚be a node. A pair ∆ " pt, uq is called a pointed tree. With a pointed tree ∆ 1 " pt 1 , u 1 q and a tree t 2 , we associate a new tree, ∆ 1 ¨t2 , by plugging t 2 in t 1 instead of the subtree rooted at u 1 . Formally, ∆ 1 ¨t2 puq " t 1 puq if u 1 is not a prefix of u and ∆ 1 ẗ2 puq " t 2 pu 1 q if u " u 1 u 1 for some u 1 P t0, 1u ˚. We can also define the product of two pointed trees ∆ 1 " pt 1 , u 1 q and ∆ 2 " pt 2 , u 2 q by letting ∆ 1 ¨∆2 " p∆ 1 ¨t2 , u 1 ¨u2 q. Finally, with a pointed tree ∆ " pt, uq, we associate a tree ∆ ω by taking an ω-iteration of the product: ∆ ω pvq " tpv 1 q where v 1 is the shortest word s.t. v " u k v 1 for some k ě 0.

Qualitative tree languages enjoy a pumping lemma, which contrasts with regular tree languages. Lemma 1. Let A be an n-states parity automaton, t be a tree in L Qual pAq and u be a node of depth greater that n. Then there exists three pointed trees ∆ 1 , ∆ 2 and ∆ 3 such that t " ∆ 1 ¨∆2 ¨∆3 ¨trus and ∆ 1 ¨∆ω 2 P L Qual pAq.

C. Closure Properties

We now investigate the closure properties of qualitative tree languages under Boolean operations. Unsurprisingly, qualitative tree languages are not closed under complement. This is a simple consequence of Lemma 1 Proposition 5. Qualitative tree languages are not closed under complement. Proof (sketch): One shows that the complement L a of the language L a of Example 1 does not satisfy the pumping

t ∆1 ∆2 ∆3 trus q q u ∆ 1 .∆ ω 2 ∆1 ∆2 ∆2 ∆2 q q q q Figure 1
. Pumping Lemma lemma. For this, consider a tree that contains only a's except on a subtree rooted deep enough where all nodes are labelled by b. This tree belongs to L a , but if one pumps and removes the subtrees made of b's one gets a tree in L a .

D. Emptiness Problem

It is well known that tree automata (as acceptors of regular languages) and two-player (perfect information) game are closely related [START_REF] Muchnik | Mathematical metaphysics of randomness[END_REF], [START_REF] Gurevich | Trees, automata, and games[END_REF]. In particular, the emptiness problem for regular tree languages and the problem of deciding the winner in a parity game on a finite graph are polynomially equivalent. From the proof of this result also follows that a regular tree language is non-empty iff it contains a regular tree.

We show that a similar connection exists between tree automata as acceptors of qualitative tree languages and MDPs. For this, fix a parity tree automaton A " xA, Q, q ini , ∆, Coly and a tree t. Consider the arena G A,t " xS, s ini , Σ, ζy where S " Q ˆt0, 1u ˚Y tKu, s ini " pq ini , εq, Σ " ∆ and ζ is defined as follows. First we let d K be the distribution defined by d K psq " 1 if s " K and d K psq " 0 otherwise, and, for all q 0 , q 1 P Q and u P t0, 1u ˚, we let d q0,q1,u be the distribution such that d q0,q1,u pq 0 , u0q " d q0,q1,u pq 1 , u1q " 1{2 and d q0,q1,u psq " 0 for all other s P S. Then we let ζppq, uq, pq 1 , a, q 0 , q 1 qq " d K if q ‰ q 1 or a ‰ tpuq, ζppq, uq, pq, tpuq, q 0 , q 1 qq " d q0,q1,u and ζpK, σq " d K for all σ P ∆. Finally, we define a colouring function ρ by letting ρppq, uqq " Colpqq and ρpKq " 1, and we call G A,t " pG A,t , O ρ q the MDP equipped with the parity objective O ρ defined by ρ. Then, the following holds:

Proof (sketch):

The key idea here is to note that strategies for Éloïse in G A,t are in bijection with runs of A over t, and that this map preserves the measure. In particular, the set of winning plays when Éloïse follows a strategy has the same measure than the set of accepting branches in the corresponding run.

Consider the (finite) arena G A " xS, s ini , Σ, ζy where S " Q ˆt0, 1u Y tq ini , Ku, s ini " q ini , Σ " ∆ and ζ is defined as follows. First we let d K be the distribution defined by d K psq " 1 if s " K and d K psq " 0 otherwise, and, for all q 0 , q 1 P Q, we let d q0,q1 be the distribution such that d q0,q1 ppq 0 , 0qq " d q0,q1 ppq 1 , 1qq " 1{2 and d q0,q1 psq " 0 for all other s P S. Then we let ζppq, iq, pq, a, q 0 , q 1 qq " d q0,q1 , ζppq, iq, pq 1 , a, q 0 , q 1 qq " d K if q ‰ q 1 , ζpq ini , pq ini , a, q 0 , q 1 qq " d q0,q1 , ζpq ini , pq, a, q 0 , q 1 qq " d K if q ‰ q ini , and ζpK, σq " d K for all σ P ∆. Finally, we define a colouring function ρ by letting ρppq, iqq " Colpqq and ρpKq " 1, and we call G A " pG A , O ρ q the MDP equipped with the parity objective O ρ defined by ρ. Then, the following hold: Theorem 5. The language L Qual pAq is non empty iff Éloïse almost-surely wins in G A from q ini . Proof (sketch): The idea is the same as for the proof of Theorem 4 except that now strategies are seen as pairs made of an A-labeled tree and a run of A over it. Again, the value of the strategy is the same as the measure of the set of accepting branches in the run, which allows to conclude. Corollary 1. Let A be a parity tree automaton. Then one can decide whether L Qual pAq " H in polynomial time. Moreover, if L Qual pAq " H, it contains a regular tree, and such a tree can be constructed in polynomial time.

Proof (sketch): Complexity follows from theorems 5 and 2. Regular trees are associated with memoryless strategy: as those are sufficient to play optimally in finite MDP, it permits to conclude.

E. Regular Tree Languages and Qualitative Tree Languages are Incomparable

In this section, we prove that regular tree languages and qualitative tree languages are incomparable. Proposition 6. There is a regular tree language that is not qualitative.

Proof (sketch): The regular language of those ta, bulabelled trees containing at least one node labeled by b, does not satisfies Lemma 1, hence it is not qualitative. Theorem 6. There is a qualitative tree language that is not regular.

Proof: Let L a be the language of trees whose set of branches containing at least one a has measure 1. This language is qualitative as noticed in Example 1. In the sequel, we prove that L a is not regular. We first prove that, for any regular tree t, if there is no cone in t whose branches only contain the letter b, then t P L a . Let t be a regular tree, we can assume w.l.o.g. that if there is a node labelled by a then all its descendants are labeled by a. Then the property "there is no cone in t whose branches only contain b" is the same as "every subtree contains a subtree made only of a". Let X 1 , . . . , X n be the n different subtrees of t, and for all i, let µ i be the measure of the set of branches containing a in X i (we call it the value of X i ). We can assume that @i µ 1 ď µ i . If X i1 and X i2 are the two sons of X 1 , we know that µ 1 "

µi 1 `µi 2 2 . Since µ 1 ď µ i for i " i 1 , i 2 , µ i1 " µ i2 " µ 1 .
Hence we can prove by induction that for all X i of minimal value, all the subtrees of X i have minimal value too. Since there is a subtree of a (of value 1) in X 1 , µ 1 " 1 hence for all i, µ i " 1, hence the value of t is 1, hence t P L a .

We assume by contradiction that L a is regular. The closure properties of regular tree languages implies that the following language L is also regular: L " t ˇˇt R L a ^"there is no cone in t whose branches only contain b" ( Using our previous characterisation of regular trees in L a it follows that L does not contain any regular tree, hence L is empty (Theorem 1). Then, to raise a contradiction, we build a (non-regular) tree t P L.

For every node u P t0, 1u ˚, we let n u be the integer whose binary representation is 1.u. The tree t is defined as follows: let v P t0, 1u ˚, if there exists some u such that v " u.0 nu`1´|u| then t 0 pvq " a, otherwise t 0 pvq " b (see Figure 2). We now establish that t R L a . First note that the set of branches in t that contains at least one a is obtained by taking the union of those cones Cpuq such that tpuq " a. Then remark that, for every level , there is one and only one node u of depth labelled by a (except for " 0, 1 where there are no such u). Thus we can bound the measure µ of the set of branches in t that contains at least one a:

µ ď `8 ÿ "2 2 ´ " 1 2
This proves that t R L a . Moreover, it follows from the definition, that for every node u, there is a branch (the leftmost one) in the cone Cpuq that contains an a, hence t P L, which contradict the fact that L is empty.

F. The Value of a Tree May not be Reached

So far we defined qualitative acceptance of a tree by the existence of a run whose set of accepting branches has measure 1. We can refine this notion by defining the value of a tree as follows. For A a tree automaton, and t a tree we let

Val A ptq " sup ρt run of A over t µpAccBrpρ t qq
In particular L Qual pAq is the set of trees t whose value is 1 and is reached for some run (i.e. the sup is a max). The following result proves that the value may not be reached by some run.

Theorem 7. There is a reachability automaton A and a tree t such that Val A ptq " 1 but t R L Qual pAq.

Actually, the proof of Theorem 4 leads the following.

Theorem 8. Let A be a parity tree automaton and let t be a tree. Then Val A ptq " ValpG A,t q.

IV. BEYOND NON-DETERMINISTIC AUTOMATA: THE PROBABILISTIC SETTING Following [START_REF] Thomas | Languages, automata, and logic[END_REF] for finite words and [START_REF] Baier | Recognizing omegaregular languages with probabilistic automata[END_REF], [START_REF] Baier | On decision problems for probabilistic Büchi automata[END_REF] for infinite words we investigate probabilistic automata on infinite trees. That is the set of transitions of an automaton is replaced by a probability distribution over the set of all transitions which induces a probability measure on the set of runs of the automaton. Now, a tree is accepted if almost every run over the input tree is accepting. For the run, we may use either the classical or the qualitative acceptance criterion.

A. Definitions

A probabilistic tree automaton A is a tuple xA, Q, q ini , δ, Accy where A is the input alphabet, Q is a finite set of states, q ini P Q is the initial state, Acc Ď Q ω is the acceptance condition and δ is a mapping from Q ˆA ˆQ ˆQ to r0, 1s such that for all q P Q and a P A, ř q1,q2PQ δpq, a, q 1 , q 2 q " 1. Intuitively, the value δpq, a, q 1 , q 2 q is the probability for a transition q a Ñ pq 1 , q 2 q to be used by the automaton when it is in state q and reads the symbol a.

This probability distribution on the transitions induces a probability measure on the set of runs of A. In this setting, a run of A is simply a Q-labeled tree whose root is labeled by the initial state q ini . We denote by RunspAq (or simply Runs if A is clear from the context) the set of all runs of A. We denote by AccRunspAq the set of accepting runs of A and by QualAccRunspAq the set of qualitatively accepting runs of A.

Let t be a tree. A partial run λ is a mapping from t0, 1u n to Q for some n ě 0 with λpεq " q ini . A partial run λ is a prefix of a run ρ if for all w P Dompλq, λpwq " ρpwq. The cylinder for a partial run λ, denoted Cyl A pλq, is the set of runs of A admitting λ as a prefix. Let F R be the σ-algebra generated by the cylinders. By Carathéorody's extension theorem, there exists a unique probability measure µ t on the measurable space pRuns, F R q such for all partial run λ : t0, 1u n Ñ Q, µ t pCyl A pλqq is equal to ś wPt0,1u n´1 δpλpwq, tpwq, λpw0q, λpw1qq. Note that both µ t and pRuns, F R q depend on t.

Proposition 7. For all probabilistic tree automata A with an ω-regular acceptance condition, the sets AccRunspAq and QualAccRunspAq are measurable.

A tree t is (almost-surely) accepted by A with the classical semantic if almost all runs of A on t are accepting (i.e. µ t pAccRunspAqq " 1). We denote by L "1 pAq the set of trees accepted by A with the classical semantics for runs. A tree t is (almost-surely) accepted by A with the qualitative semantic if almost all runs of A on t are accepting (i.e. µ t pQualAccRunspAqq " 1). We note L "1

Qual pAq the set of trees accepted by A with the qualitative semantics for runs.

Remark 4. Our motivation for considering almost-sure acceptation and not positive acceptation is discussed in Section V.

The almost-sure acceptation of a tree t by an automaton A for the qualitative semantic can be defined by integrating the mapping f A : Runs ˆBr Ñ r0, 1s associating to a pair pρ, πq P Runs ˆBr the value 1 if ρpπq belongs to Acc and 0 otherwise. Proposition 8. Let A be a probabilistic tree automaton with an ω-regular acceptance condition and let t be a tree. The mapping f A is integrable in the product space pRunspAq, F R , µ T q b pBr, F Br , µq and we have:

t P L "1 Qual pAq ô ż f A dµ t b µ " 1
Proof sketch: First we show that f A is measurable. Then, by Fubini's theorem [3, Thm 23.6 -p. 138], the mapping g : Runs Ñ r0, 1s associating with a run ρ P Runs the value ş Br f A pρ, ¨qdµ is measurable.

t belongs to L "1 Qual pAq iff µ t pg ´1pt1uqq " 1 iff ş Runs g dµ t " 1 iff ş Runs ş Br f A dµdµ t " 1 by definition of g iff ş RunsˆBr f A dµ T b µ " 1 by Fubini's thm.
We conclude this section with examples of languages accepted by probabilistic tree automata.

For an ω-word language L Ď ta, bu ω , we denote by Path "1 pLq the set of trees labeled by ta, bu with almost all their branch labels in L (i.e. µptπ P Br | tpπq P Luq " 1). It is easy to see that, for any ω-regular language L, the tree language Path "1 pLq is a qualitative tree language. More interesting, if L is almost-surely accepted by a probabilistic ω-word automaton5 with an ω-regular acceptance condition, we can show that Path "1 pLq is accepted by a probabilistic tree automaton (with the qualitative semantic). Proposition 9. Given a probabilistic ω-word automaton B with an ω-regular acceptance condition, there exists a probabilistic tree automaton A with the same acceptance condition such that L "1

Qual pAq is equal to Path "1 pL "1 pBqq. Proof (sketch): Let B " xA " ta, bu, Q, q ini , δ, Accy be a probabilistic ω-word automaton with an ω-regular condition. Consider the probabilistic tree automaton A simulating B along all branches. Formally A is equal to xA, Q, q ini , δ 1 , F y where, for all p, q P Q and x P A, δ 1 pp, x, q, qq " δpp, x, qq and otherwise is equal to 0.

Let t be a tree and let g : Br Ñ r0, 1s be the mapping associating to a branch π the value ş f A p¨, πq dµ t . For any π P Br, gpπq " 1 if and only if tpπq belongs to L "1 pBq.

t P L "1 Qual pAq ô ş f A dµ t b µ " 1 by Proposition 8 ô ş gdµ " 1 by Fubini's thm ô gpπq " 1 almost everywhere ô µptπ | tpπq P L "1 pBquq " 1 ô t P Path "1 pBq

B. Acceptance games for qualitative probabilistic tree automata

Fix a probabilistic tree automaton A " xA, Q, q ini , δ, Accy and a tree t. We define a Markov chain M A,t " pG A,t , O Acc q such that M A,t almost-surely fulfils its objective iff t belongs to L "1 Qual pAq. Compared with the acceptance game for qualitative tree automata, the transition is no longer chosen by Éloïse: it is now randomly chosen with the probability distribution given by A. Hence we simply obtain a Markov chain instead of an MDP.

The arena G A,t is equal to xS, s ini , ζy where S " Q t0, 1u ˚Y ∆ ˆt0, 1u ˚with ∆ " Q ˆQ ˆQ, s ini " pq ini , εq and ζ : S Þ Ñ DpSq is defined as follows. For all w P t0, 1u ånd all q P Q, ζppq, wq, pq, q 0 , q 1 qq " δpq, tpwq, q 0 , q 1 q for all q 0 , q 1 P Q and is equal to 0 otherwise. For all w P t0, 1u ˚and q 0 , q 1 P Q, ζpppq, q 0 , q 1 q, wq, pq 0 , w0q " ζpppq, q 0 , q 1 q, wq, pq 1 , w1qq " 1 2 and 0 otherwise. Recall that µ M A,t denotes the probability measure associated to M A,t .

To simplify the presentation, note that a trace in M A,t can be uniquely represented by an infinite sequence ppp 0 , q 0 0 , q 1 0 q, a 0 qppp 1 , q 0 1 , q 0 1 q, a 1 q . . . labeled by ∆ t0, 1u such that p 0 " q ini and for all i ě 0, p i`1 " q ai i . The objective O Acc is the set of traces

ź i"1 p1 ´λki q ą 0u
In [START_REF] Baier | On decision problems for probabilistic Büchi automata[END_REF], L λ is shown to be almost-surely accepted by a co-Büchi probabilistic automaton 6 . Therefore, by Proposition 9, Path "1 pL λ q is a co-Büchi probabilistic qualitative tree language.

Proposition 11. For all 0 ă λ ă 1, Path "1 pL λ q is not a qualitative tree language.

Proof (sketch): For all 0 ă λ ă 1, Path "1 pL λ q is nonempty and does not contain any regular tree. Hence according to Corollary 1, it is not a qualitative tree language.

Remark 5. Using the correspondence with POMDP introduced in Theorem 9, any co-Büchi automaton accepting Path "1 pL λ q gives rise to an example of a co-Büchi POMDP G A in which Éloïse needs infinite memory to almost-surely win.

V. DISCUSSION

Throughout this paper, we favoured the almost-sure condition (i.e. requiring the measure to be equal to 1) over the positive one (i.e. requiring the measure to be strictly positive). However, the decidability results on MDPs stated in Theorem 2 still hold if we replace the almost-sure acceptance by the positive acceptance [START_REF] Emerson | On model-checking for fragments of µ-calculus[END_REF], [START_REF] Church | Logic, arithmetic and automata[END_REF]. Similarly the decidability and undecidability results on POMDP stated in Theorem 3 transfer to positive acceptance provided that one replaces Büchi by co-Büchi and vice versa [START_REF] Baier | On decision problems for probabilistic Büchi automata[END_REF]. In this discussion, we summarise the impact when considering positive acceptance instead of almost-sure acceptance, and motivate our choices.

A run is ą 0-qualitively accepting if the measure of its set of accepting branches is strictly positive. The class of ą 0qualitative tree languages is defined similarly to the class of qualitative tree languages by consider ą 0-qualitatively accepting run instead of qualitatively accepting run. The two classes are incomparable. However, ą 0-qualitative languages enjoy most of the good properties of qualitative languages presented in Section III-C. In particular, the decidability results stated in Theorem 4, Theorem 5 and Corollary 1 transfer to ą 0-qualitative languages (of course almost-sure acceptance needs to be replaced by positive acceptance). In addition, the ą 0-qualitative languages are also incomparable with regular tree languages. The most notable difference between the two classes is that ą 0qualitative languages are not closed under intersection. In addition, the pumping lemma (Lemma 1) and the restriction to complete automata (Proposition 2) no longer hold.

Moving to the probabilistic automata setting, we now have to consider two possible acceptance conditions on the set of runs -almost-sure (" 1) and positive (ą 0)and two possible definitions for a run to be acceptingqualitative (" 1) and positive (ą 0). By combining these conditions, we obtain four semantics for probabilistic tree automata denoted by pą 0, ą 0q, pą 0, " 1q, p" 1, ą 0q and p" 1, " 1q where the first component corresponds to the requirement on the set of accepting runs and the second to the requirement on the set of accepting branches of a run. In Section IV, we mainly dealt with p" 1, " 1qprobabilistic automata which have a tight link with POMDP for the almost-sure winning condition (cf. Theorem 9). It can be shown that pą 0, ą 0q-probabilistic automata share the same connection with POMDP with the positive winning condition. It implies that the emptiness problem for the pą 0, ą 0q-probabilistic automata with the co-Büchi acceptance condition is ExpTime-complete.

When the two conditions are not of the same nature (as for the pą 0, " 1q and p" 1, ą 0q semantics), we were unable to define a proper acceptance game -see for instance a similar discussion at the end of Subsection IV-B for the semantic p" 1, @q.

Proposition 4 .

 4 Qualitative tree languages are closed under union and intersection.

Theorem 4 .

 4 The tree t belongs to L Qual pAq iff Éloïse almost-surely wins in G A,t .

Figure 2 .

 2 Figure 2. The tree t 0

We do not consider here randomised strategies as in the setting of this paper they are useless. Note that for finite MDP, optimal strategies -when exists -can always be chosen to be pure.

By abuse of notation, we shall write ϕps 0 ¨¨¨snq to mean ϕprs 0 s" ¨¨¨rsns"q

In the context of this article, probabilistic ω-word automata are simply probabilistic tree automata running over unary trees. For such an automaton B, we denote by L "1 pBq the language almost-surely accepted by B.

They show that L λ is positively accepted by a Büchi automaton. But as previously remarked in the introduction, the two classes coincide.

Acknowledgment. This work was supported by the following projects: AMIS (ANR 2010 JCJC 0203 01 AMIS) and FREC (ANR 2010 BLAN 0202 02 FREC).

ppp 0 , q 0 0 , q 1 0 q, a 0 qppp 1 , q 0 1 , q 0 1 q, a 1 q . . . such that p 0 p 1 . . . P Acc.

Proposition 10. Let A be a probabilistic tree automaton with an ω-regular acceptance condition and let t be a tree. t P L "1 Qual pAq iff M A,t almost-surely fulfils its objective. Proof (sktech): Let AccPairspAq " tpρ, πq | ρpπq P Accu. By Proposition 8, to establish the desired equivalence, it is sufficient to show that µ t b µpAccPairspAqq " µ M A,t pO Acc q.

Consider the mapping ψ : Runs ˆBr Þ Ñ Traces associating with any pair pρ, a 0 a 1 . . .q the trace pρpεq, ρp0q, ρp1qqa 0 pρpa 0 q, ρpa 0 0q, ρpa 0 1qqa 1 . . . of the Markov chain. It is clear that AccPairspAq " ψ ´1pO Acc q. The mapping ψ is measurable and µ M A,t is the image of µ t b µ under ψ. In particular it implies that µ M A,t pO Acc q " µ t b µpAccPairspAqq.

Let us now consider the case of probabilistic tree automata with the usual semantic for runs (i.e. all branches must be accepting). In this setting, a naive definition of an acceptance game consists, when choosing the successor, in replacing random by a second player, Abelard, However this game does not faithfully reflect the acceptation of the automaton.

Consider the reachability probabilistic tree automaton A " xtau, tq 0 , q f u, q 0 , δ, tq f uy with δpq 0 , a, q 0 , q 0 q " 3 4 , δpq 0 , a, q f , q f q " 1 4 , δpq f , a, q f , q f q " 1 and 0 otherwise. Consider the tree t a where all nodes are labeled by a. It can be shown that the set of accepting runs of A over t a has measure 1 3 . Hence the tree t a does not belong to L "1 pAq. Now consider the naive acceptance game for A on t a . Intuitively in this game, player random chooses a transition pp, q 0 , q 1 q and Abelard chooses to proceed either to q 0 or to q 1 . The set of states is t0, 1u ˚ˆtθ 0 , θ 1 , θ f u with θ 0 " pq 0 , q 0 , q 0 q, θ 1 " pq 0 , q f , q f q and θ f " pq f , q f , q f q, the initial state is pε, θ 0 q and the actions of Abelard are in t0, 1u. For x P t0, 1u, the transition function is such that for all w P t0, 1u ˚we have: ζppw, θ 0 q, xq is the probability distribution assigning 3 4 to pwx, θ 0 q and 1 4 to pwx, θ 1 q, ζppw, θ 1 q, xq " ζppw, θ f q, xq is the probability distribution assigning 1 to pwx, θ f q. The objective O is the set of plays containing θ f .

It is easy to check that the strategy of Abelard has no influence on the value of the game. In fact for any fixed strategy, the game is equivalent to the Markov chain depicted below which fulfils its objective with probability 1.

C. Decidability results

In this section, we show that the emptiness problem for probabilistic Büchi tree automata is decidable for the qualitative semantics for runs. This result is by reduction to deciding almost-surely winning in a POMDP, and the reduction works for any ω-regular acceptance condition. However, the decision problem on POMDPs is only decidable for the Büchi condition.

Let A " xA, Q, q ini , δ, Accy be a probabilistic automaton with an ω-regular acceptance condition and ∆ " QˆQˆQ.

We consider the POMDP G "1 A " pG, ", Oq. The arena G is equal to xS, s ini , Σ, ζy where S " Q ˆt0, 1, Ku p∆ Y tKuq, s ini " pq 0 , K, Kq, Σ " A and ζ is defined as follows. For all a P A and pp, x, tq P S, ζppp, x, tq, aq is the distribution that assigns 1 2 δpp, a, q 0 , q 1 q to pq y , y, pp, q 0 , q 1 qq where y " 0, 1 and 0 to all other state. The objective O is the set of plays for which the sequence of states obtained when projecting on the first component belongs to Acc. The equivalence " is defined by pq, x, tq " pq 1 , x 1 , t 1 q iff x " x 1 . Theorem 9. Let A be a probabilistic tree automaton with an ω-regular acceptance condition. The language L "1

Qual pAq is non-empty if and only if Éloïse almost-surely wins in G A .

Proof: From the definitions, we easily have that trλs " | λ P Plays " rKs " tr0s " , r1s " u ˚. Hence it is sufficient to consider strategies from rKs " tr0s " , r1s " u ˚to A, that can also be seen as A-labeled trees. Once such a strategy ϕ t (seen as a tree t) is fixed, the resulting Markov chain is, up to renaming, G A,t , meaning that the value of ϕ t is the value of G A,t . In particular, Éloïse almost-surely wins in G A iff there is some t such that ValpG A,t q " 1 iff t P L "1 Qual pAq (thanks to Proposition 10).

Corollary 2. Let A be a probabilistic Büchi tree automaton. Deciding whether L "1

Qual pAq " H is ExpTime-complete. Moreover, if L "1

Qual pAq ‰ H, it contains a regular tree. Proof: The Exptime upper-bound follows from the polynomial time reduction to deciding almost-surely winning in a Büchi POMDP. Existence of finite memory optimal strategies in POMDP implies the existence of a regular tree when L "1

Qual pAq ‰ H. The lower bound follows from Proposition 9: emptiness of probabilistic Büchi ω-word automata with the almost-sure acceptation (which is Exptimecomplete [START_REF] Baier | On decision problems for probabilistic Büchi automata[END_REF]) can be reduced to our problem.

We show that the emptiness problem for probabilistic co-Büchi tree automata is undecidable for both the classical and qualitative semantics for runs. These results are obtained by reduction to the undecidability of the emptiness problem for co-Büchi ω-word automata with the almost-sure acceptation [START_REF] Baier | On decision problems for probabilistic Büchi automata[END_REF].

Theorem 10. The following problems are undecidable :

1) given a probabilistic co-Büchi tree automaton A, decide if L "1 pAq " H, 2) given a probabilistic co-Büchi tree automaton A, decide if L "1 Qual pAq " H. Proof: Both undecidability results are shown by reduction to the undecidability of the emptiness problem for co-Büchi ω-word automata (with the almost-sure acceptation). The case of qualitative semantic directly follows from Proposition 9. It remains to treat the case of the classical semantic for runs.

Let B " xA " ta, bu, Q, q ini , δ, F y be a probabilistic co-Büchi ω-word automaton. We construct a probabilistic co-Büchi automaton A which simulates B on the left-most branch of the tree and checks that all other branches contain only as. Formally A is equal to xA, Q Y tq K u, q ini , δ 1 , F Y tq K uy. The probability distribution δ 1 is given by: $ ' ' & ' ' % δ 1 pq a , a, q a , q a q " 1 δ 1 pq a , b, q K , q K q " 1 δ 1 pq K , x, q K , q K q " 1 for x P A δ 1 pp, x, q, q a q " δpp, x, qq for x P A and q P Q In all other cases, δ 1 is equal to 0. A tree t belongs to L "1 pAq if and only if for all u R 0 ˚, tpuq " a and tp0 ω q P L "1 pBq. In particular L "1 pAq is empty if and only if L "1 pBq is empty.

D. Comparison with qualitative languages

In this section, we give an example of a tree language that is accepted by a co-Büchi probabilistic automaton but that is not a qualitative tree language.

For this we consider the ω-word language P λ over ta, bu defined, for all 0 ă λ ă 1, by: L λ " ta k1 ba k2 b . . . | k 1 , k 2 , . . . ą 0 s.t.