CNRS & LMF, ENS Paris-Saclay, Francehttps://orcid.org/0000-0003-3714-6145LMF,
ENS Paris-Saclay & CNRS, Francehttps://orcid.org/0009-0003-2675-6447 Laurent
Doyen and Thomas Soullard [500]Theory of computation Logic and verification
[500]Theory of computation Probabilistic computation

# Regular Games with Imperfect Information Are Not That Regular

Laurent Doyen  Thomas Soullard

###### Abstract

We consider two-player games with imperfect information and the synthesis of a
randomized strategy for one player that ensures the objective is satisfied
almost-surely (i.e., with probability $1$), regardless of the strategy of the
other player. Imperfect information is modeled by an indistinguishability
relation describing the pairs of histories that the first player cannot
distinguish, a generalization of the traditional model with partial
observations. The game is regular if it admits a regular function whose kernel
commutes with the indistinguishability relation.

The synthesis of pure strategies that ensure all possible outcomes satisfy the
objective is possible in regular games, by a generic reduction that holds for
all objectives. While the solution for pure strategies extends to randomized
strategies in the traditional model with partial observations (which is always
regular), we show that a similar reduction does not exist in the more general
model. Despite that, we show that in regular games with Büchi objectives the
synthesis problem is decidable for randomized strategies that ensure the
outcome satisfies the objective almost-surely.

###### keywords:

Imperfect-information games, randomized strategies, Synthesis

##  1 Introduction

We consider the synthesis problem for two-player turn-based games with
imperfect information, a model that has applications in several areas of
computer-science, including the design of multi-agent systems [19], logics
with uncertainty in planning and AI [5, 15], program synthesis [10], and
automata theory [1]. The synthesis problem asks to decide the existence of
(and if so, to construct) a strategy for one player that ensures a given
objective is satisfied with the largest possible probability, regardless of
the choices of the other player. We focus mostly on reachability objectives,
and will also discuss $\omega$-regular objectives [18].

Synthesis provides a natural formulation for the design of a reactive system
that interacts with an unknown environment. The interactive nature of reactive
systems is modeled by a two-player game between the system (the player) and an
adversarial environment, and the limited access of the system to the current
state of the game is modeled by imperfect information.

A simple example of a turn-based game with imperfect information is repeated
matching pennies, where the environment (secretly) chooses head or tail (say,
denoted by $x\in\\{0,1\\}$), then the player chooses $y\in\\{0,1\\}$ without
seeing $x$, and wins if $y=x$. If $y\neq x$, the game repeats for one more
round; the player loses if the game repeats forever. Is is clear that there
exists no pure (deterministic) strategy that is winning in repeated matching
pennies, as for all sequences $\bar{x}=x_{1}\ldots x_{i}$ and
$\bar{y}=y_{1}\ldots y_{i}$ that represent a history of the game (namely, the
sequence of moves played in the first $i$ rounds), given $x_{i+1}$ (chosen by
the environment), the choice of $y_{i+1}$ (by the player) must be made
independently of $x_{i+1}$, thus we may have $x_{i+1}=1-y_{i+1}$, showing that
the game may repeat forever. That the player cannot ensure to win is counter-
intuitive, and this is because pure (deterministic) strategies are considered.
With randomized strategies, the player can win with probability $1$, simply by
choosing $y_{i}\in\\{0,1\\}$ with uniform probability at every round. The
power of randomization for decision making with imperfect information is well
known and occurs in many situations [17, Section 1.3], including gene mutation
in biology, penalty kick in sports, bluffing in card games, etc. It is also
known that, even for simple objectives like reachability, optimal strategies
may need memory [12].

In the sequel, we distinguish the synthesis of a pure strategy (which we call
a sure winning strategy, as it ensures all possible outcomes satisfy the
objective), and the synthesis of a randomized strategy (which we call an
almost-sure winning strategy, as it ensures that the objective is satisfied
with probability $1$). Note that the synthesis problem for strategies that
ensure the objective is satisfied with probability at least $\lambda$ (given
$0<\lambda<1$) is undecidable for probabilistic automata [21], a model that
can be reduced to two-player turn-based games with imperfect information [11].

Given a finite alphabet $\Gamma$ of moves, we denote by $\Gamma^{*}$ the set
of all histories in a game. The traditional model of imperfect information in
games is a (regular) observation function defined on $\Gamma^{*}$ that assigns
to each history of the game a color that is visible to the player, while the
history itself is not visible [22]. We call them partial-observation games, or
games à la Reif. This model of games with imperfect information (even turn-
based and non-stochastic) with randomized strategies generalizes many models
such as concurrent games (e.g., matching pennies), Markov chains, Markov
decision processes, and stochastic games [11, Theorem 5]. The synthesis of
pure strategies in partial-observation games à la Reif with $\omega$-regular
objectives can be done using automata-based techniques analogous to the subset
construction for finite automata [22, 12]. The synthesis of randomized
(almost-sure winning) strategies can be done for reachability (and Büchi)
objectives with a more involved technique based on the same approach of subset
construction. The synthesis problem is EXPTIME-complete in both cases. Note
that for $\omega$-regular (and even for coBüchi) objectives, the synthesis
problem with randomized strategies is undecidable [4].

A more abstract (and more general) model of imperfect information is given by
a function $f:\Gamma^{*}\times\Gamma^{*}\to\\{0,1\\}$ that specifies an
indistinguishability relation [6, 7]: two histories $\tau,\tau^{\prime}$ are
indistinguishable if $f(\tau,\tau^{\prime})=1$. In analogy to the partial-
observation model, indistinguishable histories have the same length and their
prefixes (of the same length) are also indistinguishable. Hence this function
can be viewed as a set of pairs of finite words of the same length (over
alphabet $\Gamma$), or alternatively as a language of finite words over the
alphabet $\Gamma\times\Gamma$. Applications of this model include the
synthesis of full-information protocols, which cannot be expressed by a
partial-observation game à la Reif [7, Section 6].

A generic approach to the synthesis problem with this more general model is to
construct a so-called rectangular morphism $h$ defined on $\Gamma^{*}$ with
finite range [7]. Note that a morphism with finite range is a regular function
(that can be defined by a finite-state automaton with output), and we say that
a game is _regular_ if such a rectangular morphism $h$ exists. For instance,
all partial-observation games à la Reif are regular as they admit a natural
rectangular morphism, which is essentially the subset construction. The
existence of a rectangular morphism guarantees that the information tree has a
finite bisimulation quotient, and thus (pure) strategies can be transferred
back and forth (by copying the action played in a bisimilar position of the
other game), preserving the outcome of the game for arbitrary objectives [7].
Hence, for the synthesis of pure strategies, regular games with imperfect
information can be reduced to finite games with perfect information.

In this paper, we consider the synthesis problem with randomized strategies,
which is central in games with imperfect information (such as matching
pennies). Given the existence of a finite bisimulation quotient in regular
games, the fact that a solution based on a rectangular morphism (the subset
construction) works for the synthesis of randomized strategies in reachability
games à la Reif gives hope that synthesis in regular games is solvable along a
similar path, by a reduction to a simpler equivalent game from which
randomized strategies can be transferred back and forth, copying both the
action and the probability of playing that action. The hope is reinforced by
the existence of a bijection between the set of randomized strategies in a
game à la Reif and the set of strategies in the simpler equivalent game, which
relates strategies with same (probabilistic measure on the) outcome for
arbitrary objectives [12, Theorem 4.2].

Surprisingly, we show that even a much weaker variant of such a reduction does
not exist for regular games. First the hope for a bijective transfer of
strategies is not reasonable because the information tree of regular games
have in general unbounded branching [6], whereas the simpler equivalent games
induced by (finite) rectangular morphism have a bounded-branching information
tree. On the other hand, we show that even a non-bijective transfer of
strategies, as general as it can be, may not exist for some regular game with
a specific rectangular morphism (Section 4.3). Despite their nice structural
properties, the existence of a finite bisimulation in their information tree,
and their apparent similarity with games à la Reif where a bijection between
randomized strategies is induced by a rectangular morphism, regular games are
not as well-behaved as games à la Reif.

In this context, we present an algorithmic solution of the synthesis problem
with randomized strategies for regular games with a reachability objective.
The solution exploits the properties of rectangular morphisms to define a
fixpoint computation with complexity quadratic in the size of the range of the
rectangular morphism (which is of exponential size in the case of games à la
Reif [12], and of non-elementary size in the case of full-information
protocols [7]). Our algorithm shares the common features of the solutions of
almost-sure reachability objectives in Markov decision processes [13],
concurrent games [14], and games à la Reif [12], namely a nested fixpoint
computation that iteratively constructs the almost-sure winning set by
computing the set $S_{i+1}$ of states from which the player can win with
positive probability while ensuring to never leave the set $S_{i}$, where
$S_{0}$ is the entire state space (Section 3). Our solution immediately
extends to Büchi objectives, using reductions to reachability objectives from
the literature.

In conclusion, this paper generalizes the positive (decidability) results
about randomized strategies from games à la Reif to regular games (namely for
reachability and Büchi objectives), whereas the reductions that worked in
games à la Reif for arbitrary objectives no longer hold.

Omitted proofs are provided in the appendix.

##  2 Definitions

We recall basic definitions from logic and automata theory that will be useful
in the rest of the paper, and then we discuss our model of games.

###  2.1 Basic notions

Regular functions. A _Moore machine_ is a finite-state automaton with outputs,
consisting of a finite input alphabet $\Gamma$, a finite output alphabet
$\Sigma$, and a tuple ${\cal M}=\langle
Q,q_{\varepsilon},\delta,\lambda\rangle$ with a finite set $Q$ of states
(sometimes called the memory), an initial state $q_{\varepsilon}\in Q$, a
(deterministic) transition function $\delta:Q\times\Gamma\to Q$, and an output
function $\lambda:Q\to\Sigma$.

We extend the transition function to input words in the natural way, defining
$\delta:Q\times\Gamma^{*}\to Q$ by $\delta(q,\varepsilon)=q$ for all states
$q\in Q$, and inductively $\delta(q,\tau c)=\delta(\delta(q,\tau),c)$ for all
histories $\tau\in\Gamma^{*}$ and moves $c\in\Gamma$.

The object of interest is the extension of the output function to a function
$\lambda:\Gamma^{*}\to\Sigma$ defined by
$\lambda(\tau)=\lambda(\delta(q_{\varepsilon},\tau))$ for all histories
$\tau\in\Gamma^{*}$. A function $\lambda$ defined on $\Gamma^{*}$ is _regular_
if it is (the extension of) the output function of a Moore machine. The
_cumulative extension_ of $\lambda$ is denoted by
$\hat{\lambda}:\Gamma^{*}\to\Sigma^{*}$ and defined by
$\hat{\lambda}(\varepsilon)=\varepsilon$ and inductively $\hat{\lambda}(\tau
c)=\hat{\lambda}(\tau)\lambda(\tau c)$, thus $\hat{\lambda}(c_{1}\ldots
c_{k})=\lambda(c_{1})\lambda(c_{1}c_{2})\ldots\lambda(c_{1}\ldots c_{k})$.
Note that $\lambda={\rm last}\circ\hat{\lambda}$ where ${\rm last}(c_{1}\ldots
c_{k})=c_{k}$. The function $\hat{\lambda}$ is further extended to infinite
words as expected:
$\hat{\lambda}(\pi)=\lambda(c_{1})\lambda(c_{1}c_{2})\ldots$ for all
$\pi=c_{1}c_{2}\ldots\in\Gamma^{\omega}$.

Fixpoint formulas. We briefly recall the interpretation of $\mu$-calculus
fixpoint formulas [8, 9] based on the Knaster-Tarski theorem. Given a
monotonic function $\psi:2^{Q}\to 2^{Q}$ (i.e., such that $X\subseteq Y$
implies $\psi(X)\subseteq\psi(Y)$), the expression $\nu Y.\psi(Y)$ is the
(unique) greatest fixpoint of $\psi$, which can be computed as the limit of
the sequence $(Y_{i})_{i\in{\rm Nature}}$ defined by $Y_{0}=Q$, and
$Y_{i}=\psi(Y_{i-1})$ for all $i\geq 1$. Dually, the expression $\mu
X.\leavevmode\nobreak\ \psi(X)$ is the (unique) least fixpoint of $\psi$, and
the limit of the sequence $(X_{i})_{i\in{\rm Nature}}$ defined by
$X_{0}=\varnothing$, and $X_{i}=\psi(X_{i-1})$ for all $i\geq 1$. If $\lvert
Q\rvert=n$, then it is not difficult to see that the limit of those sequences
is reached after at most $n$ iterations, $X_{n}=X_{n+1}$ and $Y_{n}=Y_{n+1}$.

On equivalence relations. Given an equivalence relation $\sim\,\subseteq
S\times S$ and a set $T\subseteq S$, the _closure_ of $T$ under $\sim$ is the
set $[T]_{\sim}=\\{t\in S\mid\exists t^{\prime}\in T:t\sim t^{\prime}\\}$, and
the _interior_ of $T$ under $\sim$ is the set ${\rm int}_{\sim}(T)=\\{t\in
S\mid[t]_{\sim}\subseteq T\\}$. The closure and interior are monotone
operators, that is if $T\subseteq U$, then $[T]_{\sim}\subseteq[U]_{\sim}$ and
${\rm int}_{\sim}(T)\subseteq{\rm int}_{\sim}(U)$. Note the duality
$S\setminus{\rm int}_{\sim}(T)=[S\setminus T]_{\sim}$, the complement of the
interior of $T$ is the closure of the complement of $T$. We say that $T$ is
_closed_ under $\sim$ if $T=[T]_{\sim}$ (or equivalently $T={\rm
int}_{\sim}(T)$).

###  2.2 Games with imperfect information

We consider an abstract model of game, given by a (nonempty) set $A$ of
actions, a set $\Gamma$ of moves, and a surjective function ${\sf
act}:\Gamma\to A$. The game is played over infinitely many rounds (or steps).
In each round, the player chooses an action $a\in A$, then the environment
chooses a move $c\in\Gamma$ such that ${\sf act}(c)=a$. We say that the move
$c$ is _supported_ by the action $a$.

The outcome of the game is an infinite sequence $\pi\in\Gamma^{\omega}$ of
moves of the environment, called a _play_ , from which we can reconstruct the
infinite sequence of actions of the player using the function ${\sf act}$. A
finite sequence of moves is called a _history_.

The winning condition is a set $W\subseteq\Gamma^{\omega}$ of plays that are
winning for the player. We specify the winning condition by the combination of
a coloring function $\lambda:\Gamma^{*}\to C$ for some finite alphabet $C$ of
colors, and a logical objective $L\subseteq C^{\omega}$. The coloring function
is regular, and specified by a Moore machine. The induced winning condition is
the set $W=\\{\pi\in\Gamma^{\omega}\mid\hat{\lambda}(\pi)\in L\\}$ of plays
whose coloring satisfies the objective.

We consider the following classical objectives, for $C=\\{0,1\\}$:

  * •

the reachability objective is ${\sf Reach}=0^{*}1\\{0,1\\}^{\omega}$ and for
$x\in{\rm Nature}$ let ${\sf Reach}^{\leq x}=\bigcup_{i\leq
x}0^{i}1\\{0,1\\}^{\omega}$;

  * •

the safety objective is ${\sf Safe}=0^{\omega}=\\{0,1\\}^{\omega}\setminus{\sf
Reach}$;

  * •

the Büchi objective is $\text{\sf B\"{u}chi}=(0^{*}1)^{\omega}$;

  * •

the coBüchi objective is $\text{\sf
coB\"{u}chi}=\\{0,1\\}^{*}0^{\omega}=\\{0,1\\}^{\omega}\setminus\text{\sf
B\"{u}chi}$;

It is convenient to consider that the coloring function $\lambda$ is part of a
game instance, while the objective $L$ can be specified independently of the
game. This allows to quantify separately the game instances and the
objectives. We recall that the traditional games played on graphs [18, 3] are
an equivalent model, in particular they can be translated into our abstract
model of game, for example by letting moves be the edges of the game graph and
the corresponding action be the label of the edge, while the graph structure
can be encoded in the winning condition [23]. When we refer to a game played
on a graph, we assume that all move sequences that contain two consecutive
moves (i.e., edges) $c_{i}=(q_{1},q_{2})$ and $c_{i+1}=(q_{3},q_{4})$ such
that $q_{2}\neq q_{3}$ belong to the winning condition (for the player).

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$x$$q_{0}$$a_{1},b_{1}$$a_{2},b_{2}$$a_{1},a_{2}$$b_{1},b_{2}$$b_{1},b_{2}$$a_{1},a_{2}$
(a)

$U_{1}$$U_{2}$$U_{3}$$X$$U_{1}$$a,b$$a,b$$a,b$ (b)

Figure 1: A game with imperfect information representing matching pennies, and
its information tree.

Imperfect information is represented by an indistinguishability relation
$\sim\,\in\Gamma^{*}\times\,\Gamma^{*}$ that specifies the pairs of histories
that the player cannot distinguish. An indistinguishability relation is an
equivalence that satisfies the following conditions [6], for all histories
$\tau,\tau^{\prime}\in\Gamma^{*}$ and moves $c,c^{\prime}\in\Gamma$: $(i)$ if
$\tau\sim\tau^{\prime}$, then $\lvert\tau\rvert=\lvert\tau^{\prime}\rvert$
(indistinguishable histories have the same length); $(ii)$ if $\tau
c\sim\tau^{\prime}c^{\prime}$, then $\tau\sim\tau^{\prime}$ (the relation is
prefix-closed) and ${\sf act}(c)={\sf act}(c^{\prime})$ (the action is
visible). Indistinguishability relations may be specified using two-tape
automata, but the results of this paper hold for arbitrary
indistinguishability relations.

Given a history $\tau\in\Gamma^{*}$ we call the equivalence class
$[\tau]_{\sim}=\\{\tau^{\prime}\in\Gamma^{*}\mid\tau^{\prime}\sim\tau\\}$
containing $\tau$ an _information set_. A function $\lambda$ defined on
$\Gamma^{*}$ is _information consistent_ if $\lambda$ is constant over every
information set: $\lambda(\tau)=\lambda(\tau^{\prime})$ for all
indistinguishable histories $\tau\sim\tau^{\prime}$. An equivalent requirement
is that the cumulative extension $\hat{\lambda}$ is constant over every
information set, since indistinguishability relations are prefix-closed. We
always require the coloring function of a game to be information consistent
(with respect to the indistinguishability relation of the game). For every
action $a\in A$, we define a successor relation $\to_{a}$ over information
sets, where $[\tau]_{\sim}\to_{a}[\tau c]_{\sim}$ for all moves $c\in\Gamma$
such that ${\sf act}(c)=a$. The relations $\to_{a}$ are obviously acyclic, and
induce a structure called the _information tree_. Note that there is a natural
extension of the coloring function $\lambda$ to information sets, defined by
$\lambda([\tau]_{\sim})=\lambda(\tau)$ for all histories $\tau\in\Gamma^{*}$,
since $\lambda$ is information-consistent.

Given the above definitions, we represent a game with imperfect information as
a tuple ${\cal G}=\langle A,{\sf act},\sim,\lambda\rangle$, together with an
objective $L\subseteq C^{\omega}$, where the (finite) alphabet of moves is
$\Gamma$, and the (finite) alphabet of colors is $C$. The information tree of
${\cal G}$ is denoted by $\mathcal{U}_{\sim}({\cal G})$ (consisting of the
information sets of ${\cal G}$, the successor relations $\to_{a}$, and the
coloring $\lambda$ extended to information sets). The special case of perfect-
information games corresponds the indistinguishability relation $\sim$ being
the identity (or equivalently by the information sets
$[\tau]_{\sim}=\\{\tau\\}$ being singletons for all histories
$\tau\in\Gamma^{*}$).

Figures provide a very informal (but readable) description of games. The main
components of a game that figures represent are the coloring function and the
indistinguishability relation. Strictly speaking, the figures do not show a
game but provide sufficient information to reconstruct the Moore machine
defining the coloring function, and the two-tape automaton defining the
indistinguishability relation. It should be possible to infer the color of a
history (when its color is relevant), and the information set containing a
given history. States are normally depicted as circles, but we may use boxes
to emphasize that the action choice of the player is not relevant and only the
move of the environment determines the successor state.

In the game ${\cal G}$ of Figure 1(a), representing matching pennies, the
player has two actions, $A=\\{a,b\\}$, and the environment has two possible
responses for each of them, thus four moves,
$\Gamma=\\{a_{1},a_{2},b_{1},b_{2}\\}$ where ${\sf act}(a_{i})=a$ and ${\sf
act}(b_{i})=b$ for $i=1,2$. Intuitively, the adversarial environment chooses
head ($1$) or tail ($2$) in the first round (at $q_{0}$) by choosing a
response $1$ or $2$ (the action of the player is not relevant) that the player
cannot observe (all histories of length $1$ are indistinguishable, as
suggested by the dashed line in Figure 1(a)). The player chooses head (action
$a$) or tail (action $b$) in the next round, wins if the choice is matching
the environment’s choice, and replays the same game otherwise ($x$ is a
placeholder for the whole tree of Figure 1(a)).

The information tree of ${\cal G}$ is shown in Figure 1(b) where
$U_{1}=[\varepsilon]_{\sim}=\\{\varepsilon\\}$ and
$U_{2}=[a_{1}]_{\sim}=\\{a_{1},a_{2},b_{1},b_{2}\\}=\Gamma$. The information
set $U_{3}$ contains eight of the sixteen histories of length $2$. The node
$X$ is a placeholder for a tree that is isomorphic to the tree rooted at
$U_{1}$.

We recall that the nodes in information trees have a finite number of
successors (there is at most $\lvert\Gamma\rvert^{n}$ information sets
containing histories of length $n$), however the branching degree in a given
information tree may be unbounded [6]. The partial-observation games à la Reif
[22] are characterized by their information tree having bounded branching [6,
Theorem 7].

Strategies. A _probability distribution_ on a finite set $S$ is a function
$d:S\to[0,1]$ such that $\sum_{s\in S}d(s)=1$. A _Dirac distribution_ assigns
probability $1$ to a (unique) element $s\in S$. We denote by ${\cal D}(S)$ the
set of all probability distributions on $S$.

A strategy for the player is a function $\alpha:\Gamma^{*}\to{\cal D}(A)$ that
is information consistent, thus $\alpha(\tau)=\alpha(\tau^{\prime})$ for all
indistinguishable histories $\tau\sim\tau^{\prime}$. The strategy $\alpha$ is
_pure_ (or, deterministic) if $\alpha(\tau)$ is a Dirac distribution for all
$\tau\in\Gamma^{*}$. A strategy for the environment is a function
$\beta:\Gamma^{*}\times A\to{\cal D}(\Gamma)$ such that for all histories
$\tau\in\Gamma^{*}$, actions $a\in A$, and moves $c\in\Gamma$, if the move $c$
is played with positive probability $\beta(\tau,a)(c)>0$, then it is supported
by the action $a$, ${\sf act}(c)=a$. The strategy $\beta$ is _pure_ (or,
deterministic) if $\beta(\tau,a)$ is a Dirac distribution for all
$\tau\in\Gamma^{*}$ and $a\in A$. We denote by ${\cal A}_{{\cal G}}$ (resp.,
by ${\cal B}_{{\cal G}}$) the set of all strategies for the player (resp., for
the environment), and by ${\cal A}^{{\sf pure}}_{{\cal G}}$ (resp., by ${\cal
B}^{{\sf pure}}_{{\cal G}}$) the set of all pure strategies for the player
(resp., for the environment).

A pair of strategies $(\alpha,\beta)$ for the player and the environment
induce a probability measure $\mathrm{Pr}^{\alpha,\beta}$ on the sigma-algebra
over the set of (infinite) plays. By Carathéodory’s extension theorem, it is
sufficient to define the probability measure over cylinder sets spanned by
(finite) prefixes of plays. We define a family of probability measures
$\mathrm{Pr}_{\tau}^{\alpha,\beta}$ where $\tau\in\Gamma^{*}$ corresponds to
starting the game after history $\tau$. We set
$\mathrm{Pr}^{\alpha,\beta}=\mathrm{Pr}_{\varepsilon}^{\alpha,\beta}$. Given
$\rho\in\Gamma^{*}$, the measure of the cylinder set ${\sf
Cyl}(\rho)=\rho\Gamma^{\omega}=\\{\pi\in\Gamma^{\omega}\mid\rho\text{ is a
prefix of }\pi\\}$ is defined as follows:

  * •

if $\rho$ is a prefix of $\tau$, then

$\mathrm{Pr}_{\tau}^{\alpha,\beta}({\sf Cyl}(\rho))=1;$

  * •

if $\rho=\tau c_{1}\dots c_{k}$ where $c_{1},\dots,c_{k}\in\Gamma$ for some
$k\geq 1$, then

$\mathrm{Pr}_{\tau}^{\alpha,\beta}({\sf Cyl}(\rho))=\prod_{i=1}^{k}\alpha(\tau
c_{1}\dots c_{i-1})({\sf act}(c_{i}))\cdot\beta(\tau c_{1}\dots c_{i-1},{\sf
act}(c_{i}))(c_{i});$

  * •

all other cylinder sets have measure $0$.

Given an objective $L\subseteq C^{\omega}$ defined on colors, assuming the
game ${\cal G}$ (and thus $\hat{\lambda}$) is clear from the context we take
the freedom to denote by $\mathrm{Pr}^{\alpha,\beta}(L)$ the probability
$\mathrm{Pr}^{\alpha,\beta}(\\{\pi\in\Gamma^{\omega}\mid\hat{\lambda}(\pi)\in
L\\})$ that the objective $L$ is satisfied by an outcome of the pair of
strategies $(\alpha,\beta)$ in ${\cal G}$. A strategy $\alpha$ of the player
is _almost-sure winning_ from an information set $[\tau]_{\sim}$ (or simply
_almost-sure winning_ if $\tau=\varepsilon$) for objective $L$ if
$\mathrm{Pr}_{\tau^{\prime}}^{\alpha,\beta}(L)=1$ for all
$\tau^{\prime}\in[\tau]_{\sim}$ and all strategies $\beta\in{\cal B}_{{\cal
G}}$ of the environment. We are interested in solving the synthesis problem,
which is to decide, given a game ${\cal G}$ and objective $L$, whether there
exists an almost-sure winning strategy in ${\cal G}$ for $L$.

Note that the definition of almost-sure winning is equivalent to a formulation
where only _pure_ strategies of the environment are considered, that is where
we require $\mathrm{Pr}_{\tau^{\prime}}^{\alpha,\beta}(L)=1$ for all
$\beta\in{\cal B}^{{\sf pure}}_{{\cal G}}$ only, as once a strategy for the
player is fixed, the environment plays in a (possibly infinite-state) Markov
decision process, for which pure strategies are sufficient [20, 11].

We say that a history $\tau\in\Gamma^{*}$ is _compatible_ with $\alpha$ and
$\beta$ if $\mathrm{Pr}^{\alpha,\beta}({\sf Cyl}(\tau))>0$. An _outcome_ of
the pair of strategies $(\alpha,\beta)$ is a play $\pi\in\Gamma^{\omega}$ all
of whose prefixes are compatible with $\alpha$ and $\beta$. We note that if
$\mathrm{Pr}^{\alpha,\beta}({\sf Cyl}(\tau))>0$, then
$\mathrm{Pr}_{\tau}^{\alpha,\beta}({\sf Cyl}(\tau c_{1}c_{2}\dots
c_{n}))=\mathrm{Pr}^{\alpha,\beta}({\sf Cyl}(\tau c_{1}c_{2}\dots
c_{n})\mid{\sf Cyl}(\tau))$.

##  3 Almost-Sure Reachability

Throughout this section, we consider games with a (fixed) reachability
objective ${\sf Reach}=0^{*}1\\{0,1\\}^{\omega}$ over color alphabet
$C=\\{0,1\\}$, thus a play is winning if it has a finite prefix with color $1$
according to the coloring function $\lambda$ of the game. By extension, we say
that a history $\tau$ is winning if $\lambda(\tau)=1$. We also assume without
loss of generality that if $\lambda(\tau)=1$, then $\lambda(\tau c)=1$ for all
$\tau\in\Gamma^{*}$ and all $c\in\Gamma$. In the rest of this section, we fix
a game ${\cal G}$ as defined in Section 2.2 and we show how to decide the
existence of an almost-sure winning strategy in games with a reachability
objective, relying on the existence of a rectangular morphism (defined below).
Two interesting classes of games are known to admit rectangular morphisms,
namely the partial-observation games à la Reif and the full-information
protocols [7].

###  3.1 Regular games with imperfect information

A _rectangular morphism_ for ${\cal G}$ is a surjective function
$h:\Gamma^{*}\to P$ (for some finite set $P$) such that for all
$\tau,\tau^{\prime}\in\Gamma^{*}$ and $c\in\Gamma$:

Rectangularity11footnotemark: 1

if $h(\tau)=h(\tau^{\prime})$, then
$h([\tau]_{\sim})=h([\tau^{\prime}]_{\sim})$,

Morphism

if $h(\tau)=h(\tau^{\prime})$, then $h(\tau c)=h(\tau^{\prime}c)$,

Refinement

if $h(\tau)=h(\tau^{\prime})$, then $\lambda(\tau)=\lambda(\tau^{\prime})$.

Note that, as $h$ is a finite-valued morphism, it can be represented by an
automaton (whose output is not relevant) with input alphabet $\Gamma$ and
state space $P$. Games that admit a finite-valued rectangular morphism are
called _regular_. Define the relation
$\approx\,=\\{(h(\tau),h(\tau^{\prime}))\mid\tau\sim\tau^{\prime}\\}$ and
recall a non-trivial fundamental result.

######  Lemma 3.1.

[7, Lemma 3 & Lemma 4] The relation $\approx$ is an equivalence and
$h([\tau]_{\sim})=[h(\tau)]_{\approx}$ for all $\tau\in\Gamma^{*}$.

We call the elements of $P$ _abstract states_. We extend the relation
$\approx$ to elements of $P\times A$ as follows: for all $p,p^{\prime}\in P$
and $a,a^{\prime}\in A$, let $(p,a)\approx(p^{\prime},a^{\prime})$ if
$p\approx p^{\prime}$ and $a=a^{\prime}$.

Thanks to the morphism property, there exists a function
$\delta^{P}:P\times\Gamma\to P$ such that $\delta^{P}(h(\tau),c)=h(\tau c)$
for all $\tau\in\Gamma^{*}$ and $c\in\Gamma$. Define the set $P_{F}=\\{p\in
P\mid\exists\tau\in\Gamma^{*}:h(\tau)=p\land\lambda(\tau)=1\\}$ of target (or
final) states, which are the images by $h$ of winning histories. Note that the
coloring function is information-consistent and therefore the set $P_{F}$ is
closed under $\approx$ by Lemma 3.1. Moreover, by our assumption on the
coloring function the states in $P_{F}$ form a sink set, that is
$\delta^{P}(p,c)\in P_{F}$ for all states $p\in P_{F}$ and moves $c\in\Gamma$.

Rectangular morphisms are central to the solution of the synthesis problem for
_pure_ strategies [7], by showing that the following abstract game is
equivalent to ${\cal G}$: starting from $p_{0}=h(\varepsilon$, the game is
played in rounds where each round starts with a value $p$ and the player
chooses an action $a\in A$, the next round starts in $p^{\prime}$ chosen by
the environment such that $p^{\prime}\approx\delta^{P}(p,c)$ for some move
$c\in\Gamma$ such that ${\sf act}(c)=a$. The player wins if a value in $P_{F}$
eventually occurs along a play. We may view the elements of $P$ as positions
of the player, and elements of $P\times A$ as positions of the environment. We
further discuss this abstract game in Section 4.2.

An abstract state $p\in P$ is _existentially winning_ if there exists a
history $\tau\in\Gamma^{*}$ such that $h(\tau)=p$ and the player has an
_almost-sure winning_ strategy from $[\tau]_{\sim}$. We denote by
$P_{\exists}$ the set of all existentially winning states. Note that the set
$P_{\exists}$ is closed under $\approx$, since for all $p\in P_{\exists}$ and
$p^{\prime}\approx p$, by Lemma 3.1 there exists
$\tau^{\prime}\in[\tau]_{\sim}$, such that $h(\tau^{\prime})=p^{\prime}$ and
the player has an _almost-sure winning_ strategy from
$[\tau^{\prime}]_{\sim}=[\tau]_{\sim}$.

An abstract state $p\in P$ is _universally winning_ if for all histories
$\tau\in\Gamma^{*}$ such that $h(\tau)=p$, the player has an _almost-sure
winning_ strategy from $[\tau]_{\sim}$. We denote by $P_{\forall}$ the set of
all universally winning states. Note that the set $P_{\forall}$ is closed
under $\approx$, by an argument analogous to the case of $P_{\exists}$. As we
consider a reachability objective, it is easy to see that $P_{F}\subseteq
P_{\forall}\subseteq P_{\exists}$ (the latter inclusion holds since $h$ is
surjective).

Note that in games of perfect information, the existentially and universally
winning states coincide by definition since information sets are singletons,
$P_{\forall}=P_{\exists}$. A corollary of our results is that
$P_{\forall}=P_{\exists}$ also holds in games of imperfect information with a
reachability objective.

###  3.2 Algorithm

We present an algorithm to decide if the player is almost-sure winning for
reachability in a game of imperfect information, assuming we have a
rectangular morphism.

Given a set $X\subseteq P\cup(P\times A)$, define the _predecessor_ operator
as follows:

$\displaystyle{\sf Pre}(X)=\;$ $\displaystyle\\{p\in P\mid\exists a\in
A:(p,a)\in X\\}$ $\displaystyle\cup\large$ $\displaystyle\\{(p,a)\in P\times
A\mid\forall c:{\sf act}(c)=a\implies\delta^{P}(p,c)\in X\\}$

It is easy to verify that if $X_{1}\subseteq X_{2}$, then ${\sf
Pre}(X_{1})\subseteq{\sf Pre}(X_{2})$, that is ${\sf Pre}(\cdot)$ is monotone.
Intuitively, from a history $\tau$ such that $h(\tau)\in{\sf Pre}(X)$ the
player can choose an action $a$ such that $(h(\tau),a)\in X$, and if
$(h(\tau),a)\in{\sf Pre}(X)$ then for all moves chosen by the environment and
supported by action $a$ we have $h(\tau c)\in X$. In a game of perfect
information, iterating the predecessor operator from the target set $P_{F}$
until obtaining a fixpoint $X_{*}=\mu X.{\sf Pre}(X)\cup P_{F}$ gives the
(existentially and universally) winning states, that is
$P_{\forall}=P_{\exists}=X_{*}$.

In a game of imperfect information with randomized strategies for the player,
given $X_{i+1}={\sf Pre}(X_{i})$, from a history $\tau$ such that $h(\tau)\in
X_{i+1}$, we may consider playing all actions $a$ such that $(h(\tau),a)\in
X_{i}$ uniformly at random. However, an action played in a history $\tau$ is
also played in every indistinguishable history $\tau^{\prime}\sim\tau$.
Therefore, we need to ensure that for all actions $a$ played in $\tau$ (such
that $(h(\tau),a)\in X_{i}$), playing $a$ in $\tau^{\prime}$ does not leave
$X_{*}$. Hence for $p=h(\tau)$, even if $(p,a)\in X_{*}$, the action $a$
should not be played from $\tau$ if there exists $p^{\prime}\approx p$ such
that $(p^{\prime},a)\not\in X_{*}$.

In our algorithm, we remove from $X_{*}$ all elements $(p,a)$ such that
$(p^{\prime},a)\not\in X_{*}$ for some $p^{\prime}\approx p$, that is we
replace $X_{*}$ by its interior. We define

$Y_{*}=\nu Y.\,\mu X.\,\,{\rm int}_{\approx}(Y)\cap({\sf Pre}(X)\cup P_{F})$

and we show that the sets $Y_{*}$, $P_{\forall}$, and $P_{\exists}$ coincide.
Note that the $\mu$-calculus formula for $Y_{*}$ is well defined since ${\sf
Pre}(\cdot)$ and ${\rm int}_{\approx}(\cdot)$ are monotone operators, and that
the fixpoint can be effectively computed since $P$ is finite.

As the fixpoint satisfies $Y_{*}={\rm int}_{\approx}(Y_{*})\cap({\sf
Pre}(Y_{*})\cup P_{F})$, it follows that $Y_{*}={\rm int}_{\approx}(Y_{*})$ is
closed under $\approx$, and $Y_{*}\subseteq{\sf Pre}(Y_{*})\cup P_{F}$.
Moreover it is easy to verify from the fixpoint iteration that $P_{F}\subseteq
Y_{*}$ since $P_{F}$, which is closed under $\approx$, is always contained in
the least fixpoint, and never removed from the greatest fixpoint.

######  Theorem 3.2.

The abstract states in the fixpoint $Y_{*}$ are the existentially winning
states, which coincide with the universally winning states, $Y_{*}\cap
P=P_{\forall}=P_{\exists}$.

Theorem 3.2 entails the decidability of the existence of an almost-sure
winning strategy in games with reachability objective: if there exists an
almost-sure winning strategy (from $\varepsilon$), then $h(\varepsilon)\in
P_{\exists}=Y_{*}$, and conversely if $h(\varepsilon)\in Y_{*}$ then
$h(\varepsilon)\in P_{\forall}$ since $h(\varepsilon)\in P$, and there exists
an almost-sure winning strategy from $[\varepsilon]_{\sim}=\\{\varepsilon\\}$.

######  Corollary 3.3.

There exists an almost-sure winning strategy if and only if $h(\varepsilon)\in
Y_{*}$.

The result of Theorem 3.2 follows from the chain of inclusions $Y_{*}\cap
P\subseteq P_{\forall}$ (Lemma 3.4), the already established
$P_{\forall}\subseteq P_{\exists}$, and $P_{\exists}\subseteq Y_{*}\cap P$
(Lemma 3.5),

To show that $Y_{*}\cap P\subseteq P_{\forall}$ we construct a strategy for
the player that is almost-sure winning from all $\tau$ (and from
$[\tau]_{\sim}$) such that $h(\tau)\in Y_{*}$. The strategy plays uniformly at
random all actions that ensure the successor $\tau c$ of $\tau$ remains in
$Y_{*}$, more precisely $h(\tau c)\in Y_{*}$. We show that at least one such
action ensures progress towards reaching a target state in $P_{F}$, thus with
probability at least $\frac{1}{\lvert A\rvert}$. The target is reachable in at
most $\lvert P\rvert$ steps, which entails bounded probability (at least
$\nu=\frac{1}{\lvert A\rvert^{\lvert P\rvert}}$) to reach $P_{F}$ (from every
state of $Y_{*}$) and since the strategy ensures that $Y_{*}$ is never left,
the probability of _not_ reaching $P_{F}$ is at most $(1-\nu)^{k}$ for all
$k\geq 0$, and as $(1-\nu)^{k}\to 0$ when $k\to\infty$ the probability to
eventually reach $P_{F}$ is $1$.

######  Lemma 3.4.

$Y_{*}\cap P\subseteq P_{\forall}$.

The last inclusion of the chain is proved by showing that there exists a
fixpoint that contains $P_{\exists}$ and since $Y_{*}$ is defined as the
greatest fixpoint, we have $P_{\exists}\subseteq Y_{*}$.

######  Lemma 3.5.

$P_{\exists}\subseteq Y_{*}\cap P$.

The fixpoint computation for $Y_{*}$ can be implemented by a quadratic
algorithm, with respect to the number $\lvert P\rvert$ of abstract states
(assuming a constant number of actions).

Both stochastic games on graphs and Büchi objectives are subsumed by the
results of this paper: in stochastic games, almost-sure Büchi reduces to
almost-sure reachability [4, Lemma 8.3], and games with stochastic transitions
can be simulated by (non-stochastic) games with imperfect information [11,
Theorem 5]. These results can easily be lifted to the more general framework
of games with imperfect information defined by indistinguishability relations.
On the other hand, we recall that almost-sure coBüchi is undecidable, already
in probabilistic automata with pure strategies [4], and also with randomized
strategies [11, Corollary 2], but without the assumption that the coloring
function is information consistent. For the special case of information-
consistent coBüchi objectives, the decidability status of the synthesis
problem for almost-sure winning is open (even in games à la Reif), to the best
of our knowledge. Finally for safety objectives, almost-sure winning is
equivalent to sure winning (which requires that all possible outcomes satisfy
the objective), and the problem is equivalent to synthesis with pure
strategies [7].

######  Theorem 3.6.

Given a regular game ${\cal G}$ with imperfect information and a rectangular
morphism $h:\Gamma^{*}\to P$ for ${\cal G}$, the synthesis problem for almost-
sure reachability and Büchi objectives can be solved in time $O(\lvert
P\rvert^{2})$.

Since $\lvert P\rvert$ is already exponential in games à la Reif (for which
the synthesis problem is EXPTIME-complete), the quadratic blow-up is not
significant. For example, we get a $(k+1)$-EXPTIME complexity upper bound for
the synthesis problem in the model of full-information protocols (FIP) with
$k$ observers, using the rectangular morphism of [7, Section 5.2]. The model
of full-information protocols as presented in [7] features explicit
communication actions that entail full disclosure of all available information
of the sender. The game involves several players who may communicate, but only
one active player who takes control actions, which reduces the synthesis
problem to a game with imperfect information as considered here.

A matching $(k+1)$-EXPTIME lower bound can be obtained by a straightforward
adaptation of the proof of [7, Theorem 3], which presents a reduction from the
membership problem for alternating $k$-EXPSPACE Turing machines to the
synthesis problem of (pure) winning strategies. The reduction is such that in
the constructed game, randomization does not help the player. If the player
takes a chance in deviating from the faithful simulation of the Turing
machine, a losing sink state is reached, thus with positive probability.

######  Theorem 3.7.

The synthesis problem for FIP games with $k$ observers (and almost-sure
reachability objective) is $(k+1)$-EXPTIME-complete.

The construction of an almost-sure winning strategy $\alpha$ can be done by
following the first step in the proof of Lemma 3.4, which constructs $\alpha$
given the value of the fixpoint $Y_{*}$. It follows that the constructed
strategy is a regular function that can be represented by the automaton
underlying the rectangular morphism of the game, and thus memory of size
$\lvert P\rvert$ is sufficient to define an almost-sure winning strategy.

##  4 Reductions

The results of Section 3 may suggest the existence of a (strong)
correspondence, possibly an equivalence, between the game ${\cal G}$ with
regular indistinguishability relation and a simpler (finite-state) game ${\cal
H}$ (essentially the abstract game presented in Section 3.1) that would hold
for arbitrary objectives.

While it is virtually impossible to establish the non-existence of a
reasonably strong such correspondence, we show for a natural notion of game
equivalence that such a correspondence does not hold in general.

###  4.1 Alternating probabilistic trace equivalence

Inspired by the notion of alternating refinement relations [2] in non-
stochastic game graphs with perfect information (also called alternating
transition systems), we consider the following definition of _game
refinement_.

Given two games ${\cal G}$ and ${\cal H}$, we say that ${\cal G}$ _reduces_ to
${\cal H}$ (denoted by ${\cal G}\preceq{\cal H}$) if for all strategies
$\alpha_{{\cal G}}$ of the player in ${\cal G}$, there exists a strategy
$\alpha_{{\cal H}}$ of the player in ${\cal H}$, such that for all strategies
$\beta_{{\cal H}}$ of the environment in ${\cal H}$, there exists a strategy
$\beta_{{\cal G}}$ of the environment in ${\cal G}$, such that the probability
measures $\mathrm{Pr}^{\alpha_{{\cal G}},\beta_{{\cal G}}}$ in ${\cal G}$ and
$\mathrm{Pr}^{\alpha_{{\cal H}},\beta_{{\cal H}}}$ in ${\cal H}$ coincide (on
all objectives $L\subseteq C^{\omega}$, that is $\mathrm{Pr}^{\alpha_{{\cal
G}},\beta_{{\cal G}}}(L)=\mathrm{Pr}^{\alpha_{{\cal H}},\beta_{{\cal H}}}(L)$
for all $L$), in short:

$\forall\alpha_{{\cal G}}\cdot\exists\alpha_{{\cal H}}\cdot\forall\beta_{{\cal
H}}\cdot\exists\beta_{{\cal G}}\cdot\forall L\subseteq
C^{\omega}:\mathrm{Pr}^{\alpha_{{\cal G}},\beta_{{\cal
G}}}(L)=\mathrm{Pr}^{\alpha_{{\cal H}},\beta_{{\cal H}}}(L).$

As expected, the quantifications over strategies of the player range over
information-consistent randomized strategies (in their respective game), and
the quantification over $L$ ranges over measurable sets. Under theses
quantifications, the condition $\mathrm{Pr}^{\alpha_{{\cal G}},\beta_{{\cal
G}}}(L)=\mathrm{Pr}^{\alpha_{{\cal H}},\beta_{{\cal H}}}(L)$ can be replaced
by $\mathrm{Pr}^{\alpha_{{\cal G}},\beta_{{\cal
G}}}(L)\leq\mathrm{Pr}^{\alpha_{{\cal H}},\beta_{{\cal H}}}(L)$ (consider the
complement of $L$, which is also a measurable set), and then game refinement
can be interpreted as the game ${\cal H}$ being easier333The words “easier”,
“better”, “lower”, etc. are interpreted in a non-strict sense. than ${\cal G}$
for the player because for every strategy of the player in ${\cal G}$ there is
a better strategy for the player in ${\cal H}$ (as reflected by the quantifier
sequence $\forall\alpha_{{\cal G}}\cdot\exists\alpha_{{\cal H}}$), which means
that the environment can always ensure a lower value in ${\cal G}$ (against
$\alpha_{{\cal G}}$) than in ${\cal H}$ (against $\alpha_{{\cal H}}$), as
reflected by the quantifier sequence $\forall\beta_{{\cal
H}}\cdot\exists\beta_{{\cal G}}$).

Note that in the special case of pure strategies (and non-stochastic games)
where the probability measures assign probability $1$ to a single play, game
refinement boils down to

$\forall\alpha_{{\cal G}}\in{\cal A}^{{\sf pure}}_{{\cal
G}}\cdot\exists\alpha_{{\cal H}}\in{\cal B}^{{\sf pure}}_{{\cal
H}}:\mathrm{outcome}_{{\cal H}}(\alpha_{{\cal
H}})\subseteq\mathrm{outcome}_{{\cal G}}(\alpha_{{\cal G}})$

where $\mathrm{outcome}_{X}(\alpha)$ denotes the set of plays compatible with
$\alpha$ in game $X$. The condition $\mathrm{outcome}_{{\cal H}}(\alpha_{{\cal
H}})\subseteq\mathrm{outcome}_{{\cal G}}(\alpha_{{\cal G}})$ is equivalent to

$\forall\beta_{{\cal H}}\in{\cal B}^{{\sf pure}}_{{\cal
H}}\cdot\exists\beta_{{\cal G}}\in{\cal B}^{{\sf pure}}_{{\cal
G}}:\mathrm{outcome}_{{\cal H}}(\alpha_{{\cal H}},\beta_{{\cal
H}})=\mathrm{outcome}_{{\cal G}}(\alpha_{{\cal G}},\beta_{{\cal G}}),$

where $\mathrm{outcome}_{X}(\alpha,\beta)$ denotes the set of plays compatible
with $\alpha$ and $\beta$ in game $X$. This is essentially the definition of
alternating trace containment [2, Section 4]. Hence our definition of game
refinement is a natural generalization of both alternating trace containment
to a stochastic and imperfect-information setting, and of refinement for
labeled Markov decision processes [16, Section 4] to games.

We say that two games ${\cal G}$ and ${\cal H}$ are _equivalent_ (or inter-
reducible) if ${\cal G}\preceq{\cal H}$ and ${\cal H}\preceq{\cal G}$. We
sometimes refer to this equivalence as _alternating probabilistic trace
equivalence_.

###  4.2 Bijection and bisimulation

We compare the approach in Section 3 and the technique for solving almost-sure
reachability in games with partial observation à la Reif [12]. Recall that
games with partial observation are a special case of games with regular
indistinguishability relation.

The solution of the synthesis problem with randomized strategies for games à
la Reif established a bijection (denoted by $h$, but we call it $\hat{h}$ to
emphasize that it is a mapping between sequences) between the histories in the
original game ${\cal G}$ and in a game ${\cal H}$ of partial observation
played as follows: given a history $\rho$ (initially $\varepsilon$), the
player chooses an action $a\in A$, and the environment extends the history to
$\rho^{\prime}=\hat{h}(\tau c)$ where $\hat{h}(\tau)=\rho$ and $c$ is a move
(in ${\cal G}$) such that ${\sf act}(c)=a$. Two histories are
indistinguishable if all their respective prefixes (of the same length) are
$\approx$-equivalent (according to the definition of $\approx$ before Lemma
3.1). We call ${\cal H}$ the _abstract game induced_ from ${\cal G}$ by
$\hat{h}$, and by an abuse of notation, we denote by $\approx$ the
indistinguishability relation of ${\cal H}$.

The bijection $\hat{h}$ naturally extends to a bijection between plays in
${\cal G}$ and plays in ${\cal H}$, and further to a bijection between
strategies in ${\cal G}$ and strategies in ${\cal H}$ that preserves
probability measures. The existence of this bijection immediately ensures that
the games ${\cal G}$ and ${\cal H}$ are equivalent (in the sense of
alternating probabilistic trace equivalence). Another important consequence is
that the information trees of ${\cal G}$ and ${\cal H}$ are isomorphic, a
situation that is not guaranteed when ${\cal G}$ is a game with regular
indistinguishability relation and ${\cal H}$ is a finite-state game (i.e., the
set $h(\Gamma^{*})=\\{{\rm last}(\hat{h}(\tau))\mid\tau\in\Gamma^{*}\\}$ is
finite). Indeed, the branching degree of the information tree of ${\cal G}$
may be unbounded [6], whereas the branching degree of the information tree of
${\cal H}$ is necessarily bounded since ${\cal H}$ is a finite game. It is
therefore impossible to follow the same route as in games à la Reif, using
bijections.

Since bijection is too strong for our general setting, a more realistic hope
is to rely on the existence of a bisimulation between the information tree of
${\cal G}$ and the information tree of ${\cal H}$ [7, Theorem 1]. Note that
bisimulation is insensitive to the branching degree. The bisimulation ensures
that, under pure strategies for the player, the (perfect-information) games
played on the information trees are equivalent (in the sense of alternating
trace equivalent). The equivalence induced by the bisimulation is such that
the transfer of strategies (the construction of $\alpha_{{\cal H}}$ given
$\alpha_{{\cal G}}$) is of the form $\alpha_{{\cal H}}(\cdot)=\alpha_{{\cal
G}}(\mu(\cdot))$ where $\mu$ is a mapping between bisimilar histories444In
games played over information trees, the histories are sequences of
information sets; we do not denote them by a symbol to avoid having to define
them formally. that is sequential, that is the image of a prefix of a history
is a prefix of the image of that history. So, for pure strategies the action
played by $\alpha_{{\cal H}}$ at a history is a copy of the action played by
$\alpha_{{\cal G}}$ in a bisimilar history in ${\cal G}$. In the case of
randomized strategies, the player chooses a distribution over actions, which
we may view as attaching probabilities to actions, in a way that could be
copied along with the action to transfer randomized strategies (on one hand
from ${\cal G}$ to ${\cal H}$, and on the other hand from ${\cal H}$ to ${\cal
G}$) and establish alternating probabilistic trace equivalence (containment in
both directions) of the two games.

We recall the strong relationships between games with imperfect information
and their induced abstract game (Figure 2). First, there is a natural
bijection between an imperfect-information game ${\cal G}$ and the perfect-
information game played on its information tree $\mathcal{U}_{\sim}(G)$, which
is a witness of alternating trace equivalence of the two games [7, Lemma 1].
Second, assuming the existence of a rectangular morphism $h$ for ${\cal G}$,
the information trees of ${\cal G}$ and of ${\cal H}$ (the abstract game
induced from ${\cal G}$ by $h$) are bisimilar. The bijections and the
bisimulation (Figure 2) entail alternating trace equivalence of the games
${\cal G}$ and ${\cal H}$ and their information trees, and thus equivalence of
the synthesis problems with pure strategies in ${\cal G}$ and in ${\cal H}$
[7, Lemma 2,Theorem 1].

${\cal G}$$\mathcal{U}_{\sim}(G)$${\cal H}$$\mathcal{U}_{\approx}(H)$$(1)$
alternating
---
trace equivalence
(via bijection)
bisimulation alternating
---
trace equivalence
(via bijection)
$(1)$$(2)$ imperfect-information games
---
perfect-information games
(information trees)
${\cal H}$

Figure 2: Equivalences between the game ${\cal G}$, its induced abstract game
${\cal H}$, and their information trees.

###  4.3 Counter-examples

We present two examples showing the difficulty to adapt the results of
alternating trace equivalence for games with pure strategies, to alternating
probabilistic trace equivalence for games with randomized strategies.

First, we show that with randomized strategies, playing on the information
tree of a game with imperfect information is not equivalent to playing in the
original game, although this is true for pure strategies (links (1) of Figure
2).

Second, we show an example where the abstract game ${\cal H}$ induced by a
game ${\cal G}$ with imperfect information and (the cumulative extension of) a
rectangular morphism $h$ is not equivalent to ${\cal G}$ (for alternating
probabilistic trace equivalence), showing the absence of a direct link, marked
(2) in Figure 2. Such a direct link exists in partial-observation games à la
Reif, via the bijection $\hat{h}$ mentioned in Section 4.2.

The first example is matching pennies (the game ${\cal G}$ in Figure 1(a)).
Recall that the set of actions is $A=\\{a,b\\}$, the set of moves is
$\Gamma=\\{a_{1},a_{2},b_{1},b_{2}\\}$ with ${\sf act}(a_{i})=a$ and ${\sf
act}(b_{i})=b$ for $i=1,2$. It is well known that the player cannot win
matching pennies using a pure strategy, but wins almost-surely by choosing
head and tail uniformly at random in every round. However, in the game played
on the information tree of ${\cal G}$ (Figure 1(b)), the player cannot win,
even with positive probability. After the first round the information set is
$U_{2}=\Gamma$, which has two successors on both actions $a$ and $b$. This is
because $U_{2}$ contains both a history $\tau$ such that $\tau a_{i}$ is
winning and a history $\tau^{\prime}$ such that $\tau^{\prime}b_{i}$ is
winning, hence $U_{3}$ is a successor of $U_{2}$ (on both actions $a$ and
$b$), and analogously $X$ is a successor of $U_{2}$ ($X$ is a placeholder for
the whole tree of Figure 1(b)). Therefore, after any choice of action by the
player in $U_{2}$, the environment can always choose $X$ and continue the
game, ensuring that the reachability objective is never satisfied.

This first example illustrates a crucial difference between pure and
randomized strategies. Considering a game ${\cal G}$ (with imperfect
information induced by an indistinguishability relation $\sim$) and the game
played on its information tree $\mathcal{U}_{\sim}(G)$ (which is of perfect
information), there is a natural bijection between (information-consistent)
strategies in ${\cal G}$ and strategies in $\mathcal{U}_{\sim}(G)$. The
bijection exists for both pure and randomized strategies. However, only in the
case of pure strategies, the bijection is a witness of alternating trace
equivalence (Figure 2). Intuitively, this is because once a _pure_ strategy
for the player is fixed, the environment “knows” the specific action played in
every history (which is the same within an information set), and therefore
constructing a path in the original game ${\cal G}$ compatible with the player
strategy is equivalent to constructing a path in $\mathcal{U}_{\sim}(G)$
(informally, the information tree is a valid abstraction for “existence of
paths”). In contrast, once a _randomized_ strategy for the player is fixed,
the environment only “knows” the specific distribution over actions played in
every history, which leaves an element of surprise as to which action will be
played when the strategy is executed. In this context, the information tree is
no longer a valid abstraction, intuitively because it allows the environment
to choose a history within the current information set _after_ the randomly
chosen action is known, as illustrated by matching pennies (Figure 1(b)). To
be valid, the abstraction should force the environment to stick to a single
choice of a history, before the action is drawn from the distribution chosen
by the player. We may consider the abstract game ${\cal H}$ induced from
${\cal G}$ as a candidate for a richer abstraction, and establish a direct
link (2) between ${\cal G}$ and ${\cal H}$, given the link (1) breaks (Figure
2). Unfortunately, our second example shows that ${\cal G}$ does not reduce to
${\cal H}$ in general (${\cal G}\not\preceq{\cal H}$).

$q_{0}$$q_{1}$$q^{\prime}_{1}$$1$$2$$3$$4$$5$$6$$3$$4$$5$$6$$q_{2}$$q^{\prime}_{2}$$q_{3}$$q^{\prime}_{3}$$q_{4}$$q^{\prime}_{4}$$t_{1}$$1-t_{1}$$x_{1}$$x_{1}$$1-{\color[rgb]{.4,.8,.1}x_{1}}$$1-{\color[rgb]{.4,.8,.1}x_{1}}$$t_{2}$$1-t_{2}$$t_{3}$$1-t_{3}$$x_{2}$$1\\!-\\!{\color[rgb]{.1,.1,.8}x_{2}}$$x_{3}$$1-{\color[rgb]{.7,.12,.12}x_{3}}$$x_{3}$$1-{\color[rgb]{.7,.12,.12}x_{3}}$$x_{2}$$1\\!-\\!{\color[rgb]{.1,.1,.8}x_{2}}$
(a)

$p_{0}$$p_{1}$$p^{\prime}_{1}$$1$$2$$3$$4$$5$$6$$3$$4$$5$$6$$p_{2}$$p^{\prime}_{2}$$p_{3}$$p_{3}$$p_{4}$$p_{4}$$z_{1}$$1-z_{1}$$y_{1}$$y_{1}$$1-{\color[rgb]{.4,.8,.1}y_{1}}$$1-{\color[rgb]{.4,.8,.1}y_{1}}$$z_{2}$$1-z_{2}$$z_{3}$$1-z_{3}$$y_{2}$$1\\!-\\!{\color[rgb]{.1,.1,.8}y_{2}}$$y_{2}$$1-{\color[rgb]{.1,.1,.8}y_{2}}$$y_{2}$$1-{\color[rgb]{.1,.1,.8}y_{2}}$$y_{2}$$1\\!-\\!{\color[rgb]{.1,.1,.8}y_{2}}$
(b)

$q_{0}$$q_{1}$$q^{\prime}_{1}$$1$$2$$3$$6$$4$$5$$q_{2}$$q^{\prime}_{2}$$q_{3}$$q^{\prime}_{3}$$q_{4}$$q^{\prime}_{4}$$t_{1}$$1-t_{1}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$\frac{1}{2}$$t_{2}$$1-t_{2}$$t_{3}$$1-t_{3}$$1$$1$$1$$1$
(c)

$\cdot$$p_{0}$$p_{1}$$1$$3$$4$$5$$6$$p_{2}$$p_{3}$$p_{4}$$1$$\frac{1}{2}$$\frac{1}{2}$$1-{\color[rgb]{.1,.1,.8}y_{2}}$$y_{2}$$y_{2}$$1\\!-\\!{\color[rgb]{.1,.1,.8}y_{2}}$$y_{2}$$1-{\color[rgb]{.1,.1,.8}y_{2}}$
(d)

Figure 3: A game ${\cal G}$ and the abstract game ${\cal H}$ induced by a
rectangular morphism, with randomized strategies encoded by the variables
$\bar{x},\bar{t}$ (in ${\cal G}$) and $\bar{y},\bar{z}$ (in ${\cal H}$).

The second example (Figure 3(a)) shows a game ${\cal G}$ and its abstract game
${\cal H}$ induced by a rectangular morphism. To avoid tedious description of
the game, we present the key features informally. The game ${\cal G}$ has two
actions for the player and two possible responses for the adversary. The
actions and moves are not shown in Figure 3(a), and states are depicted as
circles when only the action of the player determines the successor, and as
boxes when only the move of the environment determines the successor. All
states have color $0$ except the leaves, labeled by their color $1,2,\dots,6$.
The leaves are sink states (with a self-loop on every move). The dashed lines
show the indistinguishability classes. It is easy to check that the coloring
function is information-consistent.

Figure 3(b) shows the abstract game ${\cal H}$, as a tree with the same shape
as in Figure 3(a) for ${\cal G}$. The value $h(\tau)$ of a history can be read
as the label of the node in Figure 3(b) corresponding to the path defined by
$\tau$ in Figure 3(a). For example, the histories (of length $3$) in ${\cal
G}$ that correspond to the nodes $q_{3}$ and $q^{\prime}_{3}$ are mapped by
$h$ to the abstract state $p_{3}$. Figure 3(b) can be viewed as the unraveling
of the morphism $h$. It is easy to verify that $h$ is a rectangular refinement
of the coloring function, and that $\approx$-equivalent abstract states are
grouped within the dashed lines.

We show that ${\cal G}$ does not reduce to ${\cal H}$ according to alternating
probabilistic trace containment (${\cal G}\not\preceq{\cal H}$). We describe
all randomized strategies of the player and of the environment by specifying
the probability to play an action or a move in each (relevant, i.e., non-leaf)
history. We use variables $\bar{x}=x_{1},x_{2},x_{3}$ for $\alpha_{{\cal G}}$;
$\bar{y}=y_{1},y_{2}$ for $\alpha_{{\cal H}}$; $\bar{z}=z_{1},z_{2},z_{3}$ for
$\beta_{{\cal H}}$; and $\bar{t}=t_{1},t_{2},t_{3}$ for $\beta_{{\cal G}}$.
Note that the player may only use information-consistent strategies, hence the
same variable is used from indistinguishable histories to describe
$\alpha_{{\cal G}}$ and $\alpha_{{\cal H}}$. The claim ${\cal
G}\not\preceq{\cal H}$ can be written as

$\psi\equiv\exists\bar{x}\cdot\forall\bar{y}\cdot\exists\bar{z}\cdot\forall\bar{t}:\bigvee_{c=1}^{6}\varphi_{c}$

where $\varphi_{c}$ is expresses that the mass of probability on color $c$
differs in ${\cal G}$ and in ${\cal H}$. For example,

$\varphi_{1}\equiv\,t_{1}x_{1}\neq z_{1}y_{1},\text{and}$
$\varphi_{3}\equiv\,t_{1}t_{2}x_{2}(1-x_{1})+t_{3}x_{3}(1-t_{1})(1-x_{1})\neq
z_{1}z_{2}y_{2}(1-y_{1})+z_{3}y_{2}(1-z_{1})(1-y_{1}).$

To show that $\psi$ holds, we fix $x_{1}=\frac{1}{2}$, $x_{2}=1$, and
$x_{3}=0$. Now, consider all possible values of $\bar{y}$ and observe that if
$y_{1}\neq\frac{1}{2}$, then $\psi$ holds since the probability mass in colors
$\\{1,2\\}$ is $\frac{1}{2}$ in ${\cal G}$ and $y_{1}$ in ${\cal H}$ (and thus
$\varphi_{1}\lor\varphi_{2}$ must hold regardless of the value of $\bar{z}$
and $\bar{t}$). So, it remains to show that $\psi$ holds for
$y_{1}=\frac{1}{2}$ (and for all values of $y_{2}$). Fix $z_{1}=1$ and
$z_{2}=1-y_{2}$ (the value of $z_{3}$ is arbitrary), as illustrated in Figure
3(c) and Figure 3(d).

Consider all possible values of $\bar{t}$ and observe that if $t_{1}\neq 1$,
then $\psi$ holds since the probability mass in color $1$ is $\frac{1}{2}$ in
${\cal G}$ and $t_{1}$ in ${\cal H}$ (thus $\varphi_{1}$ holds). With
$t_{1}=1$, we show that $\varphi_{4}\lor\varphi_{5}$ holds, that is:

$0\neq\frac{(1-y_{2})^{2}}{2}\ \lor\ 0\neq\frac{(y_{2})^{2}}{2}$

which holds since either $y_{2}\neq 0$ or $1-y_{2}\neq 0$.

We conclude that $\psi$ holds and thus ${\cal G}$ does not reduce to ${\cal
H}$ (${\cal G}\not\preceq{\cal H}$). Note that slightly stronger statements
can be proved by a similar argument: first, the strategy $\beta_{{\cal H}}$
(represented by the variables $\bar{z}$) can be chosen pure, by setting
$z_{2}=1$ if $y_{2}=0$ and $z_{2}=0$ if $y_{2}=1$ (and setting $z_{2}$ to an
arbitrary value in $\\{0,1\\}$ otherwise); second, the example does not even
preserve almost-sure probabilities, in the following sense. Given a target set
$T\subseteq C=\\{1,\dots,6\\}$ of colors, let ${\sf Reach}(T)=\bigcup_{k\in
T}C^{*}kC^{\omega}$ be the reachability objective with target $T$. Consider
the formula

$\psi^{\prime}\equiv\exists\bar{x}\cdot\forall\bar{y}\cdot\exists\bar{z}\cdot\forall\bar{t}:\bigvee_{T\subseteq
C}\lnot(\mathrm{Pr}_{{\cal G}}^{\bar{x},\bar{t}}({\sf
Reach}(T))=1\Leftrightarrow\mathrm{Pr}_{{\cal H}}^{\bar{y},\bar{z}}({\sf
Reach}(T))=1)$

where $\mathrm{Pr}_{{\cal G}}^{\bar{x},\bar{t}}({\sf Reach}(T))$ is the
probability that the objective ${\sf Reach}(T)$ is satisfied in ${\cal G}$
under strategies $\alpha_{{\cal G}}$ defined by the variables $\bar{x}$ for
the player and $\beta_{{\cal G}}$ defined by $\bar{t}$ for the environment
(and analogously for $\mathrm{Pr}_{{\cal H}}^{\bar{y},\bar{z}}({\sf
Reach}(T))$ in ${\cal H}$). It is easy to check that the condition
$\psi^{\prime}$ entails $\psi$.

To prove that $\psi^{\prime}$ holds, we fix $x_{1}=\frac{1}{2}$, $x_{2}=1$,
and $x_{3}=0$ as before (Figure 3(c)). Consider three possible cases for
$\bar{y}$: $(i)$ if $y_{1}=0$, then no matter the value of the other variables
the objective ${\sf Reach}(\\{1,2\\})$ has probability $\frac{1}{2}$ in ${\cal
G}$ and probability $0$ in ${\cal H}$, so we take
$T=C\setminus\\{1,2\\}=\\{3,4,5,6\\}$; $(ii)$ if $y_{1}=1$, we take
$T=\\{1,2\\}$ (the probability mass is $\frac{1}{2}$ in ${\cal G}$ and $1$ in
${\cal H}$); $(iii)$ otherwise $0<y_{1}<1$, and we take $z_{1}=1$ and
$z_{2}=1-y_{2}$ (illustrated in Figure 3(d) for $y_{1}=\frac{1}{2}$), and
consider all possible values of $\bar{t}$: if $t_{1}\neq 1$ then ${\sf
Reach}(\\{2\\})$ has positive probability in ${\cal G}$ and probability $0$ in
${\cal H}$, so we take $T=C\setminus\\{2\\}=\\{1,3,4,5,6\\}$, and if
$t_{1}=1$, then ${\sf Reach}(\\{4,5\\})$ has probability $0$ in ${\cal G}$ and
positive probability in ${\cal H}$, so we take
$T=C\setminus\\{4,5\\}=\\{1,2,3,6\\}$.

######  Theorem 4.1.

There exists a regular game ${\cal G}$ such that the abstract game ${\cal H}$
induced from ${\cal G}$ is not alternating probabilistic trace equivalent to
${\cal G}$.

## References

  * [1] S. Almagor, U. Boker, and O. Kupferman.  What’s decidable about weighted automata?  Inf. Comput., 282:104651, 2022.
  * [2] R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi.  Alternating refinement relations.  In Proc. of CONCUR: Concurrency Theory, LNCS 1466, pages 163–178. Springer, 1998.
  * [3] K. R. Apt and E. Grädel, editors.  Lectures in Game Theory for Computer Scientists.  Cambridge University Press, 2011.
  * [4] C. Baier, M. Größer, and N. Bertrand.  Probabilistic $\omega$-automata.  J. ACM, 59(1):1, 2012.
  * [5] C. Baral, T. Bolander, H. van Ditmarsch, and S. McIlrath.  Epistemic Planning (Dagstuhl Seminar 17231).  Dagstuhl Reports, 7(6):1–47, 2017.
  * [6] D. Berwanger and L. Doyen.  Observation and distinction. representing information in infinite games.  In Proceedings of STACS: Symposium on Theoretical Aspects of Computer Science, LIPIcs, pages 48:1–48:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2020.
  * [7] D. Berwanger, L. Doyen, and T. Soullard.  Synthesising full-information protocols.  CoRR, abs/2307.01063, 2023.
  * [8] J. C. Bradfield and C. Stirling.  Modal mu-calculi.  In Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721–756. North-Holland, 2007.
  * [9] J. C. Bradfield and I. Walukiewicz.  The mu-calculus and model checking.  In Handbook of Model Checking, pages 871–919. Springer, 2018.
  * [10] P. Cerný, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh.  Quantitative synthesis for concurrent programs.  In Proc. of CAV: Computer Aided Verification, LNCS 6806, pages 243–259. Springer, 2011.
  * [11] K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger.  Randomness for free.  Information and Computation, 245:3–16, 2017.
  * [12] K. Chatterjee, L. Doyen, T. A. Henzinger, and J.-F. Raskin.  Algorithms for omega-regular games of incomplete information.  Logical Methods in Computer Science, 3(3:4), 2007.
  * [13] C. Courcoubetis and M. Yannakakis.  The complexity of probabilistic verification.  Journal of the ACM, 42(4):857–907, 1995.
  * [14] L. de Alfaro, T. A. Henzinger, and O. Kupferman.  Concurrent reachability games.  Theoretical Computer Science, 386(3):188–217, 2007.
  * [15] S. Demri and R. Fervari.  Model-checking for ability-based logics with constrained plans.  In Proc. of AAAI, pages 6305–6312. AAAI Press, 2023.
  * [16] L. Doyen, T. A. Henzinger, and J.-F. Raskin.  Equivalence of labeled Markov chains.  Inernational Journal of Foundations of Computer Science, 19(3):549–563, 2008.
  * [17] R. Gibbons.  Game Theory for Applied Economists.  Princeton University Press, 1992.
  * [18] E. Grädel, W. Thomas, and T. Wilke, editors.  Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS 2500. Springer, 2002.
  * [19] D. Gurov, V. Goranko, and E. Lundberg.  Knowledge-based strategies for multi-agent teams playing against nature.  Artif. Intell., 309:103728, 2022.
  * [20] D.A. Martin.  The determinacy of Blackwell games.  The Journal of Symbolic Logic, 63(4):1565–1581, 1998.
  * [21] A. Paz.  Introduction to probabilistic automata.  Academic Press, 1971.
  * [22] John H. Reif.  The complexity of two-player games of incomplete information.  Journal of Computer and System Sciences, 29(2):274–301, 1984.
  * [23] W. Thomas.  On the synthesis of strategies in infinite games.  In Proc. of STACS: Symposium on Theoretical Aspects of Computer Science, LNCS 900. Springer, 1995.

##  Appendix A Proof of Lemma 3.4

The abstract states computed by the fixpoint $Y_{*}$ are all universally
winning.

See 3.4

######  Proof A.1.

Given $p\in Y_{*}\cap P$, we show that $p\in P_{\forall}$. Let $A_{p}=\\{a\in
A\mid(p,a)\in Y_{*}\\}$ and show that $A_{p}\neq\varnothing$. Since
$Y_{*}\subseteq{\sf Pre}(Y_{*})\cup P_{F}$, either $(i)$ $p\in P_{F}$ and then
$A_{p}=A\neq\varnothing$ as $P_{F}\times A\subseteq{\sf Pre}(P_{F})$ (states
in $P_{F}$ form a sink set and $P_{F}$ is closed under $\approx$); or $(ii)$
$p\in{\sf Pre}(Y_{*})$ and by definition there exists $a\in A$ such that
$(p,a)\in Y_{*}$, hence $A_{p}\neq\varnothing$.

Consider the strategy $\alpha$ for the player defined, for all
$\tau\in\Gamma^{*}$, by $\alpha(\tau)=d_{U}(A_{p})$ where $p=h(\tau)$ and
$d_{U}(\cdot)$ is the uniform distribution. We show that $\alpha$ is
information-consistent. Given $\tau^{\prime}\sim\tau$, let $p=h(\tau)$ and
$p^{\prime}=h(\tau^{\prime})$. Hence we have $p\approx p^{\prime}$, and since
$Y_{*}$ is closed under $\approx$, if $(p,a)\in Y_{*}$ then $(p^{\prime},a)\in
Y_{*}$. It follows that $A_{p}=A_{p^{\prime}}$ and thus
$\alpha(\tau)=\alpha(\tau^{\prime})$.

The strategy $\alpha$ ensures that $Y_{*}$ is never left: if $h(\tau)\in
Y_{*}$ and $a\in{\sf Supp}(\alpha(\tau))$, then $h(\tau c)\in Y_{*}$ for all
$c$ such that ${\sf act}(c)=a$. Indeed, for $p=h(\tau)$ we have $a\in A_{p}$
and $(p,a)\in Y_{*}$ thus $(p,a)\in{\sf Pre}(Y_{*})$ which imply
$\delta^{P}(p,c)=h(\tau c)\in Y_{*}$.

We now show that $\alpha$ ensures from $Y_{*}$ a target state is reached
within the next $N=\lvert P\rvert$ steps with probability at least
$\nu=\frac{1}{\lvert A\rvert^{N}}$, that is
$\mathrm{Pr}_{\tau}^{\alpha,\beta}({\sf
Reach}^{\leq\lvert\tau\rvert+N})\geq\nu$ for all strategies $\beta$ of the
environment and for all $\tau\in\Gamma^{*}$ such that $h(\tau)\in Y_{*}$.

Since $Y_{*}=\mu X.\,{\rm int}_{\approx}(Y_{*})\cap({\sf Pre}(X)\cup P_{F})$,
the set $Y_{*}$ is the limit of the (non-decreasing) sequence
$(X_{i})_{i\in{\rm Nature}}$ where $X_{0}=\varnothing$ and
$X_{i+1}=Y_{*}\cap({\sf Pre}(X_{i})\cup P_{F})$. The _rank_ of an element
$y\in Y_{*}$ is the least $i\geq 0$ such that $y\in X_{i}$ (i.e., such that
$y\in X_{i}$ and $y\not\in X_{i-1}$). By extension, the rank of a history
$\tau$ such that $h(\tau)\in Y_{*}$ is the rank of $h(\tau)$. Note that states
$p\in Y_{*}\cap P$ have odd rank, and the state-action pairs $(p,a)\in
Y_{*}\cap(P\times A)$ have even rank. The smallest rank is $1$ and corresponds
to the set $P_{F}$ of target states. Let $N_{*}$ be the largest rank, which is
bounded by $\lvert Y_{*}\rvert$.

Intuitively, from any history $\tau$ such that $h(\tau)\in Y_{*}$ the strategy
$\alpha$ ensures, against all strategies of the environment, that the history
$\tau c$ after the next round has a lower rank (unless the rank of $\tau$ is
$1$, and thus $\tau$ is a winning history) with probability at least
$\frac{1}{\lvert A\rvert}$. Let $r>1$ be the rank of $h(\tau)$, then
$h(\tau)\in{\sf Pre}(X_{r-1})$ and thus there is an action $a\in A$ such that
$(h(\tau),a)\in X_{r-1}$, thus $(h(\tau),a)\in{\sf Pre}(X_{r-2})$ and $h(\tau
c)\in X_{r-2}$ for all $c$ with ${\sf act}(c)=a$. It follows that $a\in A_{p}$
is played with probability at least $\frac{1}{\lvert A\rvert}$ and the
intuitive claim follows.

Combined with the fact that the strategy $\alpha$ ensures $Y_{*}$ is never
left, this claim shows that from all $\tau$ such that $h(\tau)\in Y_{*}$,
against all strategies $\beta$ of the environment, the reachability objective
is satisfied (i.e., the rank decreases to $1$) within the next $N_{*}$ rounds
with probability at least $\nu=\frac{1}{\lvert A\rvert^{N_{*}}}$. Formally
$\mathrm{Pr}_{\tau}^{\alpha,\beta}({\sf
Reach}^{\leq\lvert\tau\rvert+N_{*}})\geq\nu$ against all strategies. It
follows that the probability of _not_ reaching a target state within $k\cdot
N_{*}$ rounds is at most $(1-\nu)^{k}$ which tends to $0$ as $k\to\infty$,
thus $\mathrm{Pr}_{\tau}^{\alpha,\beta}({\sf Reach})=1$ by the squeeze
theorem. We conclude that the player is almost-sure winning from
$[\tau]_{\sim}$ since $Y_{*}$ is closed under $\approx$, which implies that
$p=h(\tau)\in P_{\forall}$.

##  Appendix B Proof of Lemma 3.5

The fixpoint $Y_{*}$ contains all existentially winning states.

See 3.5

######  Proof B.1.

As a preliminary, it will be useful to note that if a strategy $\alpha_{{\sf
as}}$ for the player is almost-sure winning from an information set
$[\tau]_{\sim}$, then for all actions $a\in{\sf Supp}(\alpha_{{\sf
as}}(\tau))$, for all moves $c$ supported by $a$, ${\sf act}(c)=a$, the
strategy $\alpha_{{\sf as}}$ is almost-sure winning from $[\tau c]_{\sim}$. An
equivalent conclusion is that for all actions $a\in{\sf Supp}(\alpha_{{\sf
as}}(\tau))$, the pair $(h(\tau),a)$ is in ${\rm int}_{\approx}({\sf
Pre}(P_{\exists}))\leavevmode\nobreak\ (\star)$.

We now proceed with the proof of the lemma. First, $P_{\exists}\subseteq P$ by
definition. To show that $P_{\exists}\subseteq Y_{*}$, since $Y_{*}$ is
defined as a greatest fixpoint, it is sufficient to show that
$Y_{\exists}:=P_{\exists}\cup{\rm int}_{\approx}({\sf Pre}(P_{\exists}))$ is a
fixpoint, that is $Y_{\exists}=\mu X.\,{\rm
int}_{\approx}(Y_{\exists})\cap({\sf Pre}(X)\cup P_{F})$. Since $P_{\exists}$
is closed under $\approx$ (i.e., $P_{\exists}={\rm
int}_{\approx}(P_{\exists})$) so is $Y_{\exists}$, and we only need to show
that $Y_{\exists}\subseteq\mu X.\,Y_{\exists}\cap({\sf Pre}(X)\cup
P_{F})=:X_{*}$ (the converse inclusion is trivial).

Given $y\in Y_{\exists}$, we show that $y\in X_{*}$, which concludes the
proof. We consider two cases, either $y=p\in P_{\exists}$ or $y=(p,a)\in{\rm
int}_{\approx}({\sf Pre}(P_{\exists}))$:

  * $(i)$

if $p\in P_{\exists}$, then there exists $\tau_{p}\in\Gamma^{*}$ such that
$h(\tau_{p})=p$ and the player is almost-sure winning from $[\tau_{p}]_{\sim}$
using a strategy $\alpha_{{\sf as}}$. Assume towards contradiction that
$p\not\in X_{*}$.

We construct a (pure) spoiling strategy $\beta$ for the environment as
follows. For all $\tau\in\Gamma^{*}$ such that $h(\tau)\in P_{\exists}$ and
$h(\tau)\not\in X_{*}$ (thus $h(\tau)\not\in{\sf Pre}(X_{*})$), for all
actions $a\in{\sf Supp}(\alpha_{{\sf as}}(\tau))$ played by $\alpha_{{\sf
as}}$ in $\tau$, the pair $(h(\tau),a)$ is not in $X_{*}$, and further not in
${\sf Pre}(X_{*})$ since $(h(\tau),a)\in{\rm int}_{\approx}({\sf
Pre}(P_{\exists}))$ by $(\star)$, thus there exists a move $c$ supported by
action $a$ such that $h(\tau c)=\delta^{P}(h(\tau),c)\not\in X_{*}$. Define
$\beta(\tau,a)=c$, and define $\beta(\tau^{\prime},a)$ arbitrarily for
$\tau^{\prime}$ such that $h(\tau^{\prime})\in X_{*}$.

We have the following, for all histories $\tau\in\Gamma^{*}$ and for $a\in{\sf
Supp}(\alpha_{{\sf as}}(\tau))$ and $c=\beta(\tau,a)$:

    * –

if $h(\tau)\in P_{\exists}$, then $h(\tau c)\in P_{\exists}$ (since
$\alpha_{{\sf as}}$ is almost-sure winning),

    * –

if $h(\tau)\in P_{\exists}$ and moreover $h(\tau)\not\in X_{*}$, then $h(\tau
c)\not\in X_{*}$,

    * –

$h(\tau_{p})\in P_{\exists}$ and $h(\tau_{p})\not\in X_{*}$.

It follows by an inductive argument that against $\alpha$, the constructed
strategy $\beta$ ensures from $\tau_{p}$ that $X_{*}$ and thus $P_{F}$ is
never reached, hence $\mathrm{Pr}_{\tau_{p}}^{\alpha_{{\sf as}},\beta}({\sf
Reach})=0$, which contradicts that $\alpha_{{\sf as}}$ is almost-sure winning
from $\tau_{p}$. Hence $p\in X_{*}$.

  * $(ii)$

if $(p,a)\in{\rm int}_{\approx}({\sf Pre}(P_{\exists}))$, then
$\delta^{P}(p,c))\in P_{\exists}$ for all moves $c$ supported by $a$. By an
argument similar to case $(i)$, we have $\delta^{P}(p,c))\in X_{*}$. It
follows that $(p,a)\in{\sf Pre}(X_{*})$ and thus $(p,a)\in
X_{*}=Y_{\exists}\cap({\sf Pre}(X_{*})\cup P_{F})$.