Paulin Fournier
email: paulin.fournier@labri.fr

Hugo Gimbert
email: hugo.gimbert@labri.fr

Alternating Nonzero Automata

We introduce a new class of automata on infinite trees called alternating nonzero automata, which extends the class of non-deterministic nonzero automata. We reduce the emptiness problem for alternating nonzero automata to the same problem for non-deterministic ones, which implies decidability. We obtain as a corollary algorithms for the satisfiability of a probabilistic temporal logic extending both CTL* and the qualitative fragment of pCTL*.

Introduction

The theory of automata on infinite trees is rooted in Rabin's seminal theorem which establishes an effective correspondence between the monadic second order logic (MSO) theory of the infinite binary tree and the non-deterministic automata on this tree [START_REF] Rabin | Probabilistic automata[END_REF]. In this correspondence, the satisfiability of the logic is dual to the emptiness of the algorithm and both these algorithmic problems are mutually reducible to one another. This elegant setting has been partially extended to probabilistic logics [START_REF] Lehmann | Reasoning with time and chance[END_REF][START_REF] Brázdil | Controller synthesis and verification for markov decision processes with qualitative branching time objectives[END_REF][START_REF] Michalewski | Measure quantifier in monadic second order logic[END_REF][START_REF] Michalewski | On the regular emptiness problem of subzero automata[END_REF][START_REF] Bojańczyk | Thin MSO with a probabilistic path quantifier[END_REF] and automata with probabilistic winning conditions [START_REF] Rabin | Probabilistic automata[END_REF][START_REF] Paz | Introduction to probabilistic automata[END_REF][START_REF] Baier | Probabilistic ω-automata[END_REF][START_REF] Carayol | Randomization in automata on infinite trees[END_REF][START_REF] Bojańczyk | Thin MSO with a probabilistic path quantifier[END_REF]. In this paper we make another step in this direction: we show a correspondence between the logic CTL * [∃, ∀, P >0 , P =1 ] and nonzero alternating automata with limited choice. Moreover we show that the emptiness problem of the automata is decidable and obtain as a corollary the decidability of the satisfiability of the logic.

Automata.

Alternating nonzero automata are an alternating version of non-deterministic nonzero automata introduced in [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF], which themselves are equivalent to non-deterministic zero automata introduced in [START_REF] Bojańczyk | Thin MSO with a probabilistic path quantifier[END_REF].

An alternating nonzero automaton takes as input a binary tree. Some states of the automaton are controlled by Eve, while other states are controlled by Adam, and the player controlling the current state chooses the next transition. Some transitions are local transitions, in which case the automaton stays on the same node of the input tree while other are split transitions in which case the automaton proceeds to the left son or to the right son of the current node with equal probability 1 2 . This interaction between Eve and Adam is seen as a game where Eve and Adam play according to some strategies. Once the strategies are fixed, one obtains a Markov chain whose trajectories are all possible plays consistent with the strategies. The winner is determined with respect to winning conditions introduced in [START_REF] Bojańczyk | Thin MSO with a probabilistic path quantifier[END_REF][START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF], using a total order on the set of states (used to compute the limsup of a play which is the largest state seen infinitely often during the play) and three subsets of states, respectively called the sure, almost-sure and positive states. Eve wins if and only if the three acceptance conditions hold: sure winning: every play has limsup in sure states; and almost-sure winning: almost-every play has limsup in almost-sure states; and positive winning: whenever the play enters a positive state there is positive probability that the play never exits positive states.

The input tree is accepted by the alternating automaton iff Eve has a winning strategy. Alternating nonzero automata generalize both classical alternating automata with parity conditions [9,[START_REF] Muller | Alternating automata on infinite trees[END_REF] (when all states are almost-sure and positive) as well as non-deterministic nonzero automata [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF] (in case Eve controls all states).

We do not know whether the emptiness problem for these automata is decidable or not, however we show that the answer is positive for the subclass of alternating nonzero automata with limited choice for Adam. In these automata, some choices of Adam are canonical, at most one in every state, and Adam may perform at most a bounded number of non-canonical choices during a single play.

We establish some properties of alternating nonzero automata with limited choice for Adam.

First, we show that the emptiness problem for alternating nonzero automata with limited choice for Adam is in nexptime∩ co-nexptime (Theorem 23). The proof is an exptime reduction to the emptiness problem for non-deterministic automata. This proof relies on the positional determinacy of the acceptance games for Eve (Lemma 10) and a characterization of positional winning strategies for Eve ( Lemmas 12,13 and 18). Second, we show that in the particular case where the sure winning condition is a Büchi condition, emptiness of non-deterministic nonzero automata is in ptime (Theorem 3) hence, in case of a Büchi sure winning condition, emptiness of nonalternating nonzero automata is in exptime (Theorem 23).

Logic.

The temporal logic CTL * introduced by Emerson and Halpern [START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] and its fragments CTL and LTL are prominent tools to specify properties of discrete event systems.

A variant of CTL * is the logic pCTL * [START_REF] Hansson | A logic for reasoning about time and reliability[END_REF] in which the universal and existential path quantifiers are replaced by probabilistic path quantifiers which set upper or lower bounds on the probability of a path property in a Markov chain. For example the formula P ≥ 1 2 (F Ga) specify that with probability at least 1 2 eventually all the visited states are labelled with a. To our knowledge, the satisfiability problem for this logic is an open problem.

However, for the qualitative fragment of pCTL * , where only two probabilistic quantifiers P >0 and P =1 are available, the satisfiability is decidable [START_REF] Brázdil | Controller synthesis and verification for markov decision processes with qualitative branching time objectives[END_REF]. In a variant of pCTL * called pECTL the path subformula are replaced by deterministic Büchi automaton, and the satisfiability of the qualitative fragment is 2-exptime complete [START_REF] Brázdil | Controller synthesis and verification for markov decision processes with qualitative branching time objectives[END_REF], the same complexity as for CTL * [START_REF] Moshe | Improved upper and lower bounds for modal logics of programs[END_REF].

Remark that neither pCTL * nor pECTL includes the path operators ∀ and ∃, thus these two logics are incomparable in expressivity with CTL * . For example, on the alphabet {a, b}, the CTL * formula φ 1 = ∀F G¬b, and the pCTL * formula φ 2 = P =1 (F G¬b) specify, that every branch, respectively almost-every branch, of the model has finitely many b. Neither φ 1 can be expressed in pCTL * nor φ 2 can be expressed in CTL * .

In this paper, we consider the logic CTL * [∃, ∀, P >0 , P =1 ] which is an extension of both CTL * and qualitative pCTL * and establish several properties of this logic.

The satisfiability by an arbitrary Σ-labelled Markov chain reduces to the satisfiability by (Σ ∪ {•})-labelled a binary tree with • a fresh letter (Theorem 25). The satisfiability of CTL * [∃, ∀, P >0 , P =1 ] reduces to the emptiness of alternating nonzero automata with finite choice for Adam thus it is decidable in 3-nexptime∩co-3-nexptime.

In the variant ECTL[∃, ∀, P >0 , P =1 ], where path formula are deterministic Büchi automata, this reduction gives a 2-nexptime∩ co-2-nexptime complexity and for the fragment CTL[∃, ∀, P >0 , P =1 ] the complexity is nexptime∩ co-nexptime (Theorem 24). For the fragments CTL * [P >0 , P =1 ], ECTL[P >0 , P =1 ] and CTL[P >0 , P =1 ] (i.e. qualitative pCTL * , pECTL and pCTL respectively), the F ∀ acceptance condition of the automaton is a Büchi condition and we retrieve the optimal complexity bounds of [START_REF] Brázdil | Controller synthesis and verification for markov decision processes with qualitative branching time objectives[END_REF][START_REF] Tomás; Brázdil | The satisfiability problem for probabilistic CTL[END_REF], i.e. 3exptime, 2-exptime and exptime, respectively.

Organization of the paper.

Section 2 introduces alternating nonzero automata, an example is given in Section 3. Section 4 focuses on non-deterministic automata, and provide an optimal algorithm to decide emptiness when the F ∀ condition is Büchi. In Section 5 we prove that emptiness is decidable (23) when Adam has limited choice. Section 6 presents our complexity results for the satisfiability of CTL * [∃, ∀, P >0 , P =1 ] and its variants and fragments.

Alternating nonzero automata

An alternating nonzero automaton on a finite alphabet Σ is a finite-state machine processing binary trees, equipped with a game semantics: every tree is either accepted or rejected by the machine depending on who wins the acceptance game on the tree.

Trees.

A Σ-labelled binary tree is a function t : {0, 1} * → Σ. An element n ∈ {0, 1} * is called a node of the tree and has exactly two sons n0 and n1. We use the usual notions of ancestors and descendants. A node n ′ is (strictly) below n if n is a (strict) prefix of n ′ . A path in the tree is a finite or infinite sequence of nodes n 0 , n 1 , . . . such that for every k the node n k+1 is a son of the node n k .

A branch b is an element of {0, 1} ω . If a node n is a prefix of b we say that n belongs to b or that b visits n. The set of branches is equipped with the uniform probability measure, denoted µ, corresponding to an infinite random walk taking at each step either direction 0 or 1 with equal probability 1 2 .

Automata.

An alternating nonzero automaton on alphabet Σ is presented as a tuple

A = (Q, q 0 , Q E , Q A , →, F ∀ , F 1 , F >0 ) where:
Q is a finite set of states, equipped with a total order ≤, containing the initial state

q 0 . (Q E , Q A ) is a partition of Q into Eve and Adam states.
→ is the set of transitions, there are two types of transitions: local transitions are tuples (q, a, q ′ ) with q, q ′ ∈ Q and a ∈ Σ, denoted q → a q ′ . split transitions are tuples (q, a, q 0 , q 1 ) ∈ Q × Σ × Q 2 , denoted q → a (q 0 , q 1 ). F ∀ , F 1 and F >0 are subsets of Q defining the acceptance condition.

The input of such an automaton is an infinite binary tree t : {0, 1} * → Σ. The source (resp. the target) of a local transition q → a q ′ is q (resp q ′ ). The source (resp. the targets) of a split transition q → a (q 0 , q 1 ) is q (resp q 0 and q 1 ). A state is said to be controlled by Eve or Adam whether it belongs to Q E or Q A . The controller of a transition is the controller of its source state. We always assume that (HC) the automaton is complete: for every state q and letter a there is at least one transition with source q on a.

The (HC) condition makes it easier to define the game semantics of the automaton.

Game semantics.

The acceptance of an input binary tree by the automaton is defined by mean of a stochastic game between Eve and Adam called the acceptance game.

The game of acceptance of a binary tree t : {0, 1} * → Σ by A is a two-player stochastic game with perfect information played by two strategic players Eve and Adam. The vertices of the game are all pairs (n, q) where n ∈ {0, 1} * is a node of the infinite binary tree and q is a state of the automaton. The game starts in the initial vertex (ǫ, q 0 ).

Each vertex (n, q) is controlled by either Eve or Adam depending whether q ∈ Q E or q ∈ Q A . The controller of the current state chooses any transition with source q and letter t(n). Intuitively, depending whether the transition is a local or a split transition, the automaton stays on the current node n or move with equal probability 1 2 to either node n0 or n1. If the transition is a local transition q → t(n) q ′ , the new vertex of the game is (n, q ′ ). If the transition is a split transition q → t(n) (r 0 , r 1 ) then the new vertex is chosen randomly with equal probability 1 2 between vertices (n0, r 0 ) or (n1, r 1 ). A play is a finite or infinite sequence of vertices π = (n 0 , q 0 )(n 1 , q 1 ) . . .. We denote first(π) = (n 0 , q 0 ) and last(π) = (n k , q n ) (for finite plays).

A strategy for Eve associates with every finite play whose last vertex is controlled by Eve a transition with source q n and letter t(n k ) (such a transition always exists since the automaton is complete). Strategies for Adam are defined in a symmetric way. Strategies of Eve are usually denoted σ while strategies for Adam are denoted τ .

Measuring probabilities.

Once both players Eve and Adam have chosen some strategies σ and τ , this defines naturally a non-homogenous Markov chain whose states are the vertices of the game. According to Tulcea theorem, if we equip the set of plays with the σ-field generated by cylinders, then there is a unique probability measure P σ,τ such that after a play π = (n 0 , q 0 ) . . . (n k , q k ), if δ(π) denotes the transition chosen by Eve or Adam after π (depending whether q k ∈ Q E or q k ∈ Q A ), the probability to go to vertex (n k+1 , q k+1 ) is:

                 1 if δ(π) is the local transition q k → t(n k ) q k+1 , 1 2 if δ(π) is the split transition q k → t(n k ) (r 0 , r 1 )
and

n k+1 = n k 0 and q k+1 = r 0 ; or n k+1 = n k 1 and q k+1 = r 1 .
0 otherwise .

This way we obtain a probability measure P σ,τ on the set of infinite plays.

Consistency and reachability.

If a finite play π is the prefix of another finite or infinite play π ′ we say that π ′ is a continuation of π. A finite π play is consistent with a strategy σ or, more simply, is a σ-play if there exists a strategy τ such that π may occur in the non-homogenous Markov chain induced by σ and τ . In this case, the number N of split transitions which occurred in π is exactly the depth of the node of last(π) and

P σ,τ ({ continuations of π }) = 2 -N .
A vertex w is σ-reachable if there exists a finite σ-play from the initial vertex to w. An infinite play is consistent with σ if all its prefixes are.

Bounded vs. unbounded plays.

There are two kinds of infinite plays: bounded plays are plays whose sequence of nodes is ultimately constant, or equivalently which ultimately use only local transitions while unbounded plays use infinitely many split transitions. Bounded plays consistent with σ and τ are the atoms of P σ,τ : a play π is bounded and consistent with σ and τ iff P σ,τ ({π}) > 0.

In this paper we will focus on subclasses of automata whose structural restrictions forbids the existence of bounded plays (see the (NLL) hypothesis below).

So in practice, every play π = (n 0 , q 0 )(n 1 , q 1 ) . . . we consider will visit a sequence of nodes n 0 , n 1 , n 2 , . . . which enumerates all finite prefixes of an infinite branch b ∈ {0, 1} ω of the binary tree, in a weakly increasing order: for every index i either n i+1 = n i (the player controlling (n i , q i ) played a local transition) or n i+1 = n i d for some d ∈ {0, 1} (the player controlling (n i , q i ) played a split transition and the play followed direction d).

Winning strategies.

Whether Eve wins the game is defined as follows. The limsup of an infinite play (n 0 , q 0 )(n 1 , q 1 ) . . . is lim sup i q i i.e. the largest automaton state visited infinitely often. An infinite play π ′ is a positive continuation of π if all states of π ′ visited after π belongs to F >0 .

Eve wins with σ against τ if the three following conditions are satisfied. Sure winning. Every play consistent with σ and τ has limsup in F ∀ .

Almost-sure winning. Almost-every play consistent with σ and τ has limsup in F 1 .

Positive winning. For every finite play π consistent with σ and τ whose last state belongs to F >0 , the set of positive continuations of π has nonzero probability.

We say that Eve wins the acceptance game if she has a winning strategy i.e. a strategy which wins the acceptance game against any strategy of Adam.

Büchi conditions.

A Büchi condition is a set of states R ⊆ Q which is upper-closed with respect to ≤ . Then a play has limsup in R iff it visits R infinitely often.

Language of an automaton.

◮ Definition 1 (Acception and language). A binary tree is accepted by the automaton if Eve has a winning strategy in the acceptance game. The language of the automaton is the set of its accepted trees.

We are interested in the following decision problem:

Emptiness problem: Given an automaton, decide whether its language is empty or not.

The use of game semantics makes the following closure properties trivial.

◮ Lemma 2 (Closure properties). The class of languages recognized by alternating nonzero automata is closed under union and intersection.

Normalization.

We assume all automata to be normalized in the sense where they satisfy:

(N1) every split transition whose source is in F >0 has at least one successor in F >0 ; and (N2) every local transition whose source is in F >0 has its target in F >0 as well.

We can normalize an arbitrary automaton by removing all transitions violating (N1) and (N2). This will not change the language because such transitions are never used by positively winning strategies of Eve. This normalization could lead to a violation of the completeness hypothesis, (HC). In this case we can also delete the corresponding states without modifying the language of the automaton.

If one would drop (HC) then the game graph may have dead-ends and the rules of the game would have to be extended to handle this case, typically the player controlling the state in the dead-end loses the game. This extension does not bring any extra expressiveness to our model of automaton, we can always make an automaton complete by adding local transitions leading to losing absorbing states.

Moreover, we assume: (N3) F 1 ⊆ F ∀ . This is w.l.o.g. since replacing F 1 with F 1 ∩ F ∀ does not modify the language of the automaton.

3

An example: the language of PUCE trees A tree t on the alphabet {a, b} is positively ultimately constant everywhere (PUCE for short) if for every node n, i) the set of branches visiting n and with finitely many a-nodes has > 0 probability; and ii) the set of branches visiting n and with finitely many b-nodes has > 0 probability.

No regular tree is PUCE.

There are two cases. If the regular tree has a node n which is the root of a subtree labelled with only a or b then clearly the tree is not PUCE. Otherwise, by a standard pumping argument, every node labelled a (resp. b) has a descendant labelled b (resp. a) at some depth ≤ |S|, where S is the set of states of the regular tree. But in this second case from every node n there is probability at least 1 2 |S| to reach a descendant with a different label, thus almost-every branch of the regular tree has infinitely many a and b, and the tree is not PUCE either.

There exists a PUCE tree.

However it is possible to build a non-regular tree t whose every node satisfies both i) and ii). For that, we combine together two partial non-regular trees. Let H ⊆ {0, 1} * be a subset of nodes such that a) the set of branches which visit no node in H has probability 1 2 , b) no node of H is a strict ancestor of another node in H (H is a cut), c) every node in {0, 1} * is either a descendant or an ancestor of a node in H. For example we can choose XX:7 H = {00, 100, 0100, 11000, 011000, 1010000, 11100000, 010100000, 011100000, . . .}.

To obtain t, we combine two partial trees t a and t b whose domain is {0, 1} * \ H and t a is fully labeled with a while t b is fully labelled with b. Since H is a cut, the nodes in H are exactly the leaves of t a and t b . To obtain t, we plug a copy of t b on every leaf of t a and a copy of t a on every leaf of t b . Then from every node, according to c) there is non-zero probability to enter either t a or t b and according to a) there is non-zero probability to stay in there forever.

An automaton recognizing PUCE trees.

We can design one automaton for each of the two conditions and combine them together with an extra state controlled by Adam (cf proof of Lemma 2).

We provide an alternating nonzero automaton checking condition ii), the automaton for condition i) is symmetric. The state space is:

Q = {s < w < g < ♯} .
Intuitively, Adam uses states s to search for a node n from which condition i) does not hold. Once on node n, Adam switches to state w and challenges Eve to find a path to an a-node n ′ which is the root of an a-labelled subtree T n of > 0 probability. For that Eve navigates the tree in state w to node n ′ , switches to state g on node n ′ , stays in g as long as the play stays in T n and switches definitively to ♯ whenever leaving T n .

Formally, the only state controlled by Adam is s, i.e. Q A = {s}, from which Adam can choose, independently of the current letter, between two split transitions s → (s, ♯) and s → (♯, s) and a local transition s → w. The state ♯ is absorbing. From state w, Eve can guess the path to n ′ using the split transitions:

w → (♯, w) w → (w, ♯) .
Once n ′ is reached Eve can switch to state g with a local transition w → g and, whenever the current node is an a-node, she can choose among three split transitions:

g → a (g, g) g → a (g, ♯) g → a (♯, g) .
The acceptance conditions are:

F ∀ = F 1 = Q \ {w} F >0 = {g} ,
so that from w Eve is forced to eventually switch to g (otherwise lim sup = w ∈ F ∀ ) and the a-subtree labelled by g must have positive probability for Eve to win. Adam may never exit the pathfinding state s, in which case Eve wins.

Non-deterministic nonzero automata

Non-deterministic zero automata were introduced in [3], followed by a variant of equivalent expressiveness, non-deterministic nonzero automata [5, Lemma 5]. In those automata, Adam is a dummy player, i.e. Q A = ∅ and moreover all transitions are split-transitions.

◮ Theorem 3. The emptiness problem for non-deterministic nonzero automata is in np∩conp.

If F ∀ is a Büchi condition then emptiness can be decided in ptime.

The first statement is established in [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF]Theorem 3]. The second statement is proved in the appendix. The proof idea is as follows. Assume the alphabet to be a singleton, which is w.l.o.g. for non-deterministic automata. The existence of a winning strategy for Eve can be witnessed by a subset W ⊆ Q which contains the initial state and two positional winning strategies σ 1 , σ 2 : W → W × W . Strategy σ 1 should be almost-surely and positively winning while strategy σ 2 should be surely winning. These two strategies can be combined into a (non-positional) strategy for Eve which satisfies the three objectives, thus witnesses non-emptiness of the automaton.

Deciding emptiness of automata with limited choice for Adam

In this section, we introduce the class of automata with limited choice for Adam, and show that emptiness of these automata is decidable.

For that we rely on a characterization of positional strategies of Eve which satisfy the surely and almost-surely winning conditions (Lemma 12, Lemma 13) and the positively winning condition (Lemma 18). Then we represent the positional strategies of Eve as labelled trees, called strategic trees (Definition 19). Finally we show that the language of strategic trees whose corresponding positional strategy is winning can be recognized by a non-deterministic nonzero automaton (Theorem 20).

Automata with limited choice for Adam

In the rest of the paper, we focus on the class of automata with limited choice for Adam. Our motivation is that these automata capture the logic we are interested in and their acceptance games have good properties. In particular the existence of positional winning strategies for Eve is one of the key properties used to decide emptiness.

To define the class of automata with limited choice for Adam, we rely on the transition graph of the automaton.

◮ Definition 4 (Equivalent and transient states). The transitions of the automaton define a directed graph called the transition graph and denoted G → . The vertices of G → are Q and the edges are labelled with Σ, those are all triplets (q, a, r) such that q → a r is a local transition or such that q → a (r, q ′ ) or q → a (q ′ , r) is a split transition for some state q ′ . Two states q, r are equivalent, denoted q ≡ r, if they are in the same connected component of G → .

A state is transient if it does not belong to any connected component of G → , or equivalently if there is no cycle on this state in G → .

◮ Definition 5. An automaton has limited choice for Adam if for every state q controlled by Adam, all transitions with source q are local transitions; and for every letter a, at most one of the (local) transitions q → a q ′ satisfies q ≡ q ′ . Such a transition is called a canonical transition.

In a limited choice for Adam automaton, the only freedom of choice of Adam, apart from playing canonical transitions, is deciding to go to a lower connected component of the transition graph. This non-canonical decision can be done only finitely many times, hence the name limited choice.

In the classical (non-probabilistic) theory of alternating automata, similar notions of limited alternation have already been considered, for example hesitant alternating automata [START_REF] Kupferman | An automata-theoretic approach to branching-time model checking[END_REF].

◮ Definition 6 (Canonical plays and transient vertices).

A canonical play is a play in which Adam only plays canonical transitions. A vertex (n, q) of an acceptance game is transient if it has no immediate successor (n ′ , q ′ ) (by a local or a split transition) such that q ≡ q ′ . In the acceptance game of an automaton with limited choice for Adam, every infinite play visit finitely many transient vertices and has a canonical suffix.

The no local loop assumption.

We assume that every automata with limited choice for Adam also satisfies:

(NLL) the automaton has no local loop: there is no letter a and sequence of local transitions q 0 → a q 1 → a • • • → a q i such that q 0 = q i . Under the hypothesis (NLL), for every infinite play π there is a unique branch of the binary tree b ∈ {0, 1} ω whose every prefix is visited by π. We say that π projects to b.

Assuming (NLL) does not reduce expressiveness.

◮ Lemma 7. Given an automaton A with limited choice for Adam and set of states Q one can effectively construct another automaton A ′ with limited choice for Adam satisfying (NLL) and recognizing the same language.

The interest of the (NLL) assumption is to make the acceptance game acyclic, which in turn guarantees positional determinacy for Eve, as shown in the next section.

The transformation performed in the proof of Lemma 7 creates an exponential blowup of the state space of the automaton, which is bad for complexity. We could do without this blowup by dropping the (NLL) assumption, in which case Eve might need one extra bit of memory in order to implement local loops with priority in

F ∀ \ F 1 .
However, we prefer sticking to the (NLL) assumption, which makes the alternating automata and their accepting games simpler and is anyway not restrictive when it comes to translating temporal logics into alternating automata: the natural translation produces automata with no local loop.

Another interest of the (NLL) assumption is:

◮ Lemma 8.
Assume the automaton has the (NLL) property. Let µ be the uniform measure on the set of branches of the infinite binary tree, equipped with the usual Borel σ-field. Let t be an input tree, σ and τ be two strategies in the corresponding acceptance game and X be a measurable set of plays consistent with σ and τ . Let Y ⊆ {0, 1} ω be the set of infinite branches that X projects to. If X is measurable then Y is measurable and

P σ,τ (X) = µ(Y ) .

Positional determinacy of the acceptance game

A crucial property of automata with limited choice for Adam is that their acceptance games are positionally determined for Eve.

◮ Definition 9 (Positional strategies). A strategy σ of Eve in an acceptance game is positional if for every finite plays π, π ′ whose last vertices are controlled by Eve and coincide, i.e. last(π

) = last(π ′ ) ∈ {0, 1} * × Q E , then σ(π) = σ(π ′ ).
◮ Lemma 10 (Positional determinacy for Eve). Every acceptance game of an automaton with limited choice for Adam is positionally determined for Eve: if Eve wins then she has a positional winning strategy.

Sketch of proof.

Since the (NLL) hypothesis is assumed, the underlying acceptance game is acyclic. The construction of a positional winning strategy σ ′ from a (non-positional) winning strategy σ relies on the selection of a canonical way of reaching a σ-reachable vertex w with a σ-play π(w) and setting σ ′ (w) = σ(π(w)). ◭

On winning positional strategies of Eve

In the next section we show how to use use automata-based techniques to decide the existence of a (positional) winning strategy for Eve. These techniques rely on characterizing whether a positional strategy of Eve is surely, almost-surely and positively winning.

Surely and almost-surely winning conditions

We characterize (almost-)surely winning strategies.

◮ Definition 11 (q-branches). Let q ∈ Q and σ a strategy. An infinite branch of the binary tree is a q-branch in σ if at least one σ-play which projects to this branch has limsup q.

◮ Lemma 12. Assume the automaton has limited choice for Adam. Let σ be a positional strategy for Eve. Then σ is surely winning iff for every q ∈ (Q \ F ∀ ) there is no q-branch in σ. Moreover σ is almost-surely winning iff for every q ∈ (Q \ F 1 ) the set of q-branches in σ has measure 0.

Proof. We denote µ the uniform probability measure on {0, 1} ω . For every state q, Y q denotes the set of q-branches in σ.

We show the first statement about sure winning. For every σ-play π there exists a strategy τ of Adam such that π is consistent both with σ and τ . Thus there is q ∈ (Q \ F ∀ ) such that Y q = ∅ iff there is a strategy τ of Adam and a play consistent with σ and τ with limsup in Q \ F ∀ , iff σ is not accepting.

We show that the condition ∀q ∈ Q \ F 1 , µ(Y q ) = 0 is sufficient for σ to be almost-surely winning. Let τ be a strategy of Adam and Y ′ the set of branches of plays consistent with σ and τ which have limsup in Q \ F 1 . Then Y ′ ⊆ q∈Q\F1 Y q . According to Lemma 8,

P σ,τ (lim sup ∈ F 1 ) = µ(Y ′ ) ≤ µ q∈Q\F1 Y q = 0.
Thus σ is almost-surely winning. We show that the condition µ(Y q ) > 0 for some q ∈ Q \ F 1 is sufficient for σ not to be almost-surely winning. For every infinite branch b ∈ Y q choose one σ-play π b with lim sup ∈ Q \ F 1 . Since the automaton has limited choice for Adam, a suffix of π b is canonical, let w b be the first vertex of this suffix. For every σ-reachable vertex w denote Z w = {b ∈ Y q | w b = w}. Since Y q is the countable union of the sets (Z w ) w σ-reachable there is at least one σ-reachable vertex w such that µ(Z w ) > 0. Let π w be a finite σ-play to w. Let τ w a strategy for Adam which enforces π w with positive probability and plays canonically in every continuation of π w whenever possible. We show that P σ,τw (lim sup ∈ F 1 ) > 0. Let X w be the set of continuations of π w consistent with σ and τ w whose branch belongs to Z w . An easy induction shows that every play π ′ ∈ X w with branch b coincide with π b after w b (σ is positional and τ w plays only canonical moves). Thus every play in X w has lim sup ∈ Q \ F 1 . Then P σ,τw (lim sup ∈ F 1 ) ≥ P σ,τw (X w ) = µ(Z w ) > 0, according to Lemma 8. ◭ Whether a branch is a q-branch can be checked by computing a system of σ-indexes. Intuitively, all σ-reachable vertices receives a finite index, such that along a σ-play the index does not change except when Adam performs a non-canonical move or when two plays merge on the same vertex, in which case the smallest index is kept. After a non-canonical move of Adam, a new play may start in which case it receives a fresh index not used yet in the current neither in the parent node. For this less than 2|Q| indices are required. The important properties of σ-indexes are: ◮ Lemma 13 (Characterization of q-branches). Every positional strategy σ of Eve can be associated with a function

index σ : {0, 1} * × Q → {0, 1, . . . , 2|Q|, ∞} Q with the following properties.
First, index σ can be computed on-the-fly along a branch. For every node n denote σ n the restriction of σ on {n} × Q. Then index σ (ǫ) only depends on σ ǫ . And for every node n and d ∈ {0, 1}, index σ (nd) only depends on index σ (n) and σ nd .

Second, a vertex (n, q) is reachable from the initial vertex by a σ-play iff index σ (n)(q) is finite.

Third, let b ∈ {0, 1} ω be an infinite branch of the binary tree, visiting successively the nodes n

0 , n 1 , n 2 , . . .. Denote R ∞ (b) the set of pairs (k, q) ∈ {0, . . . , 2|Q|} × Q such that: k ∈ index σ (n i )(Q)
for every i ∈ N except finitely many; and k = index σ (n i )(q) for infinitely many i ∈ N.

Then for every state q, the branch b is a q-branch if and only if there

exists k ∈ {0, 1, . . . , 2|Q|} such that q = max{r ∈ Q | (k, r) ∈ R ∞ (b)}.

Checking the positively winning condition

In order to check with a non-deterministic automaton whether a positional strategy is positively winning, we rely on the notion of positive witnesses. The point of positive witnesses is to turn the verification of up to |Q| positively-winning conditions -depending on the decisions of Adam, there may be up to |Q| different σ-reachable vertices on a given nodeinto a single one. This single condition can then be checked by a non-deterministic nonzero automaton equipped with a single positively-winning condition.

Everywhere thick subtrees.

We need the notion of everywhere thick subtrees. We measure sets of infinite branches with the uniform probability measure µ on {0, 1} ω . ◮ Definition 14 (Subtree). A set of nodes T ⊆ {0, 1} * is a subtree if it contains a node r, called the root of T , such that every node n ∈ T is a descendant of r, T contains all nodes on the path from r to n.

◮ Definition 15 (Everywhere thick sets of nodes). For every set T ⊆ {0, 1} * of nodes denote T the set of branches in {0, 1} ω whose every prefix belongs to T . Then T is everywhere thick if starting from every node n ∈ T there is nonzero probability to stay in T , i.e. if µ T ∩ n{0, 1} ω > 0.

Everywhere thick subtrees are almost everywhere. ◮ Lemma 16. Let P ⊆ {0, 1} ω be a measurable set of infinite branches. Assume µ(P ) > 0. Then there exists an everywhere thick subtree T , with root ǫ such that T ⊆ P .

The proof relies on the inner-regularity of µ, so that P can be assumed to be a closed set, i.e. a subtree from which we can prune leaves whose subtree has probability 0.

Positive witnesses.

Positive witnesses can be used to check whether a strategy is positively winning: ◮ Definition 17 (Positive plays and witnesses). Let t be a Σ-labelled binary tree and σ a positional strategy of Eve in the acceptance game of t. Let Z be the set of σ-reachable vertices whose state is in F >0 .

A play is positive if all vertices it visits belong to {0, 1} * × F >0 . A positive witness for σ is a pair (W, E) where:

W ⊆ Z are the active vertices, E ⊆ {0, 1} * × {0,
) Let z = (n, q) ∈ W . Then (n, 0) ∈ E or (n, 1) ∈ E, or both. If z → z ′ is a local transition then z ′ ∈ W as well whenever (q ∈ Q E and z → z ′ is consistent with σ) or (q ∈ Q A and z → z ′ is canonical). If z is controlled by Eve and σ(z) is a split transition q → (q 0 , q 1 ) then ((n, 0) ∈ E =⇒ (n0, q 0 ) ∈ W ) and ((n, 1) ∈ E =⇒ (n1, q 1 ) ∈ W ). c) The set of nodes {nd ∈ {0, 1} * | (n, d) ∈ E} is everywhere thick.
◮ Lemma 18 (Characterization of positively winning strategies). Assume the automaton has limited choice for Adam. A positional strategy σ for Eve is positively winning iff there exists a positive witness for σ.

Deciding emptiness

A Σ-labelled binary tree t and a positional strategy σ in the corresponding acceptance game generate a tree

T t,σ : {0, 1} * → (Q ∪ Q × Q) QE .
For every vertex (n, q) controlled by Eve, if σ(n, q) is a local transition q → t(n) q ′ then T t,σ (n)(q) = q ′ and if σ(n, q) is a split transition q → t(n) (q 0 , q 1 ) then T t,σ (n)(q) = (q 0 , q 1 ).

◮ Definition 19 (Strategic tree). A tree

T : {0, 1} * → (Q ∪ Q × Q) QE is strategic if
there exists a tree t : {0, 1} * → Σ and a positional strategy σ for Eve such that T = T t,σ .

We are interested in the strategic trees associated to winning strategies. The rest of the section is dedicated to the proof of the following theorem.

◮ Theorem 20. Fix an alternating nonzero automata with limited choice for Adam. The language of strategic trees T t,σ such that σ wins the acceptance game of t can be recognized by a non-deterministic nonzero automaton of size exponential in |Q|. If F ∀ = Q in the alternating automaton, then the sure condition of the non-deterministic automaton is Büchi.

Proof. The characterizations of surely, almost-surely and positively winning strategies given in lemmas 12, 13 and 18 can be merged as follows.

◮ Corollary 21. Let σ be a positional strategy σ for Eve. For every branch b denote

M (b) = {max{q | (k, q) ∈ R ∞ (b)} | k ∈ 0 . . . 2|Q|} .

Then σ is winning if and only if

for every branch b, M (b) ⊆ F ∀ ; and for almost-every branch b, M (b) ⊆ F 1 ; and there exists a positive witness for σ.

First of all, the non-deterministic automaton B checks whether the input tree is a strategic tree, for that it guesses on the fly the input tree t : {0, 1} * → Σ by guessing on node n the value of t(n) and checking that for every q ∈ Q E , q → t(n) T (n)(q) is a transition of the automaton.

On top of that B checks the three conditions of Corollary 21. For the first two conditions, it computes (asymptotically) along every branch b the value of R ∞ (b) and thus of M (b). For that the automaton relies on a Last Appearance Record memory (LAR) [START_REF] Gurevich | Trees, automata, and games[END_REF] whose essential properties are:

◮ Lemma 22 (LAR memory [START_REF] Gurevich | Trees, automata, and games[END_REF]). Let C be a finite set of symbols. There exists a deterministic automaton on C called the LAR memory on C with the following properties. First, the set of states, denoted Q, has size ≤ |C| |C|+1 and is totally ordered. Second, for every u ∈ C ω denote L ∞ (u) the set of letters seen infinitely often in u and LAR(u) the largest state seen infinitely often during the computation on u. Then L ∞ (u) can be inferred from LAR(u), precisely there is a mapping φ :

Q → 2 C such that: ∀u ∈ C ω , L ∞ (u) = φ(LAR(u)) .
In order to compute R ∞ (b) along a branch b, the non-deterministic automaton B computes deterministically on the fly the σ-index of the current node n, as defined in Lemma 13, and implements a LAR memory on the alphabet

C = {0, . . . , 2|Q|} × (Q ∪ {⊥}) .
When visiting node n, B injects into the LAR memory all pairs (index σ (q), q) such that q ∈ Q and index σ (q) = ∞ plus all pairs (k, ⊥) such that k ∈ index σ (n)(Q). For every branch b, the set R ∞ (b) is equal to all pairs (k, q) seen infinitely often such that (k, ⊥) is seen only finitely often. Thus, the LAR memory can be used to check the first two conditions of Corollary 21, more details are given at the end of the proof.

For now, we describe how the non-deterministic automaton B checks whether there exists a positive witness (W, E) (Definition 17). Denote by Z the set of σ-reachable vertices whose state is in F >0 . On node n the automaton guesses (resp. computes) the vertices of W (resp. Z) of the current node and guesses the elements of E by storing three sets of states:

W n = {q ∈ Q | (n, q) ∈ W } Z n = {q ∈ F >0 | index σ (n, q) < ∞} E n = {b ∈ {0, 1} | (n, b) ∈ E} .
Then B checks all three conditions a), b) and c) in the definition of a positive witness as follows.

B checks condition a) in the definition of a positive witness by guessing on the fly for every vertex in Z a canonical positive σ-play to a vertex which is either transient or in W , in which case we say the canonical positive play terminates.

For that B maintains an ordered list P n of states. On the root node, P ǫ is Z ǫ \ W ǫ . When the automaton performs a transition, it guesses for each state q in P n and direction b q a successor s q , such that (nb q , s q ) can be reached from (q, n) by a positive canonical σ-play. In direction b, every state q for which b q = b is removed from the list, while every state q for which b q = b is replaced by the corresponding s q . Then all states in Z nb are added at the end of the list. In case of duplicates copies of the same state in the list, only the first copy is kept. In case the head of the list is in W nb or is transient, a Büchi condition is triggered and the head is moved at the back of the list. Finally all entries of the list which are in W nb are removed.

This way, condition a) holds iff the Büchi condition is triggered infinitely often on every branch. We discuss below how to integrate this Büchi condition in the sure accepting condition of the automaton.

B checks condition b) in the definition of a positive witness by entering an absorbing error state as soon as 1) there is some local transition (n, q) → t(n) (n, q ′ ) such that q ∈ W n and (q

∈ Q E and z → z ′ is consistent with σ) or (q ∈ Q A and z → z ′ is canonical); or
2) there is some q ∈ W n controlled by Eve and b ∈ E n such that σ(n, q) is a split transition q → t(n) (q 0 , q 1 ) but q b ∈ W nb . The guessed sets W n are bound to satisfy condition 1) and condition 2) is checked by storing a subset of Q.

B checks condition c) in the definition of a positive witness by triggering the positive acceptance condition whenever it moves in direction b on a node n such that b ∈ E n .

The sure and almost-sure acceptance condition are defined as follows. The Büchi condition necessary for checking condition a) in the definition of a positive witness is integrated in the LAR memory, for that we add to the alphabet C of the LAR memory a new symbol ⊤ which is injected in the LAR memory whenever the Büchi condition is triggered. The order between states of B is induced by the order of the LAR memory.

This way, according to Lemma 22, the largest state seen infinitely often along a branch b reveals whether ⊤ was seen infinitely often, and reveals the value of R ∞ (b) (the set of pairs (k, q) seen infinitely often such that (k, ⊥) was seen finitely often) hence of M (b) as well. The state is surely (resp. almost-surely) accepting iff ⊤ was seen infinitely often and M (b) ⊆ F ∀ (resp. M (b) ⊆ F 1 ). In case F ∀ = Q in the alternating automaton then the sure condition boils down to the Büchi condition.

According to Corollary 21, and by construction of B, the computation of B is accepting iff the input is a strategic tree whose corresponding strategy of Eve is winning. ◭ ◮ Theorem 23. Emptiness of alternating nonzero automata with limited choice for Adam is decidable in nexptime∩co-nexptime. If F ∀ = Q, emptiness can be decided in exptime.

Proof. Emptiness of an alternating automaton reduces to the emptiness of a non-deterministic automaton of exponential size. This non-deterministic automaton guesses on-the-fly a tree {0, QE and checks it is a winning strategic tree, using the automaton given by Theorem 20. In case the alternating automaton is F ∀ -trivial, the sure condition of the non-deterministic automaton is Büchi (Theorem 20). We conclude with Theorem 3. ◭ 6 Satisfiability of CTL * [∃, ∀, P >0 , P =1 ]

1} * → (Q ∪ Q × Q)
Our result on alternating nonzero automata can be applied to decide the satisfiability of the logic CTL * [∃, ∀, P >0 , P =1 ], a generalization of CTL* which integrates both deterministic and probabilistic state quantifiers.

Markov chains.

The models of CTL * [∃, ∀, P >0 , P =1 ] formulas are Markov chains. A Markov chain with alphabet Σ is a tuple M = (S, p, t) where S is the (countable) set of states, p : S → ∆(S) are the transition probabilities and t : S → Σ is the labelling function. For every state s ∈ S, there is a unique probability measure denoted P M,s on S ω such that P M,s (sS ω ) = 1 and for every sequence

s 0 • • • s n s n+1 ∈ S * , P M,s (s 0 • • • s n s n+1 S ω ) = p(s n , s n+1 )•P M,s (s 0 s 1 • • • s n S ω
). When M is clear from the context this probability measure is simply denoted P s . A path in M is a finite or infinite sequence of states s 0 s 1 • • • such that ∀n ∈ N, p(s n , s n+1 ) > 0 .. We denote Path M (s 0 ) the set of such paths.

A binary tree t : {0, 1} * → Σ is seen as a specific type of Markov chain, where from every node n ∈ {0, 1} * there is equal probability 1 2 to perform transitions to n0 or n1.

Syntax.

For a fixed alphabet Σ, there are two kinds of formula: state formula (typically denoted ψ) and path formula (denoted φ), generated by the following grammar:

ψ ::=⊤ | ⊥ | a ∈ Σ | ψ ∧ ψ | ψ ∨ ψ | ¬ψ | ∃φ | ∀φ | P >0 (φ) | P =1 (φ) φ ::=ψ | ¬φ | φ ∧ φ | φ ∨ φ | Xφ | φU φ | Gφ .

Semantics.

Let M = (S, t, p) a Markov chain. We define simultaneously and inductively the satisfaction The satisfaction of a path formula φ by an infinite path w = s 0 s 1 • • • ∈ Path M (s 0 ) is defined as follows. If φ is produced by one of the rules ¬φ | φ ∧ φ | φ ∨ φ then its satisfaction is defined as usual. If φ is a state formula (rule φ := ψ) then w |= ψ if s 0 |= ψ . Otherwise, φ ∈ {Xφ ′ , Gφ ′ , φ 1 U φ 2 } where φ ′ , φ 1 and φ 2 are path formulas. For every integer k, we denote w

[k] the path s k s k+1 • • • ∈ Path M (s k ). Then: w |= Xφ ′ f w[1] |= φ ′ w |= Gφ ′ if ∀i ∈ N, w[i] |= φ ′ w |= φ 1 U φ 2 if ∃n ∈ N, (∀0 ≤ i < n, w[i] |= φ 1 ∧ w[n] |= φ 2 ).
The Markov chain given in Figure 1 satisfies the formula (∀(G∃(⊤U a))) ∧ (P >0 (G¬a)).

Variants and fragments.

A formula of CTL 1 -

1 2 2 1 2 3 1 - 1 2 3 1 2 n 1 - 1 2 n Figure 1 A model of (∀(G∃(⊤U a))) ∧ (P>0(G¬a))
In the variant ECTL, every path formula φ is described as the composition of a deterministic Büchi automata on some alphabet {0, 1} k with k state subformulas. A path satisfies φ if the Büchi automaton accepts the sequence of letters obtained by evaluating the k state subformulas on every state along the path. This variant augments both the expressivity and the conciseness of the logic at the cost of a less intuitive syntax. For more details see [START_REF] Brázdil | Controller synthesis and verification for markov decision processes with qualitative branching time objectives[END_REF].

We are also interested in the fragments where the operators ∃ and ∀ are not used, i.e. the qualitative fragments of the logics pCTL * , pECTL and pCTL.

Satisfiability problem.

A Markov chain M satisfies a formula ξ at state s, or equivalently (M, s) is a model of ξ, if M, s |= ξ. We are interested in the problem:

MC-SAT: given a formula, does it have a model?

The satisfiability of tmso+zero is known to be decidable [START_REF] Bojańczyk | Thin MSO with a probabilistic path quantifier[END_REF][START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF]. Since CTL * [∃, ∀, P >0 , P =1 ] is a fragment of tmso+zero, MC-SAT is decidable with non-elementary complexity. A reduction to the emptiness of alternating nonzero automata gives better complexity: ◮ Theorem 24. For CTL * [∃, ∀, P >0 , P =1 ] the satisfiability problem is in 3-nexptime ∩ co-3-nexptime. The following table summarizes complexities of the satisfiability problem for various fragments and variants of CTL * [∃, ∀, P >0 , P =1 ]:

[∃, ∀, P>0, P=1] [P>0, P=1] CTL * 3-nexptime ∩ co-3-nexptime 3-exptime [7] (qualitative pCTL * ) ECTL 2-nexptime ∩ co-2-nexptime 2-exptime [7] (qualitative pECTL) CTL nexptime ∩ co-nexptime exptime [6] (qualitative pCTL)
According to [START_REF] Tomás; Brázdil | The satisfiability problem for probabilistic CTL[END_REF][START_REF] Brázdil | Controller synthesis and verification for markov decision processes with qualitative branching time objectives[END_REF], the complexities for ECTL[P >0 , P =1 ] and CTL[P >0 , P =1 ] are optimal. The first step in the proof of Theorem 24 is a linear-time reduction from MC-SAT to:

BIN-SAT: given a formula, does it have a model among binary trees?

◮ Theorem 25. Any formula ξ of CTL * [∃, ∀, P >0 , P =1 ] on alphabet Σ can be effectively transformed into a formula ξ ′ of linear size on alphabet Σ ∪ {•} such that ξ is MC-SAT iff ξ ′ is BIN-SAT. As a consequence, MC-SAT linearly reduces to BIN-SAT. This transformation stabilizes the fragment CTL * [P >0 , P =1 ].

The second step is a standard translation from logic to alternating automata [START_REF] Kupferman | An automata-theoretic approach to branching-time model checking[END_REF].

◮ Lemma 26. For every formula ξ of CTL * [∃, ∀, P >0 , P =1 ] (resp. ECTL[∃, ∀, P >0 , P =1 ]), there is an alternating automaton A with limited choice for Adam whose language is the set of binary trees satisfying the formula at the root. The automaton is effectively computable, of size O(2 2 |ξ| ) (resp. O(2 |ξ| )). If ξ is a CTL formula, the size of A is O(|ξ|). In case the formula does not use the ∃ and ∀ operators, the F ∀ condition is trivial i.e. F ∀ = Q.

XX:17

Proof of Theorem 24. All the complexity results are obtained by reduction of MC-SAT to the emptiness problem for an alternating nonzero automaton with limited choice for Adam, which is decidable in nexptime∩co-nexptime (Theorem 23). The size of the automaton varies from doubly-exponential to linear size depending whether the formula is in CTL * , ECTL or CTL (Lemma 26). In case the formula does not use the deterministic operators ∃ and ∀ (i.e. for qualitative pCTL * , pECTL and pCTL) the F ∀ condition of the alternating automaton is trivial thus its emptiness is decidable in exptime (Theorem 23). ◭

Conclusion

We have introduced the class of alternating nonzero automata, proved decidability of the emptiness problem for the subclass of automata with limited choice for Adam and obtained as a corollary algorithms for the satisfiability of a temporal logic extending both CTL* and the qualitative fragment of pCTL*.

A natural direction for future work is to find more general classes of alternating nonzero automata with a decidable emptiness problem, which requires some more insight on the properties of the acceptance games.

Accepting runs

In a non-deterministic automaton, only Eve takes decisions. Once the strategy of Eve is fixed, there is for every node n a single vertex (n, q) which is σ-reachable, and the strategy of Eve can be represented as a mapping S : {0, 1} * → Q such that S(ǫ) = q 0 and for every node n, (S(n), S(n0), S(n1)) is a transition of the automaton. Such a mapping is called a run of the automaton.

Notions of sure, almost-sure and positive acceptance extend naturally to runs (see [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF] for full details).

Almost-sure policies

◮ Definition 27 (Policy). Let W ⊆ Q. A policy with domain W is a mapping σ : W → W 2 such that for every q ∈ W , q → σ(q) is a (split) transition of the automaton.

A policy σ induces a Markov chain M σ with states W , whose transition probabilities are defined as follows. From every state q ∈ W with σ(q) = (q 0 , q 1 ), if q 0 = q 1 there is probability 1 2 to go to either states q 0 or q 1 and if q 0 = q 1 there is probability 1 to go to the state q 0 = q 1 . ◮ Definition 28 (Almost-sure policies). A policy σ with domain W is almost-sure if: XX:20 Alternating Nonzero Automata the maximal state of every ergodic class of M σ is in F 1 , from every state in F >0 ∩ W there is a path in M σ staying in F >0 ∩ W and reaching an ergodic class included in F >0 .

We will use twice this auxiliary lemma.

◮ Lemma 29. Let σ 1 and σ 2 be two almost-sure policies with domains W 1 and W 2 . Then there exists an almost-sure policy with domain

W 1 ∪ W 2 . Proof. We define σ 3 (w) = σ 1 (w) if w ∈ W 1 σ 2 (w) otherwise
. Then σ 3 is a almost-sure policy. For that, remark that once a play in the Markov chain M σ3 enters W 1 it stays in W 1 . Thus every ergodic class of M σ3 is an ergodic class of either σ 1 or σ 2 ◭

The notion of almost-sure policy is similar to the notion of acceptance witnesses in [4, Definition 11], where is established the following result: ◮ Theorem 30. [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF]Theorem 10] Assume the non-deterministic automaton is F ∀ -trivial i.e. F ∀ = Q. Then it is non-empty iff there exists an almost-sure policy whose domain contains the initial state of the automaton. This is decidable in ptime.

Perfect plays

It is an exercice to design a sequence of integers 0 = n 0 ≤ n 1 ≤ n 2 ≤ . . . which is (very slowly) converging to ∞ and such that, starting from any vertex of any ergodic component of M σ , there is at least probability 1 2 that for every k, at step k every state of the ergodic component has already been visited at least n k times. This sequence can be constructed either explicitely, by elementary calculations, or using the inner-regularity of the probability measure (cf. [START_REF] Kechris | Classical descriptive set theory[END_REF]Theorem 17.10]).

Let M σ be a Markov chain induced by an almost-sure policy σ. A perfect play of σ is a path in M σ with the following properties: a) whenever the path enters F >0 , its stays in F >0 afterwards, b) each step of the path strictly reduces the distance to the ergodic classes , until such a class is reached, c) k steps after the entry inside an ergodic class, every state of the ergodic class has been visited at least n k times.

◮ Lemma 31 (Perfect plays happen with > 0 probability). For every almost-sure policy σ and every state q of its domain, the set of perfect plays starting from q has probability ≥ 1 2 |Q|+1 .

Proof. Properties a) and b) hold with probability at least 1 2 |Q| because by definition of almost-sure policies, there is at least one direction which reduces the distance to the ergodic classes, and moreover stays in F >0 once it enters F >0 . Property c) holds with probability at least 1 2 by choice of n 1 , n 2 , . . .. ◭

The F ∀ -Büchi case ◮ Lemma 32. Assume F ∀ is a Büchi condition. Then its language is non-empty iff there exists W ⊆ Q and two policies σ 1 , σ 2 with domain W such that: W contains the initial state of the automaton. σ 1 is almost-sure.

σ 2 guarantees infinitely many visits to F ∀ in the sense where every infinite play in M σ2 visits F ∀ infinitely often.

Proof. Similar proof techniques have been independently used in the framework of beyond worst-case synthesis [START_REF] Berthon | Threshold constraints with guarantees for parity objectives in markov decision processes[END_REF]. We first show that the conditions are sufficient. Eve can win by combining σ 1 and σ 2 into a strategy σ defined as follows. Eve starts with playing σ 1 and keeps playing σ 1 as long as the play is perfect. In case the play is not perfect anymore, Eve switches to σ 2 until F ∀ ∩ W is reached. Once F ∀ ∩ W has been reached, Eve switches again to σ 1 and keeps playing σ 1 as long as the suffix of the play since the last switch is perfect. Since there is probability ≥ 1 2 |Q|+1 that a play consistent with σ 1 is perfect (Lemma 31), almost-surely Eve switches only finitely many times to σ 2 , thus almost-surely a suffix of the play is perfect and consistent with σ 1 .

The strategy σ is almost-surely winning because almost every play consistent with σ has a perfect suffix. Such a suffix enters an ergodic component of M σ1 and visits all its states infinitely often. Since σ 1 is almost-surely winning, the maximal state of every of its ergodic components is in F 1 , thus almost-every play consistent with σ has limsup in F 1 .

Moreover σ is positively winning: the automaton is normalized thus every finite play π reaching F >0 has at least one infinite continuation π ′ in F >0 . In π ′ Eve eventually switches to σ 1 and with positive probability from this moment on the play is perfect thus eventually stays in an ergodic component of M σ1 intersecting F >0 . Such a component is actually included in F >0 because σ 1 is positively winning.

And σ is surely-winning. There are two types of plays. In plays where Eve switches infinitely often from one strategy to the other then infinitely many F ∀ states are visited, because switches from σ 2 to σ 1 occur precisely under this condition. And plays where Eve switches finitely often have a perfect suffix, and as already seen these plays have limsup in F 1 , which is included in F ∀ since the automaton is normalized.

To show that the conditions are necessary, start from a surely, almost-surely and positively accepting run S : {0, 1} * → Q. Let W be the image of S.

Remark that for every node n, the run S n : m → S(nm) is also almost-surely and positively accepting. Then according to Theorem 30, for every state q ∈ W , Eve has an almost-sure policy σ q whose domain contains q. According to Lemma 29, Eve has an almostsure policy σ 1 whose domain contains W . Now we construct σ 2 . Since S is surely accepting, then every branch of S visits F ∀ infinitely often. As a consequence, Eve wins the Büchi game to F ∀ where Eve chooses the transitions and Adam chooses the direction. The policy σ 2 is a positional winning strategy for Eve in this Büchi game. ◭

Proof of Theorem 3

The np∩conp upperbound is established by [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF]Theorem 3].

For the Büchi case, we show that the caracterization given in Lemma 32 can be decided in polynomial time, thanks to a fixpoint algorithm.

We can compute in polynomial time the largest domain X(W ) ⊆ W of an almostsure policy σ 1 , which exists according to Lemma 29. For every w ∈ W and W ⊆ Q, we denote A w,W the F ∀ -trivial automaton with initial state w and restricted to states in W and transitions in W × W 2 . For that for every w ∈ W we check whether the language of A w,W is empty or not, which can be done in ptime according to [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF]Theorem 10]. Then X(w) is exactly the union of all w for which A w,W has a non-empty language.

We can also compute in polynomial time the largest domain Y (W ) ⊆ W of a policy σ 2 which guarantees infinitely many visits to F ∀ . This simply amounts to computing the winning vertices of the Büchi game played on W where from state w ∈ W Eve chooses any transition w → (w 0 , w 1 ) with both w 0 ∈ W and w 1 ∈ W , loses if there is no such transition, and Adam selects either w 0 or w 1 . The play is won by Eve iff F ∀ is visited infinitely often. Now consider the largest fixpoint W ∞ of the monotonic operator on 2 Q defined by W → Y (X(W )) . We claim that W ∞ contains the initial state of the automaton if and only if the characterization given in Lemma 32 holds. Since W ∞ is a fixpoint, then W ∞ = X(W ∞ ) = Y (W ∞ ) thus there are policies σ 1 and σ 2 with domain W ∞ which satisfy the characterization. Conversely, if there is W and σ 1 and σ 2 which satisfy the characterization then W = X(W ) = Y (W ) thus by monotonicity , W ⊆ W ∞ . ◭

C Proof of Lemma 7

Let π be a path which arrives for the first time on a node n in a vertex (n, q), such that q belongs to some connected component C q . Let P be the player controlling q.

The exit-profile of π in σ is the set of pairs (q ′ , t) such that there is an extension of π consistent with σ which leaves node n in which t is the last transition played before leaving the node and q ′ is the largest state seen on the path from (n, q) up to now. The loop-profile is the set of states q ′ such that there is an extension of π consistent with σ which never leaves the current node n and has limsup q ′ . The set of possible exit-profiles and loop-profiles actually implementable by a strategy is easy to precompute, since only one bit of memory is needed to implement any implementable profile.

Then in A ′ , P announces an exit-profile and a loop-profile that she effectively can implement Her opponent P ′ picks up an element of these profiles. If this element is a cycle profile q ′ then the new state is the sink state (q ′ , * ) and the only transition available from there is a split transition staying in (q ′ , * ) on both directions. If this element is an exit profile (t, q ′ ) then the transition t is performed. The accepting sets are adapted in A ′ in order to have the natural correspondence between plays in A and plays in A ′ which preserves sure, almost-sure and positive winning conditions.

D Positional determinacy for Eve

Proof of Lemma 10. Fix an input tree t and an automaton A.

We show that if Eve has a winning strategy σ then she has a positional winning strategy. A finite σ-play π has a canonical σ-extension to some vertex w if π has a continuation π ′ consistent with σ, whose last vertex is w and in which Adam only play canonical moves after the prefix π. In other words, if after π Eve continues to play σ and Adam is bound to play only canonical moves then there is positive probability that the play reaches w.

We equip the set of finite plays with any total order such that the shorter is a play the smaller it is.

Let P be a player and σ a winning strategy for P . For every vertex w, denote f (w) the smaller play for the order among the plays starting in the initial vertex which have a canonical σ-extension to w. According to the (NLL) hypothesis, the game graph is acyclic, thus there are finitely many plays having a canonical σ-extension to w and f (w) is well-defined.

Denote l(w) = last(f (w)). Let g(w) be a finite play such that f (w)g(w) is a canonical σextension of f (w) to w. Remark that g(w) is uniquely defined: this is the unique continuation of f (w) in which Eve plays σ, Adam plays only canonical moves and the play follows the branch connecting the node of l(w) to the node of w. For every vertex w we define h(w) = f (w)g(w) .

The winning positional strategy σ ′ of Eve is defined by:

σ ′ (w) = σ(h(w)) .
This strategy σ ′ is well-defined because its definition inductively guarantees that a play consistent with σ ′ visits only σ-reachable vertices.

Let π = w 0 , w 1 , . . . = (n 0 , q 0 )(n 1 , q 1 ), . . . be an infinite play consistent with σ ′ . Remark first that, ( †) if all moves of Adam between some dates i ≤ j are canonical, then f (w t ) i≤t≤j is nonincreasing for the -order. The reason is that for every i ≤ t < j, the concatenation of g(w t ) and w t+1 is a canonical σ-extension of f (w t ) to w t+1 . Hence by minimality of f (w t+1 ), we get f (w t+1 ) f (w t ).

The sequence (q i ) i∈N is a path in the transition graph G → thus it ends up in a connected component C of G → . Let t π be minimum such that q tπ ∈ C. Then after date t π all moves of Adam in π are canonical. According to ( †), the sequence (f (w i )) i≥tπ is non-increasing. And the shorter is a play the smaller it is thus according to (NLL) this sequence takes finitely many values. Thus it becomes constant after some index, denote it k π and denote P (π) the prefix of π of length k π and S(π) the suffix of π such that π = P (π)S(π). By definition of σ ′ and since k π ≥ t π , ( † †) S(π) is canonical and h(w kπ )S(π) is a σ-play.

We show that σ ′ is winning. We fix for the rest of the proof a strategy τ for Adam and show that σ ′ is almost-surely and positively winning against τ .

For every finite play π 1 denote W (π 1 ) = {S(π) | π a play consistent with σ ′ and τ such that P (π) = π 1 } .

Then, according to ( † †), ( † † †) every play π ∈ W (π 1 ) is canonical and h(last(π 1 ))π is a σ-play.

As a consequence, σ ′ is surely-winning: let π be an infinite σ ′ -play then S(π) ∈ W (P (π)) thus according to ( † † †) the play S(π) is the suffix of a σ-play and since σ is surely-winning the limsup of S(π) is in F ∀ hence the limsup of π as well since π = P (π)S(π).

Fix some finite play π 1 consistent with σ and τ and focus on W (π 1 ). Let π ′ 1 = h(last(π 1 )). Let τ ′ a strategy for Adam such that π ′ 1 is consistent with τ ′ and after π ′ 1 happens, τ ′ performs canonical moves whenever possible. We show that for every measurable set of plays E,

P σ ′ ,τ (π 1 W (π 1 ) ∩ π 1 E) = P σ,τ ′ (π ′ 1 W (π 1 ) ∩ π ′ 1 E) . ( 1
)
According to ( † † †), for every play π 2 ∈ W (π 1 ), π 1 π 2 is consistent with σ ′ and τ and π ′ 1 π 2 is consistent with σ and τ ′ . Moreover, since π 1 and π ′ 1 have the same last vertex last(π 1 ) then the set of (σ ′ , τ )-plays in π 1 W (π 1 )∩π 1 E and the set of (σ, τ ′ )-plays in π ′ 1 W (π 1 )∩π ′ 1 E project to the same set of branches. Thus according to Lemma 8 the two probabilities coincide.

F

Existence of everywhere thick subtrees (Proof of Lemma 16)

Proof of Lemma 16. The uniform measure µ on {0, 1} ω is Borel with respect to the topology whose cylinders are the basis. This topology is metrizable thus µ is inner-regular (cf. [START_REF] Kechris | Classical descriptive set theory[END_REF]Theorem 17.10]). Hence P contains a closed set such that µ(P ) > 0, w.l.o.g. we assume that P itself is closed, i.e. P contains every branch whose every node is visited by a branch in P . Given a node n ∈ {0, 1} * we denote P n the set of branches of P visiting n, i.e. P n = P ∩ (n{0, 1} ω ). Let T be the set of nodes n such that µ(P n ) > 0. By hypothesis T contains ǫ. And T is prefix-closed thus it is a tree with root ǫ. And T ⊆ P because P is closed. We show that T is everywhere thick. Let n ∈ T . By definition, T ∩ (n{0, 1} ω ) = P n \ n ′ ∈T P n ′ . By definition of T , for every n ′ ∈ T , µ(

P n ′ ) = 0 thus since T is countable, µ( n ′ ∈T P n ′ ) = 0 hence µ( T ∩ (n{0, 1} ω )) = µ(P n ) > 0 since n ∈ T . ◭

G Characterization of positively winning strategies (Proof of Lemma 18)

For commodity, we recall the definition of a positive witness. Let Z be the set of σ-reachable vertices whose state is in F >0 . A positive witness for σ is a pair (W, E) where: W ⊆ Z are the active vertices, E ⊆ {0, 1} * × {0, 1} is the set of positive edges, and they have the following properties. a) From every vertex z ∈ Z there is a positive and canonical finite σ-play starting in z which reaches a vertex in W or a transient vertex. b) Let z = (n, q) ∈ W . Then (n, 0) ∈ E or (n, 1) ∈ E, or both. If z → z ′ is a local transition then z ′ ∈ W as well whenever (q ∈ Q E and z → z ′ is consistent with σ) or (q ∈ Q A and z → z ′ is canonical). If z is controlled by Eve and σ(z) is a split transition q → (q 0 , q 1 ) then ((n, 0) ∈ E =⇒ (n0, q 0 ) ∈ W ) and ((n, 1) ∈ E =⇒ (n1, q 1 ) ∈ W ). c) The set of nodes {nd ∈ {0, 1} * | (n, d) ∈ E} is everywhere thick.

We first show that existence of a positive witness is a sufficient condition for σ to be positively winning. Let (W, E) be a positive witness for σ. Let τ be any strategy for Adam and π be a play consistent with σ and τ whose last vertex z = (n, q) belongs to Z. We show that the set X of positive continuations of π consistent with σ and τ has nonzero probability under P σ,τ . We prove this by induction on q for the topological order of Q in the transition graph of the automaton. If one of the continuations in X reaches a vertex (n ′ , q ′ ) with q ′ < q then we conclude by inductive hypothesis. In the remaining case, note that (*) in all positive continuations of π consistent with σ and τ , the strategy τ only plays canonical moves. Let π ′ be the positive play whose existence is given by property a) in the definition of positive witnesses. Since π ′ is canonical, then according to (*), ππ ′ is consistent with τ thus ππ ′ belongs to X. Thus according to (*) again, π ′ does not reach any transient vertex, hence the last vertex (n ′ , q ′ ) of π ′ belongs to W . Let N E = {nd ∈ {0, 1} * | (n, d) ∈ E}. Let Y be the set of positive continuations of ππ ′ consistent with σ and τ and staying in N E × F >0 . Since Y ⊆ X then according to (*) all plays in Y are canonical . Thus according to property b) in the definition of nonzero-witnesses, all plays in Y stay in W after ππ ′ . According to b), subtree T ′ k ∩ T i,k-1 has probability 0. Then T ′ k \ i≤n k-1 T i,k-1 has the same measure than T ′ k , which is positive, thus it contains some everywhere thick subtree T ′′ (cf. Lemma 16). By definition of T ′ k there exists a vertex z at the root of T ′′ reachable from z k by a positive canonical σ-play. The collection C k is obtained by adding to C k-1 the new entry (T ′′ , {z}) at index n k = n k-1 + 1. Properties i)-v) are inherited from the inductive hypothesis, for what concerns C k-1 and j ∈ 0 . . . k -1 for item v). Properties i) and ii) are clear for the new entry (T ′′ , {z}) at i = n k . Property iii) holds for i = n k by definition of T ′ k and because z k ∈ Z ′ . Property iv) holds because of ii) and {z} is a singleton. Property v) holds for j = k by choice of z. Shrinking case. We are left with the case where W (k-1) is not reachable from z k by a positive canonical σ-play and there is i ∈ 0 . . . n k-1 such that the set of branches of the subtree T ′ k ∩ T i,k-1 has positive probability. Then n k = n k-1 and C k is the copy of k-1 except at rank i, where we replace T i,k-1 and X i,k-1 by T i,k ⊆ T i,k-1 and X i,k defined as follows. The tree T i,k is set to be any everywhere thick subtree contained in

T ′ k ∩ T i,k-1
, whose existence is given by Lemma 16. For every vertex x ∈ X i,k-1 ∪ {z k }, the node of x is either the root of T i,k-1 (when x ∈ X i,k-1 ) or the root of T ′ k (when

x = z k ). Since T i,k-1 ⊆ T ′ k ∩ T i,k-1
, the node of x is an ancestor of the root of T i,k . We show that there is a positive canonical σ-play π x from x to a vertex on the root of T i,k . In case x ∈ X i,k-1 because T i,k ⊆ T i,k-1 and property iii). In case x = z k because T i,k ⊆ T i,k-1 and by definition of T ′ k . Denote w(x) = last(π x ). We set

X i,k = {w(x) | x ∈ X i,k-1 ∪ {z k }} .
Remark that

|X i,k | = |X i,k-1 | + 1 . (4)
The reason for (4) is that, according to iv), all the vertices (w(x)) x∈X i,k-1 are distinct. And since {w(x) | x ∈ X i,k-1 } ⊆ W (k-1) and since we are not in the copy case then

w(z k ) ∈ {w(x) | x ∈ X i,k-1 }.
The construction of C k preserves invariants i) and ii) because (T i,k ) i∈1...n k is the copy of (T i,k-1 ) i∈1...n k-1 except for the tree T i,k which is everywhere thick by construction and contained in T i,k-1 . Invariant iii) is preserved for x = w(x ′ ), x ′ ∈ X i,k-1 since w(x) is reachable from X (k-1) by a canonical positive σ-play thus W w(x),k ⊆ W w(x),k-1 Invariant iii) is true for x = w(z k ) because T i,k ⊆ T ′ k thus from z k every canonical σ-plays is positive and since z k ∈ Z ′ then no transient vertex is reached by such a play. Invariant iv) is true by hypothesis on z k . Invariant v) is preserved for j ∈ 0 . . . k -1 because from every vertex in W (k-1) there is a positive canonical σ-play to a vertex in W (k) . And invariant v) is true for j

= k because z k ∈ X i,k ⊆ X (k) ⊆ W (k) .
Let I be the set of values taken by the sequence 1 = n 0 ≤ n 1 ≤ . . .. According to (4), the shrinking case can occur at most |Q| times at the same index i ∈ I (in the copy and expansion cases X i,k is not modified). Thus, if k is the smallest rank at which n k = i, the family (T i,k ′ , X i,k ′ ) k ′ ≥k takes at most |Q| different values and is ultimately constant from some rank k i .

We are now ready to define the positive witness (E, W ) using the family (T i,ki , X i,ki ) i∈I obtained "at the limit". Let E be the set of edges appearing in one of the trees of the family (T i,ki ) i∈I i.e.

E = i∈I {(n, b) | (n ∈ T i,ki ) ∧ b ∈ {0, 1} ∧ (nb ∈ T i,ki )} XX:28 Alternating Nonzero Automata and W = i∈I,x∈X i,k i W x,ki .
According to invariant iii), W is a set of positive vertices. To prove that (W, E) is a positive witness we should establish properties a) b) and c). Property a) is clear for vertices z ∈ Z\Z ′ , because by definition of Z ′ from these vertices there is a positive canonical σ-play to a transient vertex. And if z ∈ Z ′ then z = z k for some k and a) is a consequence of v).

We prove that property b) holds. Let z = (n, q) ∈ W then there is i ∈ I and x ∈ X i,ki such that z ∈ W x,ki . Then n ∈ T i,ki , by definition of the sets W x,ki . Since T i,ki is everywhere thick then n is not a leaf of T i,ki thus there exists d ∈ {0, 1} such that nd ∈ T i,ki hence (n, d) ∈ E. Let z → z ′ a local transition like in property b). Then, by definition of W x,ki , z ′ ∈ W x,ki thus z ′ ∈ W . Assume Eve controls q and σ(z) is a split transition (q 0 , q 1 ) and let d ′ such that (n, nd ′ ) ∈ E. Since x ∈ T i,ki then according to ii) and iv), also n ∈ T i,ki thus by definition of E also n ′ ∈ T i,ki . Then, by definition of W x,ki , z ′ ∈ W x,ki thus z ′ ∈ W .

Property c) holds. We show that

N E = {nd ∈ {0, 1} * | (n, d) ∈ E} is everywhere thick. Let n ∈ N E . By definition of E, there exists i ∈ I such that n ∈ T ki thus T ki ∩ n{0, 1} ω ⊆ N E ∩ n{0, 1} ω (
actually this is an equality according to ii)) and µ( N E ∩ n{0, 1} ω ) ≥ µ( T ki ∩ n{0, 1} ω ) > 0 since T ki is everywhere thick.

H

From MC-SAT to BIN-SAT: proof of Theorem 25

Theorem 25 is a corollary of Lemma 40 at the end of the section. Before translating formulas, we turn them in positive form, where the only negations are in front of letters of the alphabet. ◮ Lemma 33. Given a formula ξ one can build an equivalent formula in positive form whose size (as a DAG) is linear in the size of the first formula.

Proof. These transformations preserve the size of the DAG of the formula and its models:

¬¬φ → φ ¬P >0 (φ) → P =1 (¬φ) ¬⊤ → ⊥ ¬P =1 (φ) → P >0 (¬φ) ¬Xφ → (X¬φ) ¬∃φ → ∀¬φ ¬Gφ → (⊤U ¬φ) ¬∀φ → ∃¬φ ¬(φ 1 U φ 2 ) → G¬φ 2 ∨ (¬φ 2 U ¬φ 1 ) .

◭

From Markov chains to binary trees: adding the delay symbol •

There is a natural transformation of a Markov chain into a binary tree, which preserves the probability measure on Σ ω , up to some projection. This transformation simulates a single transition of the original Markov chain by an unbounded number of transitions of the binary tree. This requires to introduce in the alphabet of the binary tree, on top of the alphabet Σ of the Markov chain, a new delay symbol •. In the sequel we use the notation

Σ • = Σ ∪ {•} .
Every infinite path in the Markov chain labelled by a word u = a 0 a 1 a 2 • • • ∈ Σ ω corresponds to some infinite branch of the tree labelled by a word in a

0 {•} * a 1 {•} * a 2 • • • ∈ (Σ{•} * ) ω
Intuitively, the symbol • delays the stochastic process, but it should not delay it forever and is expected to appear a finite number of times between two occurences of a non-delay symbol in Σ, thus we are interested in Σ • -labelled Markov chains with finite delay.

Equivalence between Markov chain and binary trees

◮ Lemma 37 (Every chain is the projection of a binary tree). Let M = (S, t, p) be a Σlabelled Markov chain and s 0 a state of M. Then there exists a Σ • -labelled binary tree t • : {0, 1} * → Σ • and a projection π of t • to M such that π(ǫ) = s 0 .

Proof of Lemma 37. The tree t • and the projection mapping

π : {w ∈ {0, 1} * | t(w) = •} → S
are defined inductively. Initially we set π(ǫ) = s 0 and t • (ǫ) = t(s 0 ). Assume that π and t • are already defined for some node w ∈ {0, 1} * such that π(w) ∈ S. Denote s = π(w). We fix an enumeration (finite or infinite) of the successors of s in M.

{z 1 , z 2 , . . .} = {z ∈ S | p(s, z) > 0} .
For every z i we are going to define a subtree T i rooted on w such that the leaves of T i are mapped by π to z i (and thus are labelled by t(z i )) and the inner nodes of T i are labelled by •.

The construction of T i makes use of the usual continous mapping φ : {0, 1} * → [0, 1] which associates with every finite sequence of bits

δ 1 • • • δ n ∈ {0, 1} * the real number φ(δ 1 • • • δ n ) = 1≤k≤n δ i 2 i ∈ [0, 1[ .
We set p 0 = 0 and for every successor z i of s: p i = p(s, z 1 ) + . . . + p(s, z i )

T i = δ 1 • • • δ n ∈ {0, 1} + | φ(δ 1 • • • δ n {0, 1} * ) ⊆]p i-1 , p i [ L i = {δ 1 • • • δ n ∈ T i | δ 1 • • • δ n-1 ∈ T i } .
The definition of π is expanded to zi wL i , as follows.

∀δ 1 • • • δ n ∈ L i , π(wδ 1 • • • δ n ) = z i . ( 8
)
The condition [START_REF] Bojańczyk | Emptiness of zero automata is decidable[END_REF] in the definition of a projection holds: denote µ the uniform Lebesgue measure on [0, 1], then for every successor z i ,

P t•,w ({w, w 1 , • • • , w n ∈ S * • | t • (w 1 ) = . . . = t • (w n-1 ) = • and π(w n ) = z i }) = δ1•••δn∈Li P t•,w (reach node wδ 1 • • • δ n ) = δ1•••δn∈Li 1 2 n = δ1•••δn∈Li µ(φ(δ 1 • • • δ n {0, 1} * )) = µ(]p i-1 , p i [) = p i -p i-1 = p(s, z i ) .
The first equality is by inductive definition of π and t • , the second is by definition of a Markov binary tree, the third is a simple computation, as well as the two last ones. The fourth equality holds because the collection of intervals (φ(δ Assume that property [START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] holds for some path formula {φ ′ , φ 1 , φ 2 }. We show that (10) holds for φ ∈ {Xφ ′ , Gφ ′ , φ 1 U φ 2 }. Let w ∈ Path r M• , Since w visits infinitely many Σlabelled states, there is an infinite sequence of integers n 0 , n 1 , n 2 , . . . ∈ N such that t

• (w) = a 0 • n0 a 1 • n1 a 2 • • • . Then by definition of π, t(π(w)) = a 0 a 1 a 2 • • • . We set m 0 = 0 ≤ m 1 = 1 + n 1 ≤ m 2 = 1 + n 1 + 1 + n 2 ≤ . . . the positions where the symbols in Σ appear in w. Then ∀i ∈ N, π(w[m i ]) = π(w)[i] . ( 11
)
The equivalence [START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] This terminates the inductive proof of [START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF], under the hypothesis that ( 9) and ( 10) hold for sub-formula. The proof of (9) in case ψ = ∀φ ′ is similar. In case ψ = P ∼b (φ ′ ), we denote

L φ ′ = {s • s 1 • • • ∈ Path M• (s • ) | s • s 1 • • • |= φ ′ } L φ ′ = {ss 1 • • • ∈ Path M (s) | ss 1 • • • |= φ ′ } .
Then according to the induction hypothesis [START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] for φ ′ , ii) ξ is satisfiable by a binary tree with finite delay. iii) ξ ∧ P =0 (⊤U G•) is satisfiable by a binary tree. iv) ξ ∧ P =0 (⊤U G•) is satisfiable.

π -1 (L φ ′ ) = L φ ′ ∩ Path r M• (s • ) (12)
Proof. We do a circular proof. Assume that i) holds and prove ii). Then according to i) ξ is satisfiable by some Markov chain M = (S, t M , p) and state s 0 ∈ S such that M, s 0 |= ξ. According to Lemma 37, there exists a projection π from a (S ∪ {•})-labelled binary tree t • to M, such that π(ǫ) = s 0 . According to Lemma 39 t • , ǫ |= ξ, thus ii) holds. If ii) holds then iii) holds by definition of binary trees with finite delay. Clearly iii) implies iv). Assume that iv) holds and prove i). According to iv), ξ is satisfiable by some (Σ ∪ { Proof of Lemma 26. Given a state formula ψ in positive form we denote ψ the positive form of its negation and call it the dual of ψ.

We assume that the input formula ξ is positive, which is w.l.o.g according to Lemma 33. Let SF be the set of every state subformula of the input formula ξ, and their dual, including ⊤ and ⊥. Let PF be the set of path subformula of the state formula in SF.

With every path formula φ ∈ PF is associated a deterministic parity automaton on infinite words, denoted A φ . The alphabet of A φ depends on φ. Denote SF(φ) the collection of state formulas appearing in φ i.e. SF(φ) is the set of leaves of the syntactic tree of φ. Then the alphabet of A φ is the collection of subsets of SF(φ). The automaton A φ recognizes the sequences of valuations of the formula of SF(φ) for which the path formula φ is true. The construction of such an automaton of size O 2 2 is standard (see e.g. [START_REF] Kupferman | An automata-theoretic approach to branching-time model checking[END_REF]). Note that in the case of ECTL formulas, the construction is only of size O 2 |φ| since path formulas are directly given as deterministic Büchi automata.

States and transitions.

Every state formula ψ ∈ SF is also a state of the alternating automaton.

For every letter a ∈ Σ, the transitions from ψ = a or ψ = ¬a are local and deterministic:

a → a ⊤ ∀b = a, a → b ⊥ ¬a → a ⊥ ∀b = a, ¬a → b ⊤
Other transitions of the automaton do not depend on the label of the current node and are specified without mentioning the letter.

From states ψ = ψ 1 ∨ψ 2 and ψ = ψ 1 ∧ψ 2 there are local transitions ψ → ψ 1 and ψ → ψ 2 .

In the ∨ case the choice is made by Eve and in the ∧ case by Adam. For every formula in ψ ∈ {∃φ, ∀φ, P >0 (φ), P =1 (φ)}, there are states (ψ, q) q∈R φ , controlled by Eve, where R φ is the set of states of the automaton A φ . The state ψ is the source of a unique local transition to (ψ, i φ ), where i φ is the initial state of the automaton A φ . From (ψ, q) with q ∈ R φ , Eve can choose any subset b ⊆ SF(φ) and perform a local transition (ψ, q) → (ψ, q, b). Intuitively, for every state formula ψ 0 appearing in φ, Eve has to claim whether or not this formula holds in the current node by including or not ψ 0 in b. Adam controls (ψ, q, b) and faces a choice. Adam can ask for a proof of the valuation b by selecting a state formula ψ 0 ∈ SF (φ) and playing the local transition (ψ, q, b) → ψ 0 if ψ 0 ∈ b and (ψ, q, b) → ψ 0 if ψ 0 ∈ b. Adam can accept the valuation b and plays a local transition (ψ, q, b) → (ψ, q ′ , E) where q → b q ′ is the deterministic transition of A ψ on letter b. From there Eve has to choose a split transition, her options depend on the exact type of ψ: * If ψ = ∀φ or ψ = P =1 (φ) the only option for Eve is the split transition to ((ψ, q ′ ), (ψ, q ′ )). * If ψ = ∃φ then Eve can choose between two split transitions leading to either ( ⊤ , (ψ, q ′ ) ) or ( (ψ, q ′ ) , ⊤ ) . * If ψ = P >0 (φ) then Eve can choose between three split transitions leading to either ( (ψ, q ′ ) , (ψ, q ′ ) ) or ( ♯ , (ψ, q ′ ) ) or ( (ψ, q ′ ) , ♯ ) , where ♯ is the special absorbing pruning state. Also states ⊤ and ⊥ are absorbing.

Remark that his automaton has finite choice for Adam, the canonical choice for Adam is to accept the valuation proposed by Eve, otherwise the automaton moves to a subformula.

  1} is the set of positive edges, and they have the following properties. a) From every vertex z ∈ Z there is a positive and canonical finite σ-play starting in z which reaches a vertex in W or a transient vertex. b

  M, s |= ψ of a state formula ψ by a state s ∈ S and the satisfaction M, w |= φ of a path formula φ by a path w ∈ Path M . When M is clear from the context, we simply write s |= ψ and w |= φ. If a state formula is produced by one of the rules ⊤ | ⊥ | p | ψ ∧ ψ | ψ ∨ ψ | ¬ψ, its satisfaction is defined as usual. If φ is a path formula and ξ ∈ {∃φ, ∀φ, P >0 (φ), P =1 (φ)} then s |= ∃φ if ∃w ∈ Path M (s), w |= φ s |= ∀φ if ∀w ∈ Path M (s), w |= φ s |= P ∼b (φ) if P M,s (w ∈ Path M (s) | w |= φ) ∼ b .

  holds for φ = Xφ ′ because (M • , w |= Xφ ′ ) ⇐⇒ (M • , w |= X(•U φ ′ )) (by definition of φ ′ ) ⇐⇒ (M • , w[m 1 ] |= φ ′ ) (by definition of m 1 ) ⇐⇒ (M, π(w[m 1 ]) |= φ ′ ) (by induction hypothesis)⇐⇒ (M, π(w)[START_REF] Baier | Probabilistic ω-automata[END_REF] |= φ ′ ) (according to[START_REF] Gurevich | Trees, automata, and games[END_REF])⇐⇒ (M, π(w) |= Xφ ′ ) (by definition of |= Xφ ′ ) .With the same arguments, the equivalence[START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] holds for φ = Gφ ′ because (M • , w |= Gφ ′ ) ⇐⇒ (M • , w |= G(• ∨ φ ′ )) ⇐⇒ (∀i ≥ 0, M • , w[m i ] |= φ ′ ) ⇐⇒ (∀i ≥ 0, M, π(w[m i ]) |= φ ′ ) ⇐⇒ (∀i ≥ 0, M, π(w)[i]) |= φ ′ ) ⇐⇒ (M, π(w) |= Gφ ′ ) .And the equivalence[START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] holds for φ = φ 1 U φ 2 because (M • , w |= φ 1 U φ 2 ) ⇐⇒ (M • , w |= (• ∨ φ 1 )U φ 2 ) ⇐⇒ ∃j ≥ 0, (M • , w[m j ] |= φ 2 ) ∧ ∀0 ≤ i < j, (M • , w[m i ] |= φ 1 ) ⇐⇒ ∃j ≥ 0, (M, π(w[m j ]) |= φ 2 ) ∧ ∀0 ≤ i < j, (M, π(w[m i ]) |= φ 1 ) ⇐⇒ ∃j ≥ 0, (M, π(w)[j]) |= φ 2 ) ∧ ∀0 ≤ i < j, (M, π(w)[i]) |= φ 1 )⇐⇒ (M, π(w) |= φ 1 U φ 2 ) .

Now we show that ( 9 )

 9 holds ψ ∈ {∃φ ′ , ∀φ ′ , P ∼b φ ′ } whenever property[START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] holds for φ ′ . There are three cases. In caseψ = ∃φ ′ , (M • , s • |= ∃φ ′ ) ⇐⇒ (M • , s • |= (¬•) ∧ ∃(¬(XG•) ∧ φ ′ )) def. of ∃φ ′ ⇐⇒ (M • , s • |= ∃(¬(⊤U G•) ∧ φ ′ )) t • (s • ) ∈ Σ ⇐⇒ ∃w • ∈ Path M• (s • ), (M • , w • |= ¬(⊤U G•) ∧ φ ′ ) def. of |= ∃ ⇐⇒ ∃w • ∈ Path r M• (s • ), (M • , w • |= φ ′ ) by def. ⇐⇒ ∃w • ∈ Path r M• (s • ), (M, π(w • ) |= φ ′ ) ind. hyp.⇐⇒ ∃w ∈ Path M (s), (M, w |= φ ′ ) by[START_REF] Brázdil | Controller synthesis and verification for markov decision processes with qualitative branching time objectives[END_REF] in Lemma 36 ⇐⇒ (M, s |= ∃φ ′ ) def of |= ∃.

◮

  and(M • , s• |= P ∼b (φ ′ )) ⇐⇒ (M • , s • |= (¬•) ∧ P ∼b ( φ ′ )) def. of P ∼b (φ ′ ) ⇐⇒ (M • , s • |= P ∼b ( φ ′ )) because c • (s • ) ∈ Σ ⇐⇒ P M•,s• L φ ′ ∼ b by def ⇐⇒ P M•,s• L φ ′ ∩ Path r M• (s • ) ∼ b because M • has finite delay ⇐⇒ P M,s π -1 (L φ ′ ) ∼ b by (12)⇐⇒ P M,s (L φ ′ ) ∼ b by (6) in Lemma 36 ⇐⇒ (M, s |= P ∼b (φ ′ )) by def.This terminates the inductive step, thus property[START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] holds for all path formula and property (9) holds for all state formula. ◭ Finally, Theorem 25 is a corollary of: Lemma 40 (Equivalence). Let ξ a CTL * [∃, ∀, P >0 , P =1 ] formula ξ with alphabet Σ. Let • a symbol not in Σ and ξ the lifting of ξ on Σ • . Then the following statements are equivalent: i) ξ is satisfiable.

alternating automata: proof of Lemma 26

  •})-labelled Markov chain M • with finite delay. According to Lemma 35, there exists a projection π of M • to a Σ-labelled Markov chain M. According to Lemma 39 M, π(ǫ) |= ξ, thus i) holds.

◭

I

From CTL * [∃, ∀, P >0 , P =1 ] to

Appendix

A

Closure properties

Proof of Lemma 2. Take the disjoint union of the automata, plus an initial state which is not in F >0 and two transitions leading to the initial states of the original automata, controlled by Adam for intersection and Eve for union. ◭

B

Emptiness problem in the non-deterministic case: a proof of Theorem 3

In this section we prove Theorem 3.

For the sake of completeness, we provide an algoritm to decide emptiness of nonzero automata in np∩conp and show that complexity drops to ptime when F ∀ is a Büchi condition. In the sequel we fix a non-deterministic automaton

Recall that in a non-deterministic automaton is the special case of alternating nonzero automata where all transitions are controlled by Eve and are split transitions.

Single-letter alphabets

In the case where the input alphabet has a single letter, there is a single possible input tree, thus a single possible acceptance game, which makes things easier.

There is a linear-time reduction of the emptiness problem for non-deterministic nonzero automata to the special case of single-letter alphabet: if one has an algorithm for the latter problem, then the former problem can be solved by having the non-deterministic automaton guesses the letters of the input tree on the fly, and perform its computation as usual.

In the sequel we assume the alphabet contains a single letter.

We can use [START_REF] Baier | Probabilistic ω-automata[END_REF] to show that σ ′ is almost-surely winning against τ . When E is the event lim sup ∈ F 1 , since σ is almost-surely winning, we get from (1) that P σ ′ ,τ (π 1 W (π 1 ) ∩ {lim sup ∈ F 1 }) = 0. There are countably many sets π 1 W (π 1 ), these sets are measurable and their union contains all infinite σ ′ -plays. Thus P σ ′ ,τ ({lim sup ∈ F 1 }) = 0 hence σ ′ is almost-surely winning. Now we prove that σ ′ is positively winning. Let π 2 be a play consistent with σ ′ and τ whose last state is positive. Let π 3 be a positive continuation of π 2 whose last state is minimal for the topological order on the transition graph of the automaton. Then in every positive continuation of π 3 , Adam has no choice but playing canonical moves. According to ( †), the value of f decreases along these continuations, let π 4 be a positive continuation of π 3 which minimizes f (last(π 4 )) among all positive continuations of π 3 . Then for every positive play π, π 4 π is consistent with σ ′ and τ iff h(last(π 4 ))π is consistent with σ and τ ′ , where τ ′ is a strategy playing canonical moves whenever possible. As a consequence, using Lemma 8,

Since h(last(π 4 )) is a σ-play whose last vertex is last(π 4 ) the right handside is positive thus the left handside as well. Thus σ ′ is positively winning. ◭

E Characterization of q-branches (Proof of Lemma 13)

Proof. For every vertex w = (n, q), index σ (n)(q) is defined by induction on the game graph, which is acyclic thanks to the (NLL) assumption. First in two simple cases:

is not reachable by a σ-play.

Then denote A the set of immediate predecessors of (n, q) by a canonical σ-play i.e. all the vertices (n ′ , q ′ ) such that:

is the canonical local transition; or q ′ ∈ Q E and σ(n ′ , q ′ ) is the local transition (n ′ , q ′ ) → (n, q); or q ′ ∈ Q E is controlled by Eve and σ(n ′ , q ′ ) is a split transition whose (n, q) is one of the two targets . If A = ∅ then index σ (n)(q) = min v∈A index σ (v) . Otherwise index σ (n)(q) is the smallest index not attributed yet to any vertex whose node is either the node n or its father.

We prove the third property. Assume first that the branch (n i ) i∈N is a q-branch. Let π = (n 0 , q 0 )(n 1 , q 1 ) • • • be a σ-play which projects to this branch and has limsup q. For every i ∈ N denote k i = index σ (n i , q i ). Then k i = ∞ because every vertex (n i , q i ) is σ-reachable. Adam performs finitely many non-canonical moves in π and after the last one of them, the sequence (k i ) i∈N is decreasing, hence converges to some limit k ∞ . From the moment this limit is reached, index σ (n

By definition of R ∞ , there exists i 0 large enough such that ∀i ≥ i 0 , k ∈ index σ (n i )(Q) and by definition of index σ , one can build by induction a σ-play π starting on node n i in which Adam plays only canonical moves and which visits exactly the vertices

Then By definition of R ∞ (b) this σ-play has limsup q. ◭ there exists d ∈ {0, 1} such that n ′ d ∈ N E and according to c) the set N E set is everywhere thick. The projection of Y on {0, 1} ω contains all branches of the subtree of N E rooted at n ′ d. Since N E is everywhere thick, the set of branches of this subtree has positive measure hence P σ,τ (Y ) > 0 according to Lemma 8. Now we show the condition is necessary. Let Z ′ be the subset of vertices in Z from which no canonical positive σ-play leads to a transient vertex.

If Z ′ is empty, then (∅, {0, 1} * × {0, 1}) is a positive witness which concludes the proof. Otherwise Z ′ is infinite (because of the normalization properties (N1) and (N2)). Let ((n k , q k )) k∈N be a bread-first enumeration of all nodes in Z ′ . For k ∈ N, we set z k = (n k , q k ).

Denote R k the set of vertices reachable from z k by a positive and canonical σ-play and T ′ k the set of nodes of these vertices. By definition of Z ′ , once a σ-play has visited z k ∈ Z ′ , as long as Eve plays σ and Adam plays canonical moves then no transient vertex is visited thus Adam always has a canonical choice when he has to take a decision. Thus, since σ is positively winning, the set of canonical positive σ-play starting in z k has nonzero probability. And this is true from every vertex visited from one of these plays. Thus T ′ k is an everywhere thick subtree.

We are going to combine the vertices and nodes of (R k , T ′ k ) k∈N in order to define inductively, for every k ∈ N an integer n k and a collection C k = (T i,k , X i,k ) i∈1...n k of sets of nodes and vertices with the following properties. i) For every i ∈ 1 . . . n k , the set of nodes T i,k is an everywhere thick subtree, whose root is denoted r i,k . And X i,k is a set of vertices at the root i.e.

k the set of vertices reachable by canonical σ-plays starting from x and visiting only nodes in T i,k . (The notation W x,k is unambigous because according to ii) there is a unique possible i given x and k). Denote

. Then all vertices in W (k) are positive (i.e. W (k) ⊆ {0, 1} * × F >0 ) and none of them are transient. iv) The sets in the collection (W x,k ) x∈X (k) are disjoint i.e. this collection is a partition of W (k) . v) For every j ∈ 0 . . . k, W (k) is reachable from z j by a canonical positive σ-play.

(

Initially we set n 0 = 1 and T 0,0 = T ′ 0 and X 0,0 = {z 0 }. Property v) holds since obviously z 0 ∈ W z0,0 , property iii) holds since the vertices in W z0,0 are exactly those visited by positive and canonical σ-plays starting in z 0 . Properties i) ii) and iv) are trivial since T ′ 0 is everywhere thick, n 0 = 1 and X 0,0 is a singleton.

We assume k > 0 and perform the inductive definition of

It is split in three cases: the copy case, the expansion case and shrinking case.

Copy case. Assume first that W (k-1) is reachable from z k by a positive canonical σplay. Then C k is simply the copy of C k-1 . Properties i)-iv) are maintained since they only depend on the collection C k-1 , independently of k. And v) is maintained by inductive hypothesis for j ∈ 0 . . . k -1 and by hypothesis for j = k. Expansion case. We consider T ′ k , the set of nodes visited by canonical positive plays starting in z k , which is an everywhere thick subtree as discussed previously. The expansion case occurs when for every i ≤ n k-1 the set of branches of the (possibly empty)

XX:29

◮ Definition 34 (Finite delay). A Σ • -labelled Markov chain M • has finite delay if from every state s • there is probability 0 to see the delay symbol forever:

A Σ • -labelled chain with finite delay is almost a Σ-labelled chain, up to a projection.

◮ Lemma 35 (Projecting Markov chains with finite delay). A Σ • -labelled Markov chain M • = (S • , t • , p • ) has finite delay iff there exists a Σ-labelled Markov chain M = (S, t, p) and

π is surjective; and for every state

Such a map π is called a projection of M • to M.

Before giving the proof, we start with a preliminary lemma: Actually projections preserve probability measures and path labelling. Denote Path r M• the set of pathes of M • that go through infinitely many Σ-labelled vertices. The definition of π is extended to π : Path r M• → Path M , by erasing states with label • and projecting Σ-labelled states to their image by π. Then, ◮ Lemma 36. For every state s • ∈ t -1

• (Σ) and every measurable set E ⊆ S ω ,

Proof. By definition of projections, property [START_REF] Tomás; Brázdil | The satisfiability problem for probabilistic CTL[END_REF] holds when E is a cylinder of length 1 i.e. E = stS ω . An easy induction show that it also holds when E is any cylinder E = ss 0 • • • s n S ω . Since property ( 6) is stable by complement and countable unions, it holds for every measurable set E. Property (7) holds because for every n ∈ N, the finite pathes of length n in M are exactly the projection by π of pathes in M • that go through exactly n Σ-labelled vertices. ◭

Proof of Lemma 35. The finite delay hypothesis is necessary. Let π be a projection from M • to M and s • a state of M • then

The finite delay property is sufficient. The projection M = (S, t, p) of

The projection π is the identity on S. The finite delay hypothesis guarantees that ∀s ∈ S, u p(s, u) = 1 thus M is a Markov chain. ◭ φ(w{0, 1} * ) ∩ φ(w ′ {0, 1} * ) = ∅ implies that w ⊑ w ′ or w ′ ⊑ w but L i is prefix-free and for any x ∈]p i-1 , p i [ there exists k, n such that

This terminates the inductive step of the construction of π and t • and the proof of the lemma. ◭

The correspondance between Σ • -labelled Markov chains and their projections on Σ has a logical counterpart. For every CTL * [∃, ∀, P >0 , P =1 ] formula ξ on the alphabet Σ, there is a similar CTL * [∃, ∀, P >0 , P =1 ] formula ξ on the alphabet Σ • , such that a Σ • -labelled Markov chain satisfies ξ if and only if its projection on Σ satisfies ξ.

◮ Definition 38 (Lifting of a CTL * [∃, ∀, P >0 , P =1 ] formula on Σ • ). Let ξ be a CTL * [∃, ∀, P >0 , P =1 ] formula on Σ. The lifting of ξ on Σ • is the CTL * [∃, ∀, P >0 , P =1 ] formula ξ defined inductively by

and the transformation from ξ to ξ leaves other operators invariant.

◮ Lemma 39 (Lifting are compatible with projections). Let π a projection of a Σ • -labelled Markov chain M • on a Σ-labelled Markov chain M. For every state-formula ψ, and for every Σ-labelled state s

Proof of Lemma 39. The equivalence

is proved by induction on ψ, together with the following extra property [START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF]. Denote

the set of pathes of M • that go through infinitely many Σ-labelled vertices. The definition domain of π is extended to

by projecting Σ-labelled states s to π(s) and •-labelled states to the empty word ǫ. We show by induction that for every path formula φ, and every path w

Every state formula ψ is also a path formula. Assume that property (9) holds for ψ and some state s. Then property [START_REF] Emerson | Sometimes and not never revisited: on branching versus linear time temporal logic[END_REF] holds for ψ (seen as a path formula) and every path starting from s, by definition of w |= ψ.

Acceptance conditions.

Every play of the acceptance game either ends up in one of the three absorbing states ⊤, ♯, ⊥ or eventually stays trapped in a ≡-component whose all states contain the same state formula ψ ∈ {∃φ, ∀φ, P >0 (φ), P =1 (φ)}, denoted Q ψ . The acceptance conditions are defined by:

A2) The order within Q ψ extends the order between states of A φ : if q ′ < q in A φ then (ψ, q ′ ) < (ψ, q) and all other states of Q ψ are smaller. A play eventually trapped in Q ψ is A φ -accepting if its projection on R φ is an accepting computation of A φ . A3) Every play eventually trapped in Q ψ with ψ ∈ {∃φ, ∀φ} is A φ -accepting. A4) Almost-every play eventually trapped in Q ψ with ψ ∈ {P >0 (φ), P =1 (φ)} is A φ -accepting. A5) When the play enters a component Q ψ with ψ = P >0 (φ) then with positive probability its continuation never enters neither ♯ nor ⊥.

By design, these conditions can be expressed by F ∀ , F 1 and F >0 sets thanks to:

Then π is A φ -accepting if and only if the second component of its limsup is an accepting state of A φ .

If moreover Eve plays truthfully then (π is

This automaton has limited choice for Adam because each time Adam asks for a proof, the alternating automaton exits the current ≡-class. It has size O(2 2 |ξ| ) as the union of a polynomial number of automata (the

We show that this automaton recognizes exactly the set of models of the CTL * [∃, ∀, P >0 , P =1 ] formula, for that we describe a winning strategy for Eve if the input binary tree is a model of the formula, and a winning strategy for Adam if not.

If the input tree t : {0, 1} * → Σ is a model of the formula, then Eve has a winning strategy which maintains the following invariant: IE: for every finite play π whose last state is of the form (s, ψ) with s a node of the tree and ψ a state formula then t, s |= ψ .

First, Eve is always truthful about the valuations b of the inner state formulas. Second, on vertices (s, ψ 1 ∨ψ 2 ) Eve chooses a successor (s, ψ i ) such that M, s |= ψ i , which is possible according to the invariant.

This guarantees the invariant IE to be maintained, since on vertices (s, ψ 1 ∧ψ 2 ) controlled by Adam, the invariant guarantees M, s |= ψ 1 and M, s |= ψ 2 and when Adam asks for a proof the invariant is maintained because Eve is truthful. Moreover ⊥ cannot be reached because Eve is truthful.

To terminate the description of Eve strategy, we specify the choice of Eve in a state (ψ, q, E) when ψ ∈ {∃φ, P >0 (φ)}. When the play enters Q ψ , Eve chooses a witness of M, s |= ψ (which holds according to IE). In case ψ = ∃φ the witness is a branch of the tree visiting the current node and satisfying φ. In case ψ = P >0 (φ) the witness is a thick subtree whose root is the current node and whose every branch satisfies φ which exists according to Lemma 16. If ψ = ∃φ then Eve chooses the state (ψ, q ′ ) in the direction of the witness path and ♯ in the other direction. If ψ = P >0 (φ) then Eve chooses the state (ψ, q ′ ) in either direction staying in the witness subtree and ♯ in the other direction. Now that Eve strategy is defined, we show that it is winning.

According to the invariant, no play consistent with Eve strategy reaches ψ = ⊥ thus according to Lemma 41 all plays have limsup in F ∀ and almost-all plays have limsup in F 1 .

When the finite play π enters for the first time a component Q ψ with ψ = P >0 (φ) in a vertex (s, ψ), we show by induction on the topological structure of the automaton that there is > 0 probability that continuations of π stay in F >0 , i.e. they do not enter the ♯ state. Let T ⊆ {0, 1} * be the thick subtree chosen by Eve to witness s |= P >0 (φ). Every branch of T is the projection of a continuation of π, and if this continuation stays in Q ψ then by definition of Eve strategy, it never enters ♯. Thus if all branches of T are such projections, we are done since T is thick. Otherwise, there is at least one continuation of π which leaves Q ψ in a state = ♯ and it will stay in non-♯ states as long as it does not enter another P >0 -component, thus we conclude with the inductive hypothesis.

Conversely assume that the input binary tree t : {0, 1} * → Σ is not a model of the formula. Then we describe a winning strategy for Adam which maintains the invariant: IA: whenever the play reaches a vertex (s, ψ) with ψ = ⊤ then t, s |= ψ .

If Eve is not truthful when proposing a valuation of the inner state formula, Adam asks for a proof of one of the wrong entries, which obviously maintains the invariant IA. And from every state (s, ψ 1 ∧ ψ 2 ), Adam moves to either successor (s, ψ i ) which maintains the invariant IA.

Fix some strategy σ for Eve. If any play reaches ⊥ then this falsifies the F ∀ -condition and Adam wins.

We show that there exists at least one play eventually trapped in some component Q ψ with ψ ∈ {∃φ, ∀φ, P >0 (φ), P =1 (φ)}. By design of the transitions, if a play enters ♯ then a play of the same length does not. And according to the invariant IA, the only way to enter ⊤ is from a state of the form (s, (∃φ, q, E)) and in this case there is a play of the same length which does not enter ⊤.

Let π be the finite play corresponding to the moment the play enters Q ψ , in some vertex (s, ψ). We can choose ψ minimal which implies that Eve is truthful in every continuation of π whose last state is in Q ψ . According to Lemma 41, for every continuation π ′ of π which stays in Q ψ , (π ′ is A φ -accepting) ⇐⇒ (π ′ |= φ) . According to the invariant IA t, s |= ψ thus in all cases Adam wins: if ψ = ∀φ or ψ = ∃φ one of the continuations of π stays in Q ψ but is not A φ -accepting. If ψ = P =1 (φ) there is > 0-probability that a continuation of π stays in Q ψ and is not A φ -accepting. If ψ = P >0 (φ) then there is probability 0 that the play stays in Q ψ and is A φ -accepting. Thus either almost-every continuation of π enters ♯ ∈ F >0 or there is > 0-probability that a continuation of π stays in Q ψ and is not A φ -accepting.

Thus Lemma 26 is proved when the input formula ξ is in CTL * [∃, ∀, P >0 , P =1 ].

Optimizing the construction for variants and fragments.

If ξ is an ECTL[∃, ∀, P >0 , P =1 ] formula, as already noticed the deterministic parity automaton A φ is already included in ξ, thus its size is linear in | ξ |. As a consequence, the size of the alternating automaton is "only" exponential in the size of ξ.

If ξ belongs to the fragment CTL[∃, ∀, P >0 , P =1 ], every state subformula φ of ξ has a single subformula which is a path formula of type Xφ ′ | φ 1 U φ 2 | Gφ ′ . Thus the subformula valuations proposed by Eve to Adam consist in one or two bits, thus they have constant