11institutetext:  1 Uppsala University 2 LaBRI, University of Bordeaux I 3
University of Edinburgh

# Stochastic Parity Games on Lossy Channel Systems ††thanks:  Technical Report
EDI-INF-RR-1416 of the School of Informatics at the University of Edinburgh,
UK. (http://www.inf.ed.ac.uk/publications/report/). Full version (including
proofs) of material presented at QEST 2013 (Buenos Aires, Argentina).
arXiv.org - CC BY 3.0.

Parosh Aziz Abdulla 11 Lorenzo Clemente2 Richard Mayr3 and Sven Sandberg1

###### Abstract

We give an algorithm for solving stochastic parity games with almost-sure
winning conditions on lossy channel systems, for the case where the players
are restricted to finite-memory strategies. First, we describe a general
framework, where we consider the class of $2\frac{1}{2}$-player games with
almost-sure parity winning conditions on possibly infinite game graphs,
assuming that the game contains a finite attractor. An attractor is a set of
states (not necessarily absorbing) that is almost surely re-visited regardless
of the players’ decisions. We present a scheme that characterizes the set of
winning states for each player. Then, we instantiate this scheme to obtain an
algorithm for stochastic game lossy channel systems.

##  1 Introduction

#### Background.

2-player games can be used to model the interaction of a controller (player 0)
who makes choices in a reactive system, and a malicious adversary (player 1)
who represents an attacker. To model randomness in the system (e.g.,
unreliability; randomized algorithms), a third player ‘random’ is defined who
makes choices according to a predefined probability distribution. The
resulting stochastic game is called a $2\frac{1}{2}$-player game in the
terminology of [14]. The choices of the players induce a run of the system,
and the winning conditions of the game are expressed in terms of predicates on
runs.

Most classic work on algorithms for stochastic games has focused on finite-
state systems (e.g., [24, 16, 18, 14]), but more recently several classes of
infinite-state systems have been considered as well. Stochastic games on
infinite-state probabilistic recursive systems (i.e., probabilistic pushdown
automata with unbounded stacks) were studied in [20, 21, 19]. A different (and
incomparable) class of infinite-state systems are channel systems, which use
unbounded communication buffers instead of unbounded recursion.

Channel Systems consist of finite-state machines that communicate by
asynchronous message passing via unbounded FIFO communication channels. They
are also known as communicating finite-state machines (CFSM) [12].

A Lossy Channel System (LCS) [6] consists of finite-state machines that
communicate by asynchronous message passing via unbounded unreliable (i.e.,
lossy) FIFO communication channels, i.e., messages can spontaneously disappear
from channels.

A Probabilistic Lossy Channel System (PLCS) [9, 7] is a probabilistic variant
of LCS where, in each computation step, messages are lost from the channels
with a given probability. In [4], a game extension of PLCS was introduced
where the players control transitions in the control graph and message losses
are probabilistic.

The original motivation for LCS and PLCS was to capture the behavior of
communication protocols; such protocols are designed to operate correctly even
if the communication medium is unreliable (i.e., if messages can be lost).
However, Channel Systems (aka CFSM) are a very expressive model that can
encode the behavior of Turing machines, by storing the content of a Turing
tape in a channel [12]. The only reason why certain questions are decidable
for LCS/PLCS is that the message loss induces a quasi-order on the
configurations, which has the properties of a simulation. Similarly to Turing
machines and CFSM, one can encode many classes of infinite-state probabilistic
transition systems into a PLCS. The only requirement is that the system re-
visits a certain finite core region (we call this an attractor; see below)
with probability one, e.g.,

  * •

Queuing systems where waiting customers in a queue drop out with a certain
probability in every time interval. This is similar to the well-studied class
of queuing systems with impatient customers which practice reneging, i.e.,
drop out of a queue after a given maximal waiting time; see [26] section II.B.
Like in some works cited in [26], the maximal waiting time in our model is
exponentially distributed. In basic PLCS, unlike in [26], this exponential
distribution does not depend on the current number of waiting customers.
However, an extension of PLCS with this feature would still be analyzable in
our framework (except in the pathological case where a high number of waiting
customers increases the customers patience exponentially, because such a
system would not necessarily have a finite attractor).

  * •

Probabilistic resource trading games with probabilistically fluctuating
prices. The given stores of resources are encoded by counters (i.e.,
channels), which exhibit a probabilistic decline (due to storage costs, decay,
corrosion, obsolescence).

  * •

Systems modeling operation cost/reward, which is stored in counters/channels,
but probabilistically discounted/decaying over time.

  * •

Systems which are periodically restarted (though not necessarily by a
deterministic schedule), due to, e.g., energy depletion or maintenance work.

Due to this wide applicability of PLCS, we focus on this model in this paper.
However, our main results are formulated in more general terms referring to
infinite Markov chains with a finite attractor; see below.

#### Previous work.

Several algorithms for symbolic model checking of PLCS have been presented [1,
23]. Markov decision processes (i.e., $1\frac{1}{2}$-player games) on infinite
graphs induced by PLCS were studied in [8], which shows that
$1\frac{1}{2}$-player games with almost-sure Büchi objectives are pure
memoryless determined and decidable. This result was later generalized to
$2\frac{1}{2}$-player games [4], and further extended to generalized Büchi
objectives [10]. On the other hand, $1\frac{1}{2}$-player games on PLCS with
positive probability Büchi objectives (i.e., almost-sure co-Büchi objectives
from the (here passive) opponent’s point of view) can require infinite memory
to win and are also undecidable [8]. (Undecidability and infinite memory
requirement are separate results, since decidability does not imply the
existence of finite-memory strategies in infinite-state games). If players are
restricted to finite-memory strategies, the $1\frac{1}{2}$-player game with
positive probability parity objectives (even the more general _Streett
objectives_) becomes decidable [8]. Note that the finite-memory case and the
infinite-memory one are a priori incomparable problems, and neither subsumes
the other. Cf. Section 7.

Non-stochastic (2-player) parity games on infinite graphs were studied in
[27], where it is shown that such games are determined, and that both players
possess winning memoryless strategies in their respective winning sets.
Furthermore, a scheme for computing the winning sets and winning strategies is
given. Stochastic games ($2\frac{1}{2}$-player games) with parity conditions
on _finite_ graphs are known to be memoryless determined and effectively
solvable [17, 14, 13].

#### Our contribution.

We give an algorithm to decide almost-sure parity games for probabilistic
lossy channel systems in the case where the players are restricted to finite
memory strategies. We do that in two steps. First, we give our result in
general terms (Section 4): We consider the class of $2\frac{1}{2}$-player
games with almost-sure parity wining conditions on possibly infinite game
graphs, under the assumption that the game contains a finite attractor. An
attractor is a set $A$ of states such that, regardless of the strategies used
by the players, the probability measure of the runs which visit $A$ infinitely
often is one.111 In the game community (e.g., [27]) the word attractor is used
to denote what we call a force set in Section 3. In the infinite-state systems
community (e.g., [1, 5]), the word is used in the same way as we use it in
this paper. Note that this means neither that $A$ is absorbing, nor that every
run must visit $A$. We present a general scheme characterizing the set of
winning states for each player. The scheme is a non-trivial generalization of
the well-known scheme for non-stochastic games in [27] (see the remark in
Section 4). In fact, the constructions are equivalent in the case that no
probabilistic states are present. We show correctness of the scheme for games
where each player is restricted to a finite-memory strategy. The correctness
proof here is more involved than in the non-stochastic case of [27]; we rely
on the existence of a finite attractor and the restriction of the players to
use finite-memory strategies. Furthermore, we show that if a player is winning
against all finite-memory strategies of the other player then he can win using
a _memoryless_ strategy. In the second step (Section 6), we show that the
scheme can be instantiated for lossy channel systems. The instantiation
requires the use of a much more involved framework than the classical one for
well quasi-ordered transition systems [3] (see the remark in Section 6). The
above two steps yield an algorithm to decide parity games in the case when the
players are restricted to finite memory strategies. If the players are allowed
infinite memory, then the problem is undecidable already for
$1\frac{1}{2}$-player games with co-Büchi objectives (a special case of
2-color parity objectives) [8]. Note that even if the players are restricted
to finite memory strategies, such a strategy (even a memoryless one) on an
infinite game graph is still an infinite object. Thus, unlike for finite game
graphs, one cannot solve a game by just guessing strategies and then checking
if they are winning. Instead, we show how to effectively compute a finite,
symbolic representation of the (possibly infinite) set of winning states for
each player as a regular language.

##  2 Preliminaries

#### Notation.

Let $\mathbb{O}$ and $\mathbb{N}$ denote the set of ordinal resp. natural
numbers. We use $f:X\to Y$ to denote that $f$ is a total function from $X$ to
$Y$, and use $f:X\rightharpoonup Y$ to denote that $f$ is a partial function
from $X$ to $Y$. We write $f(x)=\bot$ to denote that $f$ is undefined on $x$,
and define ${\it dom}(f):=\\{{x}|\;{f(x)\neq\bot}\\}$. We say that $f$ is an
extension of $g$ if $g(x)=f(x)$ whenever $g(x)\neq\bot$. For
$X^{\prime}\subseteq X$, we use $f|X^{\prime}$ to denote the restriction of
$f$ to $X^{\prime}$. We will sometimes need to pick an arbitrary element from
a set. To simplify the exposition, we let ${\it select}(X)$ denote an
arbitrary but fixed element of the nonempty set $X$.

A _probability distribution_ on a countable set $X$ is a function
$f:X\to[0,1]$ such that $\sum_{x\in X}f(x)=1$. For a set $X$, we use $X^{*}$
and $X^{\omega}$ to denote the sets of finite and infinite words over $X$,
respectively. The empty word is denoted by $\varepsilon$.

#### Games.

A _game_ (of _rank $n$_) is a tuple
${\mathcal{G}}=(S,S^{0},S^{1},S^{R},{\longrightarrow},P,{\tt Col})$ defined as
follows. $S$ is a set of _states_ , partitioned into the pairwise disjoint
sets of _random states_ $S^{R}$, states $S^{0}$ of Player$~{}0$, and states
$S^{1}$ of Player $1$. ${\longrightarrow}\subseteq S\times S$ is the
_transition relation_. We write $s{\longrightarrow}{}s^{\prime}$ to denote
that $(s,s^{\prime})\in{\longrightarrow}{}$. We assume that for each $s$ there
is at least one and at most countably many $s^{\prime}$ with
$s{\longrightarrow}{}s^{\prime}$. The _probability function_ $P:S^{R}\times
S\to[0,1]$ satisfies both $\forall s\in S^{R}.\forall s^{\prime}\in
S.(P(s,s^{\prime})>0\iff s{\longrightarrow}s^{\prime})$ and $\forall s\in
S^{R}.\sum_{s^{\prime}\in S}P(s,s^{\prime})=1$. (The sum is well-defined since
we assumed that the number of successors of any state is at most countable.)
${\tt Col}:S\to\\{0,\dots,n\\}$, where ${\tt Col}(s)$ is called the _color_ of
state $s$. Let $Q\subseteq S$ be a set of states. We use
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{Q}:=S-Q$ to denote the
complement of $Q$. Define $[Q]^{0}:=Q\cap S^{0}$, $[Q]^{1}:=Q\cap S^{1}$,
$[Q]^{0,1}:=[Q]^{0}\cup[Q]^{1}$, and $[Q]^{R}:=Q\cap S^{R}$. For
$n\in\mathbb{N}$ and $\sim\;\in\\{=,\leq\\}$, let $[Q]^{{\tt Col}\sim
n}:=\\{{s\in Q}|\;{{\tt Col}(s)\sim n}\\}$ denote the sets of states in $Q$
with color $\sim n$. A _run_ $\rho$ in ${\mathcal{G}}$ is an infinite sequence
$s_{0}s_{1}\cdots$ of states s.t. $s_{i}{\longrightarrow}{}s_{i+1}$ for all
$i\geq 0$; $\rho(i)$ denotes $s_{i}$. A _path_ $\pi$ is a finite sequence
$s_{0}\cdots s_{n}$ of states s.t. $s_{i}{\longrightarrow}{}s_{i+1}$ for all
$i:0\leq i<n$. We say that $\rho$ (or $\pi$) _visits_ $s$ if $s=s_{i}$ for
some $i$. For any $Q\subseteq S$, we use ${\mathrm{\Pi}}_{Q}$ to denote the
set of paths that end in some state in $Q$. Intuitively, the choices of the
players and the resolution of randomness induce a run $s_{0}s_{1}\cdots$,
starting in some initial state $s_{0}\in S$; state $s_{i+1}$ is chosen as a
successor of $s_{i}$, and this choice is made by Player 0 if $s_{i}\in S^{0}$,
by Player 1 if $s_{i}\in S^{1}$, and it is chosen randomly according to the
probability distribution $P(s_{i},\cdot)$ if $s_{i}\in S^{R}$.

#### Strategies.

For $x\in\\{0,1\\}$, a _strategy_ of Player $x$ is a partial function
$f^{x}:{\mathrm{\Pi}}_{S^{x}}\rightharpoonup S$ s.t.
$s_{n}{\longrightarrow}f^{x}(s_{0}\cdots s_{n})$ if $f^{x}(s_{0}\cdots s_{n})$
is defined. The strategy $f^{x}$ prescribes for Player $x$ the next move,
given the current prefix of the run. A run $\rho=s_{0}s_{1}\cdots$ is said to
be consistent with a strategy $f^{x}$ of Player $x$ if
$s_{i+1}=f^{x}(s_{0}s_{1}\cdots s_{i})$ whenever $f^{x}(s_{0}s_{1}\cdots
s_{i})\neq\bot$. We say that $\rho$ is induced by $(s,f^{x},f^{1-x})$ if
$s_{0}=s$ and $\rho$ is consistent with both $f^{x}$ and $f^{1-x}$. We use
${\it Runs}({\mathcal{G}},s,f^{x},f^{1-x})$ to denote the set of runs in
${\mathcal{G}}$ induced by $(s,f^{x},f^{1-x})$. We say that $f^{x}$ is total
if it is defined for every $\pi\in{\mathrm{\Pi}}_{S^{x}}$. A strategy $f^{x}$
of Player $x$ is _memoryless_ if the next state only depends on the current
state and not on the previous history of the run, i.e., for any path
$s_{0}\cdots s_{n}\in{\mathrm{\Pi}}_{S^{x}}$, we have $f^{x}(s_{0}\cdots
s_{n})=f^{x}(s_{n})$.

A _finite-memory strategy_ updates a finite memory each time a transition is
taken, and the next state depends only on the current state and memory.
Formally, we define a _memory structure_ for Player $x$ as a quadruple
$\mathcal{M}=(M,m_{0},\tau,\mu)$ satisfying the following properties. The
nonempty set $M$ is called the _memory_ and $m_{0}\in M$ is the _initial
memory configuration_. For a current memory configuration $m$ and a current
state $s$, the next state is given by $\tau:S^{x}\times M\to S$, where
$s{\longrightarrow}\tau(s,m)$. The next memory configuration is given by
$\mu:S\times M\to M$. We extend $\mu$ to paths by $\mu(\varepsilon,m)=m$ and
$\mu(s_{0}\cdots s_{n},m)=\mu(s_{n},\mu(s_{0}\cdots s_{n-1},m))$. The total
strategy $\mathit{strat}_{\mathcal{M}}:{\mathrm{\Pi}}_{S^{x}}\to S$ induced by
$\mathcal{M}$ is given by $\mathit{strat}_{\mathcal{M}}(s_{0}\cdots
s_{n}):=\tau(s_{n},\mu(s_{0}\cdots s_{n-1},m_{0}))$. A total strategy $f^{x}$
is said to have _finite memory_ if there is a memory structure
$\mathcal{M}=(M,m_{0},\tau,\mu)$ where $M$ is finite and
$f^{x}=\mathit{strat}_{\mathcal{M}}$. Consider a run
$\rho=s_{0}s_{1}\cdots\in{\it Runs}({\mathcal{G}},s,f^{x},f^{1-x})$ where
$f^{1-x}$ is induced by $\mathcal{M}$. We say that $\rho$ visits the
configuration $(s,m)$ if there is an $i$ such that $s_{i}=s$ and
$\mu(s_{0}s_{1}\cdots s_{i-1},m_{0})=m$. We use $F_{\it
all}^{x}({\mathcal{G}})$, $F^{x}_{\it finite}({\mathcal{G}})$, and
$F^{x}_{\emptyset}({\mathcal{G}})$ to denote the set of all, finite-memory,
and memoryless strategies respectively of Player $x$ in ${\mathcal{G}}$. Note
that memoryless strategies and strategies in general can be partial, whereas
for simplicity we only define total finite-memory strategies.

#### Probability Measures.

We use the standard definition of probability measures for a set of runs [11].
First, we define the measure for total strategies, and then we extend it to
general (partial) strategies. Let $\Omega^{s}=sS^{\omega}$ denote the set of
all infinite sequences of states starting from $s$. Consider a game
${\mathcal{G}}=(S,S^{0},S^{1},S^{R},{\longrightarrow},P,{\tt Col})$, an
initial state $s$, and total strategies $f^{x}$ and $f^{1-x}$ of Players $x$
and ${1-x}$. For a measurable set ${{\mathfrak{R}}}\subseteq\Omega^{s}$, we
define ${\cal P}_{{\mathcal{G}},s,f^{x},f^{1-x}}({{\mathfrak{R}}})$ to be the
probability measure of ${\mathfrak{R}}$ under the strategies $f^{x},f^{1-x}$.
This measure is well-defined [11]. For (partial) strategies $f^{x}$ and
$f^{1-x}$ of Players $x$ and ${1-x}$, $\sim\;\in\\{<,\leq,=,\geq,>\\}$, a real
number $c\in[0,1]$, and any measurable set
${\mathfrak{R}}\subseteq\Omega^{s}$, we define ${\cal
P}_{{\mathcal{G}},s,f^{x},f^{1-x}}({{\mathfrak{R}}})\sim c$ iff ${\cal
P}_{{\mathcal{G}},s,g^{x},g^{{1-x}}}({\mathfrak{R}})\sim c$ for all total
strategies $g^{x}$ and $g^{{1-x}}$ that are extensions of $f^{x}$ resp.
$f^{1-x}$.

#### Winning Conditions.

The winner of the game is determined by a predicate on infinite runs. We
assume familiarity with the syntax and semantics of the temporal logic
${\mathit{C}TL}^{*}$ (see, e.g., [15]). Formulas are interpreted on the
structure $(S,{\longrightarrow})$. We use $\llbracket{\varphi}\rrbracket^{s}$
to denote the set of runs starting from $s$ that satisfy the
${\mathit{C}TL}^{*}$ path-formula ${\varphi}$. This set is measurable [25],
and we just write ${\cal P}_{{\mathcal{G}},s,f^{x},f^{1-x}}({\varphi})\sim c$
instead of ${\cal
P}_{{\mathcal{G}},s,f^{x},f^{1-x}}(\llbracket{\varphi}\rrbracket^{s})\sim c$.

We will consider games with _parity_ winning conditions, whereby Player 1 wins
if the largest color that occurs infinitely often in the infinite run is odd,
and Player 0 wins if it is even. Thus, the winning condition for Player $x$
can be expressed in ${\mathit{C}TL}^{*}$ as $\mbox{$x$-}{\it
Parity}:=\bigvee_{i\in\\{0,\dots,n\\}\wedge(i\bmod 2)=x}(\Box\Diamond[S]^{{\tt
Col}=i}\wedge\Diamond\Box[S]^{{\tt Col}\leq i})$.

#### Winning Sets.

For a strategy $f^{x}$ of Player $x$, and a set $F^{{1-x}}$ of strategies of
Player ${1-x}$, we define
$W^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi}^{\sim c}):=\\{{s}|\;{\forall
f^{1-x}\in F^{{1-x}}.{\cal P}_{{\mathcal{G}},s,f^{x},f^{1-x}}({\varphi})\sim
c}\\}$. If there is a strategy $f^{x}$ such that $s\in
W^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi}^{\sim c})$, then we say that
$s$ is a winning state for Player $x$ in ${\mathcal{G}}$ wrt. ${\varphi}^{\sim
c}$ (and $f^{x}$ is _winning at $s$_), provided that Player ${1-x}$ is
restricted to strategies in $F^{{1-x}}$. Sometimes, when the parameters
${\mathcal{G}}$, $s$, $F^{{1-x}}$, ${\varphi}$, and $\sim c$ are known, we
will not mention them and may simply say that “$s$ is a winning state” or that
“$f^{x}$ is a winning strategy”, etc. If $s\in
W^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi}^{=1})$, then we say that Player
$x$ _almost surely (a.s.)_ wins from $s$. If $s\in
W^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi}^{>0})$, then we say that Player
$x$ wins _with positive probability (w.p.p.)_. We define
$V^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi}):=\\{{s}|\;{\forall f^{1-x}\in
F^{{1-x}}.\;{\it
Runs}({\mathcal{G}},s,f^{x},f^{1-x})\subseteq\llbracket{\varphi}\rrbracket^{s}}\\}$.
If $s\in V^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi})$, then we say that
Player $x$ surely wins from $s$. Notice that any strategy that is surely
winning from a state $s$ is also winning from $s$ a.s., i.e.,
$V^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi})\subseteq
W^{x}(f^{x},F^{{1-x}})({\mathcal{G}},{\varphi}^{=1})$.

#### Determinacy and Solvability.

A game is called _determined_ , wrt. a winning condition and two sets
$F^{0},F^{1}$ of strategies of Player $0$, resp. Player $1$, if, from every
state, one of the players $x$ has a strategy $f^{x}\in F^{x}$ that wins
against all strategies $f^{1-x}\in F^{1-x}$ of the opponent. By _solving_ a
determined game, we mean giving an algorithm to compute symbolic
representations of the sets of states which are winning for either player.

#### Attractors.

A set $A\subseteq S$ is said to be an attractor if, for each state $s\in S$
and strategies $f^{0},f^{1}$ of Player $0$ resp. Player $1$, it is the case
that ${\cal P}_{{\mathcal{G}},s,f^{0},f^{1}}(\Diamond A)=1$. In other words,
regardless of where we start a run and regardless of the strategies used by
the players, we will reach a state inside the attractor a.s.. It is
straightforward to see that this also implies that ${\cal
P}_{{\mathcal{G}},s,f^{0},f^{1}}(\Box\Diamond A)=1$, i.e., the attractor will
be visited infinitely often a.s..

#### Transition Systems.

Consider strategies $f^{x}\in F^{x}_{\emptyset}$ and $f^{1-x}\in
F^{{1-x}}_{\it finite}$ of Player $x$ resp. Player ${1-x}$, where $f^{x}$ is
memoryless and $f^{1-x}$ is finite-memory. Suppose that $f^{1-x}$ is induced
by memory structure $\mathcal{M}=(M,m_{0},\tau,\mu)$. We define the transition
system ${\mathcal{T}}$ induced by ${\mathcal{G}},f^{1-x},f^{x}$ to be the pair
$(S_{M{}},\leavevmode\hbox to15.63pt{\vbox
to3.2pt{\pgfpicture\makeatletter\hbox{\hskip 1.19998pt\lower-1.59998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}}
{} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}{{
{\pgfsys@beginscope\pgfsys@setlinewidth{0.32pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{}
{}{}{} {}{}{}
\pgfsys@moveto{-1.19998pt}{1.59998pt}\pgfsys@curveto{-1.09998pt}{0.99998pt}{0.0pt}{0.09999pt}{0.29999pt}{0.0pt}\pgfsys@curveto{0.0pt}{-0.09999pt}{-1.09998pt}{-0.99998pt}{-1.19998pt}{-1.59998pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{1.0pt}{0.9pt}\pgfsys@lineto{3.0pt}{-0.9pt}\pgfsys@lineto{5.0pt}{0.9pt}\pgfsys@lineto{7.0pt}{-0.9pt}\pgfsys@lineto{8.0pt}{0.0pt}\pgfsys@lineto{8.0pt}{0.0pt}\pgfsys@lineto{13.76639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.76639pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$ where
$S_{M{}}=S\times M$, and $\leavevmode\hbox to14.63pt{\vbox
to2.2pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-1.09999pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}}
{} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{1.0pt}{0.9pt}\pgfsys@lineto{3.0pt}{-0.9pt}\pgfsys@lineto{5.0pt}{0.9pt}\pgfsys@lineto{7.0pt}{-0.9pt}\pgfsys@lineto{8.0pt}{0.0pt}\pgfsys@lineto{8.0pt}{0.0pt}\pgfsys@lineto{13.76639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.76639pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\subseteq
S_{M{}}\times S_{M{}}$ such that $(s_{1},m_{1})\leavevmode\hbox
to14.63pt{\vbox to2.2pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.09999pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}}
{} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{0.0pt}{0.0pt}\pgfsys@lineto{1.0pt}{0.9pt}\pgfsys@lineto{3.0pt}{-0.9pt}\pgfsys@lineto{5.0pt}{0.9pt}\pgfsys@lineto{7.0pt}{-0.9pt}\pgfsys@lineto{8.0pt}{0.0pt}\pgfsys@lineto{8.0pt}{0.0pt}\pgfsys@lineto{13.76639pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.76639pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}(s_{2},m_{2})$ if
$m_{2}=\mu(s_{1},m_{1})$, and one of the following three conditions is
satisfied: (i) $s_{1}\in S^{x}$ and either $s_{2}=f^{x}(s_{1})$ or
$f^{x}(s_{1})=\bot$, (ii) $s_{1}\in S^{1-x}$ and $s_{2}=\tau(s_{1},m_{1})$, or
(iii) $s_{1}\in S^{R}$ and $P(s_{1},s_{2})>0$. Consider the directed acyclic
graph (DAG) of maximal strongly connected components (SCCs) of the transition
system ${\mathcal{T}}$. An SCC is called a bottom SCC (BSCC) if no other SCC
is reachable from it. Observe that the existence of BSCCs is not guaranteed in
an infinite transition system. However, if ${\mathcal{G}}$ contains a finite
attractor $A$ and $M$ is finite then ${\mathcal{T}}$ contains at least one
BSCC, and in fact each BSCC contains at least one element $(s_{A},m)$ with
$s_{A}\in A$. In particular, for any state $s\in S$, any run $\rho\in{\it
Runs}({\mathcal{G}},s,f^{x},f^{1-x})$ will visit a configuration $(s_{A},m)$
infinitely often a.s. where $s_{A}\in A$ and $(s_{A},m)\in B$ for some BSCC
$B$.

##  3 Reachability

In this section we present some concepts related to checking reachability
objectives in games. First, we define basic notions. Then we recall a standard
scheme (described e.g. in [27]) for checking reachability winning conditions,
and state some of its properties that we use in the later sections. Below, fix
a game ${\mathcal{G}}=(S,S^{0},S^{1},S^{R},{\longrightarrow},P,{\tt Col})$.

#### Reachability Properties.

Fix a state $s\in S$ and sets of states $Q,Q^{\prime}\subseteq S$. Let ${\it
Post}_{{\mathcal{G}}}\left(s\right):=\\{s^{\prime}:s{\longrightarrow}s^{\prime}\\}$
denote the set of _successors_ of $s$. Extend it to sets of states by ${\it
Post}_{{\mathcal{G}}}\left(Q\right):=\bigcup_{s\in Q}{\it
Post}_{{\mathcal{G}}}\left(s\right)$. Note that for any given state $s\in
S^{R}$, $P(s,\cdot)$ is a probability distribution over ${\it
Post}_{{\mathcal{G}}}\left(s\right)$. Let ${\it
Pre}_{{\mathcal{G}}}\left(s\right):=\\{s^{\prime}:s^{\prime}{\longrightarrow}s\\}$
denote the set of _predecessors_ of $s$, and extend it to sets of states as
above. We define $\widetilde{{\it
Pre}_{{\mathcal{G}}}}\left(Q\right):=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\it
Pre}_{{\mathcal{G}}}\left(\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{Q}\right)}$,
i.e., it denotes the set of states whose successors all belong to $Q$. We say
that $Q$ is _sink-free_ if ${\it Post}_{{\mathcal{G}}}\left(s\right)\cap
Q\neq\emptyset$ for all $s\in Q$, and _closable_ if it is sink-free and ${\it
Post}_{{\mathcal{G}}}\left(s\right)\subseteq Q$ for all $s\in[Q]^{R}$. If $Q$
is closable then each state in $[Q]^{0,1}$ has at least one successor in $Q$,
and all the successors of states in $[Q]^{R}$ are in $Q$.

If $\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{Q}$ is closable, we define
the _subgame_ ${\mathcal{G}}\ominus
Q:=(Q^{\prime},[Q^{\prime}]^{0},[Q^{\prime}]^{1},[Q^{\prime}]^{R},{\longrightarrow}^{\prime},P^{\prime},{\tt
Col}^{\prime})$, where
$Q^{\prime}:=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{Q}$ is the new set
of states,
${\longrightarrow}^{\prime}:={\longrightarrow}\cap({Q^{\prime}}\times{Q^{\prime}})$,
$P^{\prime}:=P|([Q^{\prime}]^{R}\times{Q^{\prime}})$, ${\tt
Col}^{\prime}:={\tt Col}|{Q^{\prime}}$. Notice that $P^{\prime}(s)$ is a
probability distribution for any $s\in S^{R}$ since
${\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{Q}}$ is closable. We use
${\mathcal{G}}\ominus Q_{1}\ominus Q_{2}$ to denote $({\mathcal{G}}\ominus
Q_{1})\ominus Q_{2}$.

For $x\in\\{0,1\\}$, we say that $Q$ is an _$x$ -trap_ if it is closable and
${\it Post}_{{\mathcal{G}}}\left(s\right)\subseteq Q$ for all $s\in[Q]^{x}$.
Notice that $S$ is both a $0$-trap and a $1$-trap, and in particular it is
both sink-free and closable. The following lemma (adapted from [27]) states
that, starting from a state inside a set of states $Q$ that is a trap for one
player, the other player can surely keep the run inside $Q$.

###### Lemma 1

If $Q$ is a $({1-x})$-trap, then there exists a memoryless strategy $f^{x}\in
F^{x}_{\emptyset}({\mathcal{G}})$ for Player $x$ such that $Q\subseteq
V^{x}(f^{x},F_{\it all}^{{1-x}}({\mathcal{G}}))({\mathcal{G}},\Box Q)$.

#### Scheme.

Given a set ${\tt Target}\subseteq S$, we give a scheme for computing a
partitioning of $S$ into two sets ${\it Force}^{x}({\mathcal{G}},{\tt
Target})$ and ${\it Avoid}^{1-x}({\mathcal{G}},{\tt Target})$ that are winning
for Players $x$ and ${1-x}$. More precisely, we define a memoryless strategy
that allows Player $x$ to force the game to ${\tt Target}$ w.p.p.; and define
a memoryless strategy that allows Player ${1-x}$ to surely avoid ${\tt
Target}$.

First, we characterize the states that are winning for Player $x$, by defining
an increasing set of states each of which consists of winning states for
Player $x$, as follows:

$\displaystyle{\mathcal{R}\,\,\\!\\!}_{0}$ $\displaystyle:={\tt Target};$
$\displaystyle{\mathcal{R}\,\,\\!\\!}_{i+1}$
$\displaystyle:={\mathcal{R}\,\,\\!\\!}_{i}\cup[{\it
Pre}_{{\mathcal{G}}}\left({\mathcal{R}\,\,\\!\\!}_{i}\right)]^{R}\cup[{\it
Pre}_{{\mathcal{G}}}\left({\mathcal{R}\,\,\\!\\!}_{i}\right)]^{x}\cup[\widetilde{{\it
Pre}_{{\mathcal{G}}}}\left({\mathcal{R}\,\,\\!\\!}_{i}\right)]^{1-x}$ if $i+1$
is a successor ordinal; $\displaystyle{\mathcal{R}\,\,\\!\\!}_{i}$
$\displaystyle:=\bigcup_{j<i}{\mathcal{R}\,\,\\!\\!}_{j}$ if $i>0$ is a limit
ordinal; ${\it Force}^{x}({\mathcal{G}},{\tt
Target}):=\bigcup_{i\in\mathbb{O}}{\mathcal{R}\,\,\\!\\!}_{i};\qquad{\it
Avoid}^{1-x}({\mathcal{G}},{\tt
Target}):=\;\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\it
Force}^{x}({\mathcal{G}},{\tt Target})}.$

First, we show that the iteration above converges (possibly in infinitely many
steps). To this end, we observe that
${\mathcal{R}\,\,\\!\\!}_{i}\subseteq{\mathcal{R}\,\,\\!\\!}_{i+1}$ if $i+1$
is a successor ordinal and
${\mathcal{R}\,\,\\!\\!}_{j}\subseteq{\mathcal{R}\,\,\\!\\!}_{i}$ if $j<i$ and
$i$ is a limit ordinal. Therefore
${\mathcal{R}\,\,\\!\\!}_{0}\subseteq{\mathcal{R}\,\,\\!\\!}_{1}\subseteq\cdots$.
Since the sequence is non-decreasing and since the sequence is bounded by $S$,
it will eventually converge. Define $\alpha$ to be the smallest ordinal such
that ${\mathcal{R}\,\,\\!\\!}_{\alpha}={\mathcal{R}\,\,\\!\\!}_{i}$ for all
$i\geq\alpha$. This gives the following lemma, which also implies that the
${\it Avoid}^{1-x}$ set is a trap for Player $x$. (Lemmas 2 and 3 are adapted
from [27], where they are stated in a non-probabilistic setting.)

###### Lemma 2

There is an $\alpha\in\mathbb{O}$ such that
${\mathcal{R}\,\,\\!\\!}_{\alpha}=\bigcup_{i\in\mathbb{O}}{\mathcal{R}\,\,\\!\\!}_{i}$.

###### Lemma 3

${\it Avoid}^{1-x}({\mathcal{G}},{\tt Target})$ is an $x$-trap.

The following lemma shows correctness of the construction. In fact, it shows
that a winning player also has a memoryless winning strategy.

###### Lemma 4

There is a memoryless strategy ${\it force}^{x}({\mathcal{G}},{\tt Target})\in
F^{x}_{\emptyset}({\mathcal{G}})$ such that
${\it Force}^{x}({\mathcal{G}},{\tt Target})\subseteq W^{x}({\it
force}^{x}({\mathcal{G}},{\tt Target}),F_{\it
all}^{{1-x}}({\mathcal{G}}))({\mathcal{G}},\Diamond{\tt Target}^{>0})$; and a
memoryless strategy ${\it avoid}^{1-x}({\mathcal{G}},{\tt Target})\in
F^{{1-x}}_{\emptyset}({\mathcal{G}})$ such that
${\it Avoid}^{x}({\mathcal{G}},{\tt Target})\subseteq V^{1-x}({\it
avoid}^{1-x}({\mathcal{G}},{\tt Target}),F_{\it
all}^{x}({\mathcal{G}}))({\mathcal{G}},\Box(\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\tt
Target}}))$.

The first claim of the lemma can be proven using transfinite induction on $i$
to show that it holds for each state $s\in{\mathcal{R}\,\,\\!\\!}_{i}$. The
second claim follows from Lemma 3 and Lemma 1.

##  4 Parity Conditions

We describe a scheme for solving stochastic parity games with almost-sure
winning conditions on infinite graphs, under the conditions that the game has
a finite attractor (as defined in Section 2), and that the players are
restricted to finite-memory strategies.

By induction on $n$, we define two sequences of functions
${\mathcal{C}}_{0},{\mathcal{C}}_{1},\ldots$ and
${\mathcal{D}}_{0},{\mathcal{D}}_{1},\ldots$ s.t., for each $n\geq 0$ and game
${\mathcal{G}}$ of rank at most $n$, ${\mathcal{C}}_{n}({\mathcal{G}})$
characterizes the states from which Player $x$ is winning a.s., where
$x=n\bmod 2$, and ${\mathcal{D}}_{n}({\mathcal{G}})$ characterizes the set of
states from which Player $x$ is winning w.p.p.. The scheme for
${\mathcal{C}}_{n}$ is related to [27]; cf. the remark at the end of this
section. In both cases, we provide a memoryless strategy that is winning for
Player $x$; Player ${1-x}$ is always restricted to finite-memory.

For the base case, let ${\mathcal{C}}_{0}({\mathcal{G}}):=S$ and
${\mathcal{D}}_{0}({\mathcal{G}}):=S$ for any game ${\mathcal{G}}$ of rank 0.
Indeed, from any configuration Player 0 trivially wins a.s./w.p.p. because
there is only color 0.

For $n\geq 1$, let ${\mathcal{G}}$ be a game of rank $n$.
${\mathcal{C}}_{n}({\mathcal{G}})$ is defined with the help of two auxiliary
transfinite sequences $\\{{\mathcal{X}}_{i}\\}_{i\in\mathbb{O}}$ and
$\\{{\mathcal{Y}}_{i}\\}_{i\in\mathbb{O}}$. The construction ensures that
${\mathcal{X}}_{0}\subseteq{\mathcal{Y}}_{0}\subseteq{\mathcal{X}}_{1}\subseteq{\mathcal{Y}}_{1}\subseteq\cdots$,
and that the elements of ${\mathcal{X}}_{i},{\mathcal{Y}}_{i}$ are winning
w.p.p. for Player ${1-x}$. The construction alternates as follows. In the
inductive step, we have already constructed ${\mathcal{X}}_{j}$ and
${\mathcal{Y}}_{j}$ for all $j<i$. Our construction of ${\mathcal{X}}_{j}$ and
${\mathcal{Y}}_{j}$ is in three steps:

  1. 1.

${\mathcal{X}}_{i}$ is the set of states where Player ${1-x}$ can force the
run to visit $\bigcup_{j<i}{\mathcal{Y}}_{j}$ w.p.p..

  2. 2.

Find a set of states where Player ${1-x}$ wins w.p.p. in
${\mathcal{G}}\ominus{\mathcal{X}}_{i}$.

  3. 3.

Take ${\mathcal{Y}}_{i}$ to be the union of ${\mathcal{X}}_{j}$ and the set
constructed in step 2.

We next show how to find the winning states in
${\mathcal{G}}\ominus{\mathcal{X}}_{i}$ in step 2. We first compute the set of
states where Player $x$ can force the play in
${\mathcal{G}}\ominus{\mathcal{X}}_{i}$ to reach a state with color $n$
w.p.p.. We call this set ${\mathcal{Z}}_{i}$. The subgame
${\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i}$ does not
contain any states of color $n$. Therefore, this game can be completely
solved, using the already constructed function
${\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})$.
We will prove that the states where Player ${1-x}$ wins w.p.p. in
${\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i}$ are winning
w.p.p. also in ${\mathcal{G}}$. We thus take ${\mathcal{Y}}_{i}$ as the union
of ${\mathcal{X}}_{i}$ and
${\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})$.
We define the sequences formally:

$\displaystyle\begin{array}[]{rl}{\mathcal{X}}_{i}&:={\it
Force}^{1-x}({\mathcal{G}},{\textstyle\bigcup_{j<i}{\mathcal{Y}}_{j}}),\\\
{\mathcal{Z}}_{i}&:={\it
Force}^{x}({\mathcal{G}}\ominus{\mathcal{X}}_{i},[\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{X}}}_{i}]^{{\tt
Col}=n}),\\\
{\mathcal{Y}}_{i}&:={\mathcal{X}}_{i}\cup{\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i}),\end{array}\qquad\qquad{\mathcal{C}}_{n}({\mathcal{G}}):=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{\textstyle(\bigcup_{i\in\mathbb{O}}{\mathcal{X}}_{i})}.$

Notice that the subgames ${\mathcal{G}}\ominus{\mathcal{X}}_{i}$ and
${\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i}$ are well-
defined since (by Lemma 3)
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{X}}}_{i}$ is closable
in ${\mathcal{G}}$, and
$\stackrel{{{}_{{\mathcal{G}}\ominus{\mathcal{X}}_{i}}}}{{{}_{\neg}}}{{\mathcal{Z}}}_{i}$
is closable in ${\mathcal{G}}\ominus{\mathcal{X}}_{i}$.

We now construct ${\mathcal{D}}_{n}({\mathcal{G}})$. Assume that we can
construct ${\mathcal{C}}_{n}({\mathcal{G}})$. We will define the transfinite
sequence $\\{{{\mathcal{U}}}_{i}\\}_{i\in\mathbb{O}}$ and the auxiliary
transfinite sequence $\\{{{\mathcal{V}}}_{i}\\}_{i\in\mathbb{O}}$. We again
precede the formal definition with an informal explanation of the idea. The
construction ensures that
${\mathcal{U}}_{0}\subseteq{\mathcal{V}}_{0}\subseteq{\mathcal{U}}_{1}\subseteq{\mathcal{V}}_{1}\subseteq\cdots$,
and that all ${\mathcal{U}}_{i}$, ${\mathcal{V}}_{i}$ are winning w.p.p. for
Player $x$ in ${\mathcal{G}}$. The construction alternates in a similar manner
to the construction of ${\mathcal{C}}_{n}$. In the inductive step, we have
already constructed ${\mathcal{V}}_{j}$ for all $j<i$. We first compute the
set of states where Player $x$ can force the play to reach ${\mathcal{V}}_{j}$
w.p.p. for some $j<i$. We call this set ${\mathcal{U}}_{i}$. It is clear that
${\mathcal{U}}_{i}$ is winning w.p.p. for Player $x$ in ${\mathcal{G}}$, given
the induction hypothesis that all ${\mathcal{V}}_{j}$ are winning. Then, we
find a set of states where Player $x$ wins w.p.p. in
${\mathcal{G}}\ominus{\mathcal{U}}_{i}$. It is clear that
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$ is such a set. This
set is winning w.p.p. for Player $x$, because a play starting in
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$ either stays in
this set and Player $x$ wins with probability 1, or the play leaves
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$ and enters
${\mathcal{U}}_{i}$ which, as we already know, is winning w.p.p.. We thus take
${\mathcal{V}}_{i}$ as the union of ${\mathcal{U}}_{i}$ and
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$. We define the
sequences formally by

$\begin{array}[]{rl}{\mathcal{U}}_{i}&:={\it
Force}^{x}({\mathcal{G}},\textstyle{\bigcup_{j<i}{\mathcal{V}}_{j}}),\\\
{\mathcal{V}}_{i}&:={\mathcal{U}}_{i}\cup{\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i}),\end{array}\qquad\qquad{\mathcal{D}}_{n}({\mathcal{G}}):=\textstyle{\bigcup_{i\in\mathbb{O}}{\mathcal{U}}_{i}}.$

By the definitions, for $j<i$ we get
${\mathcal{Y}}_{j}\subseteq{\mathcal{X}}_{i}\subseteq{\mathcal{Y}}_{i}$ and
${\mathcal{V}}_{j}\subseteq{\mathcal{U}}_{i}\subseteq{\mathcal{V}}_{i}$. As in
Lemma 2, we can prove that these sequences converge.

###### Lemma 5

There are $\alpha,\beta\in\mathbb{O}$ such that (i)
${\mathcal{X}}_{\alpha}={\mathcal{Y}}_{\alpha}=\bigcup_{i\in\mathbb{O}}{\mathcal{Y}}_{i}$,
(ii)
${\mathcal{C}}_{n}({\mathcal{G}})=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{X}}}_{\alpha}$,
(iii)
${\mathcal{U}}_{\beta}={\mathcal{V}}_{\beta}=\bigcup_{i\in\mathbb{O}}{\mathcal{V}}_{i}$,
and (iv) ${\mathcal{D}}_{n}({\mathcal{G}})={\mathcal{U}}_{\beta}$.

The following lemma shows the correctness of the construction. Recall that we
assume that ${\mathcal{G}}$ is of rank $n$ and that it contains a finite
attractor. Let $x=n\bmod 2$.

###### Lemma 6

There are memoryless strategies $f^{x}_{c},f^{x}_{d},\in
F^{x}_{\emptyset}({\mathcal{G}})$ and $f^{1-x}_{c},f^{1-x}_{d}\in
F^{{1-x}}_{\emptyset}({\mathcal{G}})$ such that the following properties hold:
(i)
${\mathcal{C}}_{n}({\mathcal{G}})\;\subseteq\;W^{x}(f^{x}_{c},F^{{1-x}}_{\it
finite}({\mathcal{G}}))({\mathcal{G}},{\mbox{$x$-}{\it Parity}}^{=1})$.
(ii)
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{C}}_{n}({\mathcal{G}})}\;\subseteq\;W^{1-x}(f^{1-x}_{c},F^{x}_{\it
finite}({\mathcal{G}}))({\mathcal{G}},{\mbox{$(1-x)$-}{\it Parity}}^{>0})$.
(iii)
${\mathcal{D}}_{n}({\mathcal{G}})\;\subseteq\;W^{x}(f^{x}_{d},F^{{1-x}}_{\it
finite}({\mathcal{G}}))({\mathcal{G}},{\mbox{$x$-}{\it Parity}}^{>0})$.
(iv)
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{D}}_{n}({\mathcal{G}})}\;\subseteq\;W^{1-x}(f^{1-x}_{d},F^{x}_{\it
finite}({\mathcal{G}}))({\mathcal{G}},{\mbox{$(1-x)$-}{\it Parity}}^{=1})$.

###### Proof

Using induction on $n$, we define the strategies
$f^{x}_{c},f^{x}_{d},f^{1-x}_{c},f^{1-x}_{d}$, and prove that the strategies
are indeed winning.

####  $f^{x}_{c}$.

For $n\geq 1$, let $\alpha$ be as defined in Lemma 5. Let
$\overline{{\mathcal{X}}_{\alpha}}:=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{X}}_{\alpha}}$
and
$\overline{{\mathcal{Z}}_{\alpha}}:=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{Z}}_{\alpha}}$.
We know that
${\mathcal{C}}_{n}({\mathcal{G}})=\overline{{\mathcal{X}}_{\alpha}}$. For a
state $s\in{\mathcal{C}}_{n}({\mathcal{G}})$, we define $f^{x}_{c}(s)$
depending on the membership of $s$ in one of the following three partitions of
${\mathcal{C}}_{n}({\mathcal{G}})$: (1)
$\overline{{\mathcal{X}}_{\alpha}}\cap\overline{{\mathcal{Z}}_{\alpha}}$, (2)
$\overline{{\mathcal{X}}_{\alpha}}\cap[{\mathcal{Z}}_{\alpha}]^{{\tt Col}<n}$,
and (3) $\overline{{\mathcal{X}}_{\alpha}}\cap[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}=n}$.

  1. 1.

$s\in\overline{{\mathcal{X}}_{\alpha}}\cap\overline{{\mathcal{Z}}_{\alpha}}$.
Define
${\mathcal{G}}^{\prime}:={\mathcal{G}}\ominus{\mathcal{X}}_{\alpha}\ominus{\mathcal{Z}}_{\alpha}$.
From Lemma 5, we have that
${\mathcal{X}}_{\alpha+1}-{\mathcal{X}}_{\alpha}=\emptyset$. By the
construction of ${\mathcal{Y}}_{i}$ we have, for arbitrary $i$, that
${\mathcal{D}}^{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})={\mathcal{Y}}_{i}-{\mathcal{X}}_{i}$,
and by the construction of ${\mathcal{X}}_{i+1}$, we have that
${\mathcal{Y}}_{i}-{\mathcal{X}}_{i}\subseteq{\mathcal{X}}_{i+1}-{\mathcal{X}}_{i}$.
By combining these facts we obtain
${\mathcal{D}}^{n-1}({\mathcal{G}}^{\prime})\subseteq{\mathcal{X}}_{\alpha+1}-{\mathcal{X}}_{\alpha}=\emptyset$.
Since ${\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i}$ does not
contain any states of color $n$ (or higher), it follows by the induction
hypothesis that there is a memoryless strategy $f_{1}\in
F^{x}_{\emptyset}({\mathcal{G}}^{\prime})$ such that
$\stackrel{{{}_{{\mathcal{G}}^{\prime}}}}{{{}_{\neg}}}{{\mathcal{D}}_{n-1}({\mathcal{G}}^{\prime})}\;\subseteq\;W^{x}(f_{1},F^{{1-x}}_{\it
finite}({\mathcal{G}}^{\prime}))({\mathcal{G}}^{\prime},{\mbox{$x$-}{\it
Parity}}^{=1})$. We define $f^{x}_{c}(s):=f_{1}(s)$.

  2. 2.

$s\in\overline{{\mathcal{X}}_{\alpha}}\cap[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}<n}$. Define $f^{x}_{c}(s):={\it
force}^{x}({\mathcal{G}}\ominus{\mathcal{X}}_{\alpha},[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}=n})(s)$.

  3. 3.

$s\in\overline{{\mathcal{X}}_{\alpha}}\cap[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}=n}$. By Lemma 3 we know that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\cap\overline{{\mathcal{X}}_{\alpha}}\neq\emptyset$.
Define $f^{x}_{c}(s):={\it select}({\it
Post}_{{\mathcal{G}}}\left(s\right)\cap\overline{{\mathcal{X}}_{\alpha}})$.

Let $f^{1-x}\in F^{{1-x}}_{\it finite}({\mathcal{G}})$ be a finite-memory
strategy for Player ${1-x}$. We show that
${\cal P}_{{\mathcal{G}},s,f^{x}_{c},f^{1-x}}(\mbox{$x$-}{\it Parity})=1$ for
any state $s\in{\mathcal{C}}_{n}({\mathcal{G}})$. First, we show that, any run
$s_{0}s_{1}\cdots\in{\it Runs}({\mathcal{G}},s,f^{x}_{c},f^{1-x})$ will always
stay inside $\overline{{\mathcal{X}}_{\alpha}}$, i.e.,
$s_{i}\in\overline{{\mathcal{X}}_{\alpha}}$ for all $i\geq 0$. We use
induction on $i$. The base case follows from
$s_{0}=s\in\overline{{\mathcal{X}}_{\alpha}}$. For the induction step, we
assume that $s_{i}\in\overline{{\mathcal{X}}_{\alpha}}$, and show that
$s_{i+1}\in\overline{{\mathcal{X}}_{\alpha}}$. We consider the following
cases:

  * •

$s_{i}\in[\overline{{\mathcal{X}}_{\alpha}}]^{1-x}\cup[\overline{{\mathcal{X}}_{\alpha}}]^{R}$.
The result follows since $\overline{{\mathcal{X}}_{\alpha}}$ is a
(${1-x}$)-trap in ${\mathcal{G}}$ (by Lemma 3).

  * •

$s_{i}\in[\overline{{\mathcal{X}}_{\alpha}}\cap\overline{{\mathcal{Z}}_{\alpha}}]^{x}$.
We know that $s_{i+1}=f_{1}(s_{i})$. Since $f_{1}\in
F^{x}_{\emptyset}({\mathcal{G}}\ominus{\mathcal{X}}_{\alpha}\ominus{\mathcal{Z}}_{\alpha})$
it follows that
$s_{i+1}\in\overline{{\mathcal{X}}_{\alpha}}\cap\overline{{\mathcal{Z}}_{\alpha}}$
and in particular $s_{i+1}\in\overline{{\mathcal{X}}_{\alpha}}$.

  * •

$s_{i}\in[\overline{{\mathcal{X}}_{\alpha}}\cap[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}<n}]^{x}$. We know that $s_{i+1}={\it
force}^{x}({\mathcal{G}}\ominus{\mathcal{X}}_{\alpha},[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}=n})(s_{i})$. The result follows by the fact that ${\it
force}^{x}({\mathcal{G}}\ominus{\mathcal{X}}_{\alpha},[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}=n})$ is a strategy in ${\mathcal{G}}\ominus{\mathcal{X}}_{\alpha}$.

  * •

$s_{i}\in[\overline{{\mathcal{X}}_{\alpha}}\cap[{\mathcal{Z}}_{\alpha}]^{{\tt
Col}=n}]^{x}$. We have $s_{i+1}\in{\it
Post}_{{\mathcal{G}}}\left(s_{i}\right)\cap\overline{{\mathcal{X}}_{\alpha}}$
and in particular $s_{i+1}\in\overline{{\mathcal{X}}_{\alpha}}$.

Let us again consider a run $\rho\in{\it
Runs}({\mathcal{G}},s,f^{x},f^{1-x})$. We show that $\rho$ is a.s. winning for
Player $x$ with respect to $\mbox{$x$-}{\it Parity}$ in ${\mathcal{G}}$. Let
$f^{1-x}$ be induced by a memory structure $\mathcal{M}=(M,m_{0},\tau,\mu)$.
Let ${\mathcal{T}}$ be the transition system induced by ${\mathcal{G}}$,
$f^{x}$, and $f^{1-x}$. As explained in Section 2, $\rho$ will a.s. visit a
configuration $(s_{A},m)\in B$ for some BSCC $B$ in ${\mathcal{T}}$. This
implies that each state that occurs in $B$ will a.s. be visited infinitely
often by $\rho$. There are two possible cases: (i) There is a configuration
$(s_{B},m)\in B$ with ${\tt Col}(s_{B})=n$. Since each state in
${\mathcal{G}}$ has color at most $n$, Player $x$ will a.s. win. (ii) There is
no configuration $(s_{B},m)\in B$ with ${\tt Col}(s_{B})=n$. This implies that
$\\{{s_{B}}|\;{(s_{B},m)\in B}\\}\subseteq\overline{{\mathcal{Z}}}$, and hence
Player $x$ uses the strategy $f_{1}$ to win the game.

####  $f^{1-x}_{c}$.

We define a strategy $f^{1-x}_{c}$ such that
${\mathcal{X}}_{i}\subseteq{\mathcal{Y}}_{i}\subseteq
W^{1-x}(f^{1-x}_{c},F^{x}_{\it
finite}({\mathcal{G}}))({\mathcal{G}},{\mbox{$(1-x)$-}{\it Parity}}^{>0})$ for
all $i$. The result follows then from the definition of
${\mathcal{C}}_{n}({\mathcal{G}})$. The inclusion
${\mathcal{X}}_{i}\subseteq{\mathcal{Y}}_{i}$ holds by the definition of
${\mathcal{Y}}_{i}$. For any state
$s\in\overline{{\mathcal{C}}_{n}({\mathcal{G}})}$, we define $f^{1-x}_{c}(s)$
as follows. Let $\beta$ be the smallest ordinal such that
$s\in{\mathcal{Y}}_{\beta}$. Such a $\beta$ exists by the well-ordering of
ordinals and since
$\overline{{\mathcal{C}}_{n}({\mathcal{G}})}=\bigcup_{i\in\mathbb{O}}{\mathcal{X}}_{i}=\bigcup_{i\in\mathbb{O}}{\mathcal{Y}}_{i}$.
Now there are two cases:

  * •

$s\in{\mathcal{X}}_{\beta}-\bigcup_{j<\beta}{\mathcal{Y}}_{j}$. Define
$f^{1-x}_{c}(s):=f_{1}(s):={\it
force}^{1-x}({\mathcal{G}},\bigcup_{j<\beta}{\mathcal{Y}}_{j})(s)$.

  * •

$s\in{\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{\beta}\ominus{\mathcal{Z}}_{\beta})$.
By the induction hypothesis (on $n$), there is a memoryless strategy $f_{2}\in
F^{{1-x}}_{\emptyset}({\mathcal{G}})$ of Player ${1-x}$ such that $s\in
W^{1-x}(f_{2},F^{x}_{\it
finite}({\mathcal{G}}\ominus{\mathcal{X}}_{\beta}\ominus{\mathcal{Z}}_{\beta}))({\mathcal{G}}\ominus{\mathcal{X}}_{\beta}\ominus{\mathcal{Z}}_{\beta},{\mbox{$(1-x)$-}{\it
Parity}}^{>0})$. Define $f^{1-x}_{c}(s):=f_{2}(s)$.

Let $f^{x}\in F^{x}_{\it finite}({\mathcal{G}})$ be an arbitrary finite-memory
strategy for Player $x$. We now use induction on $i$ to show that ${\cal
P}_{{\mathcal{G}},s,f^{1-x}_{c},f^{x}}(\mbox{$(1-x)$-}{\it Parity})>0$ for any
state $s\in{\mathcal{Y}}_{i}$. There are three cases:

  1. 1.

If $s\in\bigcup_{j<i}{\mathcal{Y}}_{j}$ then the result follows by the
induction hypothesis (on $i$).

  2. 2.

If $s\in{\mathcal{X}}_{i}-\bigcup_{j<i}{\mathcal{Y}}_{j}$ then we know that
Player ${1-x}$, can use $f_{1}$ to force the game to
$\bigcup_{j<i}{\mathcal{Y}}_{j}$ from which she wins w.p.p..

  3. 3.

If
$s\in{\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})$
then Player ${1-x}$ uses $f_{2}$. There are now two sub-cases: either (i)
there is a run from $s$ consistent with $f^{x}$ and $f^{1-x}_{c}$ that reaches
${\mathcal{X}}_{i}$; or (ii) there is no such run. In sub-case (i), the run
reaches ${\mathcal{X}}_{i}$ w.p.p. and then by cases 1 and 2 Player ${1-x}$
wins w.p.p.. In sub-case (ii), any run stays forever outside
${\mathcal{X}}_{i}$. So the game is in effect played on
${\mathcal{G}}\ominus{\mathcal{X}}_{i}$. Notice then that any run from $s$
that is consistent with $f^{x}$ and $f^{1-x}_{c}$ stays forever in
${\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i}$. The reason is
that (by Lemma 3)
$\stackrel{{{}_{{\mathcal{G}}\ominus{\mathcal{X}}_{i}}}}{{{}_{\neg}}}{{\mathcal{Z}}}_{i}$
is an $x$-trap in ${\mathcal{G}}\ominus{\mathcal{X}}_{i}$. Since any run
remains inside
${\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i}$, Player
${1-x}$ wins w.p.p. wrt. $\mbox{$(1-x)$-}{\it Parity}$ using $f_{2}$.

####  $f^{x}_{d}$.

For any state $s$, let $\beta$ be the smallest ordinal such that
$s\in{\mathcal{Y}}_{\beta}$. We define $f^{x}_{d}(s)$ by two cases:

  * •

$s\in{\mathcal{U}}_{\beta}-\bigcup_{j<\beta}{\mathcal{V}}_{j}$. Define
$f^{x}_{d}(s):=f_{1}(s):={\it
force}^{x}({\mathcal{G}},\bigcup_{j<\beta}{\mathcal{V}}_{j})(s)$.

  * •

$s\in{\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{\beta})$. By the
induction hypothesis (on $n$), Player $x$ has a winning memoryless strategy
$f_{2}$ inside ${\mathcal{G}}\ominus{\mathcal{U}}_{i}$. Define
$f^{x}_{d}(s):=f_{2}(s)$.

Let $f^{1-x}\in F_{\it all}^{{1-x}}({\mathcal{G}})$ be an arbitrary strategy
for Player ${1-x}$. We now use induction on $i$ to show that ${\cal
P}_{{\mathcal{G}},s,f^{x}_{d},f^{1-x}}(\mbox{$x$-}{\it Parity})>0$ for any
state $s\in{\mathcal{V}}_{i}$. There are three cases:

  1. 1.

If $s\in\bigcup_{j<i}{\mathcal{V}}_{j}$ then the result follows by the
induction hypothesis (on $i$).

  2. 2.

If $s\in{\mathcal{U}}_{i}-\bigcup_{j<i}{\mathcal{V}}_{j}$ then we know that
Player $x$ can use $f_{1}$ to force the game to
$\bigcup_{j<i}{\mathcal{V}}_{j}$ from which she wins w.p.p. by the previous
case.

  3. 3.

If $s\in{\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$ then Player
$x$ uses $f_{2}$. There are now two sub-cases: either (i) there is a run from
$s$ consistent with $f^{x}_{d}$ and $f^{1-x}$ that reaches
${\mathcal{U}}_{i}$; or (ii) there is no such run. In sub-case (i), the run
reaches ${\mathcal{U}}_{i}$ w.p.p. and then by cases 1 and 2 Player $x$ wins
w.p.p.. In sub-case (ii), any run stays forever outside ${\mathcal{U}}_{i}$.
Hence, Player $x$ wins a.s. wrt. $\mbox{$x$-}{\it Parity}$ using $f_{2}$.

####  $f^{1-x}_{d}$.

By the definition of ${\mathcal{U}}_{i}$ we know that
$\bigcup_{j<i}{\mathcal{V}}_{j}\subseteq{\mathcal{U}}_{i}$, and by the
definition of ${\mathcal{V}}_{i}$ we know that
${\mathcal{U}}_{i}\subseteq{\mathcal{V}}_{i}$. Thus,
${\mathcal{U}}_{0}\subseteq{\mathcal{V}}_{0}\subseteq{\mathcal{U}}_{1}\subseteq{\mathcal{V}}_{1}\subseteq\cdots$,
and hence there is an $\alpha\in\mathbb{O}$ such that
${\mathcal{U}}_{i}={\mathcal{V}}_{i}={\mathcal{U}}_{\alpha}$ for all
$i\geq\alpha$. This means that
${\mathcal{D}}_{n}({\mathcal{G}})={\mathcal{U}}_{\alpha}$ and hence by Lemma 3
we know that
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{D}}}_{n}({\mathcal{G}})$
is an $x$-trap. Furthermore, since
${\mathcal{V}}_{\alpha}={\mathcal{U}}_{\alpha}\cup{\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{\alpha})$,
where the union is disjoint, it follows that
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{\alpha})=\emptyset$ and
hence, by the induction hypothesis, Player ${1-x}$ has a memoryless strategy
$f\in F^{{1-x}}_{\emptyset}({\mathcal{G}})$ that is winning w.p.p. against all
finite memory strategies $f^{x}\in F^{x}_{\it finite}({\mathcal{G}})$ on all
states in
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{U}}}_{\alpha}=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{D}}}_{n}({\mathcal{G}})$.
Below, we show that $f$ indeed allows Player ${1-x}$ to win almost surely.

Fix a finite-memory strategy $f^{x}\in F^{x}_{\it finite}({\mathcal{G}})$. Let
$f^{x}$ be induced by a memory structure $\mathcal{M}=(M,m_{0},\tau,\mu)$.
Consider a run $\rho\in{\it Runs}({\mathcal{G}},s,f,f^{x})$. Then, $\rho$ will
surely stay inside ${\mathcal{G}}\ominus{\mathcal{U}}_{\alpha}$. The reason is
that $\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{U}}}_{\alpha}$ is
a trap for Player $x$ by Lemma 3, and that $f$ is a strategy defined inside
${\mathcal{G}}\ominus{\mathcal{U}}_{\alpha}$. Let ${\mathcal{T}}$ be the
transition system induced by ${\mathcal{G}}$, $f^{x}$, and $f$. As explained
in Section 2, $\rho$ will a.s. visit a configuration $(s_{A},m)\in B$ for some
BSCC $B$ in ${\mathcal{T}}$. This implies that each configuration in $B$ will
a.s. be visited infinitely often by $\rho$. Let $n$ be the maximal color
occurring among the states of $B$. Then, either (i) $n\bmod 2=x$ in which case
all states inside $B$ are almost sure losing for Player ${1-x}$; or (ii)
$n\bmod 2=1-x$ in which case all states inside $B$ are almost sure winning for
Player ${1-x}$. The result follows from the fact that case (i) gives a
contradiction since all states in
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{U}}}_{\alpha}=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{D}}}_{n}({\mathcal{G}})$
(including those in $B$) are winning for Player ${1-x}$ w.p.p.. Define
$f^{1-x}_{d}(s):=f(s)$.

The following theorem follows immediately from the previous lemmas.

###### Theorem 4.1

Stochastic parity games with almost sure winning conditions on infinite graphs
are memoryless determined, provided there exists a finite attractor and the
players are restricted to finite-memory strategies.

#### Remark.

The scheme for ${\mathcal{C}}_{n}$ is adapted from the well-known scheme for
non-stochastic games in [27]; in fact, the constructions are equivalent in the
case that no probabilistic states are present. Our contribution _to the
scheme_ is: (1) ${\mathcal{C}}_{n}$ is a non-trivial extension of the scheme
in [27] to handle probabilistic states; (2) we introduce the alternation
between ${\mathcal{C}}_{n}$ and ${\mathcal{D}}_{n}$; (3) the construction of
${\mathcal{D}}_{n}$ is new and has no counterpart in the non-stochastic case
of [27].

##  5 Lossy Channel Systems

A _lossy channel system (LCS)_ [6] is a finite-state machine equipped with a
finite number of unbounded fifo channels (queues). The system is _lossy_ in
the sense that, before and after a transition, an arbitrary number of messages
may be lost from the channels. We consider _stochastic game-LCS (SG-LCS)_ :
each individual message is lost independently with probability $\lambda$ in
every step, where $\lambda>0$ is a parameter of the system. The set of states
is partitioned into states belonging to Player $0$ and $1$. The player who
owns the current control-state chooses an enabled outgoing transition.
Formally, a SG-LCS of rank $n$ is a tuple ${\mathcal{L}}=({\tt S},{\tt
S}^{0},{\tt S}^{1},{\tt C},{\tt M},{\tt T},\lambda,{\tt Col})$ where ${\tt S}$
is a finite set of _control-states_ partitioned into states ${\tt S}^{0},{\tt
S}^{1}$ of Player $0$ and $1$; ${\tt C}$ is a finite set of _channels_ , ${\tt
M}$ is a finite set called the _message alphabet_ , ${\tt T}$ is a set of
_transitions_ , $0<\lambda<1$ is the _loss rate_ , and ${\tt
Col}:S\to\\{0,\dots,n\\}$ is the coloring function. Each transition ${\tt
t}\in{\tt T}$ is of the form ${\tt s}\overset{{{\tt
op}}}{{\longrightarrow}}{\tt s}^{\prime}$, where ${\tt s},{\tt
s}^{\prime}\in{\tt S}$ and ${\tt op}$ is one of the following three forms:
${\tt c}!{\tt m}$ (send message ${\tt m}\in{\tt M}$ in channel ${\tt c}\in{\tt
C}$), ${\tt c}?{\tt m}$ (receive message ${\tt m}$ from channel ${\tt c}$), or
${\tt nop}$ (do not modify the channels). The SG-LCS ${\mathcal{L}}$ induces a
game ${\mathcal{G}}=(S,S^{0},S^{1},S^{R},{\longrightarrow},P,{\tt Col})$,
where $S={\tt S}\times({\tt M}^{*})^{\tt C}\times\\{0,1\\}$. That is, each
state in the game consists of a control-state, a function that assigns a
finite word over the message alphabet to each channel, and one of the symbols
0 or 1. States where the last symbol is 0 are random: $S^{R}={\tt
S}\times({\tt M}^{*})^{\tt C}\times\\{0\\}$. The other states belong to a
player according to the control-state: ${S^{x}}={\tt S}^{x}\times({\tt
M}^{*})^{\tt C}\times\\{1\\}$. Transitions out of states of the form $s=({\tt
s},{\tt x},1)$ model transitions in ${\tt T}$ leaving state ${\tt s}$. On the
other hand, transitions leaving states of the form $s=({\tt s},{\tt x},0)$
model message losses. If $s=({\tt s},{\tt x},1),s^{\prime}=({\tt
s}^{\prime},{\tt x}^{\prime},0)\in S$, then there is a transition
$s{\longrightarrow}s^{\prime}$ in the game iff one of the following holds: (i)
${\tt s}\overset{{{\tt nop}}}{{\longrightarrow}}{\tt s}^{\prime}$ and ${\tt
x}={\tt x}^{\prime}$; (ii) ${\tt s}\overset{{{\tt c}!{\tt
m}}}{{\longrightarrow}}{\tt s}^{\prime}$, ${\tt x}^{\prime}({\tt c})={\tt
x}({\tt c}){\tt m}$, and for all ${\tt c}^{\prime}\in{\tt C}-\\{{\tt c}\\}$,
${\tt x}^{\prime}({\tt c}^{\prime})={\tt x}({\tt c}^{\prime})$; and (iii)
${\tt s}\overset{{{\tt c}?{\tt m}}}{{\longrightarrow}}{\tt s}^{\prime}$, ${\tt
x}({\tt c})={\tt m}{\tt x}^{\prime}({\tt c})$, and for all ${\tt
c}^{\prime}\in{\tt C}-\\{{\tt c}\\}$, ${\tt x}^{\prime}({\tt c}^{\prime})={\tt
x}({\tt c}^{\prime})$. Every state of the form $({\tt s},{\tt x},0)$ has at
least one successor, namely $({\tt s},{\tt x},1)$. If a state $({\tt s},{\tt
x},1)$ does not have successors according to the rules above, then we add a
transition $({\tt s},{\tt x},1){\longrightarrow}({\tt s},{\tt x},0)$, to
ensure that the induced game is sink-free. To model message losses, we
introduce the subword ordering $\preceq$ on words: $x\preceq y$ iff $x$ is a
word obtained by removing zero or more messages from arbitrary positions of
$y$. This is extended to channel states ${\tt x},{\tt x}^{\prime}:{\tt
C}\to{\tt M}^{*}$ by ${\tt x}\preceq{\tt x}^{\prime}$ iff ${\tt x}({\tt
c})\preceq{\tt x}^{\prime}({\tt c})$ for all channels ${\tt c}\in{\tt C}$, and
to game states $s=({\tt s},{\tt x},i),s^{\prime}=({\tt s}^{\prime},{\tt
x}^{\prime},i^{\prime})\in S$ by $s\preceq s^{\prime}$ iff ${\tt s}={\tt
s}^{\prime}$, ${\tt x}\preceq{\tt x}^{\prime}$, and $i=i^{\prime}$. For any
$s=({\tt s},{\tt x},0)$ and any ${\tt x}^{\prime}$ such that ${\tt
x}^{\prime}\preceq{\tt x}$, there is a transition $s{\longrightarrow}({\tt
s},{\tt x}^{\prime},1)$. The probability of random transitions is given by
$P(({\tt s},{\tt x},0),({\tt s},{\tt
x}^{\prime},1))=a\cdot\lambda^{b}\cdot(1-\lambda)^{c}$, where $a$ is the
number of ways to obtain ${\tt x}^{\prime}$ by losing messages in ${\tt x}$,
$b$ is the total number of messages needed to be lost in all channels in order
to obtain ${\tt x}^{\prime}$ from ${\tt x}$, and $c$ is the total number of
messages in all channels of ${\tt x}^{\prime}$ (see [1] for details). Finally,
for a state $s=({\tt s},{\tt x},i)$, we define ${\tt Col}(s):={\tt Col}({\tt
s})$. Notice that the graph of the game is bipartite, in the sense that a
state in $S^{R}$ has only transitions to states in $[S]^{0,1}$, and vice
versa.

In the qualitative parity game problem for SG-LCS, we want to characterize the
sets of configurations where Player $x$ can force the $x$-Parity condition to
hold a.s., for both players.

##  6 From Scheme to Algorithm

We transform the scheme of Section 4 into an algorithm for deciding the a.s.
parity game problem for SG-LCS. Consider an SG-LCS ${\mathcal{L}}=({\tt
S},{\tt S}^{0},{\tt S}^{1},{\tt C},{\tt M},{\tt T},\lambda,{\tt Col})$ and the
induced game ${\mathcal{G}}=(S,S^{0},S^{1},S^{R},{\longrightarrow},P,{\tt
Col})$ of some rank $n$. Furthermore, assume that the players are restricted
to finite-memory strategies. We show the following.

###### Theorem 6.1

The sets of winning states for Players $0$ and $1$ are effectively computable
as regular languages. Furthermore, from each state, memoryless strategies
suffice for the winning player.

We give the proof in several steps. First, we show that the game induced by an
SG-LCS contains a finite attractor (Lemma 7). Then, we show that the scheme in
Section 3 for computing winning states wrt. reachability objectives is
guaranteed to terminate (Lemma 9). Furthermore, we show that the scheme in
Section 4 for computing winning states wrt. a.s. parity objectives is
guaranteed to terminate (Lemma 15). Notice that Lemmas 9 and 15 imply that for
SG-LCS our transfinite constructions stabilize below $\omega$ (the first
infinite ordinal). Finally, we show that each step in the above two schemes
can be performed using standard operations on regular languages (Lemmas 16 and
17).

#### Finite attractor.

In [1] it was shown that any Markov chain induced by a Probabilistic LCS
contains a finite attractor. The proof can be carried over in a
straightforward manner to the current setting. More precisely, the finite
attractor is given by $A=({\tt
S}\times\boldsymbol{\varepsilon}\times\\{0,1\\})$ where
$\boldsymbol{\varepsilon}({\tt c})=\varepsilon$ for each ${\tt c}\in{\tt C}$.
In other words, $A$ is given by the set of states in which all channels are
empty. The proof relies on the observation that if the number of messages in
some channel is sufficiently large, it is more likely that the number of
messages decreases than that it increases in the next step. This gives the
following.

###### Lemma 7

${\mathcal{G}}$ contains a finite attractor.

#### Termination of Reachability Scheme.

For a set of states $Q\subseteq S$, we define the upward closure of $Q$ by
${Q}\\!\uparrow:=\\{{s}|\;{\exists s^{\prime}\in Q.\,s^{\prime}\preceq s}\\}$.
A set $U\subseteq Q\subseteq S$ is said to be $Q$-upward-closed (or $Q$-u.c.
for short) if $({U}\\!\uparrow)\cap Q=U$. We say that $U$ is upward closed if
it is $S$-u.c.

###### Lemma 8

If $Q_{0}\subseteq Q_{1}\subseteq\cdots$, and for all $i$ it holds that
$Q_{i}\subseteq Q$ and $Q_{i}$ is $Q$-u.c., then there is an
$\alpha\in\mathbb{N}$ such that $Q_{i}=Q_{\alpha}$ for all $i\geq\alpha$.

Now, we can show termination of the reachability scheme.

###### Lemma 9

There exists an $\alpha\in\mathbb{N}$ such that
${\mathcal{R}\,\,\\!\\!}_{i}={\mathcal{R}\,\,\\!\\!}_{\alpha}$ for all
$i\geq\alpha$.

###### Proof

First, we show that $[{\mathcal{R}\,\,\\!\\!}_{i}-{\tt Target}]^{R}$ is
$(\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\tt Target}})$-u.c. for all
$i\in\mathbb{N}$. We use induction on $i$. For $i=0$ the result is trivial
since ${\mathcal{R}\,\,\\!\\!}_{i}-{\tt Target}=\emptyset$. For $i>0$, suppose
that $s=({\tt s},{\tt x},0)\in[{\mathcal{R}\,\,\\!\\!}_{i}]^{R}-{\tt Target}$.
This means that $s{\longrightarrow}({\tt s},{\tt
x}^{\prime},1)\in{\mathcal{R}\,\,\\!\\!}_{i-1}$ for some ${\tt
x}^{\prime}\preceq{\tt x}$, and hence $s^{\prime}{\longrightarrow}({\tt
s},{\tt x}^{\prime},1)$ for all $s\preceq s^{\prime}$.

By Lemma 8, there is an $\alpha^{\prime}\in\mathbb{N}$ such that
$[{\mathcal{R}\,\,\\!\\!}_{i}]^{R}-{\tt
Target}=[{\mathcal{R}\,\,\\!\\!}_{\alpha^{\prime}}]^{R}-{\tt Target}$ for all
$i\geq\alpha^{\prime}$. Since ${\mathcal{R}\,\,\\!\\!}_{i}\supseteq{\tt
Target}$ for all $i\geq 0$ it follows that
$[{\mathcal{R}\,\,\\!\\!}_{i}]^{R}=[{\mathcal{R}\,\,\\!\\!}_{\alpha^{\prime}}]^{R}$
for all $i\geq\alpha^{\prime}$.

Since the graph of ${\mathcal{G}}$ is bipartite (as explained in Section 5),
we have $[{\it
Pre}_{{\mathcal{G}}}\left({\mathcal{R}\,\,\\!\\!}_{i}\right)]^{x}=[{\it
Pre}_{{\mathcal{G}}}\left([{\mathcal{R}\,\,\\!\\!}_{i}]^{R}\right)]^{x}$ and
$[\widetilde{{\it
Pre}_{{\mathcal{G}}}}\left({\mathcal{R}\,\,\\!\\!}_{i}\right)]^{1-x}=[\widetilde{{\it
Pre}_{{\mathcal{G}}}}\left([{\mathcal{R}\,\,\\!\\!}_{i}]^{R}\right)]^{1-x}$.
Since
$[{\mathcal{R}\,\,\\!\\!}_{i}]^{R}=[{\mathcal{R}\,\,\\!\\!}_{\alpha^{\prime}}]^{R}$
for all $i\geq\alpha^{\prime}$, we thus have $[{\it
Pre}_{{\mathcal{G}}}\left({\mathcal{R}\,\,\\!\\!}_{i}\right)]^{x}=[{\it
Pre}_{{\mathcal{G}}}\left([{\mathcal{R}\,\,\\!\\!}]^{R}_{\alpha^{\prime}}\right)]^{x}\subseteq{\mathcal{R}\,\,\\!\\!}_{\alpha^{\prime}+1}$
and $[\widetilde{{\it
Pre}_{{\mathcal{G}}}}\left({\mathcal{R}\,\,\\!\\!}_{i}\right)]^{1-x}=[\widetilde{{\it
Pre}_{{\mathcal{G}}}}\left([{\mathcal{R}\,\,\\!\\!}]^{R}_{\alpha^{\prime}}\right)]^{1-x}\subseteq{\mathcal{R}\,\,\\!\\!}_{\alpha^{\prime}+1}$.
It then follows that
${\mathcal{R}\,\,\\!\\!}_{i}={\mathcal{R}\,\,\\!\\!}_{\alpha}$ for all
$i\geq\alpha:=\alpha^{\prime}+1$.

#### Termination of Parity Scheme.

We use several auxiliary lemmas. The following lemma states that sink-freeness
is preserved by the reachability scheme.

###### Lemma 10

If ${\tt Target}$ is sink-free then ${\it Force}^{x}({\mathcal{G}},{\tt
Target})$ is sink-free.

###### Lemma 11

If ${\tt Target}$ is sink-free then $[{\it Force}^{x}({\mathcal{G}},{\tt
Target})]^{R}$ is upward closed.

###### Lemma 12

Let $\\{Q_{i}\\}_{i\in\mathbb{O}}$ and $\\{Q^{\prime}_{i}\\}_{i\in\mathbb{O}}$
be sequences of sets of states such that (i) Each $Q^{\prime}_{i}$ is sink-
free; (ii) $Q_{i}=Q^{\prime}_{i}\cup{\it
Force}^{x}({\mathcal{G}},\bigcup_{j<i}Q_{j})$; (iii) $Q^{\prime}_{i}$ and
${\it Force}^{x}({\mathcal{G}},\bigcup_{j<i}Q_{j})$ are disjoint for all $i$.
Then, there is an $\alpha\in\mathbb{N}$ such that $Q_{i}=Q_{\alpha}$ for all
$i\geq\alpha$.

To apply Lemma 12, we prove the following two lemmas.

###### Lemma 13

${\mathcal{C}}_{n}({\mathcal{G}})$ is a $({1-x})$-trap.

###### Proof

${\mathcal{C}}_{0}({\mathcal{G}})$ is trivially a $({1-x})$-trap. For $i\geq
1$, the result follows immediately from Lemma 5 and Lemma 3.

###### Lemma 14

For any game of rank $n$ both ${\mathcal{C}}_{n}({\mathcal{G}})$ and
${\mathcal{D}}_{n}({\mathcal{G}})$ are sink-free.

###### Proof

If $n=0$, then by definition
${\mathcal{C}}_{n}({\mathcal{G}})={\mathcal{D}}_{n}({\mathcal{G}})=S$, which
is sink-free by assumption. Next, assume $n\geq 1$. By Lemma 13 we know that
${\mathcal{C}}_{n}({\mathcal{G}})$ is a $({1-x})$-trap and hence also sink-
free. To prove the claim for ${\mathcal{D}}_{n}({\mathcal{G}})$, we use
induction on $i$ and prove that both ${\mathcal{U}}_{i}$ and
${\mathcal{V}}_{i}$ are sink-free. Assume ${\mathcal{U}}_{j}$ and
${\mathcal{V}}_{j}$ are sink-free for all $j<i$. Then
$\bigcup_{j<i}{\mathcal{V}}_{j}$ is sink-free, and hence ${\mathcal{U}}_{i}$
is sink-free by Lemma 10. Since
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$ and
${\mathcal{U}}_{i}$ are sink-free, it follows that ${\mathcal{V}}_{i}$ is
sink-free.

Now, we apply Lemma 12 to prove that the sequences
$\\{{\mathcal{X}}_{i}\\}_{i\in\mathbb{O}}$ and
$\\{{\mathcal{U}}_{i}\\}_{i\in\mathbb{O}}$ terminate. First, by Lemma 14 we
know that
${\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})$
is sink-free. We know that ${\mathcal{X}}_{i}$ and
${\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})$
are disjoint since
${\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})\subseteq\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{({\mathcal{X}}_{i}\cup{\mathcal{Z}}_{i})}$.
Hence, we can apply Lemma 12 with $Q_{i}={\mathcal{Y}}_{i}$,
$Q^{\prime}_{i}={\mathcal{D}}_{n-1}({\mathcal{G}}\ominus{\mathcal{X}}_{i}\ominus{\mathcal{Z}}_{i})$,
and conclude that $\\{{\mathcal{Y}}_{i}\\}_{i\in\mathbb{O}}$ terminates, and
hence $\\{{\mathcal{X}}_{i}\\}_{i\in\mathbb{O}}$ terminates. Second, by Lemma
14 we know that ${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$ is
sink-free. Since
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})\subseteq\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{U}}_{i}}$,
we know that ${\mathcal{U}}_{i}$ and
${\mathcal{C}}_{n}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$ are disjoint.
Hence, we can apply Lemma 12 with $Q_{i}={\mathcal{V}}_{i}$,
$Q^{\prime}_{i}={\mathcal{C}}_{n-1}({\mathcal{G}}\ominus{\mathcal{U}}_{i})$,
and conclude that $\\{{\mathcal{V}}_{i}\\}_{i\in\mathbb{O}}$ terminates, and
hence $\\{{\mathcal{U}}_{i}\\}_{i\in\mathbb{O}}$ terminates. This gives the
following lemma.

###### Lemma 15

There is an $\alpha\in\mathbb{N}$ such that
${\mathcal{X}}_{i}={\mathcal{X}}_{\alpha}$ for all $i\geq\alpha$. There is a
$\beta\in\mathbb{N}$ such that ${\mathcal{U}}_{i}={\mathcal{U}}_{\beta}$ for
all $i\geq\beta$.

#### Computability.

For a given regular set ${\mathcal{R}\,\,\\!\\!}$, the set ${\it
Pre}_{{\mathcal{G}}}\left({\mathcal{R}\,\,\\!\\!}\right)$ is effectively
regular [2], i.e., computable as a regular language. The following lemma then
follows from the fact that the other operations used in computing ${\it
Force}^{x}({\mathcal{G}},{\tt Target})$ are those of set complement and union,
which are effective for regular languages.

###### Lemma 16

If ${\tt Target}$ is regular then ${\it Force}^{x}({\mathcal{G}},{\tt
Target})$ is effectively regular.

###### Lemma 17

For each $n$, both ${\mathcal{C}}_{n}({\mathcal{G}})$ and
${\mathcal{D}}_{n}({\mathcal{G}})$ are effectively regular.

###### Proof

The set $S$ is regular, and hence
${\mathcal{C}}_{0}({\mathcal{G}})={\mathcal{D}}_{0}({\mathcal{G}})=S$ is
effectively regular. The result for $n>0$ follows from Lemma 16 and from the
fact that the rest of the operations used to build
${\mathcal{C}}_{n}({\mathcal{G}})$ and ${\mathcal{D}}_{n}({\mathcal{G}})$ are
those of set complement and union.

#### Remark.

Although we use Higman’s lemma for showing termination of our fixpoint
computations, our proof differs significantly from the standard ones for well
quasi-ordered transition systems [3]. For instance, the generated sets are in
general not upward closed wrt. the underlying ordering $\preceq$. Therefore,
we need to use the notion of $Q$-upward closedness for a set of states $Q$.
More importantly, we need to define new (and much more involved) sufficient
conditions for the termination of the computations (Lemma 12), and to show
that these conditions are satisfied (Lemma 14).

##  7 Conclusions and Discussion

We have presented a scheme for solving stochastic games with a.s. parity
winning conditions under the two requirements that (i) the game contains a
finite attractor and (ii) both players are restricted to finite-memory
strategies. We have shown that this class of games is memoryless determined.
The method is instantiated to prove decidability of a.s. parity games induced
by lossy channel systems. The two above requirements are both necessary for
our method. To see why our scheme fails if the game lacks a finite attractor,
consider the game in Figure 1 (a) (a variant of the Gambler’s ruin problem).

$s_{0}$$s_{1}$$s_{2}$$s_{3}$$\cdots$(a)$0.3$$0.7$$0.3$$0.7$$0.3$$0.7$$0.3$

$s_{0}$$s_{2}$$s_{1}$$s_{3}$$s_{4}$$\cdots$(b)$1$$0.5$$0.5$$0.5$$0.5$$0.5$$0.5$

Figure 1:  (a) Finite attractor requirement. (b) Finite strategy requirement.

All states are random, i.e., $S^{0}=S^{1}=\emptyset$, and ${\tt Col}(s_{0})=1$
and ${\tt Col}(s_{i})=0$ when $i>0$. The probability to go right from any
state is $0.7$ and the probability to go left (or to make a self-loop in
$s_{0}$) is $0.3$. This game does not have any finite attractor. It can be
shown that the probability to reach $s_{0}$ infinitely often is 0 for all
initial states. However, our construction will classify all states as winning
for player 1. More precisely, the construction of
${\mathcal{C}}_{1}({\mathcal{G}})$ converges after one iteration with
${\mathcal{Z}}_{i}=S,{\mathcal{X}}_{i}=\emptyset$ for all $i$ and
${\mathcal{C}}_{1}({\mathcal{G}})=S$. Intuitively, the problem is that even if
the force-set of $\\{s_{0}\\}$ (which is the entire set of states) is visited
infinitely many times, the probability of visiting $\\{s_{0}\\}$ infinitely
often is still zero, since the probability of returning to $\\{s_{0}\\}$ gets
smaller and smaller. Such behavior is impossible in a game graph that contains
a finite attractor.

We restrict both players to finite-memory strategies. This is a different
problem from when arbitrary strategies are allowed (not a sub-problem). In
fact, it was shown in [8] that for arbitrary strategies, the problem is
undecidable. Figure 1 (b) gives an example of a game graph where the two
problems yield different results (see also [8]). Player 1 controls $s_{0}$,
whereas $s_{1},s_{2},\dots$ are random; ${\tt Col}(s_{0})=0,{\tt
Col}(s_{1})=2,{\tt Col}(s_{i})=1$ if $i\geq 2$. The transition probabilities
are $P(s_{1},s_{1})=1$ and $P(s_{n},s_{n-1})=P(s_{n},s_{0})=\frac{1}{2}$ when
$n\geq 2$. Player 1 wants to ensure that the highest color that is seen
infinitely often is odd, and thus wants to avoid state $s_{1}$ (which has
color 2). If the players can use arbitrary strategies, then although player 1
cannot win with probability 1, he can win with a probability arbitrarily close
to 1 using an infinite-memory strategy: player 1 goes from $s_{0}$ to
$s_{k+i}$ when the play visits $s_{0}$ for the $i$’th time. Then player 1 wins
with probability $\prod_{i=1}^{\infty}(1-2^{-k-i+1})$, which can be made
arbitrarily close to $1$ for sufficiently large $k$. In particular, player 0
does not win a.s. in this case. On the other hand, if the players are limited
to finite-memory strategies, then no matter what strategy player 1 uses, the
play visits $s_{1}$ infinitely often with probability 1, so player 0 wins
almost surely; this is also what our algorithm computes.

As future work, we will consider extending our framework to (fragments of)
probabilistic extensions of other models such as Petri nets and noisy Turing
machines [5].

## References

  * [1] P. A. Abdulla, N. Bertrand, A. Rabinovich, and Ph. Schnoebelen.  Verification of probabilistic systems with faulty communication.  Information and Computation, 202(2):105–228, 2005.
  * [2] P. A. Abdulla, A. Bouajjani, and J. d’Orso.  Deciding monotonic games.  In CSL, volume 2803 of LNCS, pages 1–14, 2003.
  * [3] P. A. Abdulla, K. Čerāns, B. Jonsson, and Y.-K. Tsay.  Algorithmic analysis of programs with well quasi-ordered domains.  Information and Computation, 160:109–127, 2000.
  * [4] P. A. Abdulla, N. B. Henda, L. de Alfaro, R. Mayr, and S. Sandberg.  Stochastic games with lossy channels.  In FOSSACS, volume 4962 of LNCS, 2008.
  * [5] P. A. Abdulla, N. B. Henda, and R. Mayr.  Decisive Markov chains.  Logical Methods in Computer Science, 3, 2007.
  * [6] P. A. Abdulla and B. Jonsson.  Verifying programs with unreliable channels.  In LICS, pages 160–170, 1993.
  * [7] Parosh Aziz Abdulla and Alexander Rabinovich.  Verification of probabilistic systems with faulty communication.  In FOSSACS, volume 2620 of LNCS, pages 39–53, 2003.
  * [8] C. Baier, N. Bertrand, and Ph. Schnoebelen.  Verifying nondeterministic probabilistic channel systems against $\omega$-regular linear-time properties.  ACM Trans. on Comp. Logic, 9, 2007.
  * [9] N. Bertrand and Ph. Schnoebelen.  Model checking lossy channels systems is probably decidable.  In FOSSACS, volume 2620 of LNCS, pages 120–135, 2003.
  * [10] N. Bertrand and Ph. Schnoebelen.  Solving stochastic büchi games on infinite arenas with a finite attractor.  In Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages (QAPl’13), Roma, Italy, March 2013.  To appear.
  * [11] P. Billingsley.  Probability and Measure.  Wiley, New York, NY, 1986.  Second Edition.
  * [12] D. Brand and P. Zafiropulo.  On communicating finite-state machines.  Journal of the ACM, 2(5):323–342, April 1983.
  * [13] K. Chatterjee, L. de Alfaro, and T. Henzinger.  Strategy improvement for concurrent reachability games.  In QEST, pages 291–300. IEEE Computer Society Press, 2006.
  * [14] K. Chatterjee, M. Jurdziński, and T. Henzinger.  Simple stochastic parity games.  In CSL, volume 2803 of LNCS, pages 100–113. Springer Verlag, 2003.
  * [15] E.M. Clarke, O. Grumberg, and D. Peled.  Model Checking.  MIT Press, Dec. 1999.
  * [16] A. Condon.  The complexity of stochastic games.  Information and Computation, 96(2):203–224, February 1992.
  * [17] L. de Alfaro and T. Henzinger.  Concurrent omega-regular games.  In LICS, pages 141–156, Washington - Brussels - Tokyo, June 2000\. IEEE.
  * [18] L. de Alfaro, T. Henzinger, and O. Kupferman.  Concurrent reachability games.  In FOCS, pages 564–575. IEEE Computer Society Press, 1998.
  * [19] K. Etessami, D. Wojtczak, and M. Yannakakis.  Recursive stochastic games with positive rewards.  In ICALP, volume 5125 of LNCS. Springer, 2008.
  * [20] K. Etessami and M. Yannakakis.  Recursive Markov decision processes and recursive stochastic games.  In ICALP, volume 3580 of LNCS, pages 891–903, 2005.
  * [21] K. Etessami and M. Yannakakis.  Recursive concurrent stochastic games.  LMCS, 4, 2008.
  * [22] G. Higman.  Ordering by divisibility in abstract algebras.  Proc. London Math. Soc. (3), 2(7):326–336, 1952.
  * [23] A. Rabinovich.  Quantitative analysis of probabilistic lossy channel systems.  In ICALP, volume 2719 of LNCS, pages 1008–1021, 2003.
  * [24] L. S. Shapley.  Stochastic games.  Proceedings of the National Academy of Sciences, 39(10):1095–1100, October 1953.
  * [25] M.Y. Vardi.  Automatic verification of probabilistic concurrent finite-state programs.  In FOCS, pages 327–338, 1985.
  * [26] K. Wang, N. Li, and Z. Jiang.  Queueing system with impatient customers: A review.  In IEEE International Conference on Service Operations and Logistics and Informatics (SOLI), pages 82–87. IEEE, 2010.
  * [27] W. Zielonka.  Infinite games on finitely coloured graphs with applications to automata on infinite trees.  TCS, 200:135–183, 1998.

##  Appendix 0.A Proofs of Lemmas

### Lemma 1

We define a memoryless strategy $f^{x}$ of Player $x$ that is surely winning
from any state $s\in Q$, i.e., $Q\subseteq V^{x}(f^{x},F_{\it
all}^{{1-x}}({\mathcal{G}}))({\mathcal{G}},\Box Q)$. For a state
$s\in[Q]^{x}$, we define $f^{x}(s)={\it select}({\it
Post}_{{\mathcal{G}}}\left(s\right)\cap Q)$. This is well-defined since $Q$ is
a $({1-x})$-trap. We can now show that any run that starts from a state $s\in
Q$ and that is consistent with $f^{x}$ will surely remain inside $Q$. Let
$f^{1-x}$ be any strategy of Player ${1-x}$, and let
$s_{0},s_{1},\ldots\in{\it Runs}({\mathcal{G}},s,f^{x},f^{1-x})$. We show, by
induction on $i$, that $s_{i}\in Q$ for all $i\geq 0$. The base case is clear
since $s_{0}=s\in Q$. For $i>1$, we consider three cases depending on $s_{i}$:

  * •

$s_{i}\in[S]^{x}$. By the induction hypothesis we know that $s_{i}\in Q$, and
hence by definition of $f^{x}$ we know that $s_{i+1}=f^{x}(s_{i})\in Q$.

  * •

$s_{i}\in[S]^{1-x}$. By the induction hypothesis we know that $s_{i}\in Q$,
and hence $s_{i+1}\in Q$ since $Q$ is a $({1-x})$-trap.

  * •

$s_{i}\in[S]^{R}$. By the induction hypothesis we know that $s_{i}\in Q$, and
hence $s_{i+1}\in Q$ since $Q$ is closable.

### Lemma 3

By Lemma 2 and the definition of ${\it Avoid}^{1-x}({\mathcal{G}},{\tt
Target})$ it follows that
${\it Avoid}^{1-x}({\mathcal{G}},{\tt
Target})=\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}_{\alpha}}$
and that
${\mathcal{R}\,\,\\!\\!}_{\alpha+1}\subseteq{\mathcal{R}\,\,\\!\\!}_{\alpha}$.
First, we show that
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}$
is sink-free as follows. For a state $s\in S$, we show that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\cap(\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}_{\alpha}})\neq\emptyset$.
There are three cases to consider.

  * •

$s\in[\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}]^{x}$.
Suppose that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\not\subseteq(\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha})$.
It follows that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\cap{\mathcal{R}\,\,\\!\\!}_{\alpha}\neq\emptyset$.
Hence,
$s\in{\mathcal{R}\,\,\\!\\!}_{\alpha+1}\subseteq{\mathcal{R}\,\,\\!\\!}_{\alpha}$
which is a contradiction. This means that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\subseteq\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}$.
Since $S$ is sink-free, we know that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\neq\emptyset$. Consequently, ${\it
Post}_{{\mathcal{G}}}\left(s\right)\cap\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}\neq\emptyset$.

  * •

$s\in[\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}]^{1-x}$.
Suppose that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\subseteq{\mathcal{R}\,\,\\!\\!}_{\alpha}$.
It follows that
$s\in{\mathcal{R}\,\,\\!\\!}_{\alpha+1}\subseteq{\mathcal{R}\,\,\\!\\!}_{\alpha}$
which is a contradiction. Hence, ${\it
Post}_{{\mathcal{G}}}\left(s\right)\cap\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}\neq\emptyset$.

  * •

$s\in[\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}]^{R}$.
The claim follows in similar manner to the case where
$s\in[{\mathcal{R}\,\,\\!\\!}_{\alpha}]^{x}$.

Second, when proving sink-freeness above, we showed that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\subseteq\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}$
for any
$s\in[\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}]^{R}$
which means that
$\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}$
is closable. Finally, when proving sink-freeness, we also showed that ${\it
Post}_{{\mathcal{G}}}\left(s\right)\subseteq\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}$
for any
$s\in[\stackrel{{{}_{{\mathcal{G}}}}}{{{}_{\neg}}}{{\mathcal{R}\,\,\\!\\!}}_{\alpha}]^{x}$
which completes the proof.

### Lemma 4

Let ${\mathcal{R}\,\,\\!\\!}={\it Force}^{x}({\mathcal{G}},{\tt Target})$. To
prove the first claim, we define a memoryless strategy $f^{x}$ of Player $x$
that is winning from any state $s\in{\mathcal{R}\,\,\\!\\!}$, i.e.,
${\mathcal{R}\,\,\\!\\!}\subseteq W^{x}(f^{x},F_{\it
all}^{{1-x}})({\mathcal{G}},\Diamond{\tt Target}^{>0})$. For any
$s\in[{\mathcal{R}\,\,\\!\\!}_{i+1}-{\mathcal{R}\,\,\\!\\!}_{i}]^{x}$ where
$i+1$ is a successor ordinal, we define $f^{x}(s):={\it select}({\it
Post}_{{\mathcal{G}}}\left(s\right)\cap{\mathcal{R}\,\,\\!\\!}_{i})$. We show
that $f^{x}$ is a winning strategy for Player $x$. Fix a strategy $f^{1-x}$
for Player ${1-x}$. We show that ${\cal
P}_{{\mathcal{G}},s,f^{x},f^{1-x}}(\Diamond{\tt Target})>0$. We prove the
claim using transfinite induction. If $s\in{\mathcal{R}\,\,\\!\\!}_{0}$ then
the claim follows trivially. If $s\in{\mathcal{R}\,\,\\!\\!}_{i+1}$ where
$i+1$ is a successor ordinal then either $s\in{\mathcal{R}\,\,\\!\\!}_{i}$ in
which case the claim holds by the induction hypothesis, or
$s\in{\mathcal{R}\,\,\\!\\!}_{i+1}-{\mathcal{R}\,\,\\!\\!}_{i}$. We consider
three cases:

  * •

$s\in[{\mathcal{R}\,\,\\!\\!}_{i+1}-{\mathcal{R}\,\,\\!\\!}_{i}]^{x}$. By
definition of $f^{x}$, we know that $f^{x}(s)=s^{\prime}$ for some
$s^{\prime}\in{\mathcal{R}\,\,\\!\\!}_{i}$. By the induction hypothesis we
know that ${\cal P}_{{\mathcal{G}},s^{\prime},f^{0},f^{1}}(\Diamond{\tt
Target})>0$ and hence ${\cal P}_{{\mathcal{G}},s,f^{0},f^{1}}(\Diamond{\tt
Target})>0$.

  * •

$s\in[{\mathcal{R}\,\,\\!\\!}_{i+1}-{\mathcal{R}\,\,\\!\\!}_{i}]^{1-x}$. Let
$f^{1-x}(s)=s^{\prime}$. By definition of ${\mathcal{R}\,\,\\!\\!}_{i+1}$ we
know that $s^{\prime}\in{\mathcal{R}\,\,\\!\\!}_{i}$. Then, the proof follows
as in the previous case.

  * •

$s\in[{\mathcal{R}\,\,\\!\\!}_{i+1}-{\mathcal{R}\,\,\\!\\!}_{i}]^{R}$. By
definition of ${\mathcal{R}\,\,\\!\\!}_{i+1}$ we know that there is a
$s^{\prime}\in{\mathcal{R}\,\,\\!\\!}_{i}$ such that $P(s,s^{\prime})>0$. By
the induction hypothesis, it follows that ${\cal
P}_{{\mathcal{G}},s,f^{0},f^{1}}(\Diamond{\tt Target})\geq{\cal
P}_{{\mathcal{G}},s^{\prime},f^{0},f^{1}}(\Diamond{\tt Target})\cdot
P(s,s^{\prime})>0$.

Finally, if $s\in{\mathcal{R}\,\,\\!\\!}_{i}$ where $i>0$ is a limit ordinal,
then we know that $s\in{\mathcal{R}\,\,\\!\\!}_{j}$ for some $j<i$. The claim
then follows by the induction hypothesis.

From Lemma 3 and Lemma 1 it follows that there is a strategy $f^{1-x}$ for
Player ${1-x}$ such that ${\it Avoid}^{x}({\mathcal{G}},{\tt Target})\subseteq
V^{1-x}(f^{1-x},F_{\it all}^{x})({\mathcal{G}},\Box({\it
Avoid}^{x}({\mathcal{G}},{\tt Target})))$. The second claim follows then from
the fact that ${\tt Target}\cap{\it Avoid}^{x}({\mathcal{G}},{\tt
Target})=\emptyset$.

### Lemma 8

By Higman’s lemma [22], there is a $\alpha\in\mathbb{N}$ such that
$Q_{i}\uparrow=Q_{\alpha}\uparrow$ for all $i\geq\alpha$. Hence,
$Q_{i}\uparrow\cap Q=Q_{\alpha}\uparrow\cap Q$ for all $i\geq\alpha$. Since
all $Q_{i}$ are $Q$-u.c., $Q_{i}\uparrow\cap Q=Q_{i}$ for all $i\geq\alpha$.
So $Q_{i}=Q_{\alpha}$ for all $i\geq\alpha$.

### Lemma 10

We prove by induction on $i$ that ${\mathcal{R}\,\,\\!\\!}_{i}$ is sink-free
for all ordinals $i\in\mathbb{O}$. If $i=0$, the claim holds by assumption. If
$i+1$ is a successor ordinal, then the claim follows from the definition of
${\mathcal{R}\,\,\\!\\!}_{i+1}$ (all new states in
${\mathcal{R}\,\,\\!\\!}_{i+1}$ have a successor in
${\mathcal{R}\,\,\\!\\!}_{i}$). If $i>0$ is a limit ordinal, then each state
in ${\mathcal{R}\,\,\\!\\!}_{i}$ belongs to some ${\mathcal{R}\,\,\\!\\!}_{j}$
with $j<i$ for which the claim holds by the induction hypothesis.

### Lemma 11

Take any $s\in[{\it Force}^{x}({\mathcal{G}},{\tt Target})]^{R}$ and take
$s^{\prime}\in S$ such that $s\preceq s^{\prime}$. By Lemma 10, $s$ has a
successor $s^{\prime\prime}\in{\it Force}^{x}({\mathcal{G}},{\tt Target})$.
Thus, $s^{\prime\prime}\in{\mathcal{R}\,\,\\!\\!}_{i}$ for some
$i\in\mathbb{O}$. Since ${\mathcal{G}}$ is induced by a SG-LCS, $s^{\prime}$
is a predecessor of every successor of $s$ (including $s^{\prime\prime}$).
Hence, $s^{\prime}\in{\mathcal{R}\,\,\\!\\!}_{i+1}$.

### Lemma 12

First, define $F_{i}:={\it Force}^{x}({\mathcal{G}},\bigcup_{j<i}Q_{j})$. We
perform the proof in several steps: (i) $F_{0}\subseteq Q_{0}\subseteq
F_{1}\subseteq Q_{1}\subseteq\cdots$. This follows from the fact that
$Q_{i}=Q^{\prime}_{i}\cup F_{i}$ and the definition of $F_{i}$. (ii) There is
an $\alpha\in\mathbb{N}$ such that $[F_{i}]^{R}=[F_{\alpha}]^{R}$ for all
$i\geq\alpha$. By Lemma 10 (and induction on $i$), each $F_{i}$ is sink-free
and hence by Lemma 11 each $[F_{i}]^{R}$ is upward closed. By Lemma 8 it
follows that there is a $\alpha\in\mathbb{N}$ such that
$[F_{i}]^{R}=[F_{\alpha}]^{R}$ for all $i\geq\alpha$. (iii)
$[Q_{i}]^{R}=[F_{i}]^{R}=[Q_{\alpha}]^{R}$ for all $i\geq\alpha$. This follows
from the previous two steps. (iv) $[Q^{\prime}_{i}]^{R}=\emptyset$ for all
$i\geq\alpha+1$. From the assumption that $Q_{i}$ is the disjoint union of
$Q^{\prime}_{i}$ and $F_{i}$, $Q^{\prime}_{i}=Q_{i}-F_{i}$. By the previous
step, this set is empty. (v) $Q^{\prime}_{i}=\emptyset$ for all
$i\geq\alpha+1$. Since the transition system generated by an SG-LCS is
bipartite with every second state in $S^{R}$, and since every member of a
sink-free set has a successor in the set itself, it follows that any nonempty
sink-free set contains both states in $S^{R}$ and states that belong to one of
the players $0$ or $1$. Since $Q^{\prime}_{i}$ is sink-free (by assumption)
but does not contain any states in $S^{R}$ (by the result in previous step),
$Q^{\prime}_{i}$ has to be empty. (vi) $Q_{i}=Q_{\alpha}$ for all
$i\geq\alpha$. By the previous step, we know that $Q_{i}={\it
Force}^{x}({\mathcal{G}},\bigcup_{j<i}Q_{j})$ for all $i\geq\alpha+1$. By the
definition of ${\it Force}^{x}$ it follows that $Q_{i}=Q_{\alpha}$ for all
$i\geq\alpha+1$.