---
abstract: '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 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.'
author:
- Arnaud Carayol
- Christof Löding
- Olivier Serre
title: Pure Strategies in Imperfect Information Stochastic Games
---

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 [@RW87], 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 [@Reif84].

Recently in [@GS09; @BGG09] two (mainly equivalent) models of concurrent stochastic games with imperfect information have been introduced. They permit to capture several known models (as those from [@dAH00; @chatterjeePHD; @CDHR07]) while preserving the main decidability results.

In this paper we consider the games as introduced in [@GS09; @BGG09] (we use the formalism of [@GS09]). 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 (is there a final state eventually visited?), safety (are forbidden states never visited?), Büchi (is there a final state that is visited infinitely often?) and co-Büchi (are forbidden states finitely often visited?). 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.

In [@GS09; @BGG09] 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 ${\varphi}$ that is almost-surely winning against any strategy $\psi$ of [Adam]{}(meaning that an infinite play played according to ${\varphi}$ and $\psi$ [is won by [Eve]{}]{} with probability $1$). It was also established in [@BGG09] 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, [@FPS13] 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 [@CarayolHS14], 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. ]{}

Our main results are the following.

-   On the negative side, by a reduction of the value $1$ problem for probabilistic word automata [@GO10], 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 \[sec:undecidability\]).

-   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 \[sec:positive-reachability\]). 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 \[sec:as\]). Moreover, if 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 [@CD]. 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 [@CD] 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 Section \[sec:definitions\] we introduce the basic concepts. In Section \[sec:undecidability\] we present the undecidability results. In Section \[sec:positive-reachability\] we address the decidability of whether [Eve]{}positively wins in a reachability game and we use this result in section \[sec:as\] when considering almost-sure winning for Büchi conditions. Section \[sec:lowerbound\] gives matching lower bounds for the results in Sections \[sec:positive-reachability\] and \[sec:as\]. Finally Section \[sec:summary\] summarises the positive and negative results presented in the paper.]{}

Definitions {#sec:definitions}
===========

A [***probability distribution***]{} over a finite set $X$ is a mapping $d:X\rightarrow [0,1]$ such that ${\sum_{x\in X}d(x)=1}$. In the sequel we denote by ${\mathcal{D}(X)}$ the set of probability distributions over $X$. Given some set $X$ and some equivalence relation $\sim$ over $X$, $[x]_{\sim}$ stands for the equivalence class of $x$ for $\sim$ and $X/_{\sim}=\{[x]_{\sim}\mid x\in X\}$ denotes the set of equivalence classes of $\sim$. As usual we write $A^*$ ([*resp.*]{}$A^\omega$) for the set of finite ([*resp.*]{}infinite) words over some finite alphabet $A$. For $k\geq 0$ we denote by $A^{\geq k}$ ([*resp.*]{}$A^{\leq k}$) the set of words of length at least ([*resp.*]{}at most) $k$.

[ A [***concurrent arena with imperfect information***]{} (or simply an [***arena***]{}) is a tuple ${\mathcal{A}}= \langle{S},{\Sigma}_{E},{\Sigma}_{A},{\delta},{\sim}_{E},{\sim}_{A}\rangle$ where ${S}$ is a finite set of [***states***]{}; ${\Sigma}_{E}$ ([*resp.*]{}${\Sigma}_{A}$) is the (finite) set of [***actions***]{} for [Eve]{}([*resp.*]{}[Adam]{}); ${\delta}: {S}\times{\Sigma}_{E}\times {\Sigma}_{A}\rightarrow {\mathcal{D}({S})}$ is the (total) transition function; and ${\sim}_{E}$ and ${\sim}_{A}$ are equivalence [relations]{} over states.]{}

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 ${\sigma}_{E}\in{\Sigma}_{E}$ and, *simultaneously* and *independently*, the second player, [Adam]{}, chooses an action ${\sigma}_{A}\in{\Sigma}_{A}$. Then a successor state is chosen according to the probability distribution ${\delta}(s,{\sigma}_{E},{\sigma}_{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({\sigma}_{E}^0,{\sigma}_{A}^0)s_1({\sigma}_{E}^1,{\sigma}_{A}^1)s_2\cdots$ in $({S}\cdot({\Sigma}_{E}\times{\Sigma}_{A}))^\omega$ such that for every $i\geq 0$, ${{\delta}(s_i,{\sigma}_{{E}}^{i},{\sigma}_{{A}}^{i})(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 ${\sim}_{E}$ ([*resp.*]{}${\sim}_{A}$) is that two states $s_1$ and $s_2$ such that $s_1{\sim}_{{E}} s_2$ (resp. $s_1{\sim}_{{A}} s_2$) cannot be distinguished by [Eve]{}([*resp.*]{}by [Adam]{}). We easily extend relation ${\sim}_X$, with $X\in\{{E},{A}\}$, to partial plays as follows. First, for any partial play ${\lambda}=s_0({\sigma}_{E}^0,{\sigma}_{A}^0)s_1({\sigma}_{E}^1,{\sigma}_{A}^1)\cdots s_k$ denote $[{\lambda}]_{{\sim}_X}=[s_0]_{{\sim}_X}[s_1]_{{\sim}_X}\cdots [s_k]_{{\sim}_X}$; then define ${\lambda}{\sim}_X{\lambda}'$ if and only if $[{\lambda}]_{{\sim}_X}=[{\lambda}']_{{\sim}_X}$ .

[We say that [Adam]{}is [***more informed***]{} than [Eve]{}if ${\sim}_{A}\subseteq {\sim}_{E}$, and [Adam]{}is [***perfectly informed***]{} if ${\sim}_{A}$ is the equality relation.]{}

An [***observation-based pure strategy***]{} (simply called strategy in the following) for [Eve]{}is a function ${{\varphi}}:
({S}/_{{\sim}_{E}})^*\rightarrow {\Sigma}_{E}$, *i.e.*, to choose her next action, Eve considers the sequence of observations she [has seen]{} so far. We [overload]{} ${{\varphi}}$ by writing ${{\varphi}}({\lambda})$ instead of ${{\varphi}}([{\lambda}]_{{\sim}_{E}})$: in particular, a strategy ${{\varphi}}$ [for [Eve]{}]{} is such that ${{\varphi}}({\lambda})={{\varphi}}({\lambda}')$ whenever ${\lambda}{\sim}_{E}{\lambda}'$ [(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.

Let ${\mathcal{A}}= \langle{S},{\Sigma}_{E},{\Sigma}_{A},{\delta},{\sim}_{E},{\sim}_{A},\rangle$ be an arena, let $s_0\in {S}$ be an initial state, ${{\varphi}}_{E}$ be a strategy for [Eve]{}and ${{\varphi}}_{A}$ be a strategy for [Adam]{}. First we let ${Outcomes(s_0,{{\varphi}}_{E},{{\varphi}}_{A})}$ to be the set of all possible plays when the game starts in $s_0$ and when [Eve]{}and [Adam]{}respectively follows ${{\varphi}}_{E}$ and ${{\varphi}}_{A}$. More formally, a play ${\lambda}= s_0({\sigma}_{E}^0,{\sigma}_{A}^0)s_1({\sigma}_{E}^1,{\sigma}_{A}^1)\cdots$ belongs to ${Outcomes(s_0,{{\varphi}}_{E},{{\varphi}}_{A})}$ iff [${\delta}(s_i,{{\varphi}}_{E}([s_0]_{/{{\sim}_{E}}}[s_0]_{/{{\sim}_{E}}}\cdots [s_i]_{/{{\sim}_{E}}}),{{\varphi}}_{A}([s_0]_{/{{\sim}_{A}}}[s_0]_{/{{\sim}_{A}}}\cdots [s_i]_{/{{\sim}_{A}}})(s_{i+1})>0$]{} for every $i\geq 0$. Then we are interested in defining the probability of a (measurable) set of plays, knowing that [Eve]{}([*resp.*]{}[Adam]{}) uses ${{\varphi}}_{E}$ ([*resp.*]{}${{\varphi}}_{A}$). This is done in the usual way (see *e.g.* [@chatterjeePHD]): once a pair $({{\varphi}}_{E},{{\varphi}}_{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 $\sigma$-field generated by the cones, where for any partial play ${\lambda}$ starting in $s_0$ the cone for ${\lambda}$ is the set ${cone({\lambda})}={\lambda}\cdot (({\Sigma}_{E}\times{\Sigma}_{A})\cdot{S})^\omega$ of all infinite plays with prefix ${\lambda}$. We let ${{Pr}_{s_0}^{{{\varphi}}_{E},{{\varphi}}_{A}}}$ denote the corresponding probability measure over this space.

An [***objective***]{} for [Eve]{}is a (measurable) set ${\mathcal{O}}$ of plays: a play is won by [Eve]{}if it belongs to ${\mathcal{O}}$; otherwise it is won by [Adam]{}. A [***concurrent game with imperfect information***]{} (simply called game in the following) is a triple ${\mathbb{G}}= ({\mathcal{A}},s_0,{\mathcal{O}})$ where ${\mathcal{A}}$ is an arena, $s_0$ is an initial state and ${\mathcal{O}}$ is an objective. In the sequel we focus on the following special classes of objectives (note that all of them are Borel sets hence, measurable) that we define using a subset $F\subseteq {S}$ of [***final***]{} states.

A [***reachability objective***]{} ([*resp.*]{}[***safety***]{}) is of the form $({S}\cdot ({\Sigma}_{E}\times{\Sigma}_{A}))^*{F}( ({\Sigma}_{E}\times{\Sigma}_{A})\cdot{S})^\omega$ ([*resp.*]{}of the form $(({S}\setminus F)\cdot ({\Sigma}_{E}\times{\Sigma}_{A}))^\omega$) : 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 $\bigcap_{k\geq 0}({S}\cdot  ({\Sigma}_{E}\times{\Sigma}_{A}))^{\geq k}{F}(({\Sigma}_{E}\times{\Sigma}_{A})\cdot{S})^\omega$ ([*resp.*]{}of the form $({S}\cdot  ({\Sigma}_{E}\times{\Sigma}_{A}))^* (({S}\setminus F)\cdot  ({\Sigma}_{E}\times{\Sigma}_{A}))^\omega$) : 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 $\mathcal{O}$ by $F$ when it is clear from the context which objective we consider.

Fix a game ${\mathbb{G}}= ({\mathcal{A}},s_0,{\mathcal{O}})$. [ A strategy ${{\varphi}}_{E}$ for [Eve]{}is [***surely winning***]{} if, for any counter-strategy ${{\varphi}}_{A}$ for [Adam]{}, ${Outcomes(s_0,{{\varphi}}_{E},{{\varphi}}_{A})}\subseteq {\mathcal{O}}$. If such a strategy exists, we say that [Eve]{}[***surely wins***]{} ${\mathbb{G}}$.]{} A strategy ${{\varphi}}_{E}$ for [Eve]{}is [***almost-surely winning***]{} ([*resp.*]{}[***positively winning***]{}) if, for any counter-strategy ${{\varphi}}_{A}$ for [Adam]{}, ${{Pr}_{s_0}^{{{\varphi}}_{E},{{\varphi}}_{A}}}({\mathcal{O}})=1$ ([*resp.*]{}$>0$). If such a strategy exists, we say that [Eve]{}[***almost-surely wins***]{} ([*resp.*]{}[***positively wins***]{}) ${\mathbb{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:noDeterminacy\] Consider the (perfect information) concurrent reachability game depicted below with ${q_f}$ as 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.

=\[-&gt;,shorten &gt;=1pt,looseness=7,\] =\[in=55,out=125,loop\] (q\_0) at (0,0) [${q_w}$]{};

(q\_f) at (2,0) [${q_f}$]{};

(q\_0) to node\[above\] [${0}{\!\mid\!}{1}$]{} node\[above\]\[yshift=4mm\] [${1}{\!\mid\!}{0}$ ]{}(q\_f); (q\_0) edge \[loop top\] node\[above\] [${0}{\!\mid\!}{0}\;\; {1}{\!\mid\!}{1}$]{} (q\_0); (q\_f) edge \[loop top\] node\[above\] [${*}{\!\mid\!}{*}$]{} (q\_f);

Indeed, given any strategy ${{\varphi}}_{E}$ for [Eve]{}, the counter-strategy ${{\varphi}}_{A}$ for [Adam]{}mirroring the strategy of [Eve]{} (*i.e.*  ${{\varphi}}_{A}={{\varphi}}_{E}$) only allows for the play ${q_w}^\omega$ and hence, ${{Pr}_{s_0}^{{{\varphi}}_{E},{{\varphi}}_{A}}}({\mathcal{O}})=0$. Similarly [Adam]{}does not have an almost-surely winning strategy. For any fixed strategy ${{\varphi}}_{A}$ of [Adam]{}, any counter-strategy ${{\varphi}}_{E}$ for [Eve]{}that satisfies ${{\varphi}}_{E}({q_w}) \neq
 {{\varphi}}_{A}({q_w})$ is such that ${{Pr}_{s_0}^{{{\varphi}}_{E},{{\varphi}}_{A}}}({\mathcal{O}})=1$.

Undecidability Results {#sec:undecidability}
======================

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 $\omega$-automata from [@BBG08] 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 $\omega$-automaton and the strategy of [Eve]{}corresponds to the input word.]{}

\[Th:undecidabilityPOMDP\] [The decision problems whether [Eve]{}almost-surely wins a given co-Büchi game or positvely wins a given Büchi game are undecidable (even if the set of actions of [Adam]{}is a singleton). ]{}

Consider a probabilistic automaton $\mathcal{A}$ on $\omega$-words as in [@BBG08]. 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 $\mathcal{A}$ and whose states are the [ones]{} of the automaton. Moreover all states are ${\sim}_{E}$-equivalent. Now the transition function of the game mimics the [one]{} of the automaton. As [Eve]{}does not observe anything, a (pure) strategy ${\varphi}$ of [Eve]{}can be described as an infinite word $u_{\varphi}$ in $A$ (the $i$-th letter being the $i$-th action played by [Eve]{}), and ${\varphi}$ is almost-surely (*resp.* positively) winning iff the probability of a run of $\mathcal{A}$ over $u_{\varphi}$ 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 [@BBG08].

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 [@GO10]. For simpler use in our reduction we reformulate this problem in terms of games.

Consider the class of concurrent reachability games ${\mathbb{G}}$ with imperfect information with the following properties. [Eve]{}is blind (*i.e.* ${\sim}_{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 $\sharp$ 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 $\sharp$ 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 they correspond to probabilistic automata on finite words (see [@Paz71] for an introduction to probabilistic automata): a strategy of [Eve]{}corresponds to a finite word followed by $\sharp$ (without playing $\sharp$ [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 such automata [@GO10].

\[lem:value1\] For a given a PA game, it is undecidable whether Eve has for each $0 < \varepsilon < 1$ a strategy that is winning with probability $(1-\varepsilon) < p < 1$.

[3]{}[0.55]{}[0pt]{}[6]{} Our reduction that uses Lemma \[lem:value1\] starts from an example of a concurrent safety game known as *Hide-or-Run* [@dAHK07]. 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 [@dAHK07] 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 all $i$ and $\prod_i p_i>
0$ (for this, [Eve]{}does not have to distinguish the states).

Now the idea is to incorporate a gadget in ${\mathbb{G}}_{HR}$ that permits [Eve]{}to simulate random choices while playing deterministically.

\[theo:undecidable-positive-safety\] It is undecidable whether [Eve]{}positively wins in a safety game (resp. co-Büchi game), even if ${\sim}_{E}$ consists of a single equivalence class.

Consider a probabilistic automaton game ${\mathbb{G}}$ with a set of actions disjoint from the one in the game ${\mathbb{G}}_{HR}$. Let ${\mathbb{G}}_r$ and ${\mathbb{G}}_h$ be two disjoint copies of ${\mathbb{G}}$ where we removed the two states reachable by [Eve]{}playing $\sharp$ (the $\sharp$-edges are redirected as described below).

In the game ${\mathbb{G}}_{HR}'$ (see Figure \[Figure:HRB\]), the concurrent choices of the actions in ${\mathbb{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 ${\mathbb{G}}_r$ or ${\mathbb{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 ${\mathbb{G}}_r$ and ${\mathbb{G}}_h$ we removed the target states of $\sharp$ but [Eve]{}can still play $\sharp$: if in ${\mathbb{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 \[Figure:HRB\]).

Finally, in order to prevent [Eve]{}from playing an [infinite sequence of actions without $\sharp$]{}, 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 $\sharp$ from $s_c$ then the play goes to a sink state $s_w$ (that is not final); if she does not play $\sharp$ 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 $\sharp$, then the play almost-surely ends in $s_l$.

=\[-&gt;,shorten &gt;=1pt,looseness=7,\] =\[in=55,out=125,loop\] (qhide) at (0,4) [$s_{hide}$]{}; (qhome) at (-4,0) [$s_{home}$]{}; (qwet) at (4,0) [$s_{wet}$]{}; (qhome) edge \[loop left\] node\[left\] [${*}{\!\mid\!}{*}$]{} (qhome); (qwet) edge \[loop right\] node\[right\] [${*}{\!\mid\!}{*}$]{} (qwet);

(nameGr) at (-1.5,2) [${\mathbb{G}}_r$]{}; (finalGr) at (-2,1) ; (nonfinalGr) at (-1,1) ; (-2.5,2.5) – (-2.5,0.5) – (-0.5,0.5) – (-0.5,2.5) – (-2.5,2.5);

(nameGw) at (1.5,2) [${\mathbb{G}}_h$]{}; (finalGw) at (2,1) ; (nonfinalGw) at (1,1) ; (2.5,2.5) – (2.5,0.5) – (0.5,0.5) – (0.5,2.5) – (2.5,2.5);

(sc) at (-2.5,4) [$s_{c}$]{}; (sw) at (-5,1.5) [$s_{w}$]{}; (sl) at (-5,4) [$s_{l}$]{}; (inter) at (-4,4) ; (qhide) to node\[above\] [${*}{\!\mid\!}cheat$]{} (sc); (sc) to node\[right,pos=0.5\] [$\sharp{\!\mid\!}{*}$]{} (sw); (sw) edge \[loop left\] node\[left\] [${*}{\!\mid\!}{*}$]{} (sw); (sl) edge \[loop left\] node\[left\] [${*}{\!\mid\!}{*}$]{} (sl); (sc) to node\[below,pos=0.5\] [$x{\!\mid\!}{*}$]{} (inter); (inter) to node\[above,pos=0.5\] [$1/2$]{} (sl); (inter) to \[bend left=70\] node\[above,pos=0.5\] [$1/2$]{} (sc);

(qhide) to node\[left\] [${*}{\!\mid\!}r$]{} (nameGr); (finalGr) to node\[above\] [$\sharp{\!\mid\!}{*}$]{} (qhome); (nonfinalGr) to\[bend right\] node\[below\] [$\sharp{\!\mid\!}{*}$]{} (qwet);

(qhide) to node\[right\] [${*}{\!\mid\!}h$]{} (nameGw); (finalGw) to\[bend right=60\] node\[right\] [$\sharp{\!\mid\!}{*}$]{} (qhide); (nonfinalGw) to\[bend left\] node\[below\] [$\sharp{\!\mid\!}{*}$]{} (qhome);

Let ${\mathbb{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 ${\mathbb{G}}_{HR}'$ iff [Eve]{}in ${\mathbb{G}}$ has an almost sure winning strategy that is not a sure winning strategy. Indeed, consider a strategy ${\varphi}$ for [Eve]{}in ${\mathbb{G}}_{HR}'$. As [Eve]{}cannot distinguish any state in ${\mathbb{G}}_{HR}'$, and does not observe the actions played by Adam, ${\varphi}$ is independent of Adam’s choices.

[If the strategy of [[Eve]{}]{} consists in playing $\sharp$ only finitely often, it cannot be positively winning as it suffices for [Adam]{}to wait for the last $\sharp$ and then play $cheat$. More precisely, the strategy of [[Adam]{}]{} consists in playing (in state $s_{\textrm{hide}}$) the action $h$ whenever [Eve]{}’s strategy will still play $\sharp$ in the future, and $cheat$ if [Eve]{}will never play $\sharp$ 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 ${\varphi}$ of [${Eve\xspace}$]{} that play $\sharp$ infinitely often. An equivalent description of such strategies ${\varphi}$ is by a sequence $({\varphi}_i)_{i\geq 1}$ of strategies for [Eve]{}in ${\mathbb{G}}$: ${\varphi}$ consists in playing an arbitrary letter then playing as ${\varphi}_1$ until playing $\sharp$, then playing an arbitrary letter, then playing as ${\varphi}_2$ until playing $\sharp$ and so on (the arbitrary letter is used here when [Adam]{}chooses to move to ${\mathbb{G}}_r$, ${\mathbb{G}}_h$ or $s_c$).

For one direction, assume that $\varphi$ is positively winning in ${\mathbb{G}}_{HR}'$. Let $p_i$ be the probability that [Eve]{}wins in ${\mathbb{G}}$ when playing according to ${\varphi}_i$. Then, from the properties of ${\mathbb{G}}_{HR}$, it follows that ${\varphi}$ is winning iff $0<p_i<1$ for all $i\geq 1$ and $\prod_i p_i> 0$. This implies that the sequence $(p_i)_{i\geq 1}$ converges to $1$ and hence the $\varphi_i$ are strategies as in Lemma \[lem:value1\].

Conversely, if [Eve]{}has strategies winning with probabilities arbitrarily close to $1$ as in Lemma \[lem:value1\], then one can choose the ${\varphi}_i$ such that [$1 > p_i \ge
  1-\dfrac{1}{(i+1)^{2}}$]{} which ensures $0<p_i<1$ for all $i\geq 1$ and $\prod_i p_i> 0$. Indeed, $$\prod_{i \geq 1} 1 - \frac{1}{(i+1)^{2}}=\lim_{m \rightarrow \infty} \prod_{i=1}^{m} 1-\frac{1}{(i+1)^{2}} = \lim_{m \rightarrow \infty}  \frac{m+2}{2m+2} = \frac{1}{2}$$ This family $\varphi_i$ defines a strategy for [Eve]{}in ${\mathbb{G}}_{HR}'$. Again using the properties of ${\mathbb{G}}_{HR}$, this implies that [Eve]{}positively wins against all strategies of Adam: either no outcome ever reaches $s_c$, in which case ${\mathbb{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 {#sec:positive-reachability}
======================================

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

[Adam]{}is perfectly informed and

[Adam]{}is more informed than [Eve]{}.

For the rest of this section fix an arena ${\mathcal{A}}= \langle{S},{\Sigma}_{E},{\Sigma}_{A},{\delta},{\sim}_{E},{\sim}_{A}\rangle$ and a set of final states $F\subseteq S$.

To later address almost-sure winning (Section \[sec:as\]) 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 $K$ of states a game $({\mathcal{A}},K,{\mathcal{O}})$ that is played as follows: there is a new initial step where [Adam]{}picks a state $s_0$ in $K$ and then the play [proceeds as]{} in $({\mathcal{A}},s_0,{\mathcal{O}})$. Hence, a strategy ${{\varphi}}$ for [Eve]{}in such a game is almost-surely (*resp.* positively) winning iff ${{\varphi}}$ is almost-surely (*resp.* positively) winning in $({\mathcal{A}},s_0,{\mathcal{O}})$ for *every* state $s_0\in K$.

Winning in a Finite Number of Moves.
------------------------------------

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:positiveWinningReachability\] Let $K\subseteq S$ be a subset of states and assume that [Eve]{}has a positively winning strategy ${{\varphi}}$ in the reachability game $({\mathcal{A}},K,F)$. Then, there is a bound $N$ and some $0<{\varepsilon}_{{K}}\leq 1$ such that whenever [Eve]{}respects ${{\varphi}}$ in game $({\mathcal{A}},K,F)$, the probability that the resulting play visits a final state within the $N$ first moves is at least ${\varepsilon}_K$.

For any $N>0$, any $s\in K$ and any strategy $\psi_N$ for Adam, call $p_N^{\psi_N,s}$ the probability of the event *“a play in $({\mathcal{A}},s,F)$, where [Eve]{}respects ${{\varphi}}$ and [Adam]{}respects $\psi_N$ visits a final state within the $N$ first moves”*.

Let $x_N^{\psi_N}= \min\{p_N^{\psi_N,s}\mid s\in K\}$. We aim to show that there exists some $N>0$ such that for each strategy $\psi_N$ for Adam, $x_N^{\psi_N}>0$.

For this, we reason by contradiction, assuming that for any bound $N>0$, [Adam]{}has a counter strategy $\psi_N$ such that $x_N^{\psi_N}=0$. In particular, there is a state $s\in K$ such that $p_N^{\psi_N,s}=0$ for infinitely many $N$. [Hence, we can assume that the $\psi_N$ are such that]{} $p_N^{\psi_N,s}=0$ for all $N\geq 0$ (as to get the property for some $N$ [Adam]{}can always use the strategy for some $N'>N$).

Using $(\psi_N)_{N\geq 0}$ we define a strategy $\psi$ for [Adam]{}as follows. We first let $I_0=\mathbb{N}$ be the set of naturals. Next we define $\psi$ and $(I_k)_{k\geq 0}$, a decreasing sequence (for inclusion) of *infinite* subsets of the naturals. First we sort partial plays by increasing length. We assume that $\psi$ 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. There are finitely many plays of length $k+1$ while $I_k$ is infinite: hence there is an infinite subset $I_{k+1}\subseteq I_k$ such that all the $\psi_j$ for $j\in  I_{k+1}$ agree on plays of length $k+1$ [and we define $\psi$ to behave accordingly.]{}

The following is a direct consequence of the definition of $\psi$ and $(I_k)_{k\geq 0}$: for all $k\geq 0$, $I_k$ is infinite and for all $j\in I_k$, both $\psi$ and $\psi_j$ agree on any partial play of length smaller than $k$.

In particular it implies that $x_N^{\psi}=0$ for all $N\geq 0$: indeed, $x_N^{\psi_{M}}=0$ for any $M\geq N$ and $\psi$ agrees with all $\psi_{M}$ with $M\in I_N$ (and as $I_N$ is infinite such an $M$ exists). Finally, as $0\leq {{Pr}_{s}^{{{\varphi}},\psi}}({\mathcal{O}})\leq\sum_{N\geq 0} x_N^{\psi}=0$ (here ${\mathcal{O}}$ denotes the reachability objective defined by $F$), we conclude that ${{Pr}_{s}^{{{\varphi}},\psi}}({\mathcal{O}})=0$ which contradicts our initial assumption of ${{\varphi}}$ being positively winning in $({\mathcal{A}},s,F)$.

The fact that there is some ${\varepsilon}>0$ such that ${{\varphi}}$ ensures to reach a final state in less than $N$ moves with a probability greater than ${\varepsilon}$ is a direct consequence of the fact that one bounds the number of moves by $N$.

\[rk:PosReachNoProba\] Proposition \[proposition:positiveWinningReachability\] implies that finite memory suffices for [Eve]{}to positively win in a reachability game. Indeed, it suffices to follow ${{\varphi}}$ 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 ${\mathcal{A}}'$ that is exactly as ${\mathcal{A}}$ except that its transition function $\delta'$ is such that for all states $s$ and any pair of actions $({\sigma}_{E},{\sigma}_{A})$ one has $\delta(s,{\sigma}_{E},{\sigma}_{A})= 0$ iff $\delta'(s,{\sigma}_{E},{\sigma}_{A})= 0$. Then [Eve]{}positively wins in the reachability game $({\mathcal{A}},K,F)$ iff she positively wins in the reachability game $({\mathcal{A}}',K,F)$.

Positively Winning When [Adam]{}Is Perfectly Informed
-----------------------------------------------------

We now assume that [Adam]{}is perfectly informed.

Consider for all $n \geq 0$, the objective ${{\mathrm{Reach}}^{\leq n}}({F})=({S}\cdot({\Sigma}_{E}\times{\Sigma}_{A}))^{< n}{F}(({\Sigma}_{E}\times{\Sigma}_{A})\cdot{S})^{\omega}$ where a final state has to be visited within the first $n$ steps. The following inductively characterises the sets $K$ for which [Eve]{}can win $({\mathcal{A}},K,{{\mathrm{Reach}}^{\leq n}}({F}))$.

\[prop:reachN-ind\] Let $K \subseteq S$ be a set of pairwise ${\sim}_{E}$-equivalent states and let $n > 0$. [Eve]{}positively wins $({\mathcal{A}},K,{{\mathrm{Reach}}^{\leq n}}({F}))$ if and only if there exists an action ${\sigma}_{{E}} \in {\Sigma}_{{E}}$ and a set $K' \subseteq S$ such that

-   [Eve]{}positively wins $({\mathcal{A}},K',{{\mathrm{Reach}}^{\leq n-1}}({F}))$,

-   for all $s \in K \setminus F$ and for all ${\sigma}_{{A}} \in {\Sigma}_{{A}}$, there exists $s' \in K'$ such that $\delta(s,{\sigma}_{{E}},{\sigma}_{{A}})(s')>0$.

Let ${{\varphi}}$ be a positively winning ${\mathcal{T}}$-compatible strategy in ${\mathbb{G}}$. Now use ${{\varphi}}$ in ${\mathbb{G}}$: obviously it is still ${\mathcal{T}}$-compatible and we have to prove that it is positively winning. Consider a strategy $\psi'$ of [Adam]{}in ${\mathbb{G}}'$. Then, assuming [Eve]{}respects ${{\varphi}}$, strategy $\psi'$ can be mimicked in game ${\mathbb{G}}$: indeed, [Adam]{}simply has to update a state $H$ in ${\mathcal{A}}'$ which is done by computing $Up(H,{\sigma}_{E},{\sigma}_{A})$ and observing the equivalence class for ${\sim}_{A}$ relation; assuming [Eve]{}respects ${{\varphi}}$ it means that [Adam]{}always know what action ${\sigma}_{E}$ she will play and therefore can compute $Up(H,{\sigma}_{E},{\sigma}_{A})$. Call $\psi$ the strategy in ${\mathbb{G}}$ mimicking $\psi'$.

Now let $N$ be some integer and consider all those partial plays of length $N$ in ${\mathbb{G}}$ where [Eve]{}respects ${{\varphi}}$ and [Adam]{}respects $\psi$. Group all ${\sim}_{A}$-equivalent such partial play: then for every class consider the set $H$ of possible last states. Then those such $H$ are exactly those states that can be reached in ${\mathbb{G}}'$ in a partial play of length $N$ when [Eve]{}respects ${{\varphi}}$ and [Adam]{}respects $\psi'$. As ${{\varphi}}$ is positively winning in ${\mathbb{G}}$ , thanks to Proposition \[proposition:positiveWinningReachability\] 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 ${\mathbb{G}}'$ using ${{\varphi}}$ against $\psi'$. As this property does not depend on $\psi'$ we conclude that ${{\varphi}}$ is positively winning in ${\mathbb{G}}'$.

Conversely, assume she has a positively winning ${\mathcal{T}}$-compatible strategy in ${\mathbb{G}}'$. Now use ${{\varphi}}$ in ${\mathbb{G}}$: obviously it is still ${\mathcal{T}}$-compatible and we have to prove that it is positively winning. By contradiction, assume [Adam]{}has a strategy $\psi$ that ensures, provided [Eve]{}uses ${{\varphi}}$ in ${\mathbb{G}}$, that no final state is reached. Then, from $\psi$ one can define a strategy in $\psi'$ that consists in a partial play $H_0({\sigma}_{E}^0,{\sigma}_{A}^0)H_1({\sigma}_{E}^1,{\sigma}_{A}^1)\cdots H_k$ to play action $\psi([s_0]_{{\sim}_{A}}\cdots [s_k]_{{\sim}_{A}})$ where $s_i$ is any (they are all ${\sim}_{A}$-equivalent) element in $H_i$ for all $i$. Using the same argument as in the direct implication relating plays in ${\mathbb{G}}$ when using strategies $({{\varphi}},\psi)$ and plays in ${\mathbb{G}}'$ when using strategies $({{\varphi}}',\psi')$, one concludes that playing $\psi'$ against ${\varphi}$ in ${\mathbb{G}}'$ ensures that no final state is visited hence, leading a contradiction with ${\varphi}$ being positively winning in ${\mathbb{G}}'$.

Now, consider the increasing family of sets $(\mathcal{W}_{i})_{i\geq 0}$ defined by:

-   $\mathcal{W}_{0} = \{ K  \mid K \subseteq F \}$

-   $\mathcal{W}_{i+1}= \{ K \subseteq S \mid \forall r \in K,\ \exists {\sigma}_{E}\  \exists K'\in \mathcal{W}_i \  \text{ s.t. } \forall s{\sim}_{E}r \text{ with } s {\in K \setminus F},\ \forall {\sigma}_{A}\ \\\exists s'\in K' \text{ s.t. } \delta(s,{\sigma}_{E},{\sigma}_{A})(s')>0\}$

and call $\mathcal{W}$ its limit. Then the following is a simple consequence of Proposition \[prop:reachN-ind\]

\[theo:semiGame\] Let $K\subseteq{S}$ [be a non-empty set]{}. [Eve]{}has a positively winning strategy ${{\varphi}}$ in the game $({\mathcal{A}},K,{F})$ if and only if $K\in\mathcal{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.]{}

Using Proposition \[prop:reachN-ind\], by a direct induction on $n$ one gets that $K\neq \emptyset$ belongs to $\mathcal{W}_{n}$ if and only if [Eve]{}postively wins $({\mathcal{A}},K,{{\mathrm{Reach}}^{\leq n}}({F}))$.

For any $K \in \mathcal{W}$, we denote by $\mathrm{rk}(K)$ the smallest $n$ such that $K \in \mathcal{W}_n$. Now, for any $K \in \mathcal{W}$, we define a strategy for [Eve]{}denoted ${\varphi}_{K}$ that uses $\mathcal{W}$ as a finite memory. Initially the memory is $K$. For a partial play ${\lambda}$ ending in a state in some equivalence class $[s]_{{\sim}_{{E}}}$ and assuming that the memory is $K'$, we define the strategy as follows:

-   If $\mathrm{rk}(K')>0$ and if there exists $r \in [s]_{\sim_{{E}}} \cap K$, [then by definition of $(\mathcal{W}_i)_{i\geq 0}$ there exists some action ${\sigma}_{{E}}$ and some set $K''$ such that the following holds:]{}

    -   $\mathrm{rk}(K'')=\mathrm{rk}(K')-1$,

    -   $\forall r'{\sim}_{E}r \text{ with } r' \in K \setminus F, \forall {\sigma}_{A},\ \exists s'\in K'', \text{ s.t. } \delta(s,{\sigma}_{E},{\sigma}_{A})(s')>0$.

    [Then we let ${\varphi}_{K}({\lambda})={\sigma}_{{E}}$ and update the memory to $K''$.]{}

-   In all other cases, we take ${\varphi}_{K}({\lambda})$ to be an arbitrary action and update the memory to $\emptyset$.

By induction on $n$, we show that for all non-empty $K \in \mathcal{W}_{n}$, the strategy $\varphi_{K}$ is positively winning in $({\mathcal{A}},K,{{\mathrm{Reach}}^{\leq n}}({F}))$. The base case is immediate. Assume that the property is established for $n-1\geq0$. Let $K$ be a non-empty element of [$\mathcal{W}_{n}$]{}. Let $s_{0} \in K$, $\sigma_{{E}}={\varphi}_{K}([s_{0}]_{{\sim}_{{E}}})$ and $K' \in \mathcal{W}_{n-1}$ be the memory of ${\varphi}_{K}$ after the first move. Let $\psi$ be a strategy for [Adam]{}. Let $\sigma_{{A}}$ be the first action played by [Adam]{}when using $\psi$ and let $\psi'$ be the strategy followed by [Adam]{}after this first step, [*i.e.* ]{}$\psi'({\lambda}) = \psi(s_0 \cdot {({\sigma}_{E},{\sigma}_{A})\cdot}{\lambda})$ for all partial play ${\lambda}$. By definition of $K'$, there exists $s' \in K'$ such that $\delta(s_{0},{\sigma}_{{E}},{\sigma}_{{A}})(s')>0$. Hence, we have: $${{Pr}_{s_0}^{{\varphi}_{K},\psi}}({{\mathrm{Reach}}^{\leq n}}({F})) \geq  \delta(s_{0},{\sigma}_{{E}},{\sigma}_{{A}})(s') \cdot {{Pr}_{s'}^{{\varphi}_{K'},\psi'}}({{\mathrm{Reach}}^{\leq n-1}}({F})) >0.$$ [which concludes the proof.]{}

The following is a restatement of the end of Theorem \[theo:semiGame\].

\[cor:boundingN\] In Proposition \[proposition:positiveWinningReachability\], when [Adam]{}is perfectly informed, one can always choose ${{\varphi}}$ such that $N\leq 2^{|{S}|}$.

Automaton-Compatible Strategies {#sec:automaton-driven}
-------------------------------

The aim of this section is to refine Theorem \[theo:semiGame\] to positively winning strategies that satisfy further constraints. The motivation is that in Section \[sec:as\] 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 ${\mathcal{T}}= \langle Q,{\Sigma}_{E}\times{S}_{/_{{\sim}_{E}}},q_0,q_s,{\delta_{\mathcal{T}}},{Act}\rangle $ be a deterministic finite automaton with input alphabet ${\Sigma}_{E}\times{S}_{/_{{\sim}_{E}}}$, a finite set of states $Q$, an initial state $q_0$, a sink state $q_s$, a transition function ${\delta_{\mathcal{T}}}:Q\times ({\Sigma}_{E}\times{S}_{/_{{\sim}_{E}}})\rightarrow Q$ and a function ${Act}:Q\rightarrow 2^{{\Sigma}_{E}}$ associating with any state of ${\mathcal{T}}$ a subset of actions for [Eve]{}. Moreover, we require that the following holds

-   ${Act}(q)=\emptyset$ if and only if $q=q_s$.

-   For all states $q$ and for all $({\sigma},x)\in {\Sigma}_{E}\times{S}_{/_{{\sim}_{E}}}$ one has ${\delta_{\mathcal{T}}}(q,({\sigma},x))=q_s$ if and only if ${\sigma}\notin{Act}(q)$.

Such a machine associates with any partial play ${\lambda}$ a unique state $q_{\lambda}$ defined by $q_{s_0}=q_0$ and $q_{{\lambda}\cdot ({\sigma}_{E},{\sigma}_{A})\cdot s}= {\delta_{\mathcal{T}}}(q_{\lambda},({\sigma}_{E},[s]_{{\sim}_{E}}))$; it also permits to associate with any partial play a subset of actions by letting ${{{Act}_{\mathcal{T}}}}({\lambda}) = {Act}(q_{\lambda})$.

A strategy ${{\varphi}}$ of [Eve]{}is [***${\mathcal{T}}$-compatible***]{} if for any partial play ${\lambda}$ where [Eve]{}respects ${{\varphi}}$ one has ${{\varphi}}({\lambda})\in{{{Act}_{\mathcal{T}}}}({\lambda})$. Note that it implies that $q_{\lambda}\neq q_s$.

[Remark that unconstrained strategies can be expressed by a trivial automaton that always admits all actions. Hence, any result below also holds if we drop the ${\mathcal{T}}$-compatibility constraint.]{}

In Section \[sec:as\] and for the proof of Theorem \[theo:posTcom\], we work with automata that compute the knowledge of [Eve]{}along a play, as explained below. [For an initial knowledge set $K_0 \subseteq S$ of pairwise ${\sim}_{E}$-equivalent states,]{} the knowledge (also known as belief) ${{Know}_{{E}}^{K_0}}(\lambda)$ of [Eve]{}after a partial play $\lambda$ starting in a state of $K_{0}$, intuitively corresponds to the set of possible states that can have been reached in a play ${\sim}_{E}$-equivalent to ${\lambda}$.

Formally, the value of ${{Know}_{{E}}^{K_0}}(\lambda)$ can be inductively defined as follows: ${{Know}_{{E}}^{K_0}}(s_0)=K_0$ and ${{Know}_{{E}}^{K_0}}(\lambda \cdot({\sigma}_{E},{\sigma}_{A})\cdot s)=
{{UpKnow}_{\!{E}}}({{Know}_{{E}}^{K_0}}(\lambda),{\sigma}_{E},[s]_{{\sim}_{E}})$ where the function ${{UpKnow}_{\!{E}}}:2^{S}\times{\Sigma}_{E}\times [{S}]_{/_{{\sim}_{E}}}\rightarrow 2^{{{S}}}$ is defined by: $${{UpKnow}_{\!{E}}}(K,{\sigma}_{E},[s]_{{\sim}_{E}}) =  \{t \in [s]_{{\sim}_{E}}\mid\exists r\in K,\  \exists{\sigma}_{A}\in {\Sigma}_{A}\text{ s.t. }{\delta}(r,{\sigma}_{E},{\sigma}_{A})(t)>0\}.$$

\[rk:knowtrans\] Given a family $\mathcal{K} \subseteq 2^S$ of knowledges for [Eve]{}(in the sense that each $K \in \mathcal{K}$ is a subset of a ${\sim}_{E}$-class), one can construct an automaton ${\mathcal{T}}_{\mathcal{K}}$ such that the ${\mathcal{T}}_{\mathcal{K}}$-compatible strategies are precisely those such that [Eve]{}’s knowledge always remains inside $\mathcal{K}$. The states of ${\mathcal{T}}_{\mathcal{K}}$ are the elements of $\mathcal{K}$, the transition function is defined by ${{UpKnow}_{\!{E}}}$, and the actions ${Act}(K)$ enabled at a state $K$ are those that ensure that the knowledge remains inside $\mathcal{K}$.

We now return to the strengthening of Theorem \[theo:semiGame\]. We assume that [Adam]{}is *perfectly informed* and we fix an automaton ${\mathcal{T}}= \langle Q,{\Sigma}_{E}\times{S}_{/_{{\sim}_{E}}},q_0,q_s,{\delta_{\mathcal{T}}},{Act}\rangle $ as in Section \[sec:automaton-driven\]. We are interested in checking whether [Eve]{}has a ${\mathcal{T}}$-compatible strategy that is positively winning in the reachability game $({\mathcal{A}},K,F)$.

Our main result is the following and its proof is by two successive reductions and an application of Theorem \[theo:semiGame\].

\[theo:posTcom\] One can decide in time polynomial in $2^{|S|}$ and polynomial in $|Q|$ whether [Eve]{}has a ${\mathcal{T}}$-compatible strategy that is positively winning in the reachability game $({\mathcal{A}},K,F)$. [If such a strategy exists, one can construct one that uses memory of size polynomial in $|Q|$ and exponential in $|S|$.]{}

Note that adding the condition on the strategy being ${\mathcal{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 ${\mathcal{T}}$ ([*i.e.* ]{}she must avoid to produce a partial play ${\lambda}$ with $q_{\lambda}=q_s$). Hence, it is natural to consider an enriched arena ${\mathcal{A}}_{\mathcal{T}}$ that embeds ${\mathcal{T}}$. For this let ${\mathcal{A}}_{\mathcal{T}}= \langle{S}\times Q,{\Sigma}_{E},{\Sigma}_{A},{\delta}',{\approx}_{E},{\approx}_{A}\rangle$ where

-   $\delta'((s,q),{\sigma}_{E},{\sigma}_{A})(s',q')$ equals $\delta(s,{\sigma}_{E},{\sigma}_{A})(s')$ if $q'={\delta_{\mathcal{T}}}(q,({\sigma}_{E},[s']_{{\sim}_{E}}))$ and otherwise it equals $0$;

-   $(s_1,q_1){\approx}_{E}(s_2,q_2)$ if and only if $s_1{\sim}_{E}s_2$ and $q_1=q_2$; and

-   ${\approx}_{A}$ is the equality relation, [*i.e.* ]{}[Adam]{}is perfectly informed.

Of special interest is the safety game $({\mathcal{A}}_{\mathcal{T}},K\times\{q_0\},S\times \{q_s\})$ and we are interested in sure winning for [Eve]{}because of the following straightforward lemma

\[lemma-red1\] [Eve]{}has a (possibly loosing) ${\mathcal{T}}$-compatible strategy in the reachability game $({\mathcal{A}},K,F)$ if and only if she has a surely winning strategy in the safety game $({\mathcal{A}}_{\mathcal{T}},K\times\{q_0\},S\times \{q_s\})$.

It is a known result [@Berwanger08] that when one considers sure winning for [Eve]{}in a safety game, winning strategies only depend on the knowledge of [Eve]{}(in the sense of Section \[sec:automaton-driven\]). More precisely consider the (unique) largest subset $\mathcal{K}$ of knowledges and the (unique) mapping $Aut:\mathcal{K}\rightarrow 2^{{\Sigma}_{E}}$ such that the following holds.

-   No knowledge $K\in\mathcal{K}$ contains a forbidden state.

-   For every $K\in \mathcal{K}$, the set $Aut(K)$ [which]{} consists of all those actions ${\sigma}_{E}\in Aut(K)$ such that for every action ${\sigma}_{A}\in {\Sigma}_{A}$ one has ${{UpKnow}_{\!{E}}}(K,{\sigma}_{E},[s]_{{\sim}_{E}})\in\mathcal{K}\cup\{\emptyset\}$, [is not empty]{}; [*i.e.* ]{}actions in $Aut(K)$ are those that ensure that the updated knowledge will still be in $\mathcal{K}$ regardless of the action of [Adam]{}.

Then [Eve]{}surely wins the safety game from configurations where her knowledge $K$ is in $\mathcal{K}$ and a strategy consists in choosing any action in $Aut(K)$.

Note that in the safety game $({\mathcal{A}}_{\mathcal{T}},K\times\{q_0\},S\times \{q_s\})$, [Eve]{}’s knowledges are elements in $2^S\times Q$ (as we have that $(s_1,q_1){\approx}_{E}(s_2,q_2)$ implies $q_1=q_2$).

Now consider an automaton ${\mathcal{T}}'=\langle Q',{\Sigma}_{E}\times{S}_{/_{{\sim}_{E}}},q_0',q_s',{\delta_{\mathcal{T}'}},{Act}'\rangle $ that *computes* [Eve]{}’s knowledge (as explained in Remark \[rk:knowtrans\]. [Hence, ${\mathcal{T}}'$ is the same as ${\mathcal{T}}_{\mathcal{K}}$]{}) in the previous safety game and uses function $Aut={Act}'$ to define those authorised actions. To fit the definition, merge all knowledges not in $\mathcal{K}$ in a sink state and define $Aut$ to be equal to $\emptyset$ on it. The states $Q'$ of ${\mathcal{T}}'$ are elements of $\mathcal{K}$ (plus the sink state) and take as initial state $q_0'=K\times\{q_0\}$ (which possibly is the sink state). In particular the number of states of ${\mathcal{T}}'$ is exponential in $|S|$ and linear in $|Q|$.

Now one can go back to the original arena and consider the enriched arena ${\mathcal{A}}_{{\mathcal{T}}'}$. Then we have the following easy lemma.

\[lemma-red2\] [Eve]{}has a ${\mathcal{T}}$-compatible positively winning strategy in the reachability game $({\mathcal{A}},K,F)$ if and only if she has a positively winning strategy in the reachability game $({\mathcal{A}}_{{\mathcal{T}}'},K\times\{q_0'\},F\times (Q'\setminus\{q_s'\}))$.

Moreover, from a positively winning strategy in the second game using memory of size $N$ one can effectively construct a ${\mathcal{T}}$-compatible positively winning strategy in the reachability game $({\mathcal{A}},K,F)$ that uses a memory of size $\mathcal{O}(N\times 2^{|S|}\times |Q|)$.

If Eve positively wins in $({\mathcal{A}}_{{\mathcal{T}}'},K\times\{q_0'\},F\times (Q'\setminus\{q_s'\}))$ then we can safely assume that she necessarily always plays authorised (according to ${Act}'$) actions (otherwise the play goes directly to $S\times \{q_s'\}$ and gets trap in it forever, hence cannot reach $F\times (Q'\setminus\{q_s'\}$), hence is ${\mathcal{T}}$-compatible thanks to Lemma \[lemma-red1\]. Such a strategy can be mimicked in the original game and it requires to simulate automaton ${\mathcal{T}}'$ hence, costs an extra memory of size the one of ${\mathcal{T}}'$. Conversely, if it she has a positively winning ${\mathcal{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 \[lemma-red2\] together with Theorem \[theo:semiGame\] concludes the proof of Theorem \[theo:posTcom\].

The Case Where [Adam]{}Is More Informed Than [Eve]{}
----------------------------------------------------

We now assume that [Adam]{}is more informed than [Eve]{}and we fix an automaton ${\mathcal{T}}= \langle Q,{\Sigma}_{E}\times{S}_{/_{{\sim}_{E}}},q_0,q_s,{\delta_{\mathcal{T}}},{Act}\rangle $ as in Section \[sec:automaton-driven\]. Again, we are interested in checking whether [Eve]{}has a ${\mathcal{T}}$-compatible strategy that is positively winning in the reachability game $({\mathcal{A}},K,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 \[theo:posTcom\].

For this let $\mathcal{H}$ be all those subsets of ${S}$ that consist of pairwise ${\sim}_{A}$-equivalent states. For such a subset $H$ and for any pair of actions $({\sigma}_{E},{\sigma}_{A})\in({\Sigma}_{E}\times {\Sigma}_{A})$ define the set $Up(H,{\sigma}_{E},{\sigma}_{A})\in \mathcal{H}$ as follows. First, define $M=\{s'\in S\mid \exists s\in H \text{ s.t. } {\delta}(s,{\sigma}_{E},{\sigma}_{A})(s')>0)\}$ as the set of all possible successors of states in $H$ when playing the pair of actions $({\sigma}_{E},{\sigma}_{A})$ and let $Up(H,{\sigma}_{E},{\sigma}_{A})$ consist of all those non-empty subsets $H'$ that can be written as $H'=M\cap [s]_{{\sim}_{A}}$, [*i.e.* ]{}all possible indistinguishable (for [Adam]{}) subsets of $M$.

Define now a new arena ${\mathcal{A}}' = \langle\mathcal{H},{\Sigma}_{E},{\Sigma}_{A},{\delta}',{\approx}_{E},{\approx}_{A}\rangle$ by letting

-   ${\delta}'(H,{\sigma}_{E},{\sigma}_{A})(H') = 1/|Up(H,{\sigma}_{E},{\sigma}_{A})|$ if $H'\in Up(H,{\sigma}_{E},{\sigma}_{A})$ and $0$ otherwise;

-   $H_1{\approx}_{E}H_2$ if $s_1{\sim}_{E}s_2$ for all $s_1\in H_1$ and $s_2\in H_2$; and

-   ${\approx}_{A}$ is the equality relation, [*i.e.* ]{}[Adam]{}is perfectly informed.

Define the set of final states $F'$ as those elements $H$ in $\mathcal{H}$ such that $H\cap F\neq \emptyset$.

Note that the equivalence classes of ${\approx}_{E}$ can be identified with the equivalence classes of ${\sim}_{E}$ (because ${\sim}_{A}\subseteq {\sim}_{E}$) and therefore one can define ${\mathcal{T}}$-compatible strategies for [Eve]{}also in a play in ${\mathcal{A}}'$. More generally, any [Eve]{}’s strategy in one game can be used in the other one.

For a set $K\subseteq {S}$ define $\nu(K)\in \mathcal{H}$ as $\nu(K)=\{\{s\}\mid s\in K\}$. The following proposition relates game $({\mathcal{A}},K,F)$ and game $({\mathcal{A}}',\nu(K),F')$.

\[prop:moreinftoperfect\] An [Eve]{}’s strategy is a positively winning ${\mathcal{T}}$-compatible strategy in ${\mathbb{G}}=({\mathcal{A}},K,F)$ if and only if it is a positively winning ${\mathcal{T}}$-compatible strategy in ${\mathbb{G}}'=({\mathcal{A}}',\nu(K),F')$.

Let ${{\varphi}}$ be a positively winning ${\mathcal{T}}$-compatible strategy in ${\mathbb{G}}$. Now use ${{\varphi}}$ in ${\mathbb{G}}$: obviously it is still ${\mathcal{T}}$-compatible and we have to prove that it is positively winning. Consider a strategy $\psi'$ of [Adam]{}in ${\mathbb{G}}'$. Then, assuming [Eve]{}respects ${{\varphi}}$, strategy $\psi'$ can be mimicked in game ${\mathbb{G}}$: indeed, [Adam]{}simply has to update a state $H$ in ${\mathcal{A}}'$ which is done by computing $Up(H,{\sigma}_{E},{\sigma}_{A})$ and observing the equivalence class for ${\sim}_{A}$ relation; assuming [Eve]{}respects ${{\varphi}}$ it means that [Adam]{}always know what action ${\sigma}_{E}$ she will play and therefore can compute $Up(H,{\sigma}_{E},{\sigma}_{A})$. Call $\psi$ the strategy in ${\mathbb{G}}$ mimicking $\psi'$.

Now let $N$ be some integer and consider all those partial plays of length $N$ in ${\mathbb{G}}$ where [Eve]{}respects ${{\varphi}}$ and [Adam]{}respects $\psi$. Group all ${\sim}_{A}$-equivalent such partial play: then for every class consider the set $H$ of possible last states. Then those such $H$ are exactly those states that can be reached in ${\mathbb{G}}'$ in a partial play of length $N$ when [Eve]{}respects ${{\varphi}}$ and [Adam]{}respects $\psi'$. As ${{\varphi}}$ is positively winning in ${\mathbb{G}}$ , thanks to Proposition \[proposition:positiveWinningReachability\] 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 ${\mathbb{G}}'$ using ${{\varphi}}$ against $\psi'$. As this property does not depend on $\psi'$ we conclude that ${{\varphi}}$ is positively winning in ${\mathbb{G}}'$.

Conversely, assume she has a positively winning ${\mathcal{T}}$-compatible strategy in ${\mathbb{G}}'$. Now use ${{\varphi}}$ in ${\mathbb{G}}$: obviously it is still ${\mathcal{T}}$-compatible and we have to prove that it is positively winning. By contradiction, assume [Adam]{}has a strategy $\psi$ that ensures, provided [Eve]{}uses ${{\varphi}}$ in ${\mathbb{G}}$, that no final state is reached. Then, from $\psi$ one can define a strategy in $\psi'$ that consists in a partial play $H_0({\sigma}_{E}^0,{\sigma}_{A}^0)H_1({\sigma}_{E}^1,{\sigma}_{A}^1)\cdots H_k$ to play action $\psi([s_0]_{{\sim}_{A}}\cdots [s_k]_{{\sim}_{A}})$ where $s_i$ is any (they are all ${\sim}_{A}$-equivalent) element in $H_i$ for all $i$. Using the same argument as in the direct implication relating plays in ${\mathbb{G}}$ when using strategies $({{\varphi}},\psi)$ and plays in ${\mathbb{G}}'$ when using strategies $({{\varphi}}',\psi')$, one concludes that playing $\psi'$ against ${\varphi}$ in ${\mathbb{G}}'$ ensures that no final state is visited hence, leading a contradiction with ${\varphi}$ being positively winning in ${\mathbb{G}}'$.

Combining Proposition \[prop:moreinftoperfect\] with Theorem \[theo:posTcom\] directly leads the following result.

\[theo:posTcomMore\] One can decide in time polynomial in $2^{2^{|S|}}$ and polynomial in $|Q|$ whether [Eve]{}has a ${\mathcal{T}}$-compatible strategy that is positively winning in the reachability game $({\mathcal{A}},K,F)$. [If such a strategy exists, one can construct one that uses memory of size polynomial in $|Q|$ and doubly exponential in $|S|$.]{}

Almost-Surely Winning [for Büchi Conditions]{} {#sec:as}
==============================================

For the rest of this section fix an arena ${\mathcal{A}}= \langle{S},{\Sigma}_{E},{\Sigma}_{A},{\delta},{\sim}_{E},{\sim}_{A}\rangle$ and a set of final states $F\subseteq 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 knowledges***]{} of [Eve]{}, denoted ${\mathcal{K}^{{AS}}_{}}$, which is the set of subsets $K \subseteq {S}$ such that $K \subseteq [s]_{{\sim}_{E}}$ for some $s \in {S}$ and for which [Eve]{}has an almost-surely winning strategy in the Büchi game ${\mathbb{G}}_K=({\mathcal{A}},K,F)$.

Theorem \[theo:KASFixpoint\] below states that the set ${\mathcal{K}^{{AS}}_{}}$ can be expressed as the greatest fix-point of a [(monotone)]{} mapping ${\Xi}: 2^{2^{S}} \rightarrow
2^{2^{S}}$ defined as follows. Let $\mathcal{K}\subseteq
2^{S}$ and let $K\in\mathcal{K}$. We say that $K$ belongs to ${\Xi}(\mathcal{K})$ if [Eve]{}has a strategy in the *reachability* game $({\mathcal{A}},K,F)$ which is positively winning and guarantees that her knowledge always stays in $\mathcal{K}$.

\[theo:KASFixpoint\] ${\mathcal{K}^{{AS}}_{}}$ is the greatest fixpoint of ${\Xi}$.

For a subset $\mathcal{K}$ of knowledges, say that an [Eve]{}’s knowledge $K$ is [***$\mathcal{K}$-good***]{} if she has a strategy in the *reachability* game $({\mathcal{A}},K,F)$ which is positively winning and guarantees that her knowledge always stays in $\mathcal{K}$.

We first argue that ${\mathcal{K}^{{AS}}_{}}$ is a fixpoint for ${\Xi}$. For this we consider [any]{} $K\in{\mathcal{K}^{{AS}}_{}}$ and prove that it is ${\mathcal{K}^{{AS}}_{}}$-good. We denote by ${\mathbb{G}}_K$ the Büchi game $({\mathcal{A}},K,F)$ and we start with a simple lemma.

\[lemma:StayInWK\] Let $K\in{\mathcal{K}^{{AS}}_{}}$. Let ${\varphi}$ be *any* strategy for [Eve]{}that is almost-surely winning for her in ${\mathbb{G}}_K$ and let ${\sigma}_{E}= {\varphi}([K]_{{\sim}_{E}})$. Then, for any ${\sigma}_{A}\in {\Sigma}_{A}$, for any $t$ such that $\exists s\in K$ with ${\delta}(s,{\sigma}_{E},{\sigma}_{A})(t)>0$, ${{UpKnow}_{\!{E}}}(K,{\sigma}_{E},[t]_{{\sim}_{E}}) \in{\mathcal{K}^{{AS}}_{}}$.

Consider some action ${\sigma}_{A}$ and some $t$ such that ${\delta}(s,{\sigma}_{E},{\sigma}_{A})(t)>0$ and let $K'={{UpKnow}_{\!{E}}}(K,{\sigma}_{E},[t]_{{\sim}_{{E}}})$. By definition of [${{UpKnow}_{\!{E}}}$]{}, for all $t'\in K'$, there is some $s'\in K$ and some action ${\sigma}^{t'}_{A}$ such that ${\delta}(s',{\sigma}_{E},{\sigma}^{t'}_{A})(t')>0$. Now, define the strategy ${\varphi}'$ of [Eve]{}by letting ${\varphi}'(\lambda) = {\varphi}([s]_{{\sim}_{E}}\cdot \lambda)$ for any partial play $\lambda$. We claim that ${\varphi}'$ is almost-surely winning for [Eve]{}in ${\mathbb{G}}_{t'}$ for any $t'\in K'$, hence implying that $K'\in {\mathcal{K}^{{AS}}_{}}$. By contradiction, assume that ${\varphi}'$ is not almost-surely winning for some ${\mathbb{G}}_{t'}$ with $t'\in K'$ and let $\psi'$ be a counter-strategy for [Adam]{}in ${\mathbb{G}}_{t'}$, *i.e.* ${{Pr}_{t'}^{{\varphi}',\psi'}}({\mathcal{O}})<1$ (recall that ${\mathcal{O}}$ denotes here the Büchi objective). Now, pick $s'\in K$ such that ${\delta}(s',{\sigma}_{E},{\sigma}^{t'}_{A})(t')>0$ and define a strategy $\psi$ of [Adam]{}by letting $\psi(s') = {\sigma}^{t'}_{A}$ and $\psi(s'\cdot \lambda) = \psi'(\lambda)$. Then as ${{Pr}_{t'}^{{\varphi}',\psi'}}({\mathcal{O}})<1$ one also has that ${{Pr}_{s'}^{{\varphi},\psi}}({\mathcal{O}})<1$ which leads to a contradiction.

Fix a strategy ${\varphi}_K$ as in Lemma \[lemma:StayInWK\]: a play $\lambda$ in ${\mathbb{G}}_K$ where [Eve]{}respects ${\varphi}_K$ is such that ${{Know}_{{E}}^{K}}(\lambda)\in{\mathcal{K}^{{AS}}_{}}$. Moreover, as ${\varphi}$ is almost-surely winning for the Büchi game ${\mathbb{G}}_K$, it is in particular positively winning in the *reachability* game $({\mathcal{A}},K,F)$. Hence, using Proposition \[proposition:positiveWinningReachability\], one gets a bound $N_K$ and some ${\varepsilon}_K$, meaning that the probability of a play $\lambda$ in ${\mathbb{G}}_K$ where [Eve]{}respects ${\varphi}_K$ to visit a final state within its first $N_K$ moves is $\geq{\varepsilon}_K$. Hence, $K$ is ${\mathcal{K}^{{AS}}_{}}$-good, implying that ${\mathcal{K}^{{AS}}_{}}$ is a fixpoint for ${\Xi}$.

Now we show that any fixpoint of ${\Xi}$ is included in ${\mathcal{K}^{{AS}}_{}}$. For this assume that ${{\Xi}}(\mathcal{K}) = \mathcal{K}$ for some $\mathcal{K}$. As any $K\in \mathcal{K}$ is $\mathcal{K}$-good it comes with some ${\varphi}_K$, $N_K$ and ${\varepsilon}_K$. We let $N = \max{\{N_K\mid K\in \mathcal{K}\}}$ and ${\varepsilon}= \min{\{{\varepsilon}_K\mid K\in \mathcal{K}\}}$.

Now we define a strategy ${\varphi}$ that consists in playing in rounds of length $N$: at the beginning of some round, [Eve]{}considers her current knowledge $H$ and plays according to ${\varphi}_H$ in the next $N$ moves; then she restarts with the updated knowledge, and so on forever.

Now consider some $K\in \mathcal{K}$. We claim that ${\varphi}$ is almost-surely winning for [Eve]{}in any in ${\mathbb{G}}_K$. Indeed, from the properties of the ${\varphi}_{{H}}$, it follows that any play in ${\mathbb{G}}_K$ where [Eve]{}respects ${\varphi}$ is such that the knowledge is in $\mathcal{K}$. Now, as the ${\varphi}_{{H}}$ ensure to visit a final state with probability $\geq {\varepsilon}$ in less than $N$ moves the Borel-Cantelli Lemma implies that ${\varphi}$ is almost-surely winning. Hence, $K\in {\mathcal{K}^{{AS}}_{}}$ and this concludes the proof.

As ${\Xi}$ is monotone for set inclusion, it suffices to compute ${\mathcal{K}^{{AS}}_{}}$ by successive applications (starting with the set of all subsets) of the operator ${\Xi}$ until reaching the fixpoint. Since ${\mathcal{K}^{{AS}}_{}}\subseteq {2^{S}}$, the fixpoint is reached in at most $2^{|{S}|}$ steps.

Now, as noted in Remark \[rk:knowtrans\] the property for a strategy to guarantee that [Eve]{}’s knowledge remains in a set $\mathcal{K}$ can be expressed as the strategy being ${\mathcal{T}}_{\mathcal{K}}$-compatible (and the number of states of ${\mathcal{T}}_{\mathcal{K}}$ is at most exponential in $|{S}|$). Therefore, thanks to Theorem \[theo:posTcom\] ([*resp.*]{}Theorem \[theo:posTcomMore\]) 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]{}).

\[thm:as\_main\] Let ${\mathbb{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$.

Decidability follows from Theorem \[theo:posTcom\]/Theorem \[theo:posTcomMore\] and the fixpoint characterisation given in Theorem \[theo:KASFixpoint\]. The result on the strategies is also a consequence of Theorem \[theo:posTcom\]/Theorem \[theo:posTcomMore\] combined with Corollary \[cor:boundingN\] which permits to bound the size of $N$ in the proof of Theorem \[theo:KASFixpoint\].

Lower Bounds {#sec:lowerbound}
============

We now give a matching lower bound to the upper bounds in Theorem \[theo:posTcomMore\] and in Theorem \[thm:as\_main\] 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 [@CDHR07].

\[theo:lowerbound\] 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.

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 initially the input tape is made of $n$ distinguished 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 $A$ is the tape alphabet (including a blank symbol) and $Q$ is the set of states of the machine (including some final states): the meaning of a configuration $a_1\cdots a_{\ell} q a_{\ell+1}\cdots a_{2^n}$ is that the tape content is $a_1\cdots a_{\ell} a_{2^n}$, the state is $q$ and the reading/writing head is on the $\ell$-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\cup 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).

Of course the problem is that [Eve]{}could cheat and do not describe 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 there is a wrong updating of it: 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 effectively 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.

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 polynomial 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 check 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. 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).

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.

Assume first 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 make 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 loosing 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 by Borel-Cantelli Lemma, the probability that he gets caught eventually is therefore $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 defeat any strategy of [Adam]{}almost-surely.

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[^2] 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 strategies 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]{}mimics it in the simulation game (and he never claims that she cheats). Then this strategy leads 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

Hence, 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 concludes the proof.

Summary {#sec:summary}
=======

The landscape of decidability and undecidability results with pointers to the literature and to the results in our paper are shown in the Table \[table:summary\]. The entries of the form “1/2-Exptime-comp.” refer to the two cases of [Adam]{}being perfectly informed and being better informed than [Eve]{}, respectively (the result from [@CD] is for the case of [Adam]{}being perfectly informed). The implication $\Rightarrow$ 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.

                                 Safety                                                     Reachability                                                             Büchi                                                 co-Büchi
  ------------ ------------------------------------------ --------------------------------------------------------------------------------- ------------------------------------------------------- -------------------------------------------------------
   Positively                 Undecidable                                                 1/2-Exptime-comp.                                                       Undecidable                                             Undecidable
                Th. \[theo:undecidable-positive-safety\]   [@CD], Th. \[theo:semiGame\]/Th. \[theo:posTcomMore\] + Th. \[theo:lowerbound\]   [@BBG08] $\Rightarrow$ Th. \[Th:undecidabilityPOMDP\]         Th. \[theo:undecidable-positive-safety\]
     Almost                  ExpTime-comp.                                                1/2-Exptime-comp.                                                    1/2-Exptime-comp.                                          Undecidable
      Sure                   [@Berwanger08]                             [@CD], Th. \[thm:as\_main\] + Th. \[theo:lowerbound\]                   Th. \[thm:as\_main\] + Th. \[theo:lowerbound\]       [@BBG08] $\Rightarrow$ Th. \[Th:undecidabilityPOMDP\]

  : Landscape of decidability and undecidability results[]{data-label="table:summary"}

[10]{}

C. Baier, N. Bertrand, and M. Gr[ö]{}[ß]{}er. On decision problems for probabilistic b[ü]{}chi automata. In [*Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2008)*]{}, volume 4962 of [*Lecture Notes in Computer Science*]{}, pages 287–301. Springer-Verlag, 2008.

N. Bertrand, B. Genest, and H. Gimbert. Qualitative determinacy and decidability of stochastic games with signals. In [*Proceedings of Logic in Computer Science (LiCS’09)*]{}, pages 319–328. IEEE Computer Society Press, 2009.

D. Berwanger and L. Doyen. On the power of imperfect information. In [*Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2008)*]{}, volume 2 of [*LIPIcs*]{}, pages 73–82. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2008.

A. Carayol, A. Haddad, and O. Serre. Randomisation in automata on infinite trees. , 15(3), 2014.

K. Chatterjee. . PhD thesis, University of California, 2007.

K. Chatterjee and L. Doyen. Partial-observation stochastic games: How to win when belief fails. , 15(2):16, 2014.

K. Chatterjee, L. Doyen, T. Henzinger, and J.-F. Raskin. Algorithms for omega-regular games with imperfect information. , 3(3), 2007.

L. de Alfaro and T. Henzinger. Concurrent omega-regular games. In [*Proceedings of Logic in Computer Science (LiCS’00)*]{}, pages 141–154. IEEE Computer Society Press, 2000.

L. de Alfaro, T. A. Henzinger, and O. Kupferman. Concurrent reachability games. , 386(3):188–217, 2007.

N. Fijalkow, S. Pinchinat, and O. Serre. Emptiness of alternating tree automata using games with imperfect information. In [*Proceedings of the 33rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS 2013)*]{}, volume 24 of [*LIPIcs*]{}, pages 299–311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013.

H. Gimbert and Y. Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In [*Proceedings of the 37th International Colloquium on Automata, Languages, and Programming (ICALP 2010)*]{}, volume 6199 of [*Lecture Notes in Computer Science*]{}, pages 527–538. Springer-Verlag, 2010.

E. Gr[ä]{}del, W. Thomas, and T. Wilke, editors. , volume 2500 of [*Lecture Notes in Computer Science*]{}. Springer-Verlag, 2002.

V. Gripon and O. Serre. Qualitative concurrent stochastic games with imperfect information. In [*Proceedings of the 36th International Colloquium on Automata, Languages, and Programming (ICALP 2009)*]{}, volume 5556 of [*Lecture Notes in Computer Science*]{}, pages 200–211. Springer-Verlag, 2009.

D. A. Martin. The determinacy of [B]{}lackwell games. , 63(4):1565–1581, 1998.

A. Paz. . Academic Press New York, 1971.

P. Ramadge and W. Wonham. . , 25:206, 1987.

J. Reif. The complexity of two-player games of incomplete information. , 29(2):274–301, 1984.

W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. , 200(1-2):135–183, 1998.

[^1]: [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.]{}

[^2]: In fact a set of indistinguishable strategies from [Eve]{}’s point of view, including the ones where [Adam]{}claims she cheats.
