# Stochastic Games with Disjunctions of Multiple Objectives††thanks: This work
was supported by the DFG RTG 2236 “UnRAVeL” (Winkler) and DFG projects
383882557 “SUV” and 427755713 “GOPro” (Weininger).

Tobias Winkler RWTH Aachen University, Germany<EMAIL_ADDRESS>aachen.de Technical University of Munich, Germany Maximilian Weininger
Technical University of Munich, Germany<EMAIL_ADDRESS>
###### Abstract

Stochastic games combine controllable and adversarial non-determinism with
stochastic behavior and are a common tool in control, verification and
synthesis of reactive systems facing uncertainty. Multi-objective stochastic
games are natural in situations where several—possibly conflicting—performance
criteria like time and energy consumption are relevant. Such _conjunctive_
combinations are the most studied multi-objective setting in the literature.
In this paper, we consider the dual _disjunctive_ problem. More concretely, we
study turn-based stochastic two-player games on graphs where the winning
condition is to guarantee at least one reachability or safety objective from a
given set of alternatives. We present a fine-grained overview of strategy and
computational complexity of such _disjunctive queries_ (DQs) and provide new
lower and upper bounds for several variants of the problem, significantly
extending previous works. We also propose a novel value iteration-style
algorithm for approximating the set of Pareto optimal thresholds for a given
DQ.

##  1 Introduction

Stochastic games (SG), e.g. [23, 38], combine controllable and adversarial
non-determinism with stochastic behavior. In their turn-based two-player
version, SGs are played on graphs where the vertices are called states, and
every state either belongs to one of the two players Eve and Adam, or is
controlled by a probabilistic environment. In each round, the player in
control of the state chooses an action—an edge of the graph—and the game
transitions to the successor state. In probabilistic states, the successor is
sampled according to a fixed observable distribution over the outgoing edges.
_Simple_ SGs [23] have just a single _reachability_ objective. A key question
is whether Eve can control her states such that a target is reached with at
least a certain probability, no matter the behavior of the opponent Adam.
Dually, Adam has a _safety objective_ in this setting: He should maximize the
chance of staying in the—from his point of view—safe region, i.e., avoiding
Eve’s target states.

_Multi-objective stochastic games_ [21] extend this by allowing Boolean
combinations of several different probability or expectation thresholds on
various objectives. Such games have been used to synthesize optimal
controllers in application scenarios where the system at hand is exposed to an
environment with both stochastic and non-deterministic aspects [7, 22, 28]. A
natural subclass of multi-objectives are _disjunctive queries_ (DQ) [21, 29]
where the player has to satisfy at least one alternative from a given set of
options.

In this paper, we study DQs with both reachability and safety options. More
specifically, given a game and a finite set of reachability and safety
objectives, each equipped with a desired threshold probability, we ask whether
Eve can satisfy at least one option with probability at least the respective
threshold. Our motivation for studying DQs is twofold. (1) DQs are interesting
in their own right as they allow for a fine-grained specification of
alternatives over desirable outcomes of a controlled stochastic system. (2)
DQs are equivalent to the more widely used _conjunctive_ queries (CQs) under
an alternative semantics, namely if the opponent Adam has to _reveal_ his
strategy to Eve before the game starts. This amounts to changing the
quantification order over strategies from $\exists\forall$—which is the
standard order—to $\forall\exists$. In general, this makes a difference since
multi-objective SGs are not _determined_ [21]. This optimistic “ _asserted-
exposure_ ” ($\forall\exists$) semantics is interesting in situations where
the non-deterministic system state can actually be observed at any given point
in time. For instance, in the smart heating case study from [36], the position
of the doors in a house is non-deterministically controlled by Adam and not
directly observable. However, if door sensors were to be installed, the
$\forall\exists$-semantics would be more adequate since the door positions are
now observable (but still uncontrollable).

$s_{0}$$s_{1}$$s_{2}$$T_{1}$$T_{2}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$
Figure 1:  Example SG with a disjunctive query $\mathbb{P}(\lozenge T_{1})\geq
x\vee\mathbb{P}(\lozenge T_{2})\geq y$. The Pareto sets, i.e., the feasible
threshold vectors $(x,y)$ are depicted next to the respective states.

The technical intricacies of DQs are best illustrated by means of an example:
Consider the SG in Figure 1. It comprises 5 states: the probabilistic state
$s_{0}$, states $s_{1}$ and $s_{2}$ controlled by Eve and Adam, respectively,
and the two targets labeled $T_{1}$ and $T_{2}$. Suppose that Eve’s objective
is the DQ “reach $T_{1}$ with probability at least $x$ _or_ $T_{2}$ with
probability at least $y$”, in symbols $\mathbb{P}(\lozenge T_{1})\geq
x\vee\mathbb{P}(\lozenge T_{2})\geq y$. The coordinate systems next to the
states show their _Pareto sets_ , i.e., the set of threshold vectors $(x,y)$
for which Eve can win the DQ, assuming the game starts in that state. For
$s_{1}$, the Pareto set is the whole box $[0,1]^{2}$ since Eve can reach
either of the targets surely from $s_{1}$ by picking the respective action.
For $s_{2}$, the Pareto set contains all convex combinations of $(0,1)$ and
$(1,0)$ and all point-wise smaller vectors, forming a triangle. This is
because Adam has to distribute the whole probability mass _somewhere_ ; for
any threshold vector $(x,y)$, $x+y\leq 1$, he cannot avoid satisfying it.
However, if $x+y>1$, Adam can prevent Eve from winning in state $s_{2}$: For
example, if $(x,y)=(0.6,0.6)$, Adam can randomize equally between both
actions, and no target is reached with at least $0.6$. This also shows that
solving a DQ is _not_ equivalent to solving each objective separately: From
$s_{2}$, Eve can neither guarantee that $T_{1}$ nor $T_{2}$ is reached with
positive probability; however, she can guarantee the thresholds $(0.5,0.5)$ in
the DQ. Finally, Eve can achieve each threshold vector $(x,y)$ with $x\leq
0.5$ or $y\leq 0.5$ from $s_{0}$ because $s_{1}$ is reached with probability
$0.5$ where she can put all probability mass on one of the targets. On the
other hand, Eve cannot ensure any vector $(x,y)$ with $x>0.5\wedge y>0.5$
because once she has fixed a strategy, Adam can mirror it so that both targets
are reached with _exactly_ $0.5$.

The example in Figure 1 demonstrates two important properties of disjunctive
queries in SGs: Firstly, Pareto frontiers are not necessarily convex, as in
state $s_{0}$. This is in contrast to _conjunctive queries_ where the set of
achievable probability thresholds is always convex [21, 26]. Secondly, as
mentioned above, SGs with multiple objectives are in general not _determined_
[21], i.e., it is relevant which player fixes their strategy first, thereby
_revealing_ it to the other player before the game starts. In fact, in the
example above, switching the quantification order allows Eve to take advantage
by reacting to the strategy of Adam. For instance, she could then ensure that
at least one of the targets is reached with probability at least $0.75$.

#### Contributions and overview

In summary, this paper makes the following contributions:

  * •

A comprehensive overview of strategy (Section 3, Table 1) and computational
complexity (Section 4, Table 2) of disjunctive reachability-safety queries in
stochastic games, significantly extending previous results from the literature
[21, 29, 37]. In particular, motivated by the observation that randomized
strategies are undesirable or meaningless for certain applications (e.g.,
medical or product design [25]), we study the setting of DQs under
_deterministic_ strategies for both players. Notably, this lead to rather high
complexities: Qualitative queries are $\mathsf{PSPACE}$-hard and quantitative
reachability is even undecidable.

  * •

A value iteration-style algorithm in the vein of [21] for approximating the
Pareto sets of DQs or CQs under the alternative asserted-exposure semantics
(Section 5).

#### Related work

SGs were introduced by Shapley [38] in 1953. Simple SGs—the turn-based variant
with a reachability objective—are one of the intriguing problems in
$\mathsf{NP}\cap\mathsf{coNP}$ but not known to be in $\mathsf{P}$ [24]. See
[23, 32] for an overview of solution algorithms. Turn-based SGs were studied
with a variety of other objectives, e.g. [14, 17, 18]. Other types of SGs
include concurrent games [12, 33], limited information games [3, 15], and
bidding games [4].

Stochastic systems with multiple objectives have been extensively studied for
more than a decade. Markov decision processes, SGs with a single player, were
investigated with multiple reachability or LTL objectives [26] as well as
multiple discounted sum [16], total reward [31] or mean payoff objectives
[20]. Further, the question of percentile queries was addressed in [30, 37],
and combinations of probabilistic and non-probabilistic objectives in [8].
Non-standard multi-objective queries were developed together with domain
experts in [6].

For SGs with multiple objectives, many decidability questions are still open.
For conjunctive reachability, it is only known that the Pareto set can be
approximated [2] with guaranteed precision, even in non-stopping games. For
total reward, the problem is proven decidable only for stopping games with
two-dimensional queries [10] but it can be approximated in higher dimensional
stopping SGs [21]. If only deterministic strategies are allowed, the exact
problem is undecidable [21], and so are generalized mean-payoff objectives in
SGs [39]. However, keeping mean-payoff above a certain threshold with some
probability is $\mathsf{coNP}$-complete [13]. Further, lexicographic
preferences over multiple reachability or safety objectives can be reduced to
single objectives [19]. The tool PRISM-games [34] implements compositional
approaches to verification and strategy synthesis of several multi-objective
problems [7, 35].

To the best of our knowledge, disjunctive queries were so far only considered
as a special case of more general Boolean combinations for expected rewards
[21], mean-payoff SGs [39], and in deterministic generalized reachability
games on graphs [29].

##  2 Preliminaries

##### General definitions.

For sets $A$ and $B$, the set of functions $A\to B$ is written $B^{A}$. The
set of finite words over a non-empty set $A$ is written $A^{*}$. For countable
sets $A$ we let $\mathsf{Dist}(A)\vcentcolon=\\{P\in[0,1]^{A}\mid\sum_{a\in
A}P(a)=1\\}$ be the set of all _probability distributions_ on $A$. The
_support_ of $d\in\mathsf{Dist}(A)$ is defined as $\mathsf{supp}(d)=\\{a\in
A\mid d(a)>0\\}$. The $i$-th component of a vector $\vec{x}\in[0,1]^{n}$ is
denoted $x_{i}$. We compare vectors $\vec{x},\vec{y}\in[0,1]^{n}$ component-
wise, i.e., $\vec{x}\leq\vec{y}$ iff $x_{i}\leq y_{i}$ for all $i=1,\ldots,n$.
A set $X\subseteq\mathbb{R}^{n}$ is _convex_ if for all $\vec{x},\vec{y}\in X$
and $p\in[0,1]$ it holds that $p\vec{x}+(1{-}p)\vec{y}\in X$. The _convex
hull_ $\mathsf{conv}(X)$ of $X$ is the smallest convex superset of $X$. Given
sets $X,Y\subseteq\mathbb{R}^{n}$ and a real number $p\in[0,1]$, we define the
$p$_-convex combination_
$pX+(1{-}p)Y\vcentcolon=\\{p\vec{x}+(1{-}p)\vec{y}\mid\vec{x}\in X,\vec{y}\in
Y\\}$. The _downward-closure_ of $X\subseteq[0,1]^{n}$ is defined as
$\mathsf{dwc}(X)\vcentcolon=\\{\vec{y}\in[0,1]^{n}\mid\exists\vec{x}\in
X\colon\vec{y}\leq\vec{x}\\}$. $X$ is called _downward-closed_ if
$X=\mathsf{dwc}(X)$. A _closed half-space_ is a set
$\\{\vec{x}\in\mathbb{R}^{n}\mid\vec{n}\cdot\vec{x}\geq d\\}$ where
$\vec{n}\in\mathbb{R}^{n}\setminus\\{\vec{0}\\}$ and $d\in\mathbb{R}$. A
_polyhedron_ is the intersection of finitely many closed half-spaces.
Polyhedra are convex.

##### Stochastic games and strategies.

Intuitively, the games considered in this paper are played by moving a pebble
along the edges (called _transitions_ from now on) of a finite directed graph.
The vertices (subsequently called _states_) of this graph are partitioned into
three classes which determine the states controlled by Eve, Adam, and the
probabilistic environment, respectively:

######  Definition 1 (SG).

A _stochastic game (SG)_ is a tuple
$\mathcal{G}=(S_{\mathsf{E}},S_{\mathsf{A}},S_{\mathsf{P}},{s_{0}},P,\mathsf{Act})$,
where $S_{\mathsf{E}}\uplus S_{\mathsf{A}}\uplus S_{\mathsf{P}}=\vcentcolon S$
are finite disjoint sets of _states_ controlled either by Eve
($S_{\mathsf{E}}$), Adam ($S_{\mathsf{A}}$), or the probabilistic environment
($S_{\mathsf{P}}$). The game starts in the _initial state_ ${s_{0}}\in S$.
Each $s\in S_{\mathsf{E}}\cup S_{\mathsf{A}}$ has a non-empty set
$\mathsf{Act}(s)\subseteq S$ of _actions_ available to Eve (Adam, resp.). For
all $s\in S_{\mathsf{P}}$, $P\colon S_{\mathsf{P}}\to\mathsf{Dist}(S)$ is a
probability distribution over the successors of $s$.

For $s\in S_{\mathsf{P}}$ and $t\in S$ we write $P(s,t)$ rather than
$P(s)(t)$. A state $s\in S$ is called _sink_ if either $s\in S_{\mathsf{P}}$
and $P(s,s)=1$ or $s\in S\setminus S_{\mathsf{P}}$ and
$\mathsf{Act}(s)=\\{s\\}$. $P$ and $\mathsf{Act}$ together induce a directed
graph on $S$. We often sketch this _game graph_ in our figures (e.g. Figure
1), drawing Eve’s, Adam’s and the probabilistic states with boxes, diamonds
and circles, respectively; and we omit the self-loops on sinks to ease the
presentation. For $k\geq 0$, we let $\mathcal{G}^{\leq k}$ be the restriction
of $\mathcal{G}$ to $k$-steps, that is, $\mathcal{G}^{\leq k}$ is obtained
from $\mathcal{G}$ by counting the transitions from ${s_{0}}$ taken so far and
entering an error sink once their number exceeds $k$. A _Markov decision
process_ (MDP) is the 1-player version of an SG, i.e., either
$S_{\mathsf{E}}=\emptyset$ or $S_{\mathsf{A}}=\emptyset$. A _Markov chain_
(MC) is a 0-player SG, i.e., $S=S_{\mathsf{P}}$. For technical reasons, we
allow MDPs and MCs with countably infinite state spaces. SGs, on the other
hand, are always _finite_ in this paper.

_Strategies_ define the semantics of SGs. A (general) strategy for Eve is a
function $\sigma\colon S^{*}S_{\mathsf{E}}\to\mathsf{Dist}(S)$ such that
$\mathsf{supp}(\sigma(\pi s))\subseteq\mathsf{Act}(s)$ for all $\pi s\in
S^{*}S_{\mathsf{E}}$. A strategy $\sigma$ is _deterministic_ if $\sigma(\pi
s)$ is a point-distribution for all $\pi s\in S^{*}S_{\mathsf{E}}$, i.e., if
it is not randomized.

To describe strategies by finite means (if possible), we use _strategy
automata_. Formally, a strategy automaton for Eve is a structure
$\mathcal{M}=(M,\mu,\nu,m_{0})$ with $M$ a countable set of memory elements,
$\mu\colon S\times M\to M$ a _memory update_ function, $\nu\colon
S_{\mathsf{E}}\times M\to\mathsf{Dist}(S)$ a _next move_ function, and
$m_{0}\in M$ an initial memory state. Given a strategy automaton
$\mathcal{M}$, the _induced MDP_ is the game

$\mathcal{G}^{\mathcal{M}}~{}\vcentcolon=~{}(\,\emptyset,\,S_{\mathsf{A}}\times
M,\,(S_{\mathsf{P}}\cup S_{\mathsf{E}})\times
M,\,(s_{0},m_{0}),\,P^{\mathcal{M}},\,\mathsf{Act}^{\mathcal{M}}\,)~{},$

where the transition probability function $P^{\mathcal{M}}$ is defined as
follows: Let $m,m^{\prime}\in M$ be arbitrary and let $s\in S$. Then, if $s\in
S_{\mathsf{P}}$, we let
$P^{\mathcal{M}}((s,m),(s^{\prime},m^{\prime}))\vcentcolon=P(s,s^{\prime})$ if
$\mu(s^{\prime},m)=m^{\prime}$; if $s\in S_{\mathsf{E}}$, then
$P^{\mathcal{M}}((s,m),(s^{\prime},m^{\prime}))\vcentcolon=\nu((s,m))(s^{\prime})$
if $\mu(s^{\prime},m)=m^{\prime}$; and
$P^{\mathcal{M}}((s,m),(s^{\prime},m^{\prime}))=0$ in all other cases.
Moreover, $\mathsf{Act}^{\mathcal{M}}((s,m))=\\{(s^{\prime},m^{\prime})\mid
s^{\prime}\in\mathsf{Act}(s)\wedge\mu(s^{\prime},m)=m^{\prime}\\}$ for all
$(s,m)\in S_{\mathsf{A}}\times M$. $\mathcal{M}$ is called a _stochastic-
update_ strategy if the memory update $\mu$ may additionally randomize over
$M$ (see [9] for details). From the definition it is clear that $\mathcal{M}$
_realizes_ a strategy in the general form $\sigma\colon
S^{*}S_{\mathsf{E}}\to\mathsf{Dist}(S)$. We define the _memory size_ of
$\sigma$ as the smallest $k\in\mathbb{N}\cup\\{\infty\\}$ such that there
exists a strategy automaton $\mathcal{M}=(M,\mu,\nu,m_{0})$ with $|M|=k$ that
realizes $\sigma$. If $k=\infty$, then $\sigma$ is _infinite-memory_ , and
otherwise _finite-memory_. If $k=1$, then $\sigma$ is called _memoryless_. An
_MD_ strategy is both memoryless and deterministic. The above definitions are
analogous for the other player Adam, interchanging $S_{\mathsf{E}}$ and
$S_{\mathsf{A}}$.

Throughout the paper, we consistently denote Eve’s strategies with $\sigma$
and Adam’s strategies with $\tau$. We usually identify strategies with their
realizing automata. Given a strategy $\sigma$, a _counter-strategy_ $\tau$ is
a strategy in the induced MDP $\mathcal{G}^{\sigma}$ and may depend on
$\sigma$.

##### Reachability-safety queries and determinacy.

Given an MC $(S,s_{0},P)$ and a set $T\subseteq S$, the _reachability
probability_ of $T$ is $\mathbb{P}(\lozenge T)\vcentcolon=\sum_{\pi\in
Paths(T)}Pr(\pi)$ where $Paths(T)$ is the set of finite paths $\pi$ of the
form $\pi={s_{0}}s_{1}\ldots s_{k}$ with $k\geq 0$, $s_{k}\in T$ and
$s_{i}\notin T$ for all $i=0,\ldots,k-1$; and
$Pr(\pi)\vcentcolon=\prod_{i=0}^{n-1}P(s_{i},s_{i+1})$. Dually, we define
$\mathbb{P}(\square T)\vcentcolon=1-\mathbb{P}(\lozenge\overline{T})$, where
$\overline{T}\vcentcolon=S\setminus T$. Intuitively, $\mathbb{P}(\lozenge T)$
is the probability to eventually reach a _target_ state in $T$ and
$\mathbb{P}(\square T)$ is the probability to stay forever within $T$, i.e.,
to avoid the _unsafe set_ $\overline{T}$. We write $\mathbb{P}^{\sigma,\tau}$
to emphasize that we consider the probability measure in the Markov chain
$\mathcal{G}^{\sigma,\tau}$ induced by some strategies $\sigma,\tau$.

######  Definition 2 (Disjunctive Queries [21]).

Given an SG $\mathcal{G}$ with state space $S$, an $n$-dimensional
_disjunctive query (DQ)_ for $\mathcal{G}$ is an expression of the form
$\varphi=\bigvee_{i=1}^{n}\mathbb{P}(\star_{i}T_{i})\geq x_{i}$ with
$\star_{i}\in\\{\lozenge,\square\\}$, $T_{i}\subseteq S$ for all
$i=1,\ldots,n$, and $\vec{x}\in(0,1]^{n}$ a threshold vector.

Note that we only allow (non-strict) _lower_ bounds in DQs. This is w.l.o.g.
as upper bounds on reachability or safety can be recast as lower bounds on the
dual objective. The standard semantics of a DQ is defined as follows [21]: Eve
can _achieve_ 111We use the term “achieve” rather than “win” for consistency
with previous works, e.g. [26, 21, 10]. $\varphi$, or equivalently, $\varphi$
is _achievable_ in $\mathcal{G}$ if
$\exists\sigma\forall\tau\colon\bigvee_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\star_{i}T_{i})\geq
x_{i}$ where $\sigma$ ranges over all strategies of Eve, $\tau$ over those of
Adam and $\mathbb{P}^{\sigma,\tau}$ is the probability measure of the induced
Markov chain $\mathcal{G}^{\sigma,\tau}$. A strategy of Eve witnessing
achievability of $\varphi$ is called an _achieving strategy_. Note that the
quantification order is such that Eve has to reveal her strategy to Adam
_before_ the game actually starts. Since the games are not determined, this
may be a disadvantage (see [21] or our example in the introduction).
Therefore, we also consider the alternative semantics obtained by swapping the
quantification order. We call this semantics _asserted-exposure_
($\forall\exists$ for short). In the $\forall\exists$-semantics, Adam’s
strategy is _exposed_ to Eve  _before_ the game begins, i.e., $\varphi$ is
$\forall\exists$-achievable if
$\forall\tau\exists\sigma\colon\bigvee_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\star_{i}T_{i})\geq
x_{i}$ holds. By definition, $\mathcal{G}$ is _determined_ for $\varphi$ iff
the standard and the alternative $\forall\exists$-semantics coincide.

We will consider the following subclasses of DQs: If $\star_{i}=\lozenge$
($\star_{i}=\square$) for all $i=1,\ldots,n$, then we call $\varphi$ a
_reachability_ (_safety_) DQ. We say that $\varphi$ is _mixed_ to emphasize
that it may contain both $\lozenge$ and $\square$. If $\vec{x}=(1,\ldots,1)$
then $\varphi$ is called _qualitative_ DQ, and otherwise _quantitative_ DQ. If
each state contained in a target/unsafe set is a sink then $\varphi$ is called
a _sink_ DQ. All of the above notions are defined analogously for _conjunctive
queries_ (CQs).

##### Pareto sets.

If the threshold vector $\vec{x}$ in a query $\varphi$ has not been fixed, we
can think of $\varphi$ as a _query template_. We define the set _Pareto set_
for query template $\varphi$ in a given SG $\mathcal{G}$ as

$\mathcal{A}(\mathcal{G},\varphi)~{}\vcentcolon=~{}\\{\,\vec{x}\in[0,1]^{n}\,\mid\,\exists\sigma\,\forall\tau\colon\bigvee_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\star_{i}T_{i})\geq
x_{i}\,\\}$

and similarly for CQs. Further, for $k\geq 0$, we call
$\mathcal{A}(\mathcal{G}^{\leq k},\varphi)$ the _horizon- $k$_ Pareto set,
i.e., the set of points achievable if the game runs for at most $k$ steps. We
define $\mathcal{A}^{\forall\exists}(\mathcal{G},\varphi)$ as the set of
vectors achievable in the alternative $\forall\exists$-semantics. Note that in
general,
$\mathcal{A}(\mathcal{G},\varphi)\subseteq\mathcal{A}^{\forall\exists}(\mathcal{G},\varphi)$,
and equality holds iff $\mathcal{G}$ is determined for all $\varphi(\vec{x})$,
$\vec{x}\in[0,1]^{n}$. The Pareto sets $\mathcal{A}(\mathcal{G},\varphi)$ and
$\mathcal{A}^{\forall\exists}(\mathcal{G},\varphi)$ generalize the notion of
_lower_ and _upper value_ in single-dimensional games. Indeed, they coincide
for $n=1$ as single-dimensional SGs are determined [24]. Furthermore,
$\mathcal{A}(\mathcal{G},\varphi)$ is convex for CQs [21].

##### Goal-unfolding.

The following construction is folklore (e.g. [29, 21]). Given an SG
$\mathcal{G}$ with states $S$ and an $n$-dimensional query $\varphi$, we
define the _goal-unfolding_ $\mathsf{Unf}(\mathcal{G},\varphi)$ of
$\mathcal{G}$ with respect to $\varphi$ as a game with state space
$S\times\\{0,1\\}^{n}$. Let $(s,\vec{v})$ be a state of the unfolding.
Intuitively, $\mathsf{Unf}(\mathcal{G},\varphi)$ remembers which
targets/unsafe sets have already been visited during a specific play. This is
encoded in the $n$-bit vector $\vec{v}$. That is, if $\mathcal{G}$ transitions
from $s$ to $t$, then in the unfolding $(s,\vec{v})$ moves to $(t,\vec{u})$
where $\vec{u}$ is obtained from $\vec{v}$ by setting all bits corresponding
to the targets/unsafe sets containing $t$ to one. Accordingly, the initial
state is $({s_{0}},(0,\ldots,0))$. If $\varphi$ is a sink query then the
unfolding is trivial, i.e., equal to $\mathcal{G}$. Strategies in
$\mathsf{Unf}(\mathcal{G},\varphi)$ can be interpreted as strategies in
$\mathcal{G}$ by incorporating the vectors $\vec{v}$ from the states of the
unfolding into the memory of the strategy.

##  3 Strategy Complexity

In this section we analyze the memory complexity of Eve’s achieving strategies
for DQs in terms of the query dimension, denoted $n$ in the following. More
formally, given a class $Q_{n}$ of DQs with $n$ objectives, we determine (or
bound) a number $b(n)$ such that

  1. 1.

$b(n)$ memory is _necessary_ for the queries in $Q_{n}$, i.e., there exists a
game $\mathcal{G}$ and query $\varphi\in Q_{n}$ such that $\varphi$ is
achievable in $\mathcal{G}$ iff Eve may use at least $b(n)$ memory;

  2. 2.

$b(n)$ memory is _sufficient_ for the queries in $Q_{n}$, i.e., for all games
$\mathcal{G}$ and $\varphi\in Q_{n}$, if $\varphi$ is achievable in
$\mathcal{G}$, then Eve has an achieving strategy using at most $b(n)$ memory.

To give a nuanced picture of the complexity, we distinguish the classes of
qualitative vs. quantitative DQs, safety vs. reachability DQs and study the
restriction to deterministic vs. general (randomized) strategies. We stress
that the latter distinction applies to both players, i.e., in the
_deterministic-strategies_ case, neither Adam nor Eve may play randomized
strategies whereas in the _general-strategies_ case, both players may follow
arbitrary—possibly randomized—strategies.

We briefly recall the case of non-stochastic games with deterministic
strategies for both players. It was shown in [29, Lem. 1] that
${n\choose\lfloor n/2\rfloor}$ memory is necessary and sufficient for safety
DQs. Notably, this means that not the _whole_ goal-unfolding is needed (though
an exponentially large fragment). Reachability DQs, on the other hand, do not
need memory at all in the purely deterministic setting because a DQ
$\bigvee_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq 1$ boils down to reaching the
set $\bigcup_{i=1}^{n}T_{i}$, and MD strategies are sufficient for winning
reachability games on finite graphs.

In the rest of the section we first treat the general-strategies case (Section
3.1) and then study the restriction to deterministic strategies (Section 3.2).
Table 1 summarizes the results.

######  Theorem 1.

The memory bounds in Table 1 are correct.

Table 1:  Memory requirements for Eve in terms of the number $n$ of objectives in the DQ. The lower bounds in column _“SG with deterministic strats.”_ apply already to sink queries.  | _SG with general strats._ | _SG with deterministic strats._ | _Non-SG with deterministic strats._
---|---|---|---
|  $\square$ / $\lozenge$ |  $\square$ / $\lozenge$ | $\square$ | $\lozenge$
_Qual._ | none [Lem. 2] |  $\geq{n\choose n/2}$ [Lem. 6] |  ${n\choose\lfloor n/2\rfloor}$ [29] | none [trivial]
_Quant._ |  $2^{n}-1$ [Lem. 1, 4, 5] |  $\infty$ [Cor. 1] | — _not applicable_ —

###  3.1 Strategy Complexity under General Strategies

Recall from above that whenever we say that a certain class of strategies are
“sufficient” or “necessary”, we are implicitly assuming that Eve actually has
a winning strategy.

######  Lemma 1.

In the general-strategies case, deterministic strategies with at most
$2^{n}{-}1$ memory states suffice for mixed quantitative DQs. Moreover, MD
strategies are sufficient for sink queries.

###### Proof (sketch).

By [21, Theorem 7], MD strategies are sufficient for quantitative DQs with
_expected reward_ objectives (see the formal definition in [21]). We reduce
reachability and safety to expected reward in the goal-unfolding (Appendix
A.1). The resulting MD strategy in the unfolding corresponds to a strategy of
Eve with at most $2^{n}{-}1$ memory. ∎

Recall that even though Lemma 1 implies that deterministic strategies are
sufficient for Eve, Adam may still use randomization. In fact, we show in
Corollary 1 in Section 3.2 that Lemma 1 does _not_ hold in the deterministic-
strategies case where both players are forced to follow a deterministic
strategy. Next we either improve the bound from Lemma 1 or prove matching
lower bounds. We consider qualitative DQs first.

######  Lemma 2.

In the general-strategies case, MD strategies suffice for mixed qualitative
DQs.

###### Proof (sketch).

It can be shown that a given strategy of Eve achieves
$\bigvee_{i=1}^{n}\mathbb{P}(\star_{i}T_{i})\geq 1$ iff it achieves the single
objective $\mathbb{P}(\star_{i}T_{i})\geq 1$ for at least one $1\leq i\leq n$
(Appendix A.2). For the latter, MD strategies are sufficient [23]. ∎

The qualitative bounds (“$\geq 1$”) are crucial in the previous proof. Indeed,
the equivalence in the above proof sketch does _not_ hold for quantitative
bounds (a minimal counter-example is the game in Fig. 1 started from $s_{2}$
with bounds $\geq\nicefrac{{1}}{{2}}$ for both objectives). For the
quantitative setting where arbitrary bounds are allowed, the following
observation relates conjunctive and disjunctive queries and enables us to
reuse some known results about CQs. Intuitively, it states that qualitative
reachability CQs can be reduced to quantitative (qualitative) DQs in the case
of general (respectively deterministic) strategies.

######  Lemma 3.

For every SG $\mathcal{G}$ with a qualitative reachability CQ
$\varphi=\bigwedge_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq 1$, there exists a
game $\mathcal{G}^{\prime}$ (where Eve’s strategies $\sigma$ are in one-to-one
correspondence) and a

  1. 1.

_quantitative_ reachability DQ $\varphi^{\prime}_{quant}$ such that $\sigma$
achieves $\varphi$ in $\mathcal{G}$ iff $\sigma$ achieves
$\varphi^{\prime}_{quant}$ in $\mathcal{G}^{\prime}$ under _general_
strategies;

  2. 2.

_qualitative_ reachability DQ $\varphi^{\prime}_{qual}$ such that $\sigma$
achieves $\varphi$ iff $\sigma$ achieves $\varphi^{\prime}_{qual}$ under
_deterministic_ strategies.

###### Proof (sketch).

$\mathcal{G}^{\prime}$ is constructed as follows: The original $\mathcal{G}$
is only played with probability $\nicefrac{{1}}{{2}}$. With the remaining
$\nicefrac{{1}}{{2}}$, Adam freely chooses one of the $n$ targets
$T_{1},\ldots,T_{n}$, after which the game ends immediately (Figure 2, left).
The following can be readily verified (Appendix A.3): In the deterministic-
strategies case, each strategy $\sigma$ of Eve achieves the CQ $\varphi$ in
$\mathcal{G}$ iff $\sigma$ achieves the _qualitative_ DQ
$\bigvee_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq 1$ in $\mathcal{G}^{\prime}$.
Otherwise, if randomization is allowed, then $\sigma$ achieves $\varphi$ in
$\mathcal{G}$ iff it achieves the _quantitative_ DQ
$\bigvee_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq\frac{1}{2}+\frac{1}{2n}$ in
$\mathcal{G}^{\prime}$. ∎

$\mathcal{G}$$T_{1}$$\vdots$$T_{n}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$

A: Env. chooses $\mathcal{T}_{1}$startB: Eve chooses
$\mathcal{T}_{2}$$\mathcal{T}$C: Adam chooses $n{-}|\mathcal{T}_{2}|{-}1$
targets$p(\mathcal{T}_{2})$$1-p(\mathcal{T}_{2})$

Figure 2:  Left: Reduction of qualitative CQs to DQs (Lemma 3). Right: Game
constructed in the proof of Lemma 5. The probability $p(\mathcal{T}_{2})$
increases with $|\mathcal{T}_{2}|$. Eve must select exactly
$\mathcal{T}_{2}=\mathcal{T}_{1}$ in Stage B to avoid visiting at least one of
the targets in $\mathcal{T}$ with maximal probability.

With Lemma 3 and a result of [29] we obtain a lower bound for quantitative
reachability:

######  Lemma 4.

In the general-strategies case, quantitative _reachability_ DQs need $2^{n}-1$
memory.

###### Proof (sketch).

[29, Lem. 2] describes a family of (deterministic) games
$(\mathcal{G}_{n})_{n\geq 1}$ where Eve needs $2^{n}-1$ memory to visit all
$n$ targets under _deterministic_ strategies, i.e., to achieve a _qualitative
reachability CQ_. A more detailed analysis of the games $\mathcal{G}_{n}$
shows that even if both players may use general strategies, Eve still needs
$2^{n}-1$ memory (Appendix A.4). We stress that this is non-trivial: in some
cases, memory _can_ be traded for randomization to achieve qualitative DQs. A
minimal example is an MDP with $S_{\mathsf{E}}=\\{s_{0}\\}$,
$S_{\mathsf{P}}=\\{t_{1},t_{2}\\}$, $P(t_{1},s_{0})=P(t_{2},s_{0})=1$,
$\mathsf{Act}(s_{0})=\\{t_{1},t_{2}\\}$, $T_{1}=\\{t_{1}\\}$,
$T_{2}=\\{t_{2}\\}$; the CQ $\mathbb{P}(\lozenge T_{1})\geq
1\wedge\mathbb{P}(\lozenge T_{2})\geq 1$ is achievable by a memoryless
randomized strategy but not by an MD strategy. By Lemma 3.1, we can reduce
each $\mathcal{G}_{n}$ to an SG with a _quantitative reachability DQ_ where
Eve’s winning strategies are the same as those in the original $\mathcal{G}$,
i.e., they require at least $2^{n}{-}1$ memory. ∎

We now prove a lower bound for safety DQs. To the best of our knowledge,
unlike Lemma 4, the bound for safety DQs does not easily follow from related
works. Therefore we propose a new construction for this case (shown on the
right of Figure 2; see Appendix A.5 for the proof).

######  Lemma 5.

In the general-strategies case, quantitative _safety_ DQs need $2^{n}-1$
memory.

In summary, quantitative DQs require the _full_ goal-unfolding—which is of
exponential size in $n$—while qualitative ones do not need memory at all.

###  3.2 Strategy Complexity under Deterministic Strategies

######  Example 1.

Consider the SG in Figure 3 (left). The qualitative DQ $\mathbb{P}(\lozenge
T_{1})\geq 1\vee\mathbb{P}(\lozenge T_{2})\geq 1$ is achievable if Adam has to
choose deterministically in $s_{0}$: If he chooses the upper path, then Eve
chooses $T_{1}$ in $s_{1}$; conversely, if he chooses the lower path, then Eve
moves to $T_{2}$. Clearly, this strategy requires Eve to use one bit of memory
(i.e., memory size $2$) and there is no memoryless strategy that achieves the
query. This example shows that Lemma 1 is not valid in the deterministic-
strategies case: memory is needed even for sink queries.

$s_{0}$$T_{1}$$T_{2}$$s_{1}$$T_{1}$$T_{2}$

$s$$t_{2}$$t_{1}$$T_{2}$$T_{1}$

Figure 3:  All probabilities are $0.5$. Left: If only deterministic strategies
are allowed, then Eve’s achieving strategies for $\mathbb{P}(\lozenge
T_{1})\geq 1\vee\mathbb{P}(\lozenge T_{2})\geq 1$ need memory, despite the
fact that targets/unsafe sets contain only sinks. Right: There exists $x$ such
that the CQ $\mathbb{P}(\lozenge T_{1})\geq x\wedge\mathbb{P}(\lozenge
T_{2})\geq 1{-}x$ is achievable under deterministic strategies iff infinite
memory is allowed.

The above example indicates that the deterministic-strategies case is already
“interesting” for sink queries. Therefore—due to space limitations of the
paper—we have decided to restrict our study of deterministic strategies to
sink queries only. The somewhat counter-intuitive situation that _more_ memory
is needed if _less general_ strategies are allowed is due to the fact that
only Adam benefits from randomization, but not Eve. In fact, Eve can in
general achieve _more_ queries in the deterministic-strategies setting.
Nonetheless, the example in Figure 3 shows that Eve’s added power does not
come for free: She has to invest more resources (memory) on her side as well.
The following shows that this is necessary in general:

######  Lemma 6.

In the deterministic-strategies case, $n\choose n/2$ memory is necessary for
qualitative reachability or safety DQs. This holds even for sink queries.

###### Proof (sketch).

We sketch the construction for qualitative reachability DQs. Let $n=2q$ be
even. The game comprises three stages, A, B, and C. In the initial Stage A,
Adam specifies a combination $\mathcal{T}_{A}$ of $q$ different targets. Those
are then visited with probability $\nicefrac{{1}}{{2}}$ and the game ends.
With the remaining probability of $\nicefrac{{1}}{{2}}$, the game moves on to
Stage B which is similar to stage A, but controlled by Eve. Let
$\mathcal{T}_{B}$ be the set of $q$ targets that Eve specifies in this stage.
Consequently, with total probability $\nicefrac{{1}}{{4}}$, the game enters
the final stage C where Adam chooses and visits $q+1$ different targets
$\mathcal{T}_{C}$. It follows that a target is visited with probability $1$
iff it is chosen in all three stages. The only achieving strategy of Eve
consists in selecting exactly $\mathcal{T}_{B}=\mathcal{T}_{A}$, requiring
${n\choose q}$ memory. See Appendix A.6 for the remaining details and the
adaptation of the construction to safety. ∎

We consider quantitative DQs next. The following lemma is the quantitative-
bounds version of Lemma 3. The difference is, however, that the reduction only
works under _deterministic_ strategies (see Appendix A.7 for the proof).

######  Lemma 7.

For every SG $\mathcal{G}$ with quantitative reachability CQ
$\varphi=\bigwedge_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq x_{i}$, there
exists a game $\mathcal{G}^{\prime}$ (where Eve’s strategies $\sigma$ are in
one-to-one correspondence) and a quantitative reachability DQ
$\varphi^{\prime}$ such that, under the assumption of _deterministic_
strategies, $\sigma$ achieves $\varphi$ in $\mathcal{G}$ iff $\sigma$ achieves
$\varphi^{\prime}$ in $\mathcal{G}^{\prime}$.

We can use the previous reduction to show that in general, infinite memory is
necessary for achieving quantitative DQs under deterministic strategies.

######  Lemma 8.

For the MDP from Figure 3 (right), there exists $x\in[0,1]$ such that the CQ
$\mathbb{P}(\lozenge T_{1})\geq x\wedge\mathbb{P}(\lozenge T_{2})\geq 1{-}x$
is only achievable by an infinite-memory strategy.

###### Proof.

Every deterministic strategy $\sigma$ can be identified with an infinite
string $\sigma=\sigma_{1}\sigma_{2}\ldots\in\\{0,1\\}^{\omega}$ where for all
$i\geq 1$, $\sigma_{i}=1$ ($\sigma_{i}=0$) indicates that $\sigma$ moves to
$t_{1}$ ($t_{2}$, resp.) when $s$ is entered for the $i$-th time. Clearly,
$\mathbb{P}^{\sigma}(\lozenge T_{1})=(0.\sigma)_{2}$, i.e., the probability to
reach $T_{1}$ is equal to the real number whose decimal binary representation
is the infinite string $0.\sigma$. We claim that the above CQ
$\mathbb{P}(\lozenge T_{1})\geq x\wedge\mathbb{P}(\lozenge T_{2})\geq 1{-}x$
with $x=(0.1^{1}01^{2}01^{3}01^{4}0...)_{2}$ can only be achieved by a
strategy that uses infinite memory. If not, then let $\mathcal{M}$ be a
finite-state strategy automaton that achieves the CQ. Since $\mathcal{M}$ is
finite, there exist two distinct prefixes $\pi_{1}\neq\pi_{2}$ of
$1^{1}01^{2}01^{3}01^{4}0...$ such that after reading $\pi_{1}$ or $\pi_{2}$,
the automaton $\mathcal{M}$ is in the same memory state $m$. Suppose that from
$m$ on, $\mathcal{M}$ plays action sequence $\pi\in\\{0,1\\}^{\omega}$. Since
$\mathcal{M}$ is achieving, we must have that
$\pi_{1}\pi=\pi_{2}\pi=1^{1}01^{2}01^{3}01^{4}0...$ which, however, implies
$\pi_{1}=\pi_{2}$, contradiction. ∎

######  Corollary 1.

In general, infinite memory is necessary for achieving quantitative
reachability or safety DQs under deterministic strategies. This holds even for
sink queries.

###### Proof.

Apply the reduction from Lemma 7 to the MDP from Lemma 8. For safety notice
that in the MDP, $\mathbb{P}(\square\overline{T}_{1})\geq x$ iff
$\mathbb{P}(\lozenge T_{2})\geq x$. ∎

##  4 Computational Complexity

In this section, we study the complexity of the achievability problem for DQs
in the standard semantics, i.e., the decision problem
“$\exists\sigma\forall\tau\colon\bigvee_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\star_{i})\geq
x_{i}$” in some given game. We consider the same variations of the problem as
in Section 3, that is, qualitative vs. quantitative DQs, reachability vs.
safety queries and deterministic vs. general strategies. For the complexity
theoretic results, we assume that all transition probabilities in the games
and thresholds in the queries are rational numbers given as binary-encoded
integer pairs.

We again briefly discuss the case of purely deterministic games on graphs.
[29, Theorem 1] shows that, in deterministic games, qualitative safety DQs are
$\mathsf{PSPACE}$-complete via a reduction from quantified Boolean formulas.
Reachability DQs, as mentioned in Section 3.1, can be reduced to solving a
standard single-target reachability game which can be solved in $\mathsf{P}$.
We now present our results in detail, first for general (Section 4.1) and then
for deterministic strategies (Section 4.2). Table 2 summarizes the results.

######  Theorem 2.

The complexity bounds in Table 2 are correct.

Table 2:  Complexity of the feasibility problem for DQs in the standard semantics. Column _“SG with deterministic strats.”_ applies exclusively to sink queries.  | _SG with general strats._ | _SG with deterministic strats._ | _Non-SG with deterministic strats._
---|---|---|---
|  $\square$ / $\lozenge$ |  $\square$ / $\lozenge$ | $\square$ | $\lozenge$
_Qual._ |  $\mathsf{P}$ [Lem. 9] |  $\geq\mathsf{PSPACE}$ [Lem. 12] |  $\mathsf{PSPACE}$ [29] |  $\mathsf{P}$ [trivial]
|  |  |  $\leq\mathsf{EXPTIME}$ [Lem. 13] / ? |  |
_Quant._ |  $\geq\mathsf{PSPACE}$ [Lem. 11,10] | undecidable [Lem. 14] | — _not applicable_ —
| $\leq\mathsf{NEXPTIME}$ |  |  |

###  4.1 Computational Complexity under General Strategies

######  Lemma 9.

In the general-strategies case, qualitative mixed DQs are decidable in
$\mathsf{P}$.

###### Proof.

As in Lemma 2, in the qualitative case it suffices to check for each objective
$\star_{i}T_{i}$, $i=1,\ldots,n$, $\star_{i}\in\\{\lozenge,\square\\}$,
individually whether Eve can satisfy it with probability $1$. Hence $n$
queries to a polynomial time algorithm for qualitative simple stochastic games
[27] suffice. ∎

######  Lemma 10.

In the general-strategies case, quantitative _reachability_ DQs are
$\mathsf{PSPACE}$-hard.

###### Proof.

The feasibility problem for qualitative reachability CQs is
$\mathsf{PSPACE}$-hard, which holds already for MDPs where
$S_{\mathsf{A}}=\emptyset$ [37, Lem. 2]. Lemma 3.1 in Section 3.1, reduces the
MDP CQ problem to a quantitative DQ problem in an SG in polynomial time. ∎

######  Lemma 11.

In the general-strategies case, quantitative _safety_ DQs are
$\mathsf{PSPACE}$-hard.

###### Proof (sketch).

It can be shown that quantitative reachability CQs with _strict bounds_ in
MDPs can be reduced to quantitative safety DQs (with non-strict bounds) in
SGs. We prove that strict-bounded reachability CQs in MDPs are
$\mathsf{PSPACE}$-hard which is done by analyzing a construction from [37,
Lem. 2] in greater detail (see Appendix B.1). ∎

$\mathsf{PSPACE}$-hardness in the previous two lemmas is caused by the
exponential size of the goal-unfolding that can, as we have shown in Section
3.1, not be avoided in general. Indeed, for sink queries the complexity of
quantitative (mixed) DQs drops to $\mathsf{NP}$-complete in the general-
strategies case [21, Corollary 1], where the upper bound stems from the fact
that MD strategies suffice and can be verified in polynomial time using linear
programming [26].

Regarding upper bounds on quantitative DQ feasibility, we remark that the
problem can be decided in $\mathsf{NEXPTIME}$: Guess an (exponentially large)
MD strategy $\sigma$ in the goal unfolding, consider the induced MDP
$\mathcal{G}^{\sigma}$ and verify in polynomial time in the size of
$\mathcal{G}^{\sigma}$ that Adam does not have a strategy violating all
thresholds at once by using the multi-objective MDP algorithm from [26]. We
currently do not know of a tighter upper bound.

###  4.2 Computational Complexity under Deterministic Strategies

As in Section 3.2, we consider only sink queries in this section.

######  Lemma 12.

Under deterministic strategies, qualitative reachability and safety DQs are
$\mathsf{PSPACE}$-hard, even in the case of sink queries.

###### Proof (sketch).

Inspired by similar constructions in [29, 37], we reduce from the problem of
deciding truth of a quantified Boolean formula (QBF). See Figure 4 for an
example and Appendix B.2 for the full proof. ∎

$s_{1}$$x_{1}$$\overline{x}_{1}$$s_{2}$$x_{2}$$\overline{x}_{2}$$s_{3}$$x_{3}$$\overline{x}_{3}$2121,221
Figure 4:  Example reduction from Lemma 12 for the QBF $\exists x_{1}\forall
x_{2}\exists x_{3}(\overline{x}_{1}\wedge
x_{2}\wedge\overline{x}_{3})\vee(\overline{x}_{2}\wedge x_{3})$. Numbers in
target states indicate whether they belong to $T_{1}$ and/or $T_{2}$. The QBF
is true as witnessed by Eve’s strategy that first goes to $\overline{x}_{1}$
and then to $x_{3}$ if Adam had selected $\overline{x}_{2}$ and otherwise to
$\overline{x}_{3}$.

Notably, the corresponding _conjunctive_ problem in the setting of Lemma 12
(qualitative sink CQ, deterministic strategies) can be solved in $\mathsf{P}$
as it reduces to simply checking if the intersection $\bigcap_{i=1}^{n}T_{i}$
can be reached with probability 1. Contrary to most other results, Lemma 12
thus identifies a setting where DQs are _much_ harder than CQs. Moreover, due
to the restriction to sink queries, Lemma 12 also yields
$\mathsf{PSPACE}$-hardness for disjunctions of expected reward objectives
under deterministic strategies. In the general-strategies case, such expected
reward DQs are decidable in $\mathsf{NP}$ [21]. Next we show an upper bound
for qualitative _safety_ DQs:

######  Lemma 13.

In the deterministic-strategies case, qualitative safety sink DQs are
decidable in $\mathsf{EXPTIME}$.

###### Proof (sketch).

The proof relies crucially on the fact that non-achievability of a qualitative
safety DQs can be witnessed after at most a bounded number steps of the game.
Indeed, if $\sigma$ is a non-achieving strategy of Eve, then Adam has a
counter-strategy that can reach all the unsafe sets $\overline{T}$ with
_positive_ probability after at most $|S|$ steps of the game. The result then
follows by constructing a polynomially space-bounded alternating Turing
machine that simulates the game for at most $|S|$ steps and accepts iff the
query is not achievable. We handle probabilistic branching via backtracking
using a stack whose content remains of polynomial size throughout the
execution (see Appendix B.3 for details). ∎

The above proof cannot simply be extended to reachability because,
intuitively, reaching a target with probability $1$ may only occur in the
limit. In fact, the question whether qualitative reachability DQs are
decidable under deterministic strategies remains open.

Regarding the quantitative case, [21, Theorem 3] proves that reachability
_CQs_ are _undecidable_ under deterministic strategies. Thus with Lemma 7 we
also have:

######  Lemma 14.

Quantitative reachability DQs are undecidable under deterministic strategies.

##  5 Value Iteration

In a nutshell, value iteration (VI) algorithms in general evaluate the
$k$-step game $\mathcal{G}^{\leq k}$ using information about the game
$\mathcal{G}^{\leq k{-}1}$ up to some reasonable $k$. In this section, we
present a VI-style algorithm for computing the Pareto sets
$\mathcal{A}(\mathcal{G}^{\leq k},\varphi)$ or
$\mathcal{A}^{\forall\exists}(\mathcal{G}^{\leq k},\varphi^{\prime})$ for a
given game $\mathcal{G}$, DQ $\varphi$ or CQ $\varphi^{\prime}$, and step
bound $k\geq 0$. Consequently, we do not fix a threshold vector $\vec{x}$ in
our queries but consider query _templates_ instead. To keep the presentation
simple, we focus on _general-strategies_ and consider only sink queries.

We briefly recall the VI from [21] (subsequently called _CQ-VI_) that for a
given CQ $\varphi$ successively outputs $\mathcal{A}(\mathcal{G}^{\leq
k},\varphi)$ for all $k\geq 0$. Let $\mathfrak{C}$ be the set of all downward-
closed polyhedra in $[0,1]^{n}$ and let $X\in\mathfrak{C}^{S}$. In the
following, we write $X_{s}$ for $X(s)$. The update function
$F\colon\mathfrak{C}^{S}\to\mathfrak{C}^{S}$ is defined according to Figure 5.
Note that $F$ is well-defined, i.e., always yields downward-closed polyhedra.
For CQ $\varphi=\bigwedge_{i=1}^{n}\mathbb{P}(\star_{i}T_{i})\geq x_{i}$ and
each $s\in S$ define the $n$-dimensional zero-one vector
$\mathbbm{1}^{\varphi}_{s}$, such that
$(\mathbbm{1}^{\varphi}_{s})_{i}\vcentcolon=1$ iff $s\in T_{i}$ and let
$X^{0}(\varphi)_{s}\vcentcolon=\mathsf{dwc}(\mathbbm{1}^{\varphi}_{s})$. Then
[21] implies that $F^{k}(X^{0}(\varphi))_{s_{0}}=\mathcal{A}(\mathcal{G}^{\leq
k},\varphi)$ for all $k\geq 0$.

| $F(X)_{s}$ | $\Phi(\mathcal{X})_{s}$
---|---|---
$s\in S_{\mathsf{A}}\quad$ | $\bigcap_{t\in\mathsf{Act}(s)}X_{t}$ | $\bigcup_{t\in\mathsf{Act}(s)}\mathcal{X}_{t}$
$s\in S_{\mathsf{E}}$ | $\mathsf{conv}\big{(}\bigcup_{t\in\mathsf{Act}(s)}X_{t}\big{)}\quad$ | $\big{\\{}\,\mathsf{conv}\big{(}\bigcup_{t\in\mathsf{Act}(s)}X_{t}\big{)}\,\mid\,X\ \dot{\in}\ \mathcal{X}\,\big{\\}}$
$s\in S_{\mathsf{P}}$ | $\sum_{t\in S}P(s,t)X_{t}$ | $\big{\\{}\,\sum_{t\in S}P(s,t)X_{t}\,\mid\,X\ \dot{\in}\ \mathcal{X}\,\big{\\}}$
Figure 5: The value iteration operators $F$ and $\Phi$ for computing
$\mathcal{A}(\mathcal{G}^{\leq k},\varphi)$ and
$\mathcal{A}^{\forall\exists}(\mathcal{G}^{\leq k},\varphi)$, respectively.

We now address the question whether an iteration analogous to CQ-VI can be
devised for _DQs_. CQ-VI computes the horizon-$(k{+}1)$ Pareto set of any
given state by taking only the horizon-$k$ sets of its successors (and the
relevant probability distribution) into account. For DQs, this is impossible
in general:

######  Observation 1.

Suppose $s\in S$ has successors $s_{1},s_{2}$. In general, the horizon-$k$
Pareto sets of $s_{1}$ and $s_{2}$ w.r.t. a DQ do _not_ uniquely determine the
horizon-$(k{+}1)$ Pareto set of $s$.

###### Proof.

Consider the game in Figure 6 (left) and the DQ
$\varphi=\mathbb{P}(\square\overline{T_{1}})\geq
x_{1}\vee\mathbb{P}(\square\overline{T_{2}})\geq x_{2}$. The horizon-$1$
Pareto sets of $s_{1},s_{2}$ and $t_{1},t_{2}$, as well as the horizon-$2$
sets of $s_{0}$ and $t_{0}$ are sketched next to the corresponding state. We
claim that the threshold vector $(x_{1},x_{2})=(0.75,0.75)$ is achievable from
$t_{0}$, but not from $s_{0}$: As deterministic strategies suffice for Eve, we
can assume by symmetry that she moves to $T_{1}$ in $s_{1}$. But then Adam can
respond by moving to $T_{2}$ in $s_{2}$ and both $\square\overline{T_{1}}$ and
$\square\overline{T_{2}}$ are satisfied with probability exactly $0.5$. Thus
$(0.75,0.75)$ is not achievable. However, at $t_{2}$ we can assume by symmetry
that Adam moves to $T_{1}$ with probability $\geq 0.5$ and so
$\square\overline{T_{2}}$ is satisfied with probability $\geq 0.75$ from
$t_{0}$. ∎

$s_{0}$$s_{1}$$s_{2}$$T_{1}$$T_{2}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$$t_{0}$$t_{1}$$t_{2}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$

$s_{0}$$s_{1}$$s_{2}$$T_{1}$$T_{2}$$T_{1,2}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$

Figure 6: Left: The successors of both $s_{0}$ and $t_{0}$ have the same
Pareto set w.r.t. the DQ $\mathbb{P}(\square\overline{T_{1}})\geq
x_{1}\vee\mathbb{P}(\square\overline{T_{2}})\geq x_{2}$, but the Pareto sets
of $s_{0}$ and $t_{0}$ are different. Right: Example run of Algorithm 1 for
$k=2$ and query $\mathbb{P}(\lozenge T_{1})\geq x_{1}\wedge\mathbb{P}(\lozenge
T_{2})\geq x_{2}$. At $s_{2}$, the rightmost polyhedron is removed by the
$\mu$-operation in line 4. The result is the intersection of the two polyhedra
at $s_{0}$.

Intuitively, the example in Figure 6 demonstrates that—unlike in CQ-VI—the
Pareto sets alone do not convey enough information to allow for a sound VI. In
the remainder of this section we present a work-around for this problem. The
idea is to account for the missing information by extending the domain of VI
to _sets_ of Pareto sets. We will not work with DQs directly but with CQs in
the $\forall\exists$-semantics. This is justified because _non-achievability_
of a DQ can be recast as follows:

$\neg\,\exists\sigma\,\forall\tau\,\bigvee_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\star_{i}T_{i})\geq
x_{i}\quad\iff\quad\forall\sigma\,\exists\tau\,\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\overline{\star_{i}}\overline{T_{i}})>1-x_{i}$
(1)

where $\overline{\lozenge}=\square$ and $\overline{\square}=\lozenge$. That
is, for deciding achievability of a DQ
$\varphi=\bigvee_{i=1}^{n}\mathbb{P}(\star_{i}T_{i})\geq x_{i}$, we can
equivalently consider the dual CQ
$\overline{\varphi}\vcentcolon=\bigwedge_{i=1}^{n}\mathbb{P}(\overline{\star_{i}}\overline{T_{i}})>1{-}x_{i}$
from (1) under the $\forall\exists$-semantics in the game
$\tilde{\mathcal{G}}$ where the roles of Adam and Eve have been swapped. In
fact, with (1), the whole Pareto set $\mathcal{A}(\mathcal{G},\varphi)$ can be
recovered from
$\mathcal{A}^{\forall\exists}(\tilde{\mathcal{G}},\overline{\varphi})$.

To define our VI, we introduce some auxiliary notation first.
$\mathcal{P}(\mathfrak{C})$ denotes the powerset of $\mathfrak{C}$. For
mappings $X\in\mathfrak{C}^{S}$ and
$\mathcal{X}\in\mathcal{P}(\mathfrak{C})^{S}$ from states to (sets of)
polyhedra, we write $X\ \dot{\in}\ \mathcal{X}$ iff $X(s)\in\mathcal{X}(s)$
for all $s\in S$. Further, we let $\\{X\\}$ be the lifting of $X$ to
$\mathcal{P}(\mathfrak{C})^{S}$, i.e., $\\{X\\}_{s}\vcentcolon=\\{X_{s}\\}$.
Formally, for any fixed CQ $\varphi$ our new VI can be seen as a function
$\Phi\colon\mathcal{P}(\mathfrak{C})^{S}\to\mathcal{P}(\mathfrak{C})^{S}$ and
is defined according to Figure 5. The iteration is started with
$\mathcal{X}^{0}(\varphi)\vcentcolon=\\{X^{0}(\varphi)\\}$, where
$X^{0}(\varphi)$ is the same initial element as for CQ-VI.

######  Lemma 15.

For all $k\geq 0$ we have that
$\bigcap\left(\Phi^{k}(\mathcal{X}^{0})_{s_{0}}\right)=\mathcal{A}^{\forall\exists}(\mathcal{G}^{\leq
k},\varphi)$.

###### Proof (sketch).

It can be shown that for all $k\geq 0$, the set
$\Phi^{k}(\mathcal{X}^{0})_{s_{0}}$ contains the Pareto sets achievable by Eve
in the $k$-step MDPs induced by each possible _deterministic_ $k$-step
strategy $\tau$ of Adam (Appendix C.1). The final intersection over
$\Phi^{k}(\mathcal{X}^{0})_{s_{0}}$ is due to the outer $\forall$-quantifier
in the $\forall\exists$-semantics. ∎

The iteration according to Lemma 15 is essentially equivalent to enumerating
all possible deterministic $k$-step strategies of Adam and analyzing the
induced MDPs. In the worst case, there are doubly exponentially many (in $k$)
such strategies and thus the number of polyhedra
$|\Phi^{k}(\mathcal{X}^{0})_{s}|$ maintained per state $s\in S$ in the $k$-th
step is also at most doubly exponential. This can be improved. In general, not
all $k$-step strategies have to be considered: If for $k$-step strategies
$\tau,\tau^{\prime}$ it holds that the set of points achievable by Eve in the
induced MDP $\mathcal{G}^{\tau}$ is contained in set of points achievable in
$\mathcal{G}^{\tau^{\prime}}$, then only $\tau$ is relevant and
$\tau^{\prime}$ can be discarded. Intuitively, Adam would always
(independently of the thresholds $\vec{x}$) prefer $\tau$ over $\tau^{\prime}$
in such a situation. We can incorporate this observation into our value
iteration: Let
$\mu\colon\mathcal{P}(\mathfrak{C})^{S}\to\mathcal{P}(\mathfrak{C})^{S}$ be
the function that removes the non-inclusion-minimal polyhedra of each
$\mathcal{X}_{s}$. We can then iterate $\mu\circ\Phi$ instead of $\Phi$
without changing the result of the “final intersection” in Lemma 15. We
summarize the overall procedure as Algorithm 1.

######  Theorem 3.

Algorithm 1 is correct.

##### Experiments.

To assess the complexity of Algorithm 1 in practice we have built a
prototypical implementation222Available at
https://doi.org/10.5281/zenodo.5047440 using the Parma Polyhedra Library [5].
We have tested our implementation on a variant of the smart heating example
from [10] that was itself inspired from the case study in [36]. Further, we
consider randomly generated 2-dimensional games with 10 states (see Appendix
C.3 for more details). To determine the relative overhead of our algorithm
compared to CQ-VI we consider the number $n^{k}_{s}$ of polyhedra maintained
at state $s$ in iteration $k$. For the floor heating example we found that
$n^{k}_{s}=1$ for all $k\geq 0$ and $s\in S$, which means that Adam has a
unique optimal strategy from each $s$ and step-bound $k$. Moreover, the game
is determined. For the randomly generated games, we observed that
approximately 90% of them also had $n^{k}_{s}=1$ for all $k\geq 0$ and $s\in
S$. We conjecture that this is indeed a typical situation (as in the floor
heating example), however, 90% might be a too high estimate due to trivial
random games. In the following, we only consider “hard” instances with
$n^{k}_{s}>1$ for at least one state $s$ and some $k\geq 0$. In Table 4, we
report the mean number of polyhedra $\overline{n}^{k}=\frac{1}{|S|}\sum_{s\in
S}n^{k}_{s}$ of 100 “hard” games for various iteration counts $k$. The
empirical average of $\overline{n}^{k}$ over the 100 instances that were
processed within the timeout is given in column $E[\overline{n}^{k}]$ and the
number of timeouts (10 seconds) in column T/O. We have also compared the
algorithm with and without the $\mu$-operation in Line 4 of Algorithm 1
(columns $\mu\circ\Phi$ and $\Phi$, respectively).

In summary, our experiments show that in many cases the necessary number of
polyhedra is low enough to be feasible, often even only 1. In “hard” cases,
our results show that after dozens of iterations the number of polyhedra blows
up dramatically, frequently resulting in a timeout (which is why the numbers
for $\Phi$ decrease after 10 iterations, as only the instances with lower
$\overline{n}^{k}$ finish). This highlights the difficulty of DQs compared to
CQs. Still, using our optimization $\mu$, in many “hard” cases the computation
finishes and the number of polyhedra per state stays below 10, and thus is 2
orders of magnitude smaller than without $\mu$.

Algorithm 1 Value Iteration for CQs in the asserted-exposure
($\forall\exists$) semantics.

1:Game $\mathcal{G}$, (mixed) CQ $\varphi$, horizon $k\geq 0$

2:The horizon-$k$ Pareto set $\mathcal{A}^{\forall\exists}(\mathcal{G}^{\leq
k},\varphi)$

3:$\mathcal{X}\leftarrow\\{X^{0}(\varphi)\\}$ $\triangleright$ Initialization

4:for $i$ from $1$ to $k$ do

5: $\mathcal{X}\leftarrow\Phi(\mathcal{X})$ $\triangleright$ Apply $\Phi$
according to Figure 5

6: $\mathcal{X}\leftarrow\mu(\mathcal{X})$ $\triangleright$ Keep only
$\subseteq$-minima of each $\mathcal{X}_{s}$

7:return $\bigcap\mathcal{X}_{s_{0}}$ $\triangleright$ Intersection of curves
at initial state

Table 3: Experimental results for a fixed timeout of 10s.

| $E[\overline{n}^{k}]$ | T/O
---|---|---
$k$ | $\Phi$ | $\mu\circ\Phi$ | $\Phi$ | $\mu\circ\Phi$
1 | 1.2 | 1.1 | 0 | 0
5 | 16.1 | 1.8 | 0 | 0
10 | 526.3 | 6.8 | 63 | 12
20 | 202.4 | 5.4 | 80 | 30
100 | 78.9 | 2.6 | 90 | 50

##  6 Conclusion and Future Work

We have presented a detailed picture of computational and strategy complexity
of SGs with DQ winning conditions. The results were obtained in part by
providing reductions from CQs to DQs and applying results from the literature.
Future work on the complexity side includes closing the gaps in Tables 1 and
2; however, we conjecture that this requires significant new insights. For
example, a major obstacle towards proving $\mathsf{PSPACE}$ membership of the
quantitative general-strategies DQs problem is that one has to reason about
_exact_ reachability probabilities in the exponentially large goal-unfolding.
It is not at all obvious that the number of bits needed for the rational
representations of these quantities remains polynomially bounded.

We have also argued that DQs are equivalent to CQs in the optimistic
“asserted-exposure” ($\forall\exists$) semantics obtained by changing the
quantification order over strategies—unlike in simple SGs, this makes a
difference since our games are not always determined. Moreover, we have
formulated the first VI-style algorithm for DQs in the standard and CQs in the
$\forall\exists$-semantics. It should be straightforward to extend our
algorithm to expected rewards as well. Another interesting application of the
algorithm is to certify determinacy (for a finite step bound). Regarding
future work, it would be appealing to implement the algorithm in a tool such
as PRISM-games and to experiment with more realistic case studies. Yet another
direction is to investigate (counter-)strategy synthesis for Eve in the
$\forall\exists$-semantics, e.g., by constructing strategy templates where
some choices depend on Adam’s observable strategy.

## References

  * [1]
  * [2] Pranav Ashok, Krishnendu Chatterjee, Jan Kretínský, Maximilian Weininger & Tobias Winkler (2020): _Approximating Values of Generalized-Reachability Stochastic Games_.  In Holger Hermanns, Lijun Zhang, Naoki Kobayashi & Dale Miller, editors: LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, ACM, pp. 102–115, 10.1145/3373718.3394761.
  * [3] Pranav Ashok, Jan Kretínský & Maximilian Weininger (2019): _PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games_.  In Isil Dillig & Serdar Tasiran, editors: Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, Lecture Notes in Computer Science 11561, Springer, pp. 497–519, 10.1007/978-3-030-25540-4_29.
  * [4] Guy Avni & Thomas A. Henzinger (2020): _A Survey of Bidding Games on Graphs (Invited Paper)_.  In Igor Konnov & Laura Kovács, editors: 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), LIPIcs 171, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 2:1–2:21, 10.4230/LIPIcs.CONCUR.2020.2.
  * [5] Roberto Bagnara, Patricia M. Hill & Enea Zaffanella (2008): _The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems_.  Sci. Comput. Program. 72(1-2), pp. 3–21, 10.1016/j.scico.2007.08.001.
  * [6] Christel Baier, Clemens Dubslaff, Sascha Klüppelholz, Marcus Daum, Joachim Klein, Steffen Märcker & Sascha Wunderlich (2014): _Probabilistic Model Checking and Non-standard Multi-objective Reasoning_.  In Stefania Gnesi & Arend Rensink, editors: Fundamental Approaches to Software Engineering - 17th International Conference, FASE 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, Lecture Notes in Computer Science 8411, Springer, pp. 1–16, 10.1007/978-3-642-54804-8_1.
  * [7] Nicolas Basset, Marta Z. Kwiatkowska & Clemens Wiltsche (2014): _Compositional Controller Synthesis for Stochastic Games_.  In Paolo Baldan & Daniele Gorla, editors: CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, Lecture Notes in Computer Science 8704, Springer, pp. 173–187, 10.1007/978-3-662-44584-6_13.
  * [8] Raphaël Berthon, Shibashis Guha & Jean-François Raskin (2020): _Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes_.  In Holger Hermanns, Lijun Zhang, Naoki Kobayashi & Dale Miller, editors: LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, ACM, pp. 195–208, 10.1145/3373718.3394805.
  * [9] Tomás Brázdil, Václav Brozek, Krishnendu Chatterjee, Vojtech Forejt & Antonín Kucera (2014): _Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes_.  Log. Methods Comput. Sci. 10(1), 10.2168/LMCS-10(1:13)2014.
  * [10] Romain Brenguier & Vojtech Forejt (2016): _Decidability Results for Multi-objective Stochastic Games_.  In Cyrille Artho, Axel Legay & Doron Peled, editors: Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, Lecture Notes in Computer Science 9938, pp. 227–243, 10.1007/978-3-319-46520-3_15.
  * [11] Ashok K. Chandra, Dexter Kozen & Larry J. Stockmeyer (1981): _Alternation_.  J. ACM 28(1), pp. 114–133.
  * [12] Krishnendu Chatterjee, Luca de Alfaro & Thomas A. Henzinger (2013): _Strategy improvement for concurrent reachability and turn-based stochastic safety games_.  J. Comput. Syst. Sci. 79(5), pp. 640–657, 10.1016/j.jcss.2012.12.001.
  * [13] Krishnendu Chatterjee & Laurent Doyen (2016): _Perfect-Information Stochastic Games with Generalized Mean-Payoff Objectives_.  In Martin Grohe, Eric Koskinen & Natarajan Shankar, editors: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, ACM, pp. 247–256, 10.1145/2933575.2934513.
  * [14] Krishnendu Chatterjee, Laurent Doyen & Thomas A. Henzinger (2009): _A Survey of Stochastic Games with Limsup and Liminf Objectives_.  In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas & Wolfgang Thomas, editors: Automata, Languages and Programming, 36th Internatilonal Colloquium, ICALP 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part II, Lecture Notes in Computer Science 5556, Springer, pp. 1–15, 10.1007/978-3-642-02930-1_1.
  * [15] Krishnendu Chatterjee, Laurent Doyen & Thomas A. Henzinger (2013): _A survey of partial-observation stochastic parity games_.  Formal Methods Syst. Des. 43(2), pp. 268–284, 10.1007/s10703-012-0164-2.
  * [16] Krishnendu Chatterjee, Vojtech Forejt & Dominik Wojtczak (2013): _Multi-objective Discounted Reward Verification in Graphs and MDPs_.  In Kenneth L. McMillan, Aart Middeldorp & Andrei Voronkov, editors: Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, Lecture Notes in Computer Science 8312, Springer, pp. 228–242, 10.1007/978-3-642-45221-5_17.
  * [17] Krishnendu Chatterjee & Thomas A. Henzinger (2008): _Value Iteration_.  In Orna Grumberg & Helmut Veith, editors: 25 Years of Model Checking - History, Achievements, Perspectives, Lecture Notes in Computer Science 5000, Springer, pp. 107–138, 10.1007/978-3-540-69850-0_7.
  * [18] Krishnendu Chatterjee & Thomas A. Henzinger (2012): _A survey of stochastic $\omega$-regular games_.  J. Comput. Syst. Sci. 78(2), pp. 394–413, 10.1016/j.jcss.2011.05.002.
  * [19] Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger & Tobias Winkler (2020): _Stochastic Games with Lexicographic Reachability-Safety Objectives_.  In Shuvendu K. Lahiri & Chao Wang, editors: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, Lecture Notes in Computer Science 12225, Springer, pp. 398–420, 10.1007/978-3-030-53291-8_21.
  * [20] Krishnendu Chatterjee, Zuzana Kretínská & Jan Kretínský (2017): _Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes_.  Log. Methods Comput. Sci. 13(2), 10.23638/LMCS-13(2:15)2017.
  * [21] Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis & Clemens Wiltsche (2013): _On Stochastic Games with Multiple Objectives_.  In Krishnendu Chatterjee & Jirí Sgall, editors: Mathematical Foundations of Computer Science 2013 - 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings, Lecture Notes in Computer Science 8087, Springer, pp. 266–277, 10.1007/978-3-642-40313-2_25.
  * [22] Taolue Chen, Marta Z. Kwiatkowska, Aistis Simaitis & Clemens Wiltsche (2013): _Synthesis for Multi-objective Stochastic Games: An Application to Autonomous Urban Driving_.  In Kaustubh R. Joshi, Markus Siegle, Mariëlle Stoelinga & Pedro R. D’Argenio, editors: Quantitative Evaluation of Systems - 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, Lecture Notes in Computer Science 8054, Springer, pp. 322–337, 10.1007/978-3-642-40196-1_28.
  * [23] Anne Condon (1990): _On Algorithms for Simple Stochastic Games_.  In Jin-Yi Cai, editor: Advances In Computational Complexity Theory, Proceedings of a DIMACS Workshop, New Jersey, USA, December 3-7, 1990, DIMACS Series in Discrete Mathematics and Theoretical Computer Science 13, DIMACS/AMS, pp. 51–71, 10.1090/dimacs/013/04.
  * [24] Anne Condon (1992): _The Complexity of Stochastic Games_.  Inf. Comput. 96(2), pp. 203–224, 10.1016/0890-5401(92)90048-K.
  * [25] Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann & Mickael Randour (2020): _Simple Strategies in Multi-Objective MDPs_.  In Armin Biere & David Parker, editors: Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, Lecture Notes in Computer Science 12078, Springer, pp. 346–364, 10.1007/978-3-030-45190-5_19.
  * [26] Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi & Mihalis Yannakakis (2008): _Multi-Objective Model Checking of Markov Decision Processes_.  Log. Methods Comput. Sci. 4(4), 10.2168/LMCS-4(4:8)2008.
  * [27] Kousha Etessami & Mihalis Yannakakis (2006): _Efficient Qualitative Analysis of Classes of Recursive Markov Decision Processes and Simple Stochastic Games_.  In Bruno Durand & Wolfgang Thomas, editors: STACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23-25, 2006, Proceedings, Lecture Notes in Computer Science 3884, Springer, pp. 634–645, 10.1007/11672142_52.
  * [28] Lu Feng, Clemens Wiltsche, Laura R. Humphrey & Ufuk Topcu (2015): _Controller synthesis for autonomous systems interacting with human operators_.  In Alexandre M. Bayen & Michael S. Branicky, editors: Proceedings of the ACM/IEEE Sixth International Conference on Cyber-Physical Systems, ICCPS 2015, Seattle, WA, USA, April 14-16, 2015, ACM, pp. 70–79, 10.1145/2735960.2735973.
  * [29] Nathanaël Fijalkow & Florian Horn (2010): _The surprizing complexity of reachability games_.  CoRR abs/1010.2420.  Available at http://arxiv.org/abs/1010.2420.
  * [30] Jerzy A Filar, Dmitry Krass & Keith W Ross (1995): _Percentile performance criteria for limiting average Markov decision processes_.  IEEE Transactions on Automatic Control 40(1), pp. 2–10, 10.1109/9.362904.
  * [31] Vojtech Forejt, Marta Z. Kwiatkowska, Gethin Norman, David Parker & Hongyang Qu (2011): _Quantitative Multi-objective Verification for Probabilistic Systems_.  In Parosh Aziz Abdulla & K. Rustan M. Leino, editors: Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, Lecture Notes in Computer Science 6605, Springer, pp. 112–127, 10.1007/978-3-642-19835-9_11.
  * [32] Jan Kretínský, Emanuel Ramneantu, Alexander Slivinskiy & Maximilian Weininger (2020): _Comparison of Algorithms for Simple Stochastic Games_.  In Jean-François Raskin & Davide Bresolin, editors: Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020, EPTCS 326, pp. 131–148, 10.4204/EPTCS.326.9.
  * [33] Marta Kwiatkowska, Gethin Norman, David Parker & Gabriel Santos (2020): _Multi-player Equilibria Verification for Concurrent Stochastic Games_.  In Marco Gribaudo, David N. Jansen & Anne Remke, editors: Quantitative Evaluation of Systems - 17th International Conference, QEST 2020, Vienna, Austria, August 31 - September 3, 2020, Proceedings, Lecture Notes in Computer Science 12289, Springer, pp. 74–95, 10.1007/978-3-030-59854-9_7.
  * [34] Marta Kwiatkowska, Gethin Norman, David Parker & Gabriel Santos (2020): _PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time_.  In Shuvendu K. Lahiri & Chao Wang, editors: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, Lecture Notes in Computer Science 12225, Springer, pp. 475–487, 10.1007/978-3-030-53291-8_25.
  * [35] Marta Kwiatkowska, David Parker & Clemens Wiltsche (2018): _PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives_.  Int. J. Softw. Tools Technol. Transf. 20(2), pp. 195–210, 10.1007/s10009-017-0476-z.
  * [36] Kim G. Larsen, Marius Mikucionis, Marco Muñiz, Jirí Srba & Jakob Haahr Taankvist (2016): _Online and Compositional Learning of Controllers with Application to Floor Heating_.  In Marsha Chechik & Jean-François Raskin, editors: Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Lecture Notes in Computer Science 9636, Springer, pp. 244–259, 10.1007/978-3-662-49674-9_14.
  * [37] Mickael Randour, Jean-François Raskin & Ocan Sankur (2017): _Percentile queries in multi-dimensional Markov decision processes_.  Formal Methods Syst. Des. 50(2-3), pp. 207–248, 10.1007/s10703-016-0262-7.
  * [38] Lloyd S Shapley (1953): _Stochastic games_.  Proceedings of the national academy of sciences 39(10), pp. 1095–1100, 10.1073/pnas.39.10.1095.
  * [39] Yaron Velner (2015): _Robust Multidimensional Mean-Payoff Games are Undecidable_.  In Andrew M. Pitts, editor: Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Lecture Notes in Computer Science 9034, Springer, pp. 312–327, 10.1007/978-3-662-46678-0_20.

##  Appendix A Full proofs of Section 3

###  A.1 Proof of Lemma 1

See 1

###### Proof.

By [21, Theorem 7], MD strategies are sufficient for quantitative DQs with
_expected reward_ objectives (see the formal definition in [21]). We reduce
our reachability and safety objectives to expected reward objectives in the
goal-unfolding. More formally, given a mixed DQ with $n$ objectives, each of
which is either reachability or safety, we define the reward functions
$r_{i}\colon S\to\mathbb{R}$, $i=1,\ldots,n$, as follows: For each
reachability objective $\lozenge T_{i}$, we grant reward $r_{i}(s)=1$ if
$T_{i}$ is visited in $s$ _for the first time_ , and $r_{i}(s)=0$ for all
other $s$. Similarly, for each safety objective $\square T_{i}$, we grant
reward $r_{i}(s)=-1$ if the unsafe set $S\setminus T_{i}$ is visited in $s$
_for the first time_ , and again $r_{i}(s)=0$ for all other $s$. Then under
any pair $\sigma,\tau$ of strategies, $\mathbb{P}^{\sigma,\tau}(\lozenge
T_{i})\geq x_{i}$ iff $\mathbb{E}^{\sigma,\tau}(r_{i})\geq x_{i}$ and
$\mathbb{P}^{\sigma,\tau}(\square T_{i})\geq x_{i}$ iff
$\mathbb{E}^{\sigma,\tau}(r_{i})\geq x_{i}-1$, where
$\mathbb{E}^{\sigma,\tau}(r_{i})$ denotes the expected value of reward
function $r_{i}$ assuming $\sigma,\tau$ are fixed. The result follows noticing
that any strategy of Eve in the goal-unfolding can be identified with a
strategy using $2^{n}$ memory in the original game. This can be slightly
lowered to $2^{n}{-}1$ because Eve’s behavior in the final stage of the
unfolding where _all_ targets/unsafe sets have been visited is irrelevant. ∎

###  A.2 Proof of Lemma 2

See 2

###### Proof.

We first show the following auxiliary claim: Any achieving strategy $\sigma$
of Eve for the qualitative DQ $\bigvee_{i=1}^{n}\mathbb{P}(\star_{i}T_{i})\geq
1$ satisfies

$\exists
i\in\\{1,\ldots,n\\},\forall\tau\colon\mathbb{P}^{\sigma,\tau}(\star_{i}T_{i})\geq
1~{}.$ (2)

Towards contradiction assume (2) does not hold. Then for all $T_{i}$,
$i=1,\ldots,n$, there exists a $\tau_{i}$ such that
$\mathbb{P}^{\sigma,\tau_{i}}(\star_{i}T_{i})<1$. Let $\tau$ be the strategy
of Adam that at the beginning of the game selects one of the strategies
$\tau_{i}$ uniformly at random and follows this strategy for the remaining
play. Note that this $\tau$ uses stochastic memory update. But then _for each_
$T_{i}$,
$\mathbb{P}^{\sigma,\tau}(\star_{i}T_{i})=\frac{1}{n}\sum_{j=1}^{n}\mathbb{P}^{\sigma,\tau_{j}}(\star_{i}T_{i})\leq\frac{n-1}{n}+\frac{1}{n}\mathbb{P}^{\sigma,\tau_{i}}(\star_{i}T_{i})<1$,
contradiction. Hence by (2), Eve can play optimal for _one specific_ target
and ignore the others. MD strategies suffice for this [23]. ∎

###  A.3 Proof of Lemma 3

See 3

###### Proof.

Let $n\geq 2$ as the claim is trivially true for $n=1$. We recall the
construction of $\mathcal{G}^{\prime}$ from the main text: The original game
$\mathcal{G}$ is only played with probability $\nicefrac{{1}}{{2}}$. With the
remaining $\nicefrac{{1}}{{2}}$, Adam freely chooses one of the $n$ targets
$T_{1},\ldots,T_{n}$, after which the game ends immediately (Figure 2, left).
If a strategy $\sigma$ of Eve achieves the CQ $\varphi$ in $\mathcal{G}$, it
follows that at least one $T_{i}$ is visited with probability $1$ if Adam has
to resolve his extra choice deterministically. Otherwise, if randomization is
allowed, then for all strategies $\tau^{\prime}$ of Adam in
$\mathcal{G}^{\prime}$ at least one $T_{i}$ is visited with probability
$\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge
T_{i})\geq\frac{1}{2}+\frac{1}{2n}$. This means that $\sigma$ achieves the
_qualitative_ DQ
$\varphi^{\prime}_{qual}\vcentcolon=\bigvee_{i=1}^{n}\mathbb{P}(\lozenge
T_{i})\geq 1$ in the deterministic-strategies case, and the _quantitative_ DQ
$\varphi^{\prime}_{quant}\vcentcolon=\bigvee_{i=1}^{n}\mathbb{P}(\lozenge
T_{i})\geq\frac{1}{2}+\frac{1}{2n}$ in the general-strategies case. On the
other hand, if $\sigma$ does not achieve the CQ $\varphi$, then Adam can
ensure with some counter-strategy $\tau$ that at least one $T_{i}$, $1\leq
i\leq n$, is visited with probability $\delta<1$ in the game
$\mathcal{G}^{\sigma}$. In the deterministic-strategies case, he can extend
$\tau$ to a strategy $\tau^{\prime}$ in $\mathcal{G}^{\prime}$ by resolving
the additional choice with $T_{i}$. Then
$\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge
T_{j})\leq\frac{1}{2}\delta+\frac{1}{2}<1$ for all $j=1,\ldots,n$ which proves
that $\sigma$ does not achieve the DQ $\varphi^{\prime}_{qual}$. In the
general-strategies case, Adam can define $\tau^{\prime}$ by selecting $T_{i}$
with probability $\frac{1}{n}+x$, where $0<x<1{-}\delta$ and all other
$T_{j}$, $j\neq i$, with probability $\frac{1}{n}-\frac{x}{n-1}$. Target
$T_{i}$ is reached with probability equal to

$\displaystyle\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge T_{i})$
$\displaystyle=\frac{1}{2}\big{(}\frac{1}{n}+x\big{)}+\frac{1}{2}\delta$
$\displaystyle<\frac{1}{2}\big{(}\frac{1}{n}+(1-\delta)\big{)}+\frac{1}{2}\delta\qquad\text{(as
$1-\delta<1$)}$ $\displaystyle=\frac{1}{2n}+\frac{1}{2}~{}.$

Each other target $T_{j}$, $j\neq i$, is reached with probability at most

$\displaystyle\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge T_{j})$
$\displaystyle\leq\frac{1}{2}\big{(}\frac{1}{n}-\frac{x}{n-1}\big{)}+\frac{1}{2}$
$\displaystyle<\frac{1}{2n}+\frac{1}{2}\qquad\text{(as $x>0$)}~{}.$

Thus $\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge
T_{j})<\frac{1}{2}+\frac{1}{2n}$ for all $j=1,\ldots,n$, implying that Eve’s
strategy $\sigma$ does also not achieve the quantitative DQ
$\varphi^{\prime}_{quant}$. ∎

###  A.4 Proof of Lemma 4

See 4

###### Proof.

As explained in [29], in the deterministic-strategies case Eve achieves the
qualitative CQ $\bigwedge_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq 1$ in the
game sketched in Figure 7 with the following strategy $\sigma$ using $2^{n}-1$
memory: She remembers exactly the set of “petals” that have been visited at
any particular moment during a play. If petal $i$ is visited for the first
time, she visits the corresponding target $T_{i}$, returning control to Adam.
If petal $i$ is visited for the second time, she plays the choice that leads
to the sink, thereby visiting all targets $T_{j}$, $j\neq i$, and the game
ends.

First observe that this is an achieving strategy even if Adam is allowed to
use randomization. Assume that Adam has a randomized counter-strategy $\tau$
in the finite MDP $\mathcal{G}^{\sigma}$. Then there exists some $T_{i}$ such
that $\mathbb{P}^{\sigma,\tau}(\lozenge T_{i})<1$. But since MD strategies are
sufficient for minimizing reachability probabilities in finite MDPs, it
follows that there exists an MD strategy $\tau^{\prime}$ such that
$\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge
T_{i})\leq\mathbb{P}^{\sigma,\tau}(\lozenge T_{i})<1$. This is a contradiction
to the fact that $\sigma$ reaches each target certainly under deterministic
strategies.

It remains to show that there is no randomized achieving strategy of Eve using
less than $2^{n}-1$ memory. To this end let $\sigma$ be a (possibly
randomized) strategy of Eve using less than $2^{n}-1$ memory. Similar to the
proof in [29], for each memory state $m$ of $\sigma$ we define the set of
petals $S_{m}\subseteq\\{1,\ldots,n\\}$ as the petals where $\sigma$ would
stop the play _with positive probability_ if Adam would choose one of them
next. Then there exists $X\subsetneq\\{1,\ldots,n\\}$ such that $S_{m}\neq X$
for all memory states $m$. But then Adam wins with a strategy $\tau$ that
always moves the token to a petal in $(X\setminus S_{m})\cup(S_{m}\setminus
X)\neq\emptyset$: There are two cases:

  * •

In each round, $\tau$ selects a petal $i\in X\setminus S_{m}$. Then the game
runs forever with probability 1 and only the targets corresponding to the
petals in $X$ are visited. Thus Eve loses.

  * •

After some finite number of rounds, $\tau$ selects a petal $i\in
S_{m}\setminus X$ for the first time. Then up to this point, only targets
corresponding to petals in $X$ have been visited. In particular, $T_{i}$ has
not been visited yet. Eve then loses because she moves the token with positive
probability to a sink that is not contained in $T_{i}$.

To conclude the proof, we use Lemma 3.1 to reduce each $\mathcal{G}_{n}$ to an
SG with a _quantitative reachability DQ_ where Eve’s winning strategies are
the same as those in the original $\mathcal{G}$, i.e., they require at least
$2^{n}{-}1$ memory. ∎

$T_{1}$$T_{2,3,4}$$T_{2}$$T_{1,3,4}$$T_{3}$$T_{1,2,4}$$T_{4}$$T_{1,2,3}$
Figure 7: The (deterministic) game from [29, Lemma 2] for $n=4$ targets.

###  A.5 Proof of Lemma 5

See 5

A: Env. chooses $\mathcal{T}_{1}$startB: Eve chooses
$\mathcal{T}_{2}$$\mathcal{T}$C: Adam chooses $n{-}|\mathcal{T}_{2}|{-}1$
targets$p(\mathcal{T}_{2})$$1-p(\mathcal{T}_{2})$ Figure 8:  For convenience,
we repeat here the right side of Figure 2, i.e., the Game constructed in the
proof of Lemma 5. The probability $p(\mathcal{T}_{2})$ increases with
$|\mathcal{T}_{2}|$. Eve must select exactly $\mathcal{T}_{2}=\mathcal{T}_{1}$
in Stage B to avoid visiting at least one of the targets in $\mathcal{T}$ with
maximal probability.

###### Proof.

For every $n\geq 1$ we describe a game with a safety DQ of the form
$\varphi=\bigvee_{i=1}^{n}\mathbb{P}(\square\overline{T_{i}})\geq x$ where
achieving strategies of Eve need at least $2^{n}-1$ memory. Note that the
objectives $\mathbb{P}(\square\overline{T_{i}})\geq x$ read “avoid $T_{i}$
with probability at least $x$”. Also note that the threshold $x$ is the same
for all objectives. Let $\mathcal{T}\vcentcolon=\\{T_{1},\ldots,T_{n}\\}$. The
game is as follows (Figure 8): In Stage A, the environment chooses one of the
$2^{n}-1$ combinations $\mathcal{T}_{1}\subsetneq\mathcal{T}$ uniformly at
random and visits all targets in the chosen $\mathcal{T}_{1}$, thereby
spoiling the objectives $\square\overline{T}$ for all $T\in\mathcal{T}_{1}$.
In Stage B, Eve then freely selects another such combination
$\mathcal{T}_{2}\subsetneq\mathcal{T}$. Depending on $\mathcal{T}_{2}$, a coin
with bias $p(\mathcal{T}_{2})$ is tossed: With a certain _penalty_ probability
$p(\mathcal{T}_{2})$, all targets $\mathcal{T}$ are visited immediately, and
with the remaining probability the game enters Stage C where Adam chooses any
probability distribution over combinations of at most $n-|\mathcal{T}_{2}|-1$
targets. The penalty $p(\mathcal{T}_{2})$ is strictly monotonically increasing
in $|\mathcal{T}_{2}|$, that is, selecting a larger set $\mathcal{T}_{2}$
involves more risk from Eve’s perspective.

Intuitively, the idea is that one can find a threshold $x$ in $\varphi$, such
that Eve must select _exactly_ $\mathcal{T}_{2}=\mathcal{T}_{1}$ in Stage B.
This clearly requires $2^{n}-1$ memory as all possible combinations
$\mathcal{T}_{1}\subsetneq\mathcal{T}$ need to be remembered. This behavior is
enforced as follows. There are two cases: (a) If
$|\mathcal{T}_{2}|<|\mathcal{T}_{1}\cup\mathcal{T}_{2}|$ then
$n-|\mathcal{T}_{2}|-1\geq n-|\mathcal{T}_{1}\cup\mathcal{T}_{2}|$ and so Adam
can visit all the remaining targets
$\mathcal{T}\setminus(\mathcal{T}_{1}\cup\mathcal{T}_{2})$ in Stage C, which
is undesirable from Eve’s point of view. (b) Otherwise
$|\mathcal{T}_{2}|\geq|\mathcal{T}_{1}\cup\mathcal{T}_{2}|$ which implies
$\mathcal{T}_{2}\supseteq\mathcal{T}_{1}$. In this case, if the game reaches
Stage C, at least one target will be avoided with positive probability. In
order to offer an incentive for Eve to not simply choose an arbitrary
$\mathcal{T}_{2}\supseteq\mathcal{T}_{1}$, we impose a higher penalty
probability on larger sets $\mathcal{T}_{2}$. Then the _unique_ optimal
strategy $\sigma^{*}$ (the one that maximizes the highest achievable threshold
probability $x$) of Eve consists in choosing exactly
$\mathcal{T}_{2}=\mathcal{T}_{1}$.

More formally, suppose that Eve fixes the strategy $\sigma^{*}$ described
above. For any counter-strategy of $\tau$ let $X^{\tau}$ be the random
variable describing the number of different visited targets. We can consider a
counter-strategy $\tau$ that maximizes the expected value $E[X^{\tau}]$ (such
a $\tau$ exists because $\mathcal{G}^{\sigma^{*}}$ is just a finite MDP). Then
since the game and the strategy $\sigma^{*}$ are completely symmetric with
respect to all targets, there is a maximal probability $y=E[X^{\tau}]/n$ such
that Adam can achieve $\bigwedge_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq y$ in
the induced MDP $\mathcal{G}^{\sigma^{*}}$. Indeed, if he could achieve
$\bigwedge_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq z$ for some $z>y$, then
$E[X^{\tau}]\geq nz>ny=E[X^{\tau}]$, which is a contradiction. Consequently,
$\sigma^{*}$ achieves the DQ
$\bigvee_{i=1}^{n}\mathbb{P}(\square\overline{T_{i}})\geq x$ with
$x\vcentcolon=1-y$.

On the other hand, if Eve plays any strategy $\sigma\neq\sigma^{*}$ we can
consider each possible combination $\mathcal{T}_{1}\subsetneq\mathcal{T}$
chosen in Stage A separately: If
$|\mathcal{T}_{2}|<|\mathcal{T}_{1}\cup\mathcal{T}_{2}|$ (case (a) from above)
then Adam can enforce visiting _all_ targets with probability 1 as explained
earlier. If $|\mathcal{T}_{2}|\geq|\mathcal{T}_{1}\cup\mathcal{T}_{2}|$ and
hence $\mathcal{T}_{2}\supseteq\mathcal{T}_{1}$ (case (b) from above) then
nothing changes compared to playing $\sigma^{*}$ if $\sigma$ actually selects
$\mathcal{T}_{2}=\mathcal{T}_{1}$, i.e., behaves exactly like $\sigma^{*}$
given $\mathcal{T}_{1}$ (which is possible). However, if $\sigma$ selects
$\mathcal{T}_{2}\supsetneq\mathcal{T}_{1}$ then for the penalties we have
$p(\mathcal{T}_{2})>p(\mathcal{T}_{1})$ which means that also in this case,
the probability to reach each individual target is strictly larger than if
$\mathcal{T}_{2}=\mathcal{T}_{1}$ had been selected by $\sigma$. Overall, Adam
can enforce $\bigwedge_{i=1}^{n}\mathbb{P}(\lozenge T_{i})\geq z$ for some
$z>y$ because for at least one combination $\mathcal{T}_{1}$ selected in Stage
A, $\sigma$ differs from $\sigma^{*}$ with positive probability. ∎

###  A.6 Proof of Lemma 6

See 6

###### Proof.

We describe the construction for qualitative reachability DQs. Let $n=2q$ be
even. The game $\mathcal{G}$ comprises three stages, A, B, and C. In the
initial stage A, Adam specifies a combination $\mathcal{T}_{A}$ of $q$
different targets. Those are then visited with probability
$\nicefrac{{1}}{{2}}$ and the game ends. With the remaining probability of
$\nicefrac{{1}}{{2}}$, the game moves on to stage B which is similar to stage
A, but controlled by Eve. Let $\mathcal{T}_{B}$ be the set of $q$ targets that
Eve specifies in this stage. Consequently, with total probability
$\nicefrac{{1}}{{4}}$, the game enters the final stage C where Adam chooses
and visits $q+1$ different targets $\mathcal{T}_{C}$. Note that this game can
be constructed such that all target states are sinks.

Observe that a target is visited with probability $1$ iff it is chosen in all
three stages. The only achieving strategy of Eve consists in selecting exactly
$\mathcal{T}_{B}=\mathcal{T}_{A}$, requiring ${n\choose q}$ memory. On the one
hand, this strategy achieves the DQ because
$\mathcal{T}_{A}\cap\mathcal{T}_{B}\cap\mathcal{T}_{C}\neq\emptyset$, hence
there is a target that is selected in all three stages and thus visited with
probability $1$. Note that, in agreement with Lemma 1, the above argument does
not work if Adam is allowed to use randomization. On the other hand, if
$\mathcal{T}_{B}\neq\mathcal{T}_{A}$, then Adam can select any $q{+}1$-element
subset of $\mathcal{T}\setminus(\mathcal{T}_{A}\cap\mathcal{T}_{B})$ in stage
C, eliminating the possibility that any of the targets is selected in all
three stages.

To conclude the proof, observe that the construction can be adapted for
qualitative safety DQs: Let $Sinks(\mathcal{G})$ be the set of all sinks in
$\mathcal{G}$. For each $T\in\mathcal{T}$, we define a safe set
$T^{\prime}\vcentcolon=T\cup(S\setminus Sinks(\mathcal{G}))$. Then for all
such $T^{\prime}$, the safety objective $\mathbb{P}(\square T^{\prime})\geq 1$
is satisfied iff $T^{\prime}$ is selected in all three stages. ∎

###  A.7 Proof of Lemma 7

See 7

###### Proof.

The proofs parallels the one of Lemma 3. Let $n\geq 2$ as the claim is
trivially true for $n=1$. We also assume that $x_{i}>0$ for all
$i=1,\ldots,n$. The game $\mathcal{G}^{\prime}$ is the same as in Lemma 3.
Suppose that $\sigma$ is a deterministic strategy of Eve that achieves
$\varphi$ in $\mathcal{G}$. Let $\tau$ be any counter-strategy of Adam in
$\mathcal{G}^{\prime}$ and suppose that it (deterministically) resolves the
extra choice by moving to $T_{i}$, for some $i$. Then
$\mathbb{P}^{\sigma,\tau}(\lozenge T_{i})\geq\frac{1}{2}x_{i}+\frac{1}{2}$ as
$\sigma$ achieves $\varphi$ in the original $\mathcal{G}$. Thus $\sigma$
achieves the DQ
$\varphi^{\prime}\vcentcolon=\bigvee_{i=1}^{n}\mathbb{P}(\lozenge
T_{i})\geq\frac{1}{2}x_{i}+\frac{1}{2}$ in $\mathcal{G}^{\prime}$.

Conversely, if $\sigma$ does not achieve $\varphi$ in $\mathcal{G}$, then
there exists some $1\leq i\leq n$ such that Adam has a counter-strategy $\tau$
satisfying $\mathbb{P}^{\sigma,\tau}(\lozenge T_{i})<x_{i}$. We extend this
$\tau$ to a strategy $\tau^{\prime}$ in $\mathcal{G}^{\prime}$ by selecting
$T_{i}$ at the additional state. Then in $\mathcal{G}^{\prime}$,
$\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge
T_{i})<\frac{1}{2}x_{i}+\frac{1}{2}$ and
$\mathbb{P}^{\sigma,\tau^{\prime}}(\lozenge
T_{j})\leq\frac{1}{2}<\frac{1}{2}x_{j}+\frac{1}{2}$ for all other targets
$j\neq i$. Therefore $\sigma$ does not achieve $\varphi^{\prime}$ in
$\mathcal{G}^{\prime}$ and the proof is complete. ∎

##  Appendix B Full proofs of Section 4

###  B.1 Proof of Lemma 11

See 11

###### Proof.

We show that the complement of the quantitative safety DQ feasibility problem
is $\mathsf{PSPACE}$-hard which proves our result as $\mathsf{PSPACE}$ is
closed under complement. Consider an MDP $\mathcal{G}$ with
$S_{\mathsf{E}}=\emptyset$. Let $\mathcal{G}^{\prime}$ be like the MDP
$\mathcal{G}$ but with $S_{\mathsf{E}}$ and $S_{\mathsf{A}}$ exchanged. For
any quantitative safety DQ $\varphi=\bigvee_{i=1}^{n}\mathbb{P}(\square
T_{i})\geq x_{i}$ it holds that

$\varphi$ is not achievable in $\mathcal{G}$ $\displaystyle\iff$
$\displaystyle\neg\exists\sigma\forall\tau\colon\bigvee_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\square
T_{i})\geq x_{i}$ $\displaystyle\iff$
$\displaystyle\forall\sigma\exists\tau\colon\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\square
T_{i})<x_{i}$ $\displaystyle\iff$
$\displaystyle\forall\sigma\exists\tau\colon\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge\overline{T_{i}})>1{-}x_{i}$
$\displaystyle\iff$
$\displaystyle\exists\tau\colon\bigwedge_{i=1}^{n}\mathbb{P}^{\tau}(\lozenge\overline{T_{i}})>1{-}x_{i}$
(because $S_{\mathsf{E}}=\emptyset$) $\displaystyle\iff$ the CQ
$\bigwedge_{i=1}^{n}\mathbb{P}(\lozenge\overline{T_{i}})>1{-}x_{i}$ with
strict bounds is achievable in $\mathcal{G}^{\prime}$

It only remains to show that the quantitative reachability CQ feasibility
problem with _strict bounds_ is $\mathsf{PSPACE}$-hard in games with
$S_{\mathsf{A}}=\emptyset$, i.e., MDPs where only Eve has choices. To this end
we analyze the reduction from [37, Lem. 2] (restated in Figure 9) which shows
that the qualitative reachability CQ feasibility problem in MDPs is
$\mathsf{PSPACE}$-hard in greater detail.

$x_{1}$$f_{1}$$t_{1}$$x_{2}$$f_{2}$$t_{2}$$\cdots$$x_{n}$$f_{n}$$t_{n}$$\nicefrac{{1}}{{2}}$$\nicefrac{{1}}{{2}}$
Figure 9:  The MDP from [37, Lem. 2] constructed from a quantified Boolean
formula (QBF) $\exists x_{1}\forall x_{2}\exists x_{3}\ldots\forall
x_{m-1}\exists x_{m}\colon C_{1}\wedge C_{2}\wedge\ldots\wedge C_{n}$ where
each clause $C_{i}$ is a disjunction of three literals from the set
$\\{x_{i},\,\overline{x_{i}}\mid i\in\\{1,\ldots,m\\}\\}$. The target sets are
$T_{i}\vcentcolon=\\{t_{j}\mid x_{j}\in
C_{i}\\}\cup\\{f_{j}\mid\overline{x_{j}}\in C_{i}\\}$ for all
$i\in\\{1,\ldots,n\\}$ and $j\in\\{1,\ldots,m\\}$. It was proved in [37] that
the QBF is true iff the qualitative reachability CQ
$\bigwedge_{i=1}^{m}\mathbb{P}(\lozenge T_{i})\geq 1$ is achievable.

We claim that the QBF is true iff the strict-bounds query
$\varphi_{>}\vcentcolon=\bigwedge_{i=1}^{m}\mathbb{P}(\lozenge
T_{i})>1-\frac{2^{-n}}{m}$ is achievable in the constructed MDP.

It was already shown in the proof of [37, Lem. 2] that if the QBF is true,
then even the qualitative query $\bigwedge_{i=1}^{m}\mathbb{P}(\lozenge
T_{i})\geq 1$ is achievable, and thus also our quantitative strict-bounds
query $\varphi_{>}$.

For the other direction assume that the QBF is false. Then for all
$\exists$-strategies in the “formula game”, there is a counter-strategy of the
$\forall$-player such that at least one clause is not satisfied. Let $\sigma$
be an arbitrary (possibly randomized) strategy of Eve in the constructed MDP.
We overload $\lozenge T$ and interpret it as the _event_ that $T$ is reached.
Formally, $\lozenge T$ can still be regarded a _set_ of paths. Thus the event
$\bigcap_{i=1}^{m}\lozenge T_{i}$ indicates that _all_ $m$ targets are
reached, and $\mathbb{P}^{\sigma}(\bigcap_{i=1}^{m}\lozenge T_{i})$ is the
probability of that event. We have

$\mathbb{P}^{\sigma}(\bigcap_{i=1}^{m}\lozenge T_{i})\leq 1-2^{-n}$ (3)

because no matter the behavior of $\sigma$, there is at least a probability of
$2^{-n}$ that the environment makes the “right” choices that make the formula
false. In the MDP this means that at least one target is not visited with
probability at least $2^{-n}$ or, equivalently, that all targets are visited
with probability at most $1-2^{-n}$. The following inequalities complete the
proof:

$\displaystyle\mathbb{P}^{\sigma}(\bigcap_{i=1}^{m}\lozenge T_{i})$
$\displaystyle=$ $\displaystyle
1-\mathbb{P}^{\sigma}(\bigcup_{i=1}^{m}\square\overline{T_{i}})$ (probability
of complement) $\displaystyle\geq$ $\displaystyle
1-\sum_{i=1}^{m}\mathbb{P}^{\sigma}(\square\overline{T_{i}})$ (union bound)
$\displaystyle=$
$\displaystyle\sum_{i=1}^{m}(1-\mathbb{P}^{\sigma}(\square\overline{T_{i}}))-(m-1)$
(arithmetic) $\displaystyle=$
$\displaystyle\sum_{i=1}^{m}\mathbb{P}^{\sigma}(\lozenge T_{i})-(m-1)$
(probability of complement)

and thus with (3) we obtain

$\sum_{i=1}^{m}\mathbb{P}^{\sigma}(\lozenge
T_{i})\leq\mathbb{P}^{\sigma}(\bigcap_{i=1}^{m}\lozenge T_{i})+m-1\leq
1-2^{-n}+m-1=m-2^{-n}~{}.$

From this it follows that

$\min_{i=1,\ldots,m}\mathbb{P}^{\sigma}(\lozenge
T_{i})\leq\frac{m-2^{-n}}{m}=1-\frac{2^{-n}}{m}<1~{}.$

Thus since $\sigma$ was arbitrary, we have shown that
$\forall\sigma\bigvee_{i=1}^{m}\mathbb{P}^{\sigma}(\lozenge T_{i})\leq
1-\frac{2^{-n}}{m}$ which is equivalent to saying that the query $\varphi_{>}$
defined above is not achievable. ∎

###  B.2 Proof of Lemma 12

See 12

###### Proof.

We reduce from the problem of deciding truth of a quantified Boolean formula
(QBF). A QBF is an expression $Q_{1}x_{1}Q_{2}x_{2}\ldots
Q_{m}x_{m}\colon\psi$ with $Q_{i}\in\\{\exists,\forall\\}$ for all
$i=1,\ldots,m$ and where $\psi$ is a Boolean formula with variables
$x_{1},\ldots,x_{m}$. Deciding truth of a QBF is known to be
$\mathsf{PSPACE}$-hard already when $\psi$ is in CNF. Consequently, since
$\mathsf{PSPACE}$ is closed under complement, the problem is
$\mathsf{PSPACE}$-hard for $\psi$ in DNF as well.

Given a QBF with $\psi=t_{1}\vee\ldots\vee t_{n}$ in DNF, we construct the
following game $\mathcal{G}_{\psi}$ (see Figure 4 for an example): There is a
target $T_{j}$ for each term $t_{j}$, $j=1,\ldots,n$, of $\psi$. Moreover,
there is a state $s_{i}$ for each variable $x_{i}$ such that $s_{i}\in
S_{\mathsf{E}}$ if $Q_{i}=\exists$ and $s_{i}\in S_{\mathsf{A}}$ if
$Q_{i}=\forall$. For all $i=1,\ldots,m$, $s_{i}$ has exactly two successors
$x_{i},\overline{x_{i}}\in S_{\mathsf{P}}$. Each $x_{i}$ (resp.
$\overline{x_{i}}$) leads with probability $\nicefrac{{1}}{{2}}$ to a state
where exactly the targets $T_{j}$ such that either (i) the literal $x_{i}$
(resp. $\overline{x_{i}}$) occurs in $t_{j}$ or (ii) the variable $x_{i}$ does
not occur at all in $t_{j}$ are satisfied. With the remaining probability of
$\nicefrac{{1}}{{2}}$, the game moves on the next $s_{i+1}$ (except if $i=m$,
in which case the game stays in $x_{m}$, respectively $\overline{x_{m}}$).
Clearly, this game can be constructed in polynomial time in the size of the
QBF.

As explained in [29], the deterministic strategies in $\mathcal{G}_{\psi}$ are
in one-to-one correspondence with the “strategies” assigning the values in the
_formula game_ $Q_{1}x_{1}Q_{2}x_{2}\ldots Q_{m}x_{m}\colon\psi$. Note that
the increase in quantifier alternations (up to $m-1$ many) in the formula game
compared to the standard DQ semantics (one alternation) is because in an SG,
players can remember the whole history and thus react to the opponent’s past
choices.

In the game $\mathcal{G}_{\psi}$, for each (deterministic) strategy pair
$\sigma,\tau$, it holds that
$\bigvee_{j=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge T_{j})\geq 1$ iff there is
at least one term $t_{j}$ such that $\sigma$ and $\tau$ never select a literal
whose negation occurs in $t_{j}$ iff the variable assignment defined by
$\sigma,\tau$ satisfies $\psi$. Therefore, an achieving strategy of Eve
witnesses truth of the QBF. Conversely, if the QBF is true, then we can map a
winning strategy of the $\exists$-player in the formula game to a
deterministic strategy in $\mathcal{G}_{\psi}$, such that for all counter-
strategies of Adam, there exists a term $t_{j}$ such that no player ever
selects a literal whose negation is contained in $t_{j}$. This leads to
reaching $T_{j}$ with probability $1$.

We can adapt the construction to qualitative safety DQs similar as in Lemma 6.
∎

###  B.3 Proof of Lemma 13

See 13

###### Proof.

Recall that we have to decide the following problem, where $\sigma$ and $\tau$
range over _deterministic_ strategies only and $\mathbb{P}$ implicitly refers
to an SG $\mathcal{G}$:
$\exists\sigma\forall\tau\bigvee_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\square
T_{i})\geq 1$. We show how to decide the complement of this problem with a
polynomially space-bounded alternating Turing machine (ATM). This implies the
claimed result as alternating $\mathsf{PSPACE}$ equals $\mathsf{EXPTIME}$
[11]. Note that the complement is the decision problem
$\forall\sigma\exists\tau\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge\overline{T_{i}})>0$
where each $\overline{T_{i}}$ occurs only in sinks. We need the following
observation:

######  Claim.

If all $T_{i}$, $i=1,\ldots,n$, contain only sinks, then

$\forall\sigma\exists\tau\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge
T_{i})>0\iff\forall\sigma\exists\tau\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge^{\leq|S|}T_{i})>0$

where $\mathbb{P}^{\sigma,\tau}(\lozenge^{\leq|S|}T_{i})$ denotes the
probability to reach $T_{i}$ in the $|S|$-step game $\mathcal{G}^{\leq|S|}$
under strategies $\sigma,\tau$.

$\triangleright$ Proof: The direction from right to left is trivial. For the
other direction observe that if there exists $\sigma$ of Eve such that Adam
cannot reach one of the targets $T_{i}$ for some $1\leq i\leq n$ within $|S|$
steps, then Adam cannot reach $T_{i}$ in any number of steps. Indeed, as
targets only need to be reached with positive probability, we can assume that
the probabilistic states behave in Adam’s favor. In other words, if Adam
cannot reach $T_{i}$ for some $i$ in $|S|$ steps against a given strategy of
Eve, then he can also not reach it even if he controlled all the random states
and so he cannot reach it in any number of steps. $\triangleleft$

For the rest of the proof we assume w.l.o.g. that all states $s\in
S_{\mathsf{P}}$ have exactly two successors, called left and right in the
following (e.g. [32, Appendix A]).

The ATM simulates the game for exactly $|S|$ steps (a similar technique was
used in [29]). States controlled by Eve correspond to universal states of the
ATM and those controlled by Adam to existential ones (note that since we
consider the complementary problem, strategies of Eve are universally
quantified and those of Adam existentially). This can be implemented in the
ATM by keeping a record of the current state of the game. The ATM also keeps
track of the history $\pi\in S^{*}$ of the current path and stores a bit
vector $(t_{1},\ldots,t_{n})\in\\{0,1\\}^{n}$ indicating which targets have
already been reached. In order to handle probabilistic states, the ATM
maintains an additional stack. When the game reaches a probabilistic state
which is not a sink, the ATM pushes the current history on the stack and
explores the left branch first. Once the ATM reaches a configuration where the
current history exceeds $|S|$ and the stack is not empty, it pops the saved
history $s_{0}\ldots s$, $s\in S_{\mathsf{P}}$ from the stack, sets its
current history to $s_{0}\ldots s$ and the current game state to $s$ and
explores the right successor of $s$. If the ATM reaches a configuration where
the current history exceeds length $|S|$ and the stack is empty, then it
accepts iff $(t_{1},\ldots,t_{n})=(1,\ldots,1)$.

Overall, the ATM accepts iff
$\forall\sigma\exists\tau\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge\overline{T_{i}})>0$
holds:

  * •

If the ATM accepts, then Adam can reach each $\overline{T_{i}}$,
$i=1,\ldots,n$, already within $|S|$ steps with positive probability against
all strategies of Eve. Thus
$\mathbb{P}^{\sigma,\tau}(\lozenge\overline{T_{i}})>0$ holds.

  * •

Conversely, if
$\forall\sigma\exists\tau\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge\overline{T_{i}})>0$
holds, then we also have
$\forall\sigma\exists\tau\bigwedge_{i=1}^{n}\mathbb{P}^{\sigma,\tau}(\lozenge^{\leq|S|}\overline{T_{i}})>0$
by the auxiliary claim. Thus the ATM accepts since it simulates the game
appropriately for $|S|$ steps.

∎

##  Appendix C Full proofs of Section 5

###  C.1 Proof of Lemma 15

First, we only have to consider _deterministic_ strategies of Adam because
from his point of view, he is trying to achieve a (mixed) _DQ_ and
deterministic strategies are sufficient for this by Lemma 1. A deterministic
_$k$ -step strategy_ of Adam is a deterministic strategy in the $k$-step game
$\mathcal{G}^{\leq k}$. Formally, such a strategy can be identified with a
mapping

$\tau^{k}\colon S^{\leq k-1}S_{\mathsf{A}}\to S$

such that $\tau^{k}(\pi s)\in\mathsf{Act}(s)$ for all $\pi s\in S^{\leq
k-1}S_{\mathsf{A}}$. Here, $S^{\leq k-1}$ denotes the set of paths of length
at most $k-1$ (by definition, $S^{-1}=\emptyset$ and $S^{0}=\\{\epsilon\\}$,
where $\epsilon$ is the “empty path”). In particular, $\tau^{k}$ needs to take
only histories of length at most $k$ into account and may not randomize. In
the following, we write $\mathcal{X}^{0}=\mathcal{X}^{0}(\varphi)$. We will
show the following invariant:

> For all $k\geq 0$ and $s\in S$, the set $\Phi^{k}(\mathcal{X}^{0})_{s}$
> contains a polyhedron $X^{k}_{s}(\tau)\in\mathfrak{C}$ for each possible
> _deterministic_ $k$-step strategy $\tau$ of Adam. This polyhedron satisfies
> $X^{k}_{s}(\tau)=\mathcal{A}(\mathcal{G}_{s}^{\leq k,\tau},\varphi)$ where
> $\mathcal{G}_{s}$ is like $\mathcal{G}$ with initial state $s$. In words,
> $X^{k}_{s}(\tau)$ is precisely the Pareto set achievable from state $s$ by
> Eve in the induced $k$-step MDP $\mathcal{G}^{\leq k,\tau}$.

The above invariant establishes the claim as the universal quantifier over
Adam’s strategies translates to intersection over the polyhedra
$X^{k}_{s}(\tau)$. The invariant is proved by induction on $k$. For $k=0$, it
holds trivially. Now let $k>0$. First observe that a deterministic $k$-step
strategy $\tau^{k}$ of Adam can be decomposed as follows: For all $s\pi t\in
SS^{\leq k{-}1}S_{\mathsf{A}}$,

$\tau(s\pi t)=\tau_{s}^{k-1}(\pi t)$

for appropriate $(k{-}1)$-step strategies $\tau_{s}^{k-1}$ for each $s\in S$.
We now prove existence of a polyhedron
$X^{k}_{s}(\tau^{k})\in\Phi^{k}(\mathcal{X}^{0})_{s}$ for each $s\in S$ as
required by the invariant. Therefore let $\tau^{k}$ be an arbitrary
deterministic $k$-step strategy and let $s\in S$ be an arbitrary state. If $s$
is a sink, then the invariant is trivially satisfied due to the choice of the
initial element $\mathcal{X}^{0}$. Thus assume that $s$ is not a sink. Then
since $\varphi$ is a sink query, $s$ is not contained in any target/unsafe set
and so we can ignore this case in the following. Let $\tau^{k-1}_{s^{\prime}}$
be the decomposition of $\tau^{k}$ into $(k{-}1)$-step strategies as above,
one for each $s^{\prime}\in S$. We make a case distinction.

  * •

$s\in S_{\mathsf{A}}$. By the induction hypothesis (IH),
$X^{k-1}_{t}(\tau_{t}^{k-1})\in\Phi^{k-1}(\mathcal{X}^{0})_{t}$ for all $t\in
S$. Let $\tau^{k}(s)=r\in\mathsf{Act}(s)$, i.e., $r$ is the successor of $s$
if Adam follows $\tau^{k}$ and the game starts in $s$. Then
$X^{k}_{s}(\tau^{k})=X^{k-1}_{r}(\tau_{r}^{k-1})$ and thus
$X^{k}_{s}(\tau^{k})\in\Phi^{k-1}(\mathcal{X}^{0})_{r}$ by the IH. By
definition,
$\Phi^{k}(\mathcal{X}^{0})_{s}=\bigcup_{t\in\mathsf{Act}(s)}\Phi^{k-1}(\mathcal{X}^{0})_{t}$
and thus $X^{k}_{s}(\tau^{k})\in\Phi^{k}(\mathcal{X}^{0})_{s}$ since
$r\in\mathsf{Act}(s)$.

  * •

$s\in S_{\mathsf{E}}$. We have
$X^{k}_{s}(\tau^{k})=\mathsf{conv}(\bigcup_{t\in\mathsf{Act}(s)}X^{k-1}(\tau^{k-1}_{t}))$,
where the convex hull reflects the fact that Eve may randomize at $s$ and
therefore she cannot only ensure the points in $X^{k-1}(\tau^{k-1}_{t})$ but
also all their convex combinations. By the IH,
$X^{k-1}_{t}(\tau_{t}^{k-1})\in\Phi^{k-1}(\mathcal{X}^{0})_{t}$ for all $t\in
S$. By definition,
$\Phi^{k}(\mathcal{X}^{0})_{s}=\\{\mathsf{conv}(\bigcup_{t\in\mathsf{Act}(s)}X_{t}\mid
X\ \dot{\in}\ \Phi^{k-1}(\mathcal{X}^{0})\\}$, and thus
$X^{k}_{s}(\tau^{k})\in\Phi^{k}(\mathcal{X}^{0})_{s}$.

  * •

$s\in S_{\mathsf{P}}$. In this case, $X^{k}_{s}(\tau^{k})=\sum_{t\in
S}P(s,t)X^{k-1}_{t}(\tau_{t}^{k-1})$. Similar to the previous case, we have
$X^{k-1}_{t}(\tau_{t}^{k-1})\in\Phi^{k-1}(\mathcal{X}^{0})_{t}$ for all $t\in
S$ by the IH and by definition, $\Phi^{k}(\mathcal{X}^{0})_{s}=\\{\sum_{t\in
S}X_{t}\mid X\ \dot{\in}\ \Phi^{k-1}(\mathcal{X}^{0})\\}$. Again, it follows
that $X^{k}_{s}(\tau^{k})\in\Phi^{k}(\mathcal{X}^{0})_{s}$.

###  C.2 Proof of Theorem 3

See 3

###### Proof.

Recall the operation
$\mu\colon\mathcal{P}(\mathfrak{C})^{S}\to\mathcal{P}(\mathfrak{C})^{S}$.
$\mu(\mathcal{X})$ removes all non-inclusion-minimal elements from each
$\mathcal{X}_{s}$, i.e., $\mu(\mathcal{X})_{s}=\\{X\in\mathcal{X}_{s}\mid
X\text{ is }\subseteq\text{-minimal in }\mathcal{X}_{s}\\}$. We first show the
following auxiliary claim:

######  Claim.

For all $\mathcal{X}\in\mathcal{P}(\mathfrak{C})^{S}$ such that
$\mathcal{X}(s)$ is finite it holds that

$\mu(\Phi(\mathcal{X}))=\mu(\Phi(\mu(\mathcal{X})))~{}.$

$\triangleright$ Proof: We first show that

$\mu(\Phi(\mathcal{X}))_{s}\subseteq\Phi(\mu(\mathcal{X}))_{s}$

for all $s\in S$. Case distinction:

  * •

$s\in S_{\mathsf{A}}$. By definition,
$\Phi(\mathcal{X})_{s}=\bigcup_{t\in\mathsf{Act}(s)}\mathcal{X}_{t}$. Let
$X\in\Phi(\mathcal{X})_{s}$ be a minimum, i.e.,
$X\in\mu(\Phi(\mathcal{X}))_{s}$. But then $X$ must also be a minimum in at
least one of the $\mathcal{X}_{t}$, $t\in\mathsf{Act}(s)$. Thus
$X\in\bigcup_{t\in\mathsf{Act}(s)}\mu(\mathcal{X})_{t}=\Phi(\mu(\mathcal{X}))_{s}$.

  * •

$s\in S_{\mathsf{E}}$. Recall that by definition,
$\Phi(\mathcal{X})_{s}=\\{\mathsf{conv}(\bigcup_{t\in\mathsf{Act}(s)}X_{t})\mid
X\ \dot{\in}\ \mathcal{X}\\}$. Let $X\in\Phi(\mathcal{X})_{s}$ be a minimum,
i.e., $X\in\mu(\Phi(\mathcal{X}))_{s}$. Then
$X=\mathsf{conv}(\bigcup_{t\in\mathsf{Act}(s)}X_{t})$ for some
$X_{t}\in\mathcal{X}_{t}$. We claim that for each $t$, we can assume that
$X_{t}$ is a minimum in $\mathcal{X}_{t}$, i.e.,
$X_{t}\in\mu(\mathcal{X})_{t}$. Indeed, suppose that for some $t$, $X_{t}$ is
not a minimum. We can then exchange this $X_{t}$ for a minimum
$X_{t}^{\prime}\in\mu(\mathcal{X})_{t}$ to construct an $X^{\prime}\subseteq
X$. This however implies that $X^{\prime}=X$ because $X$ is a minimum. Thus
again, $X\in\\{\mathsf{conv}(\bigcup_{t\in\mathsf{Act}(s)}X_{t})\mid X\
\dot{\in}\ \mu(\mathcal{X})\\}=\Phi(\mu(\mathcal{X}))_{s}$.

  * •

$s\in S_{\mathsf{P}}$. Similar to the previous case.

To conclude the proof, notice that for all finite sets
$\mathcal{X},\mathcal{Y}\in\mathcal{P}(\mathfrak{C})$ with
$\mathcal{X}\subseteq\mathcal{Y}$ and $\mu(\mathcal{Y})\subseteq\mathcal{X}$
it already holds that $\mu(\mathcal{X})=\mu(\mathcal{Y})$. It is clear that
$\Phi(\mu(\mathcal{X}))_{s}\subseteq\Phi(\mathcal{X})_{s}$ since
$\mu(\mathcal{X})_{s}\subseteq\mathcal{X}_{s}$. Putting all together yields
$\mu(\Phi(\mathcal{X}))_{s}=\mu(\Phi(\mu(\mathcal{X})))_{s}$ for all $s$ as
claimed.

$\triangleleft$

We now complete the proof of Theorem 3. Let
$\tilde{\Phi}\vcentcolon=\mu\circ\Phi$. Technically, we show that

$\bigcap(\tilde{\Phi}^{k}(\mathcal{X}^{0}(\varphi))_{s})=\bigcap(\Phi^{k}(\mathcal{X}^{0}(\varphi))_{s})$

for all $s\in S$ and $k\geq 0$, i.e., iterating $\mu\circ\Phi$ instead of just
$\Phi$ as in Lemma 15 is equivalent. To this end it suffices to show that

$\mu(\Phi^{k}(\mathcal{X}^{0}))=\tilde{\Phi}^{k}(\mathcal{X}^{0})$ (4)

because the intersection in completely determined by the $\subseteq$-minimal
sets. We show (4) by induction:

  * •

For $k=0$, $\mu(\mathcal{X}^{0})=\mathcal{X}^{0}$ clearly holds because
$\mathcal{X}^{0}_{s}$ is a singleton for each $s\in S$.

  * •

Let $k>1$. Then

$\displaystyle\mu(\Phi^{k}(\mathcal{X}^{0}))$
$\displaystyle=\mu(\Phi(\Phi^{k-1}(\mathcal{X}^{0}))$
$\displaystyle=\mu(\Phi(\mu(\Phi^{k-1}(\mathcal{X}^{0})))$ (Auxiliary claim
above) $\displaystyle=\mu(\Phi(\tilde{\Phi}^{k-1}(\mathcal{X}^{0}))$
(induction hypothesis) $\displaystyle=\tilde{\Phi}^{k}(\mathcal{X}^{0})$
(definition)

which completes the proof.

∎

###  C.3 Details on the Experimental Setup

CCerrHCCHHCCHHHerr Figure 10: Adapted floor heating model from [10].

The floor heating example from Figure 10 is as in [10] with the following
modifications:

  * •

The controller can turn on at most one of the heatings, otherwise it will run
out of energy and enter state $err$.

  * •

The objective is the CQ (template) $\mathbb{P}(\lozenge\\{HH\\})\geq
x\wedge\mathbb{P}(\square S\setminus\\{err\\})\geq y$.

The random games together with a 2-dimensional mixed query each were
constructed according to the following scheme:

  * •

Generate $m$ states.

  * •

Assign each state to $S_{\mathsf{A}},S_{\mathsf{E}}$ or $S_{\mathsf{P}}$ with
equal probability.

  * •

Assign two random successors $s_{1},s_{2}$ to each state $s$ such that
$s_{1},s_{2},s$ are pairwise different.

  * •

Select $l$ states at random, turn them into sinks and create a target set with
those states. This will be the reachability objective.

  * •

Similarly, create a safety objective in the same way by selecting $l$ random
unsafe states.

The numbers in Table 3 are for $m=10$ and $l=1$.