Arnaud Carayol
email: arnaud.carayol@u-pem.fr

Christof Löding

Olivier Serre
email: olivier.serre@cnrs.fr

Pure Strategies in Imperfect Information Stochastic Games

Keywords: Two-player imperfect information stochastic games, pure strategies, decidability/undecidability

We consider imperfect information stochastic games where we require the players to use pure (i.e. non randomised) strategies. We consider reachability, safety, Büchi and co-Büchi objectives, and investigate the existence of almost-sure/positively winning strategies for the first player when the second player is perfectly informed or more informed than the first player. We obtain decidability results for positive reachability and almost-sure Büchi with optimal algorithms to decide existence of a pure winning strategy and to compute one if it exists. We complete the picture by showing that positive safety is undecidable when restricting to pure strategies even if the second player is perfectly informed.

Introduction

The study of two-player games has received a lot of attention in the last decade, mainly motivated by applications to the verification of reactive open systems. Those systems are composed of a program (represented by the first player, Eve) and some (possibly hostile) environment (represented by the second player, Adam). The verification problem consists in deciding whether the program can be restricted so that the system meets some given specification whatever the environment does. Here, restricting the program means synthesizing a controller [START_REF] Ramadge | Supervisory Control of a Class of Discrete Event Processes[END_REF], which, in terms of games, is equivalent to designing a strategy for Eve that is winning against any strategy of Adam.

Of course, the class of games to consider depends on the class of systems that one intends to model. This may lead to consider various features such as concurrency (the players independently and simultaneously choose their action, whose parallel execution determines the next state), stochastic transitions (the next state is chosen according to a probability distribution depending on the current state and on the actions chosen by the players) or imperfect information (the players do not observe the exact state). Note that imperfect information is necessary if one wants for instance to model a system where the program and the environment share some public variables while having also their own private variables [START_REF] Reif | The Complexity of Two-Player Games of Incomplete Information[END_REF].

Recently in [START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF] two (mainly equivalent) models of concurrent stochastic games with imperfect information have been introduced. They permit to capture several known models (as those from [START_REF] De Alfaro | Concurrent Omega-Regular Games[END_REF][START_REF] Chatterjee | Stochastic ω-Regular Games[END_REF][START_REF] Chatterjee | Algorithms for Omega-Regular Games with Imperfect Information[END_REF]) while preserving the main decidability results.

In this paper we consider the games as introduced in [START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF] (we use the formalism of [START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF]). These are finite state games in which, at each round, the two players choose concurrently an action and based on these actions the successor state is chosen according to some fixed probability distribution. The resulting infinite play is won by Eve if it satisfies a given objective. The objectives we consider here are reachability (i.e. a final state is eventually visited), safety (i.e. no forbidden state is visited), Büchi (i.e. some final state is visited infinitely often) and co-Büchi (i.e. no forbidden states is visited infinitely often). Imperfect information is modelled as follows: both players have an equivalence relation over states and, instead of observing the exact state, they only observe its equivalence class. Intuitively, two equivalent states are indistinguishable by the corresponding player.

In [START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF] the authors were considering general strategies where a player is allowed to use randomisation when choosing her/his next action. It was then shown, for Büchi objectives, that one can decide whether Eve has such a strategy ϕ that is almost-surely winning against any strategy ψ of Adam (meaning that an infinite play played according to ϕ and ψ is won by Eve with probability 1). It was also established in [START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF] that one can decide for co-Büchi objectives whether Eve has a positively winning strategy.

In the present work we restrict our attention to pure strategies, i.e. we forbid the players to randomise when choosing their actions. Our initial motivation for this work comes from automata theory. The emptiness problem for automata on infinite trees can be described as the problem of computing a winning strategy in a two-player game of infinite duration. The required game model depends on the class of automata that is considered. In particular, [START_REF] Fijalkow | Emptiness Of Alternating Tree Automata Using Games With Imperfect Information[END_REF] proposes a reduction of the emptiness problem for alternating tree automata to the existence of a pure winning strategy for Eve in an imperfect information game. For capturing the automaton model with a qualitative acceptance condition as introduced in [START_REF] Carayol | Randomisation in Automata on Infinite Trees[END_REF], one furthermore needs stochastic games (and up to now this is the only known method for checking emptiness of such automata). So one of our aims is to obtain a toolbox and to understand the limits of this method for checking emptiness of tree automata.

Another motivation for studying pure strategies comes from controller synthesis. Indeed, a classical way to consider an open system (i.e. a controllable program interacting with an uncontrollable environment) is as a two-player game, and in this setting synthesising a controller for the program boils down to compute a winning strategy in the game for the player standing for the program. In the setting of open systems, imperfect information naturally arises, for instance when the program and its environment use private variables. A desirable property of a controller (in addition to its optimality) is its implementability which could be limited by its size but also by the required features. In the imperfect information setting, the main needed feature might be randomisation which is well-known to be non-trivial to implement in a non-biased fashion: hence, existence of an optimal non-randomised controller (equivalently a pure strategy) is a natural question.

Our main results are the following. On the negative side, by a reduction of the value 1 problem for probabilistic word automata [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF], we prove that even if Adam is fully informed and Eve is totally blind (i.e. all states are indistinguishable for her), it is undecidable whether Eve can positively win a safety game (Section 3). Under the same restrictions, positive winning in Büchi games and almost-sure winning in co-Büchi games are proved to be undecidable by reduction from the emptiness problem for probabilistic ω-word automata [START_REF] Baier | On Decision Problems for Probabilistic Büchi Automata[END_REF].

To obtain positive results, we have to impose restrictions on how Adam is informed. We consider the case where he has perfect information and the case where he is more informed than Eve 1 . In both situations we show that it is decidable whether Eve has a positively winning pure strategy in a reachability game (Section 4). Using this result in a fixpoint computation, we prove that one can decide whether Eve has an almost-surely winning pure strategy in a Büchi game (Section 5). Moreover, if it exists, such a strategy can be constructed and requires finite memory. In both cases, we obtain matching upper and lower complexity bounds.

The decidability results for the special case where Adam is perfectly informed were also obtained in [START_REF] Chatterjee | Partial-Observation Stochastic Games: How to Win when Belief Fails[END_REF]. However, the technique we develop here is different and in particular uses the positive winning case as a toolbox, which later permits us to handle the more general case where Adam is more informed than Eve. And while [START_REF] Chatterjee | Partial-Observation Stochastic Games: How to Win when Belief Fails[END_REF] focuses on reachability conditions and studies the memory required for winning strategies depending on how the players are informed, we focus on the case in which Adam is better informed than Eve (or even perfectly informed), and study different winning conditions.

In our setting (restricting to pure strategies) the algorithmic complexity increases to 2-EXPTIME while it is only EXPTIME in the general setting (allowing randomised strategies) when Adam is more informed than Eve. Also note that in the latter setting one has decidability results in the case where no assumption is made on how Adam and Eve are informed while in our setting this question is left open.

The resulting complete picture is summarised in the table at the end of this paper.

Definitions

A probability distribution over a finite set X is a mapping d :

X → [0, 1] such that x∈X d(x) = 1.
In the sequel we denote by D(X) the set of probability distributions over X. Given some set X and some equivalence relation ∼ over X, [x] ∼ stands for the equivalence class of x for ∼ and X/ ∼ = {[x] ∼ | x ∈ X} denotes the set of equivalence classes of ∼. As usual we write A * (resp. A ω ) for the set of finite (resp. infinite) words over some finite alphabet A. For k ≥ 0 we denote by A ≥k (resp. A ≤k ) the set of words of length at least (resp. at most) k.

A concurrent arena with imperfect information (or simply an arena) is defined as a tuple A play in such an arena proceeds as follows. First it starts in some initial state s. Then the first player, Eve, picks an action σ E ∈ Σ E and, simultaneously and independently, the second player, Adam, chooses an action σ A ∈ Σ A . Then a successor state is chosen according to the probability distribution δ(s, σ E , σ A ), and the process restarts: the players choose a new pair of actions that induces, together with the current state, a new state and so on forever. Hence, a play is an infinite sequence s 0 (σ 0

A = (S, Σ E , Σ A , δ, ∼ E , ∼ A ) where S is a finite set of states; Σ E (resp. Σ A ) is the (finite) set of s 0 s 1 s 2 s 3 s 4 * | a 1 2 1 2 * | b 1 2 1 2 f * | * a | * b | * b | * a | * b | * a | * a | * b | *
E , σ 0 A )s 1 (σ 1 E , σ 1 A )s 2 • • • in (S • (Σ E × Σ A )) ω such that for every i ≥ 0, δ(s i , σ i E , σ i A )(s i+1 ) > 0.
In the sequel we refer to a prefix of a play ending by a state as a partial play.

The intuitive meaning of ∼ E (resp. ∼ A ) is that two states s 1 and s 2 such that s 1 ∼ E s 2 (resp. s 1 ∼ A s 2 ) cannot be distinguished by Eve (resp. by Adam). We easily extend relation ∼ X , with X ∈ {E, A}, to partial plays as follows. First, for any partial play

λ = s 0 (σ 0 E , σ 0 A )s 1 (σ 1 E , σ 1 A ) • • • s k denote [λ] ∼ X = [s 0 ] ∼ X [s 1 ] ∼ X • • • [s k ] ∼ X ; then define λ ∼ X λ if and only if [λ] ∼ X = [λ ] ∼ X .
We say that Adam is more informed than Eve if ∼ A ⊆∼ E , and Adam is perfectly informed if ∼ A is the equality relation.

Example 2.1. Consider the concurrent game with imperfect information depicted in Figure 1. Let Σ E = Σ A = {a, b}. The initial state is s 0 and from s 0 if Adam plays the action a then any action played by Eve leads with probability 1 2 either to s 1 or to s 2 . Similarly if Adam plays b then any action played by Eve leads with probability 1 2 either to s 3 or to s 4 . In the states s 1 , s 2 , s 3 and s 4 , which are indistinguishable by Eve, the action of Adam has no impact. If Eve plays a from s 1 or s 4 or b from s 2 or s 3 the play goes to the final state f which is a sink state. Any other action by Eve from one of those states leave the current state unchanged.

In order to choose their moves the players respect strategies, and, for this, they may use all the information they have about what was played so far. However, if two partial plays are equivalent for ∼ E (resp. ∼ E ), then Eve (resp. Adam) cannot distinguish between them, and should behave the same. This leads to the following notion.

An observation-based pure strategy (simply called a strategy in the following) for Eve is a function ϕ : (S/ ∼ E ) * → Σ E , i.e., to choose her next action, Eve considers the sequence of observations she has seen so far. We overload ϕ by writing ϕ(λ) instead of ϕ([λ] ∼ E ): in particular, a strategy ϕ for Eve is such that ϕ(λ) = ϕ(λ ) whenever λ ∼ E λ (and similarly for Adam).

A finite-memory strategy for Eve is a strategy that can be computed by a finite automaton with output that reads the observation sequence of the partial play and outputs the next action of Eve. We do not give a precise technical definition because it is not needed in this work. The size of such a strategy corresponds to the number of states of the automaton.

Strategies for Adam are defined in a similar way by replacing ∼ E by ∼ A .

Remark 2.2. In our definition of a strategy we implicitly assume that the players only observe the sequence of states and not the corresponding sequence of actions. While the fact that a player does not observe what his adversary has played is reasonable (otherwise imperfect information on states would make less sense) one could object that the player should observe the actions she has played so far. However, as the players do not use randomisation in their strategies, they can always retrieve the actions they played so far. Moreover, in the special case where Adam is more informed than Eve (as later studied in Section 4.4), we can also note that, when playing against a fixed strategy of Eve, he can always retrieve the actions she played so far (as he knows the strategy of Eve and also [λ] ∼ E for any partial play λ).

Let A = (S, Σ E , Σ A , δ, ∼ E , ∼ A , ) be an arena, let s 0 ∈ S be an initial state, ϕ E be a strategy for Eve and ϕ A be a strategy for Adam. First we let Outcomes(s 0 , ϕ E , ϕ A ) to be the set of all possible plays when the game starts in s 0 and when Eve and Adam respectively follows ϕ E and ϕ A :

λ = s 0 (σ 0 E , σ 0 A )s 1 (σ 1 E , σ 1 A ) • • • belongs to Outcomes(s 0 , ϕ E , ϕ A ) iff δ(s i , ϕ E ([s 0 ] /∼ E [s 0 ] /∼ E • • • [s i ] /∼ E ), ϕ A ([s 0 ] /∼ A [s 0 ] /∼ A • • • [s i ] /∼ A ))(s i+1 ) > 0
for every i ≥ 0. Then we are interested in defining the probability of a (measurable) set of plays, knowing that Eve (resp. Adam) uses ϕ E (resp. ϕ A ). This is done in the usual way (see e.g. [START_REF] Chatterjee | Stochastic ω-Regular Games[END_REF]): once a pair (ϕ E , ϕ A ) of strategies for both players is fixed, one is left with a (possibly infinite) Markov chain that naturally induces a probability space over the Borel σ-field generated by the cones, where for any partial play λ starting in s 0 the cone for λ is the set cone

(λ) = λ • ((Σ E × Σ A ) • S
) ω of all infinite plays with prefix λ. We let Pr ϕ E ,ϕ A s 0 denote the corresponding probability measure over this space. An objective for Eve is a (measurable) set O of plays: a play is won by Eve if it belongs to O; otherwise it is won by Adam. A concurrent game with imperfect information (simply called a game in the following) is a triple G = (A, s 0 , O) where A is an arena, s 0 is an initial state and O is an objective. In the sequel we focus on the following special classes of ω-regular objectives (note that all of them are Borel sets hence, measurable) that we define using a subset F ⊆ S of final states.

A reachability objective (resp. safety) is of the form

(S • (Σ E × Σ A )) * F ((Σ E × Σ A ) • S) ω (resp. of the form ((S \ F ) • (Σ E × Σ A )) ω ) :
(S•(Σ E ×Σ A )) ≥k F ((Σ E ×Σ A )•S) ω (resp. of the form (S • (Σ E × Σ A )) * ((S \ F ) • (Σ E × Σ A )) ω
) : a play is winning if it goes infinitely often (resp. finitely often) through final states.

A reachability (resp. safety, Büchi, co-Büchi) game is a game equipped with a reachability (resp. safety, Büchi, co-Büchi) objective. In the sequel we may replace O by F when it is clear from the context which objective we consider.

Fix a game G = (A, s 0 , O). A strategy ϕ E for Eve is surely winning if, for any counter-strategy ϕ A for Adam, Outcomes(s 0 , ϕ E , ϕ A ) ⊆ O. If such a strategy exists, we say that Eve surely wins G. A strategy ϕ E for Eve is almost-surely winning (resp. positively winning) if, for any counter-strategy ϕ A for Adam, Pr ϕ E ,ϕ A s 0 (O) = 1 (resp. > 0). If such a strategy exists, we say that Eve almost-surely wins (resp. positively wins) G.

In this paper, we are interested in deciding existence of almost-surely/positively winning strategies for Eve for safety/reachability/Büchi/co-Büchi games.

Example 2.3. Consider the (perfect information) concurrent reachability game depicted below with q f as the unique final state. In state q w , if both players choose the same action then they stay in state q w and otherwise they move to state q f . In state q f , all choices of actions stay in state q f . Eve does not have any almost-surely winning strategy.

q w q f 0 | 1 1 | 0 0 | 0 1 | 1 * | *
Indeed, given any strategy ϕ E for Eve, the counter-strategy ϕ A for Adam mirroring the strategy of Eve (i.e. ϕ A = ϕ E ) only allows for the play q ω w and hence, Pr ϕ E ,ϕ A s 0

(O) = 0. Similarly Adam does not have an almost-surely winning strategy. For any fixed strategy ϕ A of Adam, any counter-strategy ϕ E for Eve that satisfies ϕ

E (q w ) = ϕ A (q w ) is such that Pr ϕ E ,ϕ A s 0 (O) = 1.

Undecidability Results

In this section we provide undecidability results for certain combinations of types of winning strategies and objectives. An easy consequence of undecidability results for probabilistic ω-automata from [START_REF] Baier | On Decision Problems for Probabilistic Büchi Automata[END_REF] is stated in the following theorem. In these reductions, Eve plays alone and cannot distinguish any states of the game. The states and transitions of the game are those of the ω-automaton and the strategy of Eve corresponds to the input word.

Theorem 3.1. The decision problems whether Eve almost-surely wins a given co-Büchi game or positively wins a given Büchi game are undecidable (even if the set of actions of Adam is a singleton).

Proof:

Consider a probabilistic automaton A on ω-words as in [START_REF] Baier | On Decision Problems for Probabilistic Büchi Automata[END_REF]. Now consider a concurrent game with imperfect information where Adam plays no role and where Eve's actions are the letters from the input alphabet A of A and whose states are the ones of the automaton. Moreover all states are ∼ E -equivalent. Now the transition function of the game mimics the one of the automaton. As Eve does not observe anything, a (pure) strategy ϕ of Eve can be described as an infinite word u ϕ in A (the i-th letter being

s hide s home s wet w | r t | h t | r w | h * | * * | * Figure 2:
The Hide-or-Run game the i-th action played by Eve), and ϕ is almost-surely (resp. positively) winning iff the probability of a run of A over u ϕ to be accepting is 1 (resp. strictly positive). The undecidability results follow from the undecidability of the emptiness problem for co-Büchi (resp. Büchi) probabilistic automaton with the almost-sure (resp. positive) semantics [START_REF] Baier | On Decision Problems for Probabilistic Büchi Automata[END_REF].

In the following we prove that the existence of positively winning strategies for safety objectives is undecidable. Our result is based on the undecidability of the value 1 problem for probabilistic automata on finite words [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]. For simpler use in our reduction we reformulate this problem in terms of games.

Consider the class of concurrent reachability games G with imperfect information with the following properties. Eve is blind (i.e. ∼ E consists of a unique equivalence class), and Adam has no impact on the game (i.e. his set of actions is a singleton). Furthermore, there is a special action that Eve can play at any time, and that leads (depending on the current state) either to a final sink state or to a non-final sink state. The final sink state is the only final state. Intuitively, one can think of such a game as one where Eve plays a sequence of actions and then declares by that she stops (and she wins if she stopped in a state that leads to the winning sink).

We refer to this type of game as probabilistic automaton game (PA game) because it corresponds to probabilistic automaton on finite words (see [START_REF] Paz | Introduction to probabilistic automata[END_REF] for an introduction to probabilistic automata): a strategy of Eve corresponds to a finite word followed by (without playing Eve surely loses), and the probability that it is winning is the probability of the word to be accepted in the automaton. Then we have the following result, which directly follows from the undecidability of the value 1 problem for probabilistic automata [START_REF] Gimbert | Probabilistic Automata on Finite Words: Decidable and Undecidable Problems[END_REF]. Lemma 3.2. For a given a PA game, it is undecidable whether Eve has for each 0 < ε < 1 a strategy that is winning with probability (1 -ε) < p < 1.

Our reduction that uses Lemma 3.2 starts from an example of a concurrent safety game G HR known as Hide-or-Run [START_REF] De Alfaro | Concurrent reachability games[END_REF] (see Figure 2). In this game, Adam can choose between hiding (h) and running (r), and Eve can choose between waiting (w) and throwing (t) her only snowball. If Adam hides and Eve waits, the game stays in state s hide . If Adam runs and Eve throws the snowball, then Adam is hit, and the game proceeds to sink state s wet . In all other cases, Adam gets home (either he runs without being hit or he can safely run after Eve has thrown her snowball) and the game proceeds to sink state s home . This is a safety game where Eve wants to avoid visiting s home .

In [START_REF] De Alfaro | Concurrent reachability games[END_REF] it is shown that Eve can only win by using a randomised strategy that plays action w in round i with probability p i such that 0 < p i < 1 for every i and i p i > 0 (for this, Eve does not have to distinguish the states). Now the idea is to incorporate a gadget in G HR that permits Eve to simulate random choices while playing deterministically.

Theorem 3.3. It is undecidable whether Eve positively wins in a safety game (resp. co-Büchi game), even if ∼ E consists of a single equivalence class.

Proof:

Consider a probabilistic automaton game G with a set of actions disjoint from the one in the game G HR . Let G r and G h be two disjoint copies of G where we removed the two states reachable by Eve playing (the -edges are redirected as described below).

In the game G HR (see Figure 3), the concurrent choices of the actions in G HR are simulated by the imperfect information. All states are indistinguishable by Eve. First Adam makes his choice r or h from s hide (Eve's action has no impact). The game then moves to the initial state of G r or G h , depending on the choice of Adam (ignore the action cheat for the moment, which is explained later). Because of the imperfect information Eve does not observe Adam's choice.

In G r and G h we removed the target states of but Eve can still play : if in G it was leading to the final state it now behaves as Eve playing w from s hide , and otherwise it behaves as Eve playing t from s hide (see Figure 3).

Finally, in order to prevent Eve from playing an infinite sequence of actions without , we add an extra small gadget where Adam is allowed to declare that Eve will cheat. If he plays cheat from s hide this leads to a new state s c where the following may happen depending on the next move of Eve (the action of Adam has no impact): if she plays from s c then the play goes to a sink state s w (that is not final); if she does not play from s c then with probability 1/2 the play stays in s c and with probability 1/2 the play goes to a sink final state s l . Hence, from s c if she never plays , then the play almost-surely ends in s l .

Let G HR be this new game, where we recall that all states are indistinguishable for Eve, s hide is the initial state and {s home , s l } are the final states. We claim that Eve positively wins game G HR iff Eve in G has strategies winning with probability arbitrarily close to 1. Indeed, consider a strategy ϕ for Eve in G HR . As Eve cannot distinguish any state in G HR , and does not observe the actions played by Adam, ϕ is independent of Adam's choices.

If the strategy of Eve consists in playing only finitely often, it cannot be positively winning as it suffices for Adam to wait for the last and then play cheat. More precisely, the strategy of Adam consists in playing (in state s hide ) the action h whenever Eve's strategy will still play in the future, and cheat if Eve will never play in the future. It can be shown that following this strategy Adam wins against the strategy of Eve with probability 1.

Thus, in the following we only consider strategies ϕ of Eve that play infinitely often. An equivalent description of such strategies ϕ is by a sequence (ϕ i ) i≥1 of strategies for Eve in G: ϕ consists in playing an arbitrary letter then playing as ϕ 1 until playing , then playing an arbitrary letter, then playing as ϕ 2 until playing and so on (the arbitrary letter is used here when Adam chooses to move to G r , G h or s c ).

For one direction, assume that ϕ is positively winning in G HR . Let p i be the probability that Eve wins in G when playing according to ϕ i . Then, from the properties of G HR , it follows that ϕ is winning iff 0 < p i < 1 for every i ≥ 1 and i p i > 0. This implies that the sequence (p i ) i≥1 converges to 1 and hence the ϕ i are strategies as in Lemma 3.2. Conversely, if Eve has strategies winning with probabilities arbitrarily close to 1 as in Lemma 3.2, then one can choose the ϕ i such that 1 > p i ≥ 1 -1 (i + 1) 2 which ensures 0 < p i < 1 for every i ≥ 1 and i p i > 0. Indeed,

s hide s home s wet * | * * | * G r G h s c s w s l * | cheat | * * | * * | * x | * 1/2 1/2 * | r | * | * * | h | * | *
i≥1 1 - 1 (i + 1) 2 = lim m→∞ m i=1 1 - 1 (i + 1) 2 = lim m→∞ m + 2 2m + 2 = 1 2
This family ϕ i defines a strategy for Eve in G HR . Again using the properties of G HR , this implies that Eve positively wins against all strategies of Adam: either no outcome ever reaches s c , in which case G HR is simulated, or if an outcome reaches s c , then it does with positive probability, and then it also reaches s w with positive probability.

Positive Winning in Reachability Games

We now address the decidability of whether Eve positively wins in a reachability game, and we show decidability (and matching lower bounds) for the case where (i) Adam is perfectly informed and (ii) Adam is more informed than Eve.

For the rest of this section fix an arena A = (S, Σ E , Σ A , δ, ∼ E , ∼ A ) and a set of final states F ⊆ S.

To later address almost-sure winning (Section 5) we need to consider games that may start in different states, and we are interested in strategies that are winning from all of these states. For this reason, we define for any subset B of states a game (A, B, O) that is played as follows: there is a new initial step where Adam picks a state s 0 in B and then the play proceeds as in (A, s 0 , O). Hence, a strategy ϕ for Eve in such a game is almost-surely (resp. positively) winning iff ϕ is almost-surely (resp. positively) winning in (A, s 0 , O) for every state s 0 ∈ B. We start with a general result that does not depend on how the players are informed. It states that if Eve can positively win in a reachability game then she can do so within a bounded number of moves. Proposition 4.1. Let B ⊆ S be a subset of states and assume that Eve has a positively winning strategy ϕ in the reachability game (A, B, F ). Then, there is a bound N and some 0 < ε B ≤ 1 such that whenever Eve respects ϕ in the game (A, B, F ), the probability that the resulting play visits a final state within the N first moves is at least ε B .

Proof:

For any N > 0, any s ∈ B and any strategy ψ N for Adam, call p ψ N ,s N the probability of the event "a play in (A, s, F ), where Eve respects ϕ and Adam respects ψ N visits a final state within the N first moves".

Let

x ψ N N = min{p ψ N ,s N | s ∈ B}.
We aim to show that there exists some N > 0 such that for each strategy ψ N for Adam, x ψ N N > 0. For this, we reason by contradiction, assuming that for any bound N > 0, Adam has a counter strategy ψ N such that x ψ N N = 0. In particular, there is a state s ∈ B such that p ψ N ,s N = 0 for infinitely many N . Hence, we can assume that the ψ N are such that p ψ N ,s N = 0 for every N ≥ 0 (as to get the property for some N Adam can always use the strategy for some N > N ).

Using (ψ N ) N ≥0 we define a strategy ψ for Adam as follows. We first let I 0 = N be the set of naturals. Next we define ψ and (I k ) k≥0 , a decreasing sequence (for inclusion) of infinite subsets of the naturals. First we sort partial plays by increasing length. We assume that ψ is defined on all partial plays of length smaller than k (hence initialization for k = 0 comes for free) and for plays of length k + 1 we do the following. As there are finitely many plays of length k + 1 while I k is infinite there exists an infinite subset I k+1 ⊆ I k such that, for all j 1 , j 2 ∈ I k+1 , both strategies ψ j 1 and ψ j 2 agree on plays of length k + 1; we define ψ to behave accordingly on plays of length k + 1.

Then, the following is a direct consequence of the definitions of ψ and (I k ) k≥0 : for every k ≥ 0, the set I k is infinite; and for every j ∈ I k and every partial play λ of length smaller than k, both ψ and ψ j agree on λ.

In particular it implies that x ψ N = 0 for every N ≥ 0: indeed, x ψ M N = 0 for any M ≥ N and ψ agrees with all ψ M with M ∈ I N (and as I N is infinite such an M exists). Finally, as 0 ≤ Pr ϕ,ψ s (O) ≤ N ≥0 x ψ N = 0 (here O denotes the reachability objective defined by F ), we conclude that Pr ϕ,ψ s (O) = 0 which contradicts our initial assumption of ϕ being positively winning in (A, s, F ).

The fact that there is some ε B > 0 such that ϕ ensures to reach a final state in less than N moves with a probability greater than ε B is a direct consequence of the fact that one bounds the number of moves by N .

Remark 4.2. Proposition 4.1 implies that finite memory suffices for Eve to positively win in a reachability game. Indeed, it suffices to follow ϕ for the N first moves and then play the same action forever.

Another important consequence is that the values of the probabilities do not have any influence on whether Eve positively wins in a reachability game. More precisely consider another arena A that is exactly as A except that its transition function δ is such that for every state s and every pair of actions (σ E , σ A ) one has δ(s, σ E , σ A ) = 0 iff δ (s, σ E , σ A ) = 0. Then Eve positively wins in the reachability game (A, B, F ) iff she positively wins in the reachability game (A , B, F ).

Positively Winning When Adam Is Perfectly Informed

We now assume that Adam is perfectly informed.

Consider for every n ≥ 0, the objective Reach ≤n (F ) = (S

• (Σ E × Σ A )) <n F ((Σ E × Σ A ) • S
) ω where a final state has to be visited within the first n steps. The following inductively characterises the sets B for which Eve can win (A, B, Reach ≤n (F )). • for every s ∈ B \ F and for every σ A ∈ Σ A , there exists s ∈ B such that δ(s, σ E , σ A )(s ) > 0.

Proof: Fix a set B ⊆ S of pairwise equivalent states and an integer n > 0. For the direct implication assume that Eve has a positively winning strategy ϕ in (A, B, Reach ≤n (F )). Let σ E = ϕ([B] ∼ E ) be the first action played by Eve and let ϕ be the strategy followed by Eve after this first step (i.e. ϕ (λ) = ϕ([B] ∼ E • λ) for every partial play λ). Let B be the set of states s such that ϕ is positively winning in (A, s , Reach ≤n-1 (F )).

We claim σ E and B satisfy the property of the statement. First and by definition ϕ is positively winning in (A, B , Reach ≤n-1 (F )). For the second property assume toward a contradiction that there exist some σ A ∈ Σ A and some state s 0 ∈ B such that for every s ∈ B , δ(s 0 , σ E , σ A , s) = 0 then ϕ is not positively winning in (A, s, Reach ≤n-1 (F )) (i.e. there exists a strategy ψ s of Adam such that Pr ϕ ,ψs s (Reach ≤n-1 (F )) = 0). Consider the strategy ψ for Adam consisting in playing first σ A and then the ψ s corresponding to the observed state s (i.e. ψ(s 0 ) = σ A and ψ(s 0 (σ E , σ A )λ) = ψ s (λ) for any partial play λ starting with s ∈ B ). We have the following contradiction:

Pr ϕ,ψ s 0 (Reach ≤n (F )) = s∈B δ(s 0 , σ E , σ A )(s) • Pr ϕ ,ψs s (Reach ≤n-1 (F )) =0 = 0.
For the converse implication assume that there exists an action σ E ∈ Σ E and a set B ⊆ S satisfying the properties of the statement. Fix a positively winning strategy ϕ for Eve in (A, B , Reach ≤n-1 (F )).

Consider the strategy ϕ for Eve in (A, B, Reach ≤n (F )) consisting of first playing σ E and then following ϕ

(i.e. ϕ([B] ∼ E ) = σ E and ϕ([B] ∼ E • [λ] ∼ E ) = ϕ ([λ] ∼ E )
for every partial play λ). We claim that this strategy is positively winning in (A, B, Reach ≤n (F )).

Indeed, let ψ be a strategy for Adam in (A, B, Reach ≤n (F )) and let s 0 ∈ B. Let σ A be the first action played by Adam when using ψ and let ψ be the strategy followed by Adam after this first step (i.e. ψ (λ) = ψ(s 0 (σ E , σ A ) • λ) for every partial play λ). By definition of B , there exists s ∈ B such that δ(s 0 , σ E , σ A )(s ) > 0. We have:

Pr ϕ,ψ s 0 (Reach ≤n (F )) ≥ δ(s 0 , σ E , σ A )(s ) • Pr ϕ ,ψ s (Reach ≤n-1 (F )) > 0.
Now, consider the increasing family of sets (W i ) i≥0 defined by: For any B ∈ W, we denote by rk(B) the smallest n such that B ∈ W n . Now, for any B ∈ W, we define a strategy for Eve denoted ϕ B that uses W as a finite memory. Initially the memory is B. For a partial play λ ending in a state in some equivalence class [s] ∼ E and assuming that the memory is B , we define the strategy as follows:

• W 0 = {B | B ⊆ F } • W i+1 = {B ⊆ S |
• If rk(B ) > 0 and if there exists r ∈ [s] ∼ E ∩ B , then by definition of (W i ) i≥0 there exists some action σ E and some set B such that the following holds:

rk(B ) = rk(B ) -1,

-∀r ∼ E r with r ∈ B \ F, ∀σ A , ∃s ∈ B , s.t. δ(s, σ E , σ A )(s ) > 0.
Then we let ϕ B (λ) = σ E and update the memory to B .

• In all other cases, we take ϕ B (λ) to be an arbitrary action and update the memory to ∅.

By induction on n, we show that for every non-empty B ∈ W n , the strategy ϕ B is positively winning in (A, B, Reach ≤n (F )). The base case is immediate. Assume that the property is established for n -

1 ≥ 0. Let B be a non-empty element of W n . Let s 0 ∈ B, σ E = ϕ B ([s 0 ] ∼ E ) and B ∈ W n-1
be the memory of ϕ B after the first move. Let ψ be a strategy for Adam. Let σ A be the first action played by Adam when using ψ and let ψ be the strategy followed by Adam after this first step, i.e. ψ (λ) = ψ(s 0 • (σ E , σ A )•λ) for every partial play λ. By definition of B , there exists s ∈ B such that δ(s 0 , σ E , σ A )(s ) > 0. Hence, we have:

Pr ϕ B ,ψ s 0 (Reach ≤n (F )) ≥ δ(s 0 , σ E , σ A )(s ) • Pr ϕ B ,ψ s (Reach ≤n-1 (F )) > 0.
which concludes the proof.

The following is a restatement of the end of Theorem 4.4.

Automaton-Compatible Strategies

The aim of this section is to refine Theorem 4.4 to positively winning strategies that satisfy further constraints. The motivation is that in Section 5 we compute almost-sure winning strategies for Büchi conditions using a fixpoint computation. In one iteration of this computation, we compute positively winning strategies for reachability that satisfy an extra constraint (roughly, that Eve can positively win the reachability game while ensuring that she can win another round of the reachability game once the target set is reached). This further constraint is expressible by finite automata that read partial plays and restrict the set of admissible next actions for Eve. Thus, below we develop the notion of a strategy that is compatible with such an automaton and then later apply it to the specific setting that we need.

Let T = (Q, Σ E × S /∼ E , q 0 , q s , δ T , Act) be a deterministic finite automaton with input alphabet Σ E × S /∼ E , a finite set of states Q, an initial state q 0 , a sink state q s , a transition function

δ T : Q × (Σ E × S /∼ E ) → Q and a function Act : Q → 2 Σ E
associating with any state of T a subset of actions for Eve. Moreover, we require that the following holds • Act(q) = ∅ if and only if q = q s .

• For every state q and for every (σ, x) ∈ Σ E × S /∼ E one has δ T (q, (σ, x)) = q s if and only if σ / ∈ Act(q). Such a machine associates with any partial play λ a unique state q λ defined by q s 0 = q 0 and q λ•(σ E ,σ A )•s = δ T (q λ , (σ E , [s] ∼ E )); it also permits to associate with any partial play a subset of actions by letting Act T (λ) = Act(q λ ).

A strategy ϕ of Eve is T -compatible if for every partial play λ where Eve respects ϕ one has ϕ(λ) ∈ Act T (λ). Note that it implies that q λ = q s . Remark 4.6. Consider the special case of the automaton T 0 defined as follows: Q consists only of two states, the initial state and the sink state; δ T (q 0 , (σ, x)) = q 0 and δ T (q s , (σ, x)) = q s for any (σ, x) ∈ Σ E × S /∼ E (i.e. all transitions are looping); and Act equals all actions Σ E in the initial state. Then it follows that any strategy is T 0 -compatible.

Hence, by considering the special case of T 0 , any result we obtain later will also hold if we drop the T -compatibility constraint.

In Section 5 and for the proof of Theorem 4.10, we work with automata that compute the belief of Eve along a play, as explained below. For an initial belief set B 0 ⊆ S of pairwise ∼ E -equivalent states, the belief (also known as knowledge) Belief B 0 E (λ) of Eve after a partial play λ starting in a state of B 0 , intuitively corresponds to the set of possible states that can have been reached in a play ∼ E -equivalent to λ.

Formally, the value of Belief B 0 E (λ) can be inductively defined as follows:

Belief B 0 E (s 0 ) = B 0 and Belief B 0 E (λ • (σ E , σ A ) • s) = UpBelief E (Belief B 0 E (λ), σ E , [s] ∼ E ) where the function UpBelief E : 2 S × Σ E × [S] /∼ E → 2 S is defined by: UpBelief E (B, σ E , [s] ∼ E ) = {t ∈ [s] ∼ E | ∃r ∈ B, ∃σ A ∈ Σ A s.t. δ(r, σ E , σ A )(t) > 0}.
Remark 4.7. The belief is in general smaller than the currently observed equivalence class. For instance, consider the reachability game depicted in Figure 4a in which all states are equivalent. If the strategy of Eve is to play (abb) ω , then her observation is always the same (as all states are equivalent). Her initial belief is {q 0 , q 1 } but after playing a it becomes {q 1 } and after a b it becomes {q 0 } and after another b it becomes {q 0 , q 1 }. Remark 4.9. In [START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF], it is shown that if Eve can almost-surely win (using randomised strategies) a Büchi game, she can do so using a strategy ϕ that only depends on the belief, i.e. ϕ(λ) = ϕ(λ ) whenever Belief ϕ (λ) = Belief ϕ (λ ). However, even if Eve is playing alone, this is no longer true2 (even for reachability games) in our setting where we restrict to pure (i.e. non-randomised) strategies. Consider the reachability game in Figure 4 where Eve is playing alone. The equivalence relation is given by s

q 0 q 1 b | b a | * b | * b | a a | * (a) Arena of Remark 4.7 s 0 s 2 s 1 t 2 f 2 t 1 f 1 * 1 2 1 2 a * b * a * b * (b) Arena of Remark 4.9
1 ∼ E s 2 , t 1 ∼ E f 2 and t 2 ∼ E f 1 .
If the game starts in s 0 then whatever strategy Eve uses, her belief always coincides with her observation. Eve can surely win (she can simply play the sequence aaab). But if her strategy only depends on her belief then she necessarily plays a sequence of actions of the form xu ω where x ∈ {a, b} and u is a two-letter word, and thus she has a probability 1 2 to win using such a strategy.

We now return to the strengthening of Theorem 4.4. We assume that Adam is perfectly informed and we fix an automaton T = (Q, Σ E × S /∼ E , q 0 , q s , δ T , Act) as in Section 4.3. We are interested in checking whether Eve has a T -compatible strategy that is positively winning in the reachability game (A, B, F ).

Our main result is the following and its proof is by two successive reductions and an application of Theorem 4.4.

Proof:

Note that adding the condition on the strategy being T -compatible somehow means that once a final state is reached the play is not yet won by Eve because she needs to keep playing in accordance with T (i.e. she must avoid to produce a partial play λ with q λ = q s ). Hence, it is natural to consider an enriched arena A T that embeds T . For this let

A T = (S × Q, Σ E , Σ A , δ , ≈ E , ≈ A ) where • δ ((s, q), σ E , σ A )(s , q ) equals δ(s, σ E , σ A )(s ) if q = δ T (q, (σ E , [s ] ∼ E ))
and otherwise it equals 0;

• (s 1 , q 1 ) ≈ E (s 2 , q 2 ) if and only if s 1 ∼ E s 2 and q 1 = q 2 ; and

• ≈ A is the equality relation, i.e. Adam is perfectly informed.

Of special interest is the safety game (A T , B × {q 0 }, S × {q s }) and we are interested in sure winning for Eve because of the following straightforward lemma It is a known result [START_REF] Berwanger | On the Power of Imperfect Information[END_REF] that when one considers sure winning for Eve in a safety game, winning strategies only depend on the belief of Eve (in the sense of Section 4.3). More precisely consider the (unique) largest subset B of beliefs and the (unique) mapping Aut : B → 2 Σ E such that the following holds.

• No belief B ∈ B contains a forbidden state.

• For every B ∈ B, the set Aut(B) which consists of all those actions σ E ∈ Aut(B) such that for every action σ A ∈ Σ A one has UpBelief E (B, σ E , [s] ∼ E ) ∈ B, is not empty; i.e. actions in Aut(B) are those that ensure that the updated belief will still be in B regardless of the action of Adam.

Then Eve surely wins the safety game from configurations where her belief B is in B and a strategy consists in choosing any action in Aut(B).

Note that in the safety game (A T , B × {q 0 }, S × {q s }), Eve's beliefs are elements in 2 S × Q (as we have that (s 1 , q 1 ) ≈ E (s 2 , q 2 ) implies q 1 = q 2 ). Now consider an automaton T = (Q , Σ E × S /∼ E , q 0 , q s , δ T , Act ) that computes Eve's belief (as explained in Remark 4.8. Hence, T is the same as T B ) in the previous safety game and uses function Aut = Act to define those authorised actions. To fit the definition, merge all beliefs not in B in a sink state and define Aut to be equal to ∅ on it. The states Q of T are elements of B (plus the sink state) and one takes as the initial state q 0 = B × {q 0 } (which possibly is the sink state). In particular the number of states of T is exponential in |S| and linear in |Q|.

Now one can go back to the original arena and consider the enriched arena A T . Then we have the following easy lemma. Lemma 4.12. Eve has a T -compatible positively winning strategy in the reachability game (A, B, F ) if and only if she has a positively winning strategy in the reachability game (A T , B ×{q 0 }, F ×(Q \{q s })).

Moreover, from a positively winning strategy in the second game using memory of size N one can effectively construct a T -compatible positively winning strategy in the reachability game (A, B, F ) that uses a memory of size O(N × 2 |S| × |Q|).

Proof:

If Eve positively wins in (A T , B × {q 0 }, F × (Q \ {q s })) then we can safely assume that she necessarily always plays authorised (according to Act ) actions (otherwise the play goes directly to S × {q s } and gets trap in it forever, hence cannot reach F × (Q \ {q s }), hence is T -compatible thanks to Lemma 4.11. Such a strategy can be mimicked in the original game and it requires to simulate automaton T hence, costs an extra memory of size the one of T . Conversely, if it she has a positively winning T -compatible strategy in the original game, the same strategy can be mimicked in the reduced game and is still positively winning. Now combining Lemma 4.12 together with Theorem 4.4 concludes the proof of Theorem 4.10.

The Case Where Adam Is More Informed Than Eve

We now assume that Adam is more informed than Eve and we fix an automaton T = (Q, Σ E × S /∼ E , q 0 , q s , δ T , Act) as in Section 4.3. Again, we are interested in checking whether Eve has a Tcompatible strategy that is positively winning in the reachability game (A, B, F ). The idea here is to reduce this question to one on a game where Adam is perfectly informed and therefore conclude thanks to Theorem 4.10.

Recall that in this setting, as noted in Remark 2.2, we can safely assume that, against a fixed strategy of Eve, Adam observes the actions played by both players.

For this let H be all those subsets of S that consist of ∼ A -equivalent states. For such a subset H and for any pair of actions

(σ E , σ A ) ∈ (Σ E × Σ A ) define the set U p(H, σ E , σ A ) ∈ H as follows. First, define M = {s ∈ S | ∃s ∈ H s.t. δ(s, σ E , σ A )(s ) > 0)
} as the set of all possible successors of states in H when playing the pair of actions (σ E , σ A ) and let U p(H, σ E , σ A ) consist of all those non-empty subsets H that can be written as

H = M ∩ [s] ∼ A , i.e. all possible indistinguishable (for Adam) subsets of M . Define now a new arena A = (H, Σ E , Σ A , δ , ≈ E , ≈ A ) by letting • δ (H, σ E , σ A )(H ) = 1/|U p(H, σ E , σ A )| if H ∈ U p(H, σ E , σ A ) and 0 otherwise; • H 1 ≈ E H 2 if s 1 ∼ E s 2 for every s 1 ∈ H 1 and s 2 ∈ H 2 ; and
• ≈ A is the equality relation, i.e. Adam is perfectly informed.

Define the set of final states F as those elements H in H such that H ∩ F = ∅. Note that the equivalence classes of ≈ E can be identified with the equivalence classes of ∼ E (because ∼ A ⊆∼ E ) and therefore one can define T -compatible strategies for Eve also in a play in A . More generally, any Eve's strategy in one game can be used in the other one.

Proof:

Let ϕ be a positively winning T -compatible strategy in G. Now use ϕ in G : obviously it is still Tcompatible and we only have to prove that it is positively winning. Consider a strategy ψ of Adam in G . Then, assuming Eve respects ϕ, strategy ψ can be mimicked in game G: indeed, Adam simply has to update a state H in A which is done by computing U p(H, σ E , σ A ) and observing the equivalence class for ∼ A relation; assuming Eve respects ϕ it means that Adam always knows what action σ E she will play and therefore can compute U p(H, σ E , σ A ). Call ψ the strategy in G mimicking ψ . Now let N be some integer and consider all those partial plays of length N in G where Eve respects ϕ and Adam respects ψ. Consider the ∼ A -equivalent classes among these partial plays and for every class consider the set H of possible last states. Then those such H are exactly those states that can be reached in G in a partial play of length N when Eve respects ϕ and Adam respects ψ . As ϕ is positively winning in G , thanks to Proposition 4.1 there is some N such that Eve positively wins within the N first moves and therefore for the same N we conclude that Eve positively wins within the N first moves in G using ϕ against ψ . As this property does not depend on ψ we conclude that ϕ is positively winning in G .

Conversely, assume she has a positively winning T -compatible strategy in G . Now use ϕ in G: obviously it is still T -compatible and we only have to prove that it is positively winning. By contradiction, assume Adam has a strategy ψ that ensures, provided Eve uses ϕ in G, that no final state is reached. Then, from ψ one can define a strategy in ψ that consists in a partial play

H 0 (σ 0 E , σ 0 A )H 1 (σ 1 E , σ 1 A ) • • • H k to play action ψ([s 0 ] ∼ A • • • [s k ] ∼ A )
where s i is any (they are all ∼ A -equivalent) element in H i for every i. Using the same argument as in the direct implication relating plays in G when using strategies (ϕ, ψ) and plays in G when using strategies (ϕ , ψ ), one concludes that playing ψ against ϕ in G ensures that no final state is visited hence, leading a contradiction with ϕ being positively winning in G .

Combining Proposition 4.13 with Theorem 4.10 directly leads the following result.

Almost-Surely Winning for B üchi Conditions

For the rest of this section fix an arena A = (S, Σ E , Σ A , δ, ∼ E , ∼ A ) and a set of final states F ⊆ S. We are interested in almost-sure winning strategies, and we focus on Büchi conditions, as a solution for this case permits to obtain a solution for reachability condition by a simple reduction (change the arena so that whenever a final state is reached then the play stays in it forever). For the moment we do not make any assumption on how Adam is informed.

We show how to compute the set of almost-surely winning beliefs of Eve, denoted B AS , which is the set of subsets B ⊆ S such that B ⊆ [s] ∼ E for some s ∈ S and for which Eve has an almost-surely winning strategy in the Büchi game G B = (A, B, F ). For some B ∈ B AS we let

[B] ∼ E = [s] ∼ E for s ∈ S such that B ⊆ [s] ∼ E .

Decidability Issues

As Ξ is monotone for set inclusion, it suffices to compute B AS by successive applications (starting with the set of all subsets) of the operator Ξ until reaching the fixpoint. Since B AS ⊆ 2 S , the fixpoint is reached in at most 2 |S| steps. Now, as noted in Remark 4.8 the property for a strategy to guarantee that Eve's belief remains in a set B can be expressed as the strategy being T B -compatible (and the number of states of T B is at most exponential in |S|). Therefore, thanks to Theorem 4.10 (resp. Theorem 4.14) every step in the fixpoint computation can be achieved in time exponential (resp. doubly exponential) in |S| if Adam is perfectly informed (resp. more informed than Eve). This leads the following result.

Theorem 5.3. Let G be a Büchi (or reachability) game with n states.

• If Adam is perfectly informed, one can decide whether Eve has an almost-surely winning strategy in time exponential in n. If such a strategy exists, it can be effectively constructed and requires memory at most exponential in n.

• If Adam is more informed than Eve, one can decide whether Eve has an almost-surely winning strategy in time doubly exponential in n. If such a strategy exists, it can be effectively constructed and requires memory at most doubly exponential in n.

Proof:

Decidability follows from Theorem 4.10/Theorem 4.14 and the fixpoint characterisation given in Lemma 5.1. The result on the strategies is also a consequence of Theorem 4.10/Theorem 4.14 combined with Corollary 4.5 which permits to bound the size of N in the proof of Lemma 5.1.

Lower Bound

We now give a matching lower bound to the upper bounds in Theorem 4.14 and in Theorem 5.3 for the case where Adam is more informed than Eve. Note that in the case where Adam is perfectly informed one can get a matching lower bound (ExpTime-hardness) as in the case where randomised strategies are allowed [START_REF] Chatterjee | Algorithms for Omega-Regular Games with Imperfect Information[END_REF]. Also note that in the case where Adam is more informed than Eve similar lower bounds, when randomised strategies are allowed, were obtained in [START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF] for almost-sure winning 3 ; however, even if the ideas of the proof below are similar to the ones in [START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF][START_REF] Bertrand | Qualitative Determinacy and Decidability of Stochastic Games with Signals[END_REF], namely the players simulate a run of an exponential space alternating Turing machine while gadgets prevent cheating, there is a slight but crucial difference. Indeed, Eve is in charge of describing the successive configuration while in previous proofs Adam was; we actually believe that this is needed for the proof to work (mainly because we are not only interested in almost-sure winning but also in positively winning).

Theorem 6.1. Deciding whether Eve has a positively winning (resp. an almost-surely winning) strategy in a reachability game where Adam is more informed than her is a 2-ExpTime-hard problem.

Proof:

The idea is to simulate a computation of an alternating Turing machine that uses a space of exponential size and to reduce termination to almost-surely winning for Eve. As alternating Turing machines of exponential space are equivalent to deterministic Turing machines working in doubly exponential time it permits to obtain the desired lower bound. We can safely assume that the tape alphabet A contains a blank symbol as well as a special symbol , and that initially the input tape is made of n successive symbols followed by 2 n -n blank symbols. A configuration of the machine can be described by a word of length 2 n in A * QA * where Q is the set of states of the machine (including some final states): the meaning of a configuration a

1 • • • a qa +1 • • • a 2 n is that the tape content is a 1 • • • a a 2 n ,
the state is q and the reading/writing head is on the -th cell. A run of the machine is a sequence of successive configurations separated by transitions of the machine; it is accepting if it contains a final configuration (and in that case the run is of finite length; otherwise it is of infinite length).

A classical way of thinking of an alternating Turing machine is as a game where Eve is in charge of the choice of transitions when the machine is in an existential state while Adam takes care of the universal states. The machine accepts if and only if Eve has a winning strategy to eventually reach a configuration with a final control state.

Consider now the following (informal) game. Eve is in charge of describing the run of the Turing machine (her actions' alphabet contains all the necessary symbols for that i.e. A ∪ Q that permits the game to go in some associated states). After she described a configuration either she (in case the state is existential) or Adam (in case the state is universal) describes a valid transition of the machine (again by playing some special actions), and then Eve describes the successive configuration and so on until possibly a final configuration is reached (in which case she wins the game). Hence, in the game's state one stores the state (of the Turing machine) when described as well as the adjacent symbols; this information is used when Eve/Adam has to describe the next transition of the machine (that should be consistent).

Of course the problem is that Eve could cheat by not describing a valid run. For this, Adam can, in every configuration, secretly (i.e. Eve does not observe it) mark a cell of the tape, and in the next configuration he can indicate a cell (supposedly of same index than the previously marked one) and it is checked whether it has been wrongly updated: this is easily done as the cell before and after the marked cell have been stored in the arena (and Eve does not observe it of course) and together with the transition one can compute the correct update of the cell. Now in case there is indeed a wrong update of the cell content, the play restarts (i.e. the players restart from the initial configuration of the Turing machine); otherwise the play goes to a final state and Eve wins. Hence, in the game's state one also stores (and hides to Eve) information of a cell marked by Adam and of the adjacent symbols for a later check. This marking by Adam as well as the checking later is done by him playing a distinguished action.

One problem in the previous simulation is that Adam could cheat by indicating two cells that are not with the same index. If the space used by the machine was of linear size, one could of course store the actual index and formally check it. Here, we use an extra coding to circumvent this problem. When describing the configuration, after every symbol Eve produces a sequence of n bits whose meaning is to describe, in binary counting, the index of the last symbol. When she describes such a binary number, Adam can secretly mark a bit that he claims will be not correctly updated when describing the index of the next symbol (for this he just plays an action that stands for a number between 1 and n) and this is checked next: if she made an incorrect update, the play restarts (i.e. the players restart from the initial configuration of the Turing machine); otherwise the play goes to a final state where she wins. Hence, in the game's state one also stores (and hides to Eve) the index (between 1 and n) of a bit marked by Adam as well as the value corresponding to the bit of the same index in the incremented version of the described number (this can be computed on the fly). This marking by Adam is done by him playing a distinguished action; the checking is done deterministically (thanks to a counter). One also uses this binary encoding of the index of the cell in the following way: whenever Adam marks a symbol that he claims will be incorrectly updated in the next configuration, a bit of its binary encoding is guessed (i.e. randomly chosen) and its index is stored and not observed by none of the players. Later, when Adam indicates the supposed corresponding symbol in the next configuration, the guessed bit is checked and should match: if not the play goes to a final state and Eve wins; otherwise one does as previously explained (i.e. one checks whether the symbol is correct: if not the play restarts otherwise the play goes to a final state and Eve wins). Hence, in the game's state one also stores (and hides to both players) the value and index of the randomly chosen bit.

We claim that Eve positively wins (equivalently almost-surely wins) this game if and only if the Turing machine accepts. Once this is established, the proof will be over, as one can easily notice that the previous informal game can be encoded formally as a two-player game with imperfect information of polynomial size in the one of the Turing machine.

First, assume that the Turing machine accepts. Hence, it means that the existential player Eve has a winning strategy in the acceptance game of the machine. Now, mimic this strategy in the above described game: Eve always makes a correct description of a run and, when she has to choose a transition of the machine, she does as in her winning strategy in the acceptance game of the machine. We claim that this strategy is almost-surely winning (hence, also positively winning). Indeed, any strategy of Adam that does not infinitely often claim that a cell is incorrectly updated is surely losing for him because either he makes a wrong claim (actually his claims are always wrong but here we mean he get discovered because of the hidden bit), or after some point the simulation goes to the end and finishes by a final configuration of the Turing machine. Now, against this strategy of Eve, when Adam infinitely often claims that a cell is incorrectly updated, he almost-surely gets caught because at every claim there is a (fixed positive) probability (at least 1/n) that the secret bit does not match, and therefore, by Borel-Cantelli Lemma, the probability that he gets caught eventually is 1. Of course, if Adam claims at some point that a bit is incorrectly updated by Eve he also looses (because she describes a valid run). Hence, Eve's strategy almost-surely defeats any strategy of Adam.

Conversely, assume that the Turing machine does not accept. Hence, it means that the existential player Eve has no winning strategy in the acceptance game of the machine. Now, consider a strategy of Eve. There are two possibilities.

• Either there is a strategy 4 of Adam against which Eve's strategy eventually cheats. Then, consider the strategy of Adam that plays the same except that he points the moment where she cheats: then, Eve must behave the same and therefore the play restarts. Now, consider how she behaves in the restarted play and do the same reasoning. If we are always in the same situation, by iteratively playing a strategy pointing where she cheats in every simulation of the Turing machine ensures that no final configuration is reached and therefore that she surely looses.

• Or, against any strategy of Adam, Eve's strategy never cheats (i.e. describes a valid run). Hence, Eve's strategy can be seen as a strategy in the acceptance game of the machine and therefore, one can consider the strategy of the universal player that beats it in the acceptance game and let Adam mimic it in the simulation game (and he never claims that she cheats). Then, this strategy leads to an infinite play that corresponds to the description of an infinite run of the alternating Turing machine that never visits a final configuration: hence, it surely defeats Eve's strategy

In conclusion, for any strategy of Eve in the above described game there is a strategy of Adam that surely beats this strategy, which implies that there is no positively winning (hence almost-surely winning) strategy for Eve. This terminates the proof.

Summary

In this paper we considered finite state games in which, at each round, the two players (called Eve and Adam) choose concurrently an action and based on these actions the successor state is chosen according to some fixed probability distribution. We considered several classical winning conditions: safety, reachability, Büchi and co-Büchi. Moreover, the players are imperfectly informed: each player has an equivalence relation over states and, instead of observing the exact state, he observes its equivalence class. Finally, we restricted our attention to pure strategies, i.e. we forbid the players to randomise when choosing their actions.

We studied the decidability and complexity status of the problem of deciding whether Eve has a positively (resp. almost-surely) winning strategy. To obtain positive results, we imposed restrictions on how Adam is informed: we considered the case where he has perfect information and the case where he is more informed than Eve.

The landscape of decidability and undecidability results with pointers to the literature and to the results in our paper are shown in the Table 1. The entries of the form "1/2-Exptime-complete" refer to the two cases of Adam being perfectly informed and being better informed than Eve, respectively (the results from [START_REF] Chatterjee | Partial-Observation Stochastic Games: How to Win when Belief Fails[END_REF] are for the case of Adam being perfectly informed). The implication ⇒ means that our result is an easy consequence of a result from the literature. The undecidability results already hold for the case in which Adam is perfectly informed.

Figure 1 :

 1 Figure 1: A concurrent arena where Adam is perfectly informed while Eve cannot distinguish states s 1 , s 2 , s 3 and s 4 .

Figure 3 :

 3 Figure 3: The modified version of Hide-or-Run: G HR . Black states in G r /G h correspond to states from which led to the final state in G, and x denotes any letter different from .

4. 1 .

 1 Winning in a Finite Number of Moves.

Proposition 4 . 3 .

 43 Let B ⊆ S be a set of pairwise ∼ E -equivalent states and let n > 0. Eve positively wins (A, B, Reach ≤n (F )) if and only if there exists an action σ E ∈ Σ E and a set B ⊆ S such that • Eve positively wins (A, B , Reach ≤n-1 (F )),

Corollary 4 . 5 .

 45 In Proposition 4.1, when Adam is perfectly informed, one can always choose ϕ such that N ≤ 2 |S| .

Figure 4 :

 4 Figure 4: Arenas and beliefs

Remark 4 . 8 .

 48 Given a family B ⊆ 2 S of beliefs for Eve (in the sense that each B ∈ B is a subset of a ∼ E -class), one can construct an automaton T B such that the T B -compatible strategies are precisely those such that Eve's belief always remains inside B. The states of T B are the elements of B, the transition function is defined by UpBelief E , and the actions Act(B) enabled at a state B are those that ensure that the belief remains inside B.

Theorem 4 . 10 .

 410 When Adam is perfectly informed, one can decide in exponential time in |S| and polynomial in |Q| whether Eve has a T -compatible strategy that is positively winning in the reachability game (A, B, F ). If such a strategy exists, one can construct one that uses memory of size polynomial in |Q| and exponential in |S|.

Lemma 4 . 11 .

 411 Eve has a (possibly losing) T -compatible strategy in the reachability game (A, B, F ) if and only if she has a surely winning strategy in the safety game (A T , B × {q 0 }, S × {q s }).

  For a set B ⊆ S define ν(B) ∈ H as ν(B) = {{s} | s ∈ B}. The following proposition relates game (A, B, F ) and game (A , ν(B), F ).

Proposition 4 .

 4 13. A strategy of Eve is a positively winning T -compatible strategy in G = (A, B, F ) if and only if it is a positively winning T -compatible strategy in G = (A , ν(B), F ).

Theorem 4 . 14 .

 414 When Adam is more informed than Eve, one can decide in double exponential time in |S| and polynomial in |Q| whether Eve has a T -compatible strategy that is positively winning in the reachability game (A, B, F ). If such a strategy exists, one can construct one that uses memory of size polynomial in |Q| and doubly exponential in |S|.

  a play is winning if it contains (resp. does not contain) a final state. A B üchi objective (resp. co-B üchi objective) is of the form k≥0

  ∀r ∈ B, ∃σ E ∃B ∈ W i s.t. ∀s ∼ E r with s∈ B \ F , ∀σ A ∃s ∈ B s.t. δ(s, σ E , σ A )(s ) > 0} and call W its limit. Then the following is a simple consequence of Proposition 4.3. Theorem 4.4. Let B ⊆ S be a non-empty set. Eve has a positively winning strategy ϕ in the game (A, B, F ) if and only if B ∈ W. In particular it can be decided in time exponential in |S| whether Eve has a positively winning strategy. If such a strategy exists, one can construct one that uses the set 2 S as memory, and this strategy guarantees to positively reach a final state within the 2 |S| first moves.

Proof:

Using Proposition 4.3, by a direct induction on n one gets that B = ∅ belongs to W n if and only if Eve positively wins (A, B, Reach ≤n (F )).

We say that Adam is more informed than Eve when his equivalence relation on the states of the games refines that of Eve. In particular, this is the case when Adam is perfectly informed.

This fact is also observed in[START_REF] Chatterjee | Partial-Observation Stochastic Games: How to Win when Belief Fails[END_REF].

Actually the lower bound in[START_REF] Gripon | Qualitative Concurrent Stochastic Games with Imperfect Information[END_REF] uses a game where none of the player is more informed than the other but it is easily seen how to modify it to obtain a game where Adam is more informed than Eve

In fact a set of indistinguishable strategies from Eve's point of view, including the ones where Adam claims she cheats.

Fixpoint Characterisation

Lemma 5.1 below states that the set B AS can be expressed as the greatest fix-point of a (monotone) mapping Ξ : 2 2 S → 2 2 S defined as follows. Let B ⊆ 2 S and let B ∈ B. We say that B belongs to Ξ(B) if Eve has a strategy in the reachability game (A, B, F ) which is positively winning and guarantees that her belief always stays in B.

Lemma 5.1. B AS is the greatest fixpoint of Ξ.

Proof:

We first argue that B AS is a fixpoint for Ξ. For this we consider any B ∈ B AS and prove that B ∈ Ξ(B AS ). We denote by G B the Büchi game (A, B, F ) and we start with a simple lemma. Lemma 5.2. Let B ∈ B AS . Let ϕ be any strategy for Eve that is almost-surely winning for her in G B and let

Proof: Consider some action σ A and some t such that δ(s, σ

By definition of UpBelief E , for every t ∈ B , there is some s ∈ B and some action σ t A such that δ(s , σ E , σ t A )(t ) > 0. Now, define the strategy ϕ of Eve by letting ϕ (λ) = ϕ([s] ∼ E • λ) for any partial play λ. We claim that ϕ is almost-surely winning for Eve in G t for any t ∈ B , hence implying that B ∈ B AS . By contradiction, assume that ϕ is not almost-surely winning for some G t with t ∈ B and let ψ be a counter-strategy for Adam in G t , i.e. Pr ϕ ,ψ t (O) < 1 (recall that O denotes here the Büchi objective). Now, pick s ∈ B such that δ(s , σ E , σ t A )(t ) > 0 and define a strategy ψ of Adam by letting ψ(s ) = σ t A and ψ(s • λ) = ψ (λ). Then as Pr ϕ ,ψ t (O) < 1 one also has that Pr ϕ,ψ s (O) < 1 which leads to a contradiction. Fix a strategy ϕ B as in Lemma 5.2: a play λ in G B where Eve respects ϕ B is such that Belief B E (λ) ∈ B AS . Moreover, as ϕ B is almost-surely winning for the Büchi game G B , it is in particular positively winning in the reachability game (A, B, F ). Hence, using Proposition 4.1, one gets a bound N B and some ε B , meaning that the probability of a play λ in G B where Eve respects ϕ B to visit a final state within its first

Now we show that any fixpoint of Ξ is included in B AS . For this assume that Ξ(B) = B for some B. As any B ∈ B is such that B ∈ Ξ(B) it comes with some ϕ B , N B and ε B . We let

Now we define a strategy ϕ that consists in playing in rounds of length N : at the beginning of some round, Eve considers her current belief H and plays according to ϕ H in the next N moves; then she restarts with the updated belief, and so on forever. Now consider some B ∈ B. We claim that ϕ is almost-surely winning for Eve in any in G B . Indeed, from the properties of the ϕ H , it follows that any play in G B where Eve respects ϕ is such that the belief is in B. Now, as the ϕ H ensure to visit a final state with probability ≥ ε in less than N moves the Borel-Cantelli Lemma implies that ϕ is almost-surely winning. Hence, B ∈ B AS and this concludes the proof.


Eduardo Ferreira Molina

Natana Aparecida Martins De Jesus

Serge Paofai

Peter Hammer

Maria Amela-Cortes

Malo Robin

Stéphane Cordier

Yann Molard

When a red NIR

When a red NIR emissive Cs2[Mo6Br14] interacts with an

active diureasil-PEO matrix: design of tunable and white light emitting hybrid material.

Eduardo Ferreira Molina, [a] * Natana Aparecida Martins de Jesus, [a] Serge Paofai, [b] Peter Hammer, [c] Maria Amela-Cortes, [b] Malo Robin, [b] Stephane Cordier [b] and Yann Molard [b] * Hybrid materials combining diureasil matrices and octahedral molybdenum clusters have been synthesized to design lead-, cadmium and rare earth-free emitters for lighting or optoelectronic applications. This association leads to homogeneous and stable hybrids which emission color can be tailored on the entire visible range, including white, thanks to effective energy transfers from the host to the nanocluster.

Transition metal cluster compounds are based on a metal atoms scaffold maintained by metal-metal bonds. [1] In the field of luminescent materials, octahedral clusters made of low cost and abundant metals like Mo or W, constitute attractive alternatives to toxic cadmium-or lead-, costly Ir(III)-, Pt(II)-or rare earthcontaining luminophores. [2] Recent developments in this area have highlighted their potential in optoelectronic, [3] sensing, [4] lighting, [5] theranostic, [6] luminescent solar concentrators, [7] or photocatalysis. [8] Due to their high emission stability in the red-NIR, [5,9] they show a great potential for lighting technologies to design white light emission panels. White light emission involves usually the combination of three (blue, green and red) complementary emitters, which requires tedious multilayer devices engineering. One possibility to tackle this problem is to gather all emitters in a single material and this, in a one-pot reaction. To succeed, the host matrix should be judiciously chosen in terms of thermal and photostability while being chemically compatible to circumvent phase segregation between organic and inorganic components. [10] Furthermore, it should also be able to maintain the initial photophysical properties of native dyes after their integration. [11] Diureasils [12] are hybrid materials belonging to the Ormocer® family. [13] They contain siliceous domains connected, via urea linkers, to poly(ethylene oxide)/poly(propylene oxide) (PEO/PPO) chains that provide distinct hydrophilic, swelling, mechanical and optical properties. Electron-hole radiative recombinations in both the siliceous and urea-centered domains, [14] [15] evidence that such matrix can act as active host for various luminophores like organic dyes, [16] lanthanide complexes, [17] quantum dots [18] or conjugated polymers. [19] Recently, we have shown that supramolecular interactions between PEO chains and alkali cations could be used to incorporate alkali salts of metal clusters in organic polymers. [5] Motivated by these results, we postulated that a blue-green emissive ureasil matrix could easily be associated with red NIR emissive alkali salts of metal clusters. Here we present the synthesis of molybdenum cluster compounds incorporated in the diureasil hybrid, named dUPEO, and show that molybdenum clusters can be homogeneously integrated using the diureasil solgel process. We demonstrate that the dUPEO hybrid matrix has a great potential in practical use as a solid-state luminescence device providing a tunable emissive material in which the emission color can be judiciously controlled by varying the Mo6 cluster content and/or the excitation wavelength. Figure 1 presents the molecular structure of the dUPEO precursors and the Cs2Mo6Br14 metal cluster salt (1) used as a cluster compound model due to its simple synthesis, and stability. [20] Two synthetic schemes were followed: the first one depicts the mixing of different amounts of 1 and PEO hybrid sol before the hydrolysis reaction leading to cross-linking of ureasil nodes (E1 -E5 samples). This synthesis route allows a facile preparation of dUPEO containing different amounts of 1 (see amount wt% in Table 1). The second scheme refers to the formation of monolithic xerogels (dUPEO) followed by the cluster adsorption in solution (named CA sample). In this latter case, the cluster concentration within CA was estimated by UV-Vis spectroscopy to be around 1 wt% (see Electronic Supplementary Information (ESI) and Figure S1). Cluster loading concentrations and properties of hybrids are summarized in Table 1. Both methods lead to homogeneous and transparent monoliths as shown in Figure 1. The samples were first characterized by differential scanning calorimetry and small angle X-ray scattering (see ESI TableS1 and Figure S2-S8 for DSC thermograms and interpretation and Figure S9 for SAXS patterns). In the latter case, we noticed that 1 alters the average correlation distance between the ureasil crosslinking nodes (ξd) from 48 Å for dUPEO to 43 Å for E2 and E3. This indicates a small contraction of the polymeric structure and suggests interactions between 1 and the urea or ether groups present in the xerogel, in good accordance with FTIR spectroscopy analysis (see ESI Figures S10-S12). At low q-values the contribution of 1 is observed, which arises from the high electron density contrast between clusters and matrix. A broad peak centered at ~0.35 nm -1 evidences inter-clusters S2 and Figure S15). The microanalysis reveals that 1 is well dispersed at the macroscopic level. However, the appearance of Mo and Br hotspots of tens of micrometers highlights that, at the microscopic level, the cluster distribution is not completely homogenous, in good accordance with SAXS measurements. The elemental composition of the near surface region (< 5 nm) of the loaded samples was obtained from the intensities of XPS high-resolution spectra. Within the experimental error of ±5%, the hybrids composition was close to the nominal concentration of elements. Interestingly, the signal corresponding to the nitrogen content of the xerogel matrix was reduced by a factor 2 after the incorporation of 1. This attenuation is assessed to the interaction of clusters with urea groups. Fitted Cs 3d5/2, Br 3d and Mo 3d spectra of crystalline 1 salt reference and N 1s of pure dUPEO were compared with those recorded for E5. The two cesium components fitted for 1 correspond to the two crystallographic positions of Cs + within the single crystal structure and are located at 724.3 eV and 725.0 eV, respectively. After incorporation dUPEO, only one component located at 724.3 eV was detected with a about 0.2 eV reduced peak width (FWHM), indicative of the equivalence of Cs + cations. The fitted N 1s spectrum of dUPEO shows a main component, related to the urea group at 399.7 eV, and a small sub-peak (~15% peak area) at a binding energy of 401.5 eV, attributed to a group of positively charged nitrogen. The disappearance of the small -N + component for the loaded dUPEO hybrid hints on an interaction between the [Mo6Br14] 2-anion with the urea group. This corroborates well with the attenuation of nitrogen content observed once dUPEO is loaded. Hence, the protonated urea located at the surface of the silica nodes are acting as cluster counter cations. These electrostatic interactions being stronger than those occurring between Cs + and PEO chains, it explains the inhomogeneity observed by µ-X-ray fluorescence spectroscopy at the microscopic level. Emission properties were investigated by steady state and time resolved experiments. To assess about the hybrids stability, photophysical characterizations were realized twice with a time interval of 48 months. Similar results were obtained in both cases. 1) of dUPEO are similar to those already reported for diureasil matrices. [14,21] The dUPEO emission is ascribed to electron-hole recombination mediated by a mechanism typical of donor-acceptor pairs occurring in the urea linkages and in the oxygen-related defects in the siliceous nanodomains. [21a] Increasing the cluster load from E1 to E5 leads to the decrease of the blue emission and the increase of the red-NIR one. For E4 and E5, the diureasil emission band is entirely quenched which indicates a quantitative energy transfer from the diureasil node to [Mo6Br14] 2-. The strong overlap between the absorption band of 1 and the dUPEO emission band, enables resonance energy transfers (RET) based on long-range dipoledipole interactions in the hybrids, [START_REF] Lakowicz | Principles of Fluorescence Spectroscopy[END_REF] as observed for other luminophores. [17b-d, 18-19, 23] Indeed, the Förster radius, i.e. the distance between emitters for which the energy transfer has a probability of 0.5, was estimated to be 4.6 nm (see ESI and Figure S19), [24] value close to the maximal correlation distance determined by SAXS between the diureasil cross-linking nodes. Yet, as represented on the Commission Internationale de l'Eclairage (CIE) chromaticity diagram (Figure 2b), the hybrid emission color can be tailored on the entire visible spectrum by judiciously adjusting the cluster concentration and the excitation wavelength. In particular, for E2, a white emission is observed for an excitation ranging from 365 up to 390 nm. AQY values in air were calculated for several excitations (see ESI Figure S20).

Loading dUPEO with 1 decreases the emitting efficiency of the material, that is ascribed to energy losses occurring during the energy transfers, non-radiative desexcitation and quenching of cluster emission by the surrounding triplet oxygen O2 ( 3 g -). [25] In fact, saturating samples atmosphere with N2 induces a significant increase of the AQY (Table 1 and ESI Figure S20) up to 300% depending on the cluster compound concentration. Time correlated emission properties were then investigated at exc= 375 nm (see ESI Figures S21-S38). Two spectral ranges were observed corresponding respectively to the diureasil and to the cluster emission windows. Kinetic parameters of diureasil nodes could be recorded up to a loading concentration of 1 wt%. The diureasil emission decay was fitted using a three components exponential function as suggested by Fu et al. [26] However, for the ease of understanding, only average lifetime values will be considered herein (see ESI table S3 for a full report on kinetic data). Increasing cluster content in dUPEO induces a decrease of dUPEO average lifetime value which suggests a better efficiency of the energy transfer between emitters. For the cluster emission window, emission profiles were fitted with two phosphorescent components in the tenth of microsecond scale, in line with the reported literature. [4b, 5, 6b, 9, 27] Increasing the cluster content induces a lowering of its average lifetime values (Figure 2c) assessed to the increased gas permeability of the host matrix that favors O2 diffusion within the material. Indeed, it is well known that metal cluster excited triplet states [27] are efficiently quenched by triplet oxygen, and this property was already used to design oxygen sensors. [4,25,28] In conclusion, highly stable organic inorganic emissive hybrids were obtained by combining Cs2Mo6Br14 with an ormocer diureasil containing poly(ethyleneoxide) chains. The homogeneity of samples is imparted to supramolecular interactions between the cluster salt Cs + cations and the PEO chains, and, to electrostatic interactions between the protonated urea located at the surface of silica nodes and the inorganic anions. All samples are macroscopically homogeneous up to 10 wt% doping. Steady state and lifetime emission measurements demonstrate the occurrence of an energy transfer between the blue-green emitting diureasil moieties and the red-NIR emissive clusters. This transfer becomes quantitative for cluster loads higher than 3 wt%. Hence, by an adequate choice of cluster concentration and irradiation wavelength, the emission color can be finely tuned and spread the all visible range including white, making these materials candidates of choice for optoelectronic or lighting applications.

  s c r i p t interactions, due to the coexistence of dense aggregates. The distribution of 1 within the most loaded xerogel matrices, namely E4 and E5, was further investigated by X-ray fluorescence spectroscopy (see ESI Figure S13-14) and X-ray photoelectron spectroscopy (see ESI, Table

Figure 1 .

 1 Figure 1. Structure of octahedral Cs2Mo6Br14 metal cluster compound (1), diureasil PEO (dUPEO) hybrid sol and synthetic schemes for the preparation of unloaded and loaded dUPEO xerogel containing 1.

Figure 2a

 2a Figure 2a presents the normalized emission spectra observed for all samples at exc= 350-380 nm (see ESI, Figure S16 for excitation vs. emission maps and Figures S17 -S18 for other excitation wavelength). The emission envelope and absolute quantum yield (AQY, Table1) of dUPEO are similar to those already reported for diureasil matrices.[14,21] The dUPEO emission is ascribed to electron-hole recombination mediated by a mechanism typical of donor-acceptor pairs occurring in the urea linkages and in the oxygen-related defects in the siliceous nanodomains.[21a] Increasing the cluster load from E1 to E5 leads to the decrease of the blue emission and the increase of the red-NIR one. For E4 and E5, the diureasil emission band is entirely quenched which indicates a quantitative energy transfer from the diureasil node to [Mo6Br14] 2-. The strong overlap between the absorption band of 1 and the dUPEO emission band, enables resonance energy transfers (RET) based on long-range dipoledipole interactions in the hybrids,[START_REF] Lakowicz | Principles of Fluorescence Spectroscopy[END_REF] as observed for other luminophores.[17b-d, 18-19, 23] Indeed, the Förster radius, i.e. the distance between emitters for which the energy transfer has a probability of 0.5, was estimated to be 4.6 nm (see ESI and FigureS19),[24] value close to the maximal correlation distance determined by SAXS between the diureasil cross-linking nodes. Yet, as represented on the Commission Internationale de l'Eclairage (CIE) chromaticity diagram (Figure2b), the hybrid emission color can be tailored on the entire visible spectrum by judiciously adjusting the cluster concentration and the excitation wavelength. In particular, for E2, a white emission is observed for an excitation ranging from 365 up to 390 nm. AQY values in air were calculated for several excitations (see ESI FigureS20). Loading dUPEO with 1 decreases the emitting efficiency of the material, that is ascribed to energy losses occurring during the energy transfers, non-radiative desexcitation and quenching of cluster emission by the surrounding triplet oxygen O2 ( 3 g -).[25] In fact, saturating samples atmosphere with N2 induces a significant increase of the AQY (Table1 and ESI Figure S20) up to 300% depending on the cluster compound concentration. Time correlated emission properties were then investigated at exc= 375 nm (see ESI FiguresS21-S38). Two spectral ranges were observed corresponding respectively to the diureasil and to the cluster emission windows. Kinetic parameters of diureasil nodes could be recorded up to a loading concentration of 1 wt%. The diureasil emission decay was fitted using a three components exponential function as suggested by Fu et al.[26] However, for the

Figure 2

 2 Figure 2.a) Normalized emission spectra of hybrid materials irradiated between 350-380 nm; b) CIE 1938 diagram coordinates for excitation ranging from 365 up to 450 nm: dUPEO (black), E1 (red), E2 (blue), E3 (green), E4 (purple, E5 (maroon) and CA (cyan); c) phosphorescence emission decay profiles recorded in the metal cluster emission range (662-798 nm).

  the Brazilian National Synchrotron Light Laboratory (LNLS) for his help and access to the SAXS1 beamline, and H. W. P. de Carvalho (CENA-USP) for μ-XRF analysis (EMU-FAPESP grant 2015/19121-8). Keywords: hybrid materials • luminescence • energy transfers interactions, metal nanoclusters and hybrid diureasil matrices can be intimately mixed to design tailored emissive materials. Eduardo Ferreira Molina,* Natana Aparecida Martins de Jesus, Serge Paofai, Peter Hammer, Maria Amela-Cortes, Malo Robin, Stephane Cordier,

Table 1 .

 1 Glass transition temperature, Tg, cluster content, kinetic parameters and absolute quantum yield (AQY) of prepared hybrids.

		Tg (°C) 1 (wt%)	Kinetic parameters		AQY b
				ureasil	Cluster	Air	N2
				range	range
				av/ ns a	av / µs a
	dUPEO	-58.3	0	6.0	-	0.18	-
	E1	-55.5	0.1	4.7	66.7	0.09	0.12
	E2	-51.7	0.5	4.1	44.7	0.07	0.12
	E3	-49.7	1	3.6	49.4	0.07	0.12
	E4	-48.1	3	-	37.6	0.06	0.17
	E5	-31.1	10	-	30.2	0.05	0.15
	CA	-51.3	~1	1.9	42.9	0.04	0.14

a av = (aii 2 )/(aii); b error on values is estimated at ±10%

Acknowledgements

This work was supported by the Brazilian agencies: Coordenação de Aperfeiçoamento de Pessoal de Nível Superior -(CAPES) -Finance Code 001, Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq n° 306271/2017-6, Fundação de Amparo à Pesquisa do Estado de São Paulo (SPRINT-FAPESP grant n° 2017/50286-9), and CNRS (PRC Clustobrane 2018-2019). The authors thank Huntsman Performance Products for