Quantitative Reductions and Vertex-Ranked Infinite Games (Full Version)

TL;DR

This paper introduces quantitative reductions and vertex-ranked games, providing a new framework for solving quantitative games without reducing to qualitative ones, and demonstrates their effectiveness and computational complexity.

Contribution

It presents a novel technique for structuring and solving quantitative games directly, introduces vertex-ranked games as a versatile target, and applies these concepts to request-response and Muller games.

Findings

Quantitative reductions retain optimality of solutions.

Vertex-ranked games can be solved efficiently and are useful for fault-resilient strategies.

Solving request-response and Muller games is EXPTIME-complete.

Abstract

We introduce quantitative reductions, a novel technique for structuring the space of quantitative games and solving them that does not rely on a reduction to qualitative games. We show that such reductions exhibit the same desirable properties as their qualitative counterparts and that they additionally retain the optimality of solutions. Moreover, we introduce vertex-ranked games as a general-purpose target for quantitative reductions and show how to solve them. In such games, the value of a play is determined only by a qualitative winning condition and a ranking of the vertices. We provide quantitative reductions of quantitative request-response games and of quantitative Muller games to vertex-ranked games, thus showing EXPTIME-completeness of solving the former two kinds of games. In addition, we exhibit the usefulness and flexibility of vertex-ranked games by showing how to use such games to compute fault-resilient strategies for safety specifications. This work lays the foundation for a general study of fault-resilient strategies for more complex winning conditions.

Tables

Table 1. Table 1: A summary of the proofs in work concerned with solving games. For each game,  n 𝑛 n denotes the number of vertices of the game. For vertex-ranked games,  𝒢 𝒢 \mathcal{G} denotes the underlying qualitative game while  t ​ ( | 𝒢 | ) 𝑡 𝒢 t(|\mathcal{G}|) and  s ​ ( | 𝒢 | ) 𝑠 𝒢 s(|\mathcal{G}|) denote the time and space required to solve that underlying game. Furthermore,  σ 𝜎 \sigma denotes the size of a winning strategy in the corresponding qualitative game. For request-response games,  d 𝑑 d and  W 𝑊 W denote the number of request-response pairs and the largest weight assigned to any edge in the game, respectively. For the sake of brevity and consistency, we use the shorthand b = d ​ 2 d ​ n ​ W 𝑏 𝑑 superscript 2 𝑑 𝑛 𝑊 b=d2^{d}nW .

Game	Time	Space	Memory
Vertex-ranked $sup$-games	$𝒪\left(n\right)+t\left(\left|𝒢\right|\right)$	$𝒪\left(n\right)+s\left(\left|𝒢\right|\right)$	$𝒪\left(\left|\sigma \right|\right)$
Vertex-ranked $lim\; sup$-games	$𝒪\left(n^3+n^2\cdot t\left(\left|𝒢\right|\right)\right)$	$𝒪\left(n+s\left(\left|𝒢\right|\right)\right)$	$𝒪\left(\left|\sigma \right|\right)$
Quantitative request-response games	$𝒪\left(n^2{b}^{2d}{d}^2{2}^d\right)$	–	$𝒪\left(n{b}^{d}d{2}^d\right)$
Quantitative Muller games	$𝒪\left({\left(n!\right)}^3\right)$	–	$𝒪\left({\left(n!\right)}^3\right)$

Table 2. Table 2: A summary of the proofs in work concerned with solving games optimally. For vertex-ranked games,  M 𝑀 M denotes the number of different ranks assigned to vertices in the game. The remaining symbols are defined as in Table  1 .

Game	Time	Space
Vertex-ranked $sup$-games	$𝒪\left(\log \left(M\right)\left(n+t\left(\left|𝒢\right|\right)\right)\right)$	$𝒪\left(M\right)+s\left(\left|𝒢\right|\right)$
Vertex-ranked $lim\; sup$-games	$𝒪\left(\log \left(M\right)\left(n^3+n^2\cdot t\left(\left|𝒢\right|\right)\right)\right)$	$𝒪\left(n+s\left(\left|𝒢\right|\right)\right)$
Quantitative request-response games	$𝒪\left(\log \left(b\right)\left(n^2{b}^{2d}{d}^2{2}^d\right)\right)$	–
Quantitative Muller games	$𝒪\left({\left(n!\right)}^3\right)$	–

Equations

$$\mathcal{A}\times \mathcal{M}=(V\times M,V_0\times M,V_1\times M,E^{\prime },(v_I,m_I)),$$

$${\mathrm{Upd}}_{{\mathcal{M}}_1\times {\mathcal{M}}_2}^{+}(\pi )=({\mathrm{Upd}}_{{\mathcal{M}}_1}^{+}(\pi ),{\mathrm{Upd}}_{{\mathcal{M}}_2}^{+}({\mathrm{ext}}_{{\mathcal{M}}_1}(\pi )))$$

$${\text{cap}}_b(b^{\prime })=\{\begin{array}{ll}\min \{b,b^{\prime }\}& \text{if }{b}^{\prime }\ne \infty \text{ and}\\ \infty & \text{otherwise .}\end{array}$$

$${\mathrm{ext}}_{{\mathcal{M}}_1\times {\mathcal{M}}_2}(\rho )=(v_0,m_1^0,m_2^0)(v_1,m_1^1,m_2^1)(v_2,m_1^2,m_2^2)\cdots$$

$${\mathcal{A}}_3={\mathcal{A}}_2\times {\mathcal{M}}_2={\mathcal{A}}_1\times {\mathcal{M}}_1\times {\mathcal{M}}_2.$$

$$b=\{\begin{array}{ll}{b}_1& \text{if b2≥f1(b1) and}\\ \max \{b^{\prime }\mid f_1(b^{\prime })\le b_2\}& \text{otherwise}.\end{array}$$

$$\text{textsc}{Rank}^{\sup }(\mathrm{Win},\mathrm{rk}):v_0{v}_1{v}_2\cdots \mapsto \{\begin{array}{ll}{\sup }_{j\to \infty }\mathrm{rk}(v_j)& \text{if }{v}_0{v}_1{v}_2\cdots \in \mathrm{Win}\text{ and}\\ \infty & \text{otherwise},\end{array}$$

$$\text{textsc}{Rank}^{\lim }(\mathrm{Win},\mathrm{rk}):v_0{v}_1{v}_2\cdots \mapsto \{\begin{array}{ll}{\mathrm{limsup}}_{j\to \infty }\mathrm{rk}(v_j)& \text{if }{v}_0{v}_1{v}_2\cdots \in \mathrm{Win}\text{ and}\\ \infty & \text{otherwise}.\end{array}$$

$${\text{cap}}_{b+1}(\text{textsc}{Rank}^{\sup }(\mathrm{Win},\mathrm{rk})(\rho ))=\text{textsc}{Rank}^{\sup }(\mathrm{Win},\mathrm{rk})(\rho )=\text{textsc}{Rank}^{\sup }({\mathrm{Win}}^{\prime },{\mathrm{rk}}^{\prime })(\mathrm{ext}(\rho )).$$

$$\text{textsc}{Rank}^{\sup }({\mathrm{Win}}^{\prime },{\mathrm{rk}}^{\prime })(\mathrm{ext}(\rho ))=\infty \ge {\text{cap}}_{b+1}(b+1)=b+1,$$

$${\mathfrak{G}}_{\sup }^{\text{textsc}rnk}=\{(\mathcal{A},\text{textsc}{Rank}^{\sup }(\mathrm{Win},\mathrm{rk}))\mid (\mathcal{A},\mathrm{Win})\in \mathfrak{G},\mathrm{rk}\text{ is vertex-ranking function for }\mathcal{A}\}.$$

$$\begin{gathered} {\mathrm{Attr}}_i^j(X)=\{v\in V_i\mid \exists v^{\prime }\in {\mathrm{Attr}}_i^{j-1}(X).(v,v^{\prime })\in E\}\cup \\ \{v\in V_{1-i}\mid \forall (v,v^{\prime })\in E.v^{\prime }\in {\mathrm{Attr}}_i^{j-1}(X)\}\cup {\mathrm{Attr}}_i^{j-1}(X). \end{gathered}$$

$$\mathcal{A}\setminus A=(V\setminus A,V_0\setminus A,V_1\setminus A,\{(v,v^{\prime })\in E\mid v\notin A\text{ and }{v}^{\prime }\notin A\},v_I),$$

$${\mathfrak{G}}_{\lim }^{\text{textsc}rnk}=\{(\mathcal{A},\text{textsc}{Rank}^{\lim }(\mathrm{Win},\mathrm{rk}))\mid (\mathcal{A},\mathrm{Win})\in \mathfrak{G},\mathrm{rk}\text{ is vertex-ranking function for }\mathcal{A}\}.$$

$$\text{textsc}CoB\ddot{u}chi(F)=\{\rho \in V^{\omega }\mid \inf (\rho )\cap F=\varnothing \},$$

$$\begin{gathered} \text{textsc}ReqRes((Q_c,P_c{)}_{c\in [d]})= \\ \{v_0{v}_1{v}_2\cdots \in V^{\omega }\mid \forall c\in [d]\forall j\in \mathbb{N}.v_j\in Q_c\text{ implies }\exists j^{\prime }\ge j.v_{j^{\prime }}\in P_c\}. \end{gathered}$$

$$\begin{gathered} \text{textsc}{ReqResCor}_c(v_0{v}_1{v}_2\cdots ,j)= \\ \{\begin{array}{ll}\min \{{\mathrm{Cost}}_c(v_j\cdots v_{j^{\prime }})\mid j^{\prime }\ge j\text{ and }{v}_{j^{\prime }}\in P_c\}& \text{if }{v}_j\in Q_c,\\ 0& \text{otherwise},\end{array} \end{gathered}$$

$$\text{textsc}ReqResCor(\rho ,j)={\max }_{c\in [d]}\text{textsc}{ReqResCor}_c(\rho ,j).$$

$$\text{textsc}CostReqRes(\Gamma ,\mathrm{Cost})(\rho )={\sup }_{j\to \infty }\text{textsc}ReqResCor(\rho ,j),$$

$$\mathrm{rk}(v,v,r,f)=\{\begin{array}{ll}\max \{0,{\max }_{c\in [d]}r(c)\}& \text{if }f=0\text{ and}\\ b+1& \text{otherwise}\end{array}$$

$$\begin{gathered} {\Gamma }^{\prime }=(Q_c^{\prime },P_c^{\prime }{)}_{c\in [d]}\text{, where }{Q}_c^{\prime }=Q_c\times Q_c\times R\times \{0,1\}\text{ and } \\ {P}_c^{\prime }=P_c\times P_c\times R\times \{0,1\}\text{ for all }c\in [d]. \end{gathered}$$

$$\begin{gathered} \mathcal{O}(n(d{2}^{d}nW{)}^d+(n(d{2}^{d}nW{)}^d){)}^2{d}^2{2}^d)= \\ \mathcal{O}(n(d{2}^{d}nW{)}^d+n^2(d{2}^{d}nW{)}^{2d}{d}^2{2}^d)=\mathcal{O}(n^2(d{2}^{d}nW{)}^{2d}{d}^2{2}^d). \end{gathered}$$

$$\text{textsc}Muller({\mathcal{F}}_0,{\mathcal{F}}_1)=\{\rho \in V^{\omega }\mid \inf (\rho )\in {\mathcal{F}}_0\},$$

$$({\text{Acc}}_F(\epsilon ),{\text{Score}}_F(\epsilon ))$$

$$({\text{Acc}}_F(\pi v),{\text{Score}}_F(\pi v))$$

$$\text{textsc}QuantMuller({\mathcal{F}}_0,{\mathcal{F}}_1)(\rho )={\text{Score}}_{{\mathcal{F}}_1}(\rho ).$$

$$\mathrm{Safety}(U)=\{v_0{v}_1{v}_2\cdots \in V^{\omega }\mid \forall j\in \mathbb{N}{v}_j\notin U\}.$$

Full text

We provide quantitative reductions of quantitative request-response games and of quantitative Muller games to vertex-ranked games, thus showing ExpTime-completeness of solving the former two kinds of games. In addition, we exhibit the usefulness and flexibility of vertex-ranked games by showing how to use such games to compute fault-resilient strategies for safety specifications. This work lays the foundation for a general study of fault-resilient strategies for more complex winning conditions.

1 Introduction

The study of quantitative infinite games has garnered great interest lately, as they allow for a much more fine-grained analysis and specification of reactive systems than classical qualitative games [5, 6, 7, 15, 18, 30, 31]. While there exists previous work investigating quantitative games, the approaches to solving them usually rely on ad-hoc solutions that are tailor-made to the considered winning condition. Moreover, quantitative games are usually solved by reducing them to a qualitative game in a first step, hardcoding a certain value of interest during the reduction. In particular, to the best of our knowledge, there exists no general framework for the analysis of such games that is analogous to the existing one for qualitative games. In this work, we introduce such a framework that disentangles the study of quantitative games from that of qualitative ones.

Qualitative infinite games have been applied successfully in the verification and synthesis of reactive systems [1, 2, 3, 8]. They have given rise to a multitude of algorithms that ascertain system correctness and that synthesize correct-by-construction systems. In such a game, two players, called Player [math] and Player $1$, move a token in a directed graph. After infinitely many moves, the resulting sequence of vertices is evaluated and one player is declared the winner of the play. For example, in a qualitative request-response game [28], the goal for Player [math] is to ensure that every visit to a vertex denoting some request is eventually followed by a visit to a vertex denoting an answer to that request. In order to solve qualitative games, i.e., to determine a winning strategy for one player, one often reduces a complex game to a potentially larger, but conceptually simpler one. For example, in a multi-dimensional request-response game, i.e., in a request-response game in which there exist multiple conditions that can be requested and answered, one stores the set of open requests and demands that every request is closed at infinitely many positions. As this is a Büchi condition, which is much simpler than the request-response condition, one is able to reduce request-response games to Büchi games.

In recent years the focus of research has shifted from the study of qualitative games, in which one player is declared the winner of a given play, to that of quantitative games, in which the resulting play is assigned some value or cost. Such games allow, for example, modeling systems in which requests have to be answered within a certain number of steps [7, 11, 16, 18, 19], systems with one or more finite resources which may be drained and charged [4, 9, 10, 27], or scenarios in which each move incurs a certain cost for either player [15, 31].

In general, Player [math] aims to minimize the cost of the resulting play, i.e., to maximize its value, while Player $1$ seeks to maximize the cost, thus minimizing the value. In a quantitative request-response game, for example, it is the goal of Player [math] to minimize the number of steps taken between requests and their corresponding answers. The typical questions asked in the context of such games are “Does there exist an upper bound on the time between requests and responses that Player [math] can ensure?” [11, 18, 19, 26], “Can Player [math] ensure an average cost per step greater than zero?” [31], “What is the minimal time between requests and responses that Player [math] can ensure?” [30], or “What is the minimal average level of the resource that Player [math] can ensure without it ever running out?” [4]. The former two questions can be seen as boundedness questions, while the latter two are asking for optimal solutions.

Such decision problems are usually solved by fixing some bound $b$ on the cost of the resulting plays and subsequently reducing the problem of finding a strategy for Player [math] that enforces a cost of at most $b$ in the quantitative game to the problem of solving a qualitative game, hardcoding the fixed $b$ in the process. The problem of deciding whether or not Player [math] has such a strategy is called the ($b$-)threshold problem.

For example, in order to determine the winner in a quantitative request-response game as described above for some bound $b$, we construct a Büchi game in which every time a request is opened, a counter for that request is started which counts up to the bound $b$ and is reset if the request is answered. Once any counter exceeds the value $b$, we move to a terminal position indicating that Player [math] has lost. We then require that every counter is inactive infinitely often, which is again a Büchi condition and thus much simpler than the original quantitative request-response condition. Thus, Player [math] wins the resulting qualitative game if and only if she can ensure that every request is answered within at most $b$ steps in the quantitative game.

Such reductions are usually specific to the problem being addressed. Furthermore, they immediately abandon the quantitative aspect of the game under consideration, as the bound is hardcoded during the first step of the analysis. Thus, even when only changing the bound one is interested in, the reduction has to be recomputed and the resulting qualitative game has to be solved from scratch. In our request-response example, if one is interested in deciding the $b^{\prime}$-threshold problem for some $b^{\prime}\neq b$, one constructs a new Büchi game for the bound $b^{\prime}$. This game is then solved independently of the one previously computed for the bound $b$.

In this work, we lift the concept of reductions for qualitative games to quantitative games. Such quantitative reductions enable the study of a multitude of optimization problems for quantitative games in a way similar to decision problems for qualitative games. When investigating quantitative request-response games using quantitative reductions, for example, we only compute a single, simpler quantitative game and subsequently check this game for a winning strategy for Player [math] for any bound $b$. If she has such a strategy in the latter game, the quantitative reduction yields a strategy for her satisfying the same bound in the former one.

In general, we retain the intuitive property of reductions for qualitative games: Using quantitative reductions, the properties of a complex quantitative game can be studied by investigating a potentially larger, but conceptually simpler quantitative game.

Contributions

We present the first framework for reductions between quantitative games and we provide vertex-ranked games as general-purpose targets for such reductions. Moreover, we show tight bounds on the complexity of solving vertex-ranked games with respect to a given bound.

Subsequently, we provide three examples illustrating the use of the concepts introduced in this work: First, we define quantitative request-response games and solve them using quantitative reductions to vertex-ranked games. Second, we show how to solve quantitative Muller games as defined by McNaughton [21] via quantitative reductions to vertex-ranked safety games. Third, we illustrate the versatility of vertex-ranked games by using them to compute fault-resilient strategies for safety games with faults. We summarize our contributions with regards to solving quantitative games in Table 1 and we summarize our contributions with regards to solving quantitative games optimally in Table 2.

Structure of this work

After introducing qualitative and quantitative games formally in Section 2, we define quantitative reductions in Section 3 and show that they provide a mechanism to determine the minimal bound $b$ such that Player [math] can enforce a cost of at most $b$ in a given quantitative game: If a game $\mathcal{G}$ can be reduced to a game $\mathcal{G}^{\prime}$, then we can use a strategy for Player [math] that minimizes the cost of plays in $\mathcal{G}^{\prime}$ to construct a strategy for her which minimizes the cost of plays in $\mathcal{G}$.

In Section 4, we define vertex-ranked games, very general classes of quantitative games that can be used as targets for quantitative reductions. The quantitative condition of such games is quite simple in that the cost of a play is determined only by a qualitative winning condition and by a ranking of the vertices of the game. If the resulting play is winning according to the qualitative condition, then its cost is given by the highest rank visited at all or visited infinitely often, depending on the particular variant of vertex-ranked games. Otherwise, the value of the play is infinite. We show that solving such vertex-ranked games is as hard as solving games with the underlying qualitative winning condition.

Finally, in Section 5 we provide three examples of the versatility of vertex-ranked games: First, we define and solve request-response games with costs via quantitative reductions. Second, we recall the definition of quantitative Muller games due to McNaughton [21] and show how to solve these games via quantitative reductions as well. Third, we discuss how to use vertex-ranked games to compute fault-resilient strategies in safety games with faults [14]. In such games, after Player [math] has picked a move, say to vertex $v$, a fault may occur, which overrides the choice of Player [math] and the game continues in vertex $v^{\prime}\neq v$ instead. By using vertex-ranked games, we are able to compute strategies that are resilient against as many faults as possible.

2 Preliminaries

We first define notions that are common to both qualitative and quantitative games. Afterwards, we recapitulate the standard notions for qualitative games before defining quantitative games and lifting the notions for qualitative games to the quantitative case.

We denote the non-negative integers by $\mathbb{N}$ and define $[n]=\{0,1,\ldots,n-1\}$ for every $n\geq 1$. Also, we define $\infty>n$ for all $n\in\mathbb{N}$ and $\mathbb{N}_{\infty}=\mathbb{N}\cup\{\infty\}$. Finally, for any set $V$, we write $|V|$ and $V^{\omega}$ to denote the cardinality of $V$ and the set of all infinite sequences over $V$, respectively. An arena $\mathcal{A}=(V,V_{0},V_{1},E,v_{I})$ consists of a finite, directed graph $(V,E)$, a partition $(V_{0},V_{1})$ of $V$ into the vertices of Player [math] and Player $1$, and an initial vertex $v_{I}\in V$. The size of $\mathcal{A}$, denoted by $|\mathcal{A}|$, is defined as $|V|$. A play in $\mathcal{A}$ is an infinite path $\rho=v_{0}v_{1}v_{2}\cdots$ through $(V,E)$ starting in $v_{I}$. To rule out finite plays, we require every vertex to be non-terminal, i.e., we require that for every vertex $v\in V$ there exists some vertex $v^{\prime}\in V$ such that $(v,v^{\prime})\in E$.

A strategy for Player $i$ is a mapping $\sigma\colon V^{*}V_{i}\rightarrow V$ that assigns to each play prefix $\pi$ ending in a vertex of Player $i$ a vertex $\sigma(\pi)$ to move to. Formally, we require $(v,\sigma(\pi v))\in E$ for all $\pi\in V^{*}$, $v\in V_{i}$. We say that $\sigma$ is positional if $\sigma(\pi v)=\sigma(v)$ for every $\pi\in V^{*}$, $v\in V_{i}$. A play $v_{0}v_{1}v_{2}\cdots$ is consistent with a strategy $\sigma$ for Player $i$, if $v_{j+1}=\sigma(v_{0}\cdots v_{j})$ for all $j$ with $v_{j}\in V_{i}$.

A memory structure $\mathcal{M}=(M,m_{I},\mathrm{Upd})$ for an arena $(V,V_{0},V_{1},E,v_{I})$ consists of a finite set $M$ of memory states, an initial memory state $m_{I}\in M$, and an update function $\mathrm{Upd}\colon M\times V\rightarrow M$. We extend the update function to finite play prefixes in the usual way: $\mathrm{Upd}^{+}(v_{I})=m_{I}$ and $\mathrm{Upd}^{+}(\pi v)=\mathrm{Upd}(\mathrm{Upd}^{+}(\pi),v)$ for play prefixes $\pi\in V^{+}$ and $v\in V$. A next-move function $\mathrm{Nxt}\colon V_{i}\times M\rightarrow V$ for Player $i$ has to satisfy $(v,\mathrm{Nxt}(v,m))\in E$ for all $v\in V_{i}$, $m\in M$. Each pair of a memory structure $\mathcal{M}$ and a next-move function $\mathrm{Nxt}$ induces a strategy $\sigma$ for Player $i$ with memory $\mathcal{M}$ via $\sigma(v_{0}\cdots v_{j})=\mathrm{Nxt}(v_{j},\mathrm{Upd}^{+}(v_{0}\cdots v_{j}))$. A strategy is called finite-state if it can be implemented by a memory structure. We define $|\mathcal{M}|=|M|$. In a slight abuse of notation, the size $|\sigma|$ of a finite-state strategy is the size of a memory structure implementing it.

An arena $\mathcal{A}=(V,V_{0},V_{1},E,v_{I})$ together with a memory structure $\mathcal{M}=(M,m_{I},\mathrm{Upd})$ for $\mathcal{A}$ induce the extended arena

[TABLE]

where $E^{\prime}$ is defined via $((v,m),(v^{\prime},m^{\prime}))\in E^{\prime}$ if and only if $(v,v^{\prime})\in E$ and $\mathrm{Upd}(m,v^{\prime})=m^{\prime}$. Every play $\rho=v_{0}v_{1}v_{2}\cdots$ in $\mathcal{A}$ has a unique extended play $\mathrm{ext}_{\mathcal{M}}(\rho)=(v_{0},m_{0})(v_{1},m_{1})(v_{2},m_{2})\cdots$ in $\mathcal{A}\times\mathcal{M}$ defined by $m_{0}=m_{I}$ and $m_{j+1}=\mathrm{Upd}(m_{j},v_{j+1})$, i.e., $m_{j}=\mathrm{Upd}^{+}(v_{0}\cdots v_{j})$. We omit the index $\mathcal{M}$ if it is clear from the context. The extension of a finite play prefix in $\mathcal{A}$ is defined analogously.

Let $\mathcal{A}$ be an arena, let $\mathcal{M}_{1}=(M_{1},m^{1}_{I},\mathrm{Upd}_{1})$ be a memory structure for $\mathcal{A}$, and let $\mathcal{M}_{2}=(M_{2},m^{2}_{I},\mathrm{Upd}_{2})$ be a memory structure for $\mathcal{A}\times\mathcal{M}_{1}$. We define $\mathcal{M}_{1}\times\mathcal{M}_{2}=(M_{1}\times M_{2},(m^{1}_{I},m^{2}_{I}),\mathrm{Upd})$, where $\mathrm{Upd}((m_{1},m_{2}),v)=(m^{\prime}_{1},m^{\prime}_{2})$ if $\mathrm{Upd}_{1}(m_{1},v)=m^{\prime}_{1}$ and $\mathrm{Upd}_{2}(m_{2},(v,m^{\prime}_{1}))=m^{\prime}_{2}$. Via a straightforward induction and in a slight abuse of notation we obtain

[TABLE]

for all finite play prefixes $\pi$, where we do not distinguish between the terms $(v,m_{1},m_{2})$, $((v,m_{1}),m_{2})$, and $(v,(m_{1},m_{2}))$.

2.1 Qualitative Games

A qualitative game $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ consists of an arena $\mathcal{A}$ with vertex set $V$ and a set $\mathrm{Win}\subseteq(V^{\prime})^{\omega}$ of winning plays for Player [math], for some superset $V^{\prime}\supseteq V$. We call $\mathrm{Win}$ the winning condition of $\mathcal{G}$. In, e.g., a request-response game as described in Section 1, the winning condition contains the plays $\rho$ in which for every visit to a vertex denoting a request there is a subsequent visit to a vertex denoting a response. The set of winning plays for Player $1$ is $V^{\omega}\setminus\mathrm{Win}$. As our definition of games is very general, the infinite object $\mathrm{Win}$ may not be finitely describable. If it is, however, we slightly abuse notation and define $|\mathcal{G}|$ as the sum of $|\mathcal{A}|$ and the size of a description of $\mathrm{Win}$. In, e.g., the case of a request-response game, the set $\mathrm{Win}$ can be described via two sets $Q,P\subseteq V$, where $Q$ and $P$ denote the vertices representing requests and responses, respectively. We omit, however, a general definition of the term “description of $\mathrm{Win}$”, as it is irrelevant for this work.

A strategy $\sigma$ for Player $i$ is a winning strategy for her in $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ if all plays consistent with $\sigma$ are winning for her. If Player $i$ has a winning strategy, then we say she wins $\mathcal{G}$. Solving a game amounts to determining its winner, if one exists. A game is determined if one player has a winning strategy.

2.2 Quantitative Games

Quantitative games extend the classical model of qualitative games. In a quantitative game, plays are not partitioned into winning and losing plays, but rather they are assigned some measure of quality. We keep this definition very general in order to encompass many of the already existing models. In Section 4, we give concrete examples of such games and show how to solve them optimally.

A quantitative game $\mathcal{G}=(\mathcal{A},\mathrm{Cost})$ consists of an arena $\mathcal{A}$ with vertex set $V$ and a cost-function $\mathrm{Cost}\colon(V^{\prime})^{\omega}\rightarrow\mathbb{N}_{\infty}$ for plays where $V^{\prime}\supseteq V$ is again some superset of $V$. Similarly to the winning condition in the qualitative case, $\mathrm{Cost}$ is, in general, an infinite object. If it is finitely describable, we, again slightly abusively, define the size $|\mathcal{G}|$ of $\mathcal{G}$ as the sum of $|\mathcal{A}|$ and the size of a description of $\mathrm{Cost}$. A cost function may, e.g., be described via a finite Mealy machine [22] that processes the play and outputs a natural number on each step. The cost of a play could then be defined as the supremum, infimum, or average of the resulting sequence of numbers. In such a case, a description of the cost function would consist of the Mealy machine, while the size of the description of the function could be defined as the sum of number of states of the machine and the length of the largest integer that is output by the machine.

A play $\rho$ in $\mathcal{A}$ is winning for Player [math] in $\mathcal{G}$ if $\mathrm{Cost}(\rho)<\infty$. Winning strategies, the winner of a game, and solving a game are defined as in the qualitative case. In order to simplify the presentation, we only consider the case in which Player [math] aims to minimize the cost of a play. All concepts in this work can, however, be easily adapted to the dual case in which Player [math] aims to maximize the cost of a play.

We extend the cost-function over plays to strategies by defining $\mathrm{Cost}(\sigma)=\sup_{\rho}\mathrm{Cost}(\rho)$ and $\mathrm{Cost}(\tau)=\inf_{\rho}\mathrm{Cost}(\rho)$, where $\rho$ ranges over the plays consistent with the strategy $\sigma$ for Player [math] and over the plays consistent with the strategy $\tau$ for Player $1$, respectively. Moreover, we say that a strategy $\sigma$ for Player [math] is optimal if its cost is minimal among all strategies for her. Dually, a strategy $\tau$ for Player $1$ is optimal for him if its cost is maximal among all strategies for him.

For every strategy $\sigma$ for Player [math], $\mathrm{Cost}(\sigma)<\infty$ implies that $\sigma$ is winning for Player [math]. However, the converse does not hold true: Each play consistent with some strategy $\sigma$ may have finite cost, while for every $n\in\mathbb{N}$ there exists a play $\rho$ consistent with $\sigma$ with $\mathrm{Cost}(\rho)\geq n$. In contrast, a strategy $\tau$ for Player $1$ has $\mathrm{Cost}(\tau)=\infty$, if and only if $\tau$ is winning for him.

We say that Player [math] wins $\mathcal{G}$ with respect to $b$ if she has a strategy $\sigma$ with $\mathrm{Cost}(\sigma)\leq b$. Dually, if Player $1$ has a strategy $\tau$ with $\mathrm{Cost}(\tau)>b$, then we say that he wins $\mathcal{G}$ with respect to $b$. Solving a quantitative game $\mathcal{G}$ with respect to $b$ amounts to deciding whether or not Player [math] wins $\mathcal{G}$ with respect to $b$. We call this decision problem the $b$-threshold problem of $\mathcal{G}$ and omit the $b$ if it is clear from the context.

If Player [math] has a strategy $\sigma$ with $\mathrm{Cost}(\sigma)\leq b$, then for all strategies $\tau$ for Player $1$ we have $\mathrm{Cost}(\tau)\leq b$. Dually, if Player $1$ has a strategy $\tau$ with $\mathrm{Cost}(\tau)>b$, then for all strategies $\sigma$ for Player [math] we have $\mathrm{Cost}(\sigma)>b$. We say that a quantitative game is determined if for each $b\in\mathbb{N}$, either Player [math] has a strategy with cost at most $b$, or Player $1$ has a strategy with cost strictly greater than $b$.

We say that $b\in\mathbb{N}$ is a cap of a quantitative game $\mathcal{G}$ if Player [math] winning $\mathcal{G}$ implies that she has a strategy with cost at most $b$. A cap $b$ for a game $\mathcal{G}$ is tight if it is minimal.

3 Quantitative Reductions

Before defining quantitative reductions, we first recall the definition of qualitative ones. To this end, let $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ and $\mathcal{G}^{\prime}=(\mathcal{A}^{\prime},\mathrm{Win}^{\prime})$ be qualitative games. We say that $\mathcal{G}$ is reducible to $\mathcal{G}^{\prime}$ via the memory structure $\mathcal{M}$ for $\mathcal{A}$ if $\mathcal{A}^{\prime}=\mathcal{A}\times\mathcal{M}$ and if $\rho\in\mathrm{Win}$ if and only if $\mathrm{ext}(\rho)\in\mathrm{Win}^{\prime}$. Then, Player [math] wins $\mathcal{G}$ if and only if she wins $\mathcal{G}^{\prime}$. Moreover, if $\sigma^{\prime}$ is a winning strategy for Player [math] in $\mathcal{G}^{\prime}$ that is implemented by $\mathcal{M}^{\prime}$, then a winning strategy for her in $\mathcal{G}$ is implemented by $\mathcal{M}\times\mathcal{M}^{\prime}$.

We now define quantitative reductions as an analogous technique for the study of quantitative games and show that they exhibit the same properties as qualitative reductions. Intuitively, given two quantitative games $\mathcal{G}$ and $\mathcal{G}^{\prime}$, we aim to say that $\mathcal{G}$ is reducible to $\mathcal{G}^{\prime}$ if plays in one game can be translated into plays in the other, retaining their cost along the transformation. In fact, two such associated plays do not need to carry identical cost, but it suffices that the order on plays induced by their cost is retained.

To capture such order-retaining transformations of cost functions, we introduce $b$-correction functions. Let $b\in\mathbb{N}_{\infty}$. A function $f\colon\mathbb{N}_{\infty}\rightarrow\mathbb{N}_{\infty}$ is a $b$-correction function if

• •

for all $b^{\prime}_{1}<b^{\prime}_{2}<b$ we have $f(b^{\prime}_{1})<f(b^{\prime}_{2})$,

• •

for all $b^{\prime}<b$ we have $f(b^{\prime})<f(b)$, and

• •

for all $b^{\prime}\geq b$ we have $f(b^{\prime})\geq f(b)$.

Thus, intuitively, a $b$-correction function is strictly monotonic up to, but not including, $b$, and $f(b)$ is a lower bound for all values $f(b^{\prime})$ with $b^{\prime}\geq b$.

For $b=\infty$ these requirements degenerate to demanding that $f$ is strictly monotonic, which in turn implies $f(\infty)=\infty$ and $f(b)\neq\infty$ for all $b\neq\infty$. Dually, if $b=0$, we only require that $f(0)$ bounds the values of $f(b)$ from below. As an example, for each $b\in\mathbb{N}_{\infty}$ we define the function $\text{cap}_{b}$ as follows:

[TABLE]

Then, the function $\text{cap}_{b}$ is a $b$-correction function.

Leveraging the notion of $b$-correction functions, we are now able to define quantitative reductions. Let $\mathcal{G}=(\mathcal{A},\mathrm{Cost})$ and $\mathcal{G}^{\prime}=(\mathcal{A}^{\prime},\mathrm{Cost}^{\prime})$ be quantitative games, let $\mathcal{M}$ be some memory structure for $\mathcal{A}$, let $b\in\mathbb{N}_{\infty}$, and let $f\colon\mathbb{N}_{\infty}\rightarrow\mathbb{N}_{\infty}$ be some function. We say that $\mathcal{G}$ is $b$-reducible to $\mathcal{G}^{\prime}$ via $\mathcal{M}$ and $f$ if

• •

$\mathcal{A}^{\prime}=\mathcal{A}\times\mathcal{M}$,

• •

$f$ is a $b$-correction function,

• •

$\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(\mathrm{Cost}(\rho))$ for all plays $\rho$ of $\mathcal{A}$ with $\mathrm{Cost}(\rho)<b$, and

• •

$\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\geq f(b)$ for all plays $\rho$ of $\mathcal{A}$ with $\mathrm{Cost}(\rho)\geq b$.

We write $\mathcal{G}\leq^{b}_{\mathcal{M},f}\mathcal{G}^{\prime}$ in this case. Moreover, we use $\text{cap}_{b}$ as a “default” function: If $f=\text{cap}_{b}$, we omit stating $f$ explicitly and write $\mathcal{G}\leq^{b}_{\mathcal{M}}\mathcal{G}^{\prime}$. The penultimate condition implies that for each play $\mathrm{ext}(\rho)$ in $\mathcal{A}^{\prime}$ with $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\leq f(b)$ there exists some $b^{\prime}$ such that $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})$. Clearly, quantitative reductions are downward-closed with respect to the parameter $b$: If $\mathcal{G}\leq^{b}_{\mathcal{M},f}\mathcal{G}^{\prime}$ for some $b\in\mathbb{N}_{\infty}$, then, for all $b^{\prime}\leq b$, we have $\mathcal{G}\leq^{b^{\prime}}_{\mathcal{M},f}\mathcal{G}^{\prime}$.

Qualitative reductions retain whether or not a play is winning. In quantitative games, the notion of winning is refined to the notion of cost of a play. Hence, our next aim is to show that quantitative reductions indeed retain the costs of strategies. To this end, we first demonstrate that correction functions tie the cost of plays in $\mathcal{G}^{\prime}$ to that of plays in $\mathcal{G}$.

Lemma 1

Let $\mathcal{G}$ and $\mathcal{G}^{\prime}$ be quantitative games such that $\mathcal{G}\leq^{b}_{\mathcal{M},f}\mathcal{G}^{\prime}$, for some $b\in\mathbb{N}_{\infty}$, some memory structure $\mathcal{M}$, and some $b$-correction function $f$. All of the following hold true for all $b^{\prime}\in\mathbb{N}$ and all plays $\rho$ in $\mathcal{G}$:

If $b^{\prime}<b$ and $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))<f(b^{\prime})$, then $\mathrm{Cost}(\rho)<b^{\prime}$. 2. 2.

If $b^{\prime}<b$ and $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})$, then $\mathrm{Cost}(\rho)=b^{\prime}$. 3. 3.

If $b^{\prime}<b$ and $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))>f(b^{\prime})$, then $\mathrm{Cost}(\rho)>b^{\prime}$. 4. 4.

If $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\geq f(b)$, then $\mathrm{Cost}(\rho)\geq b$.

Proof

1) Let $b^{\prime}<b$ and let $\rho$ be such that $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))<f(b^{\prime})$. Towards a contradiction assume $\mathrm{Cost}(\rho)=b^{\prime\prime}\geq b^{\prime}$. We have $f(b^{\prime\prime})=f(\mathrm{Cost}(\rho))=\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))$. If $b^{\prime\prime}<b$, then we obtain $f(b^{\prime})\leq f(b^{\prime\prime})$, which implies $f(b^{\prime})\leq\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))$, contradicting $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))<f(b^{\prime})$. If, however, $b^{\prime\prime}\geq b$, then $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime\prime})\geq f(b)>f(b^{\prime})$, again contradicting $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))<f(b^{\prime})$.

2) Let $b^{\prime}<b$ and let $\rho$ be such that $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})$. Towards a contradiction assume $\mathrm{Cost}(\rho)=b^{\prime\prime}\neq b^{\prime}$. We again have $f(b^{\prime\prime})=\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))$. First assume $b^{\prime\prime}<b^{\prime}$. Then we have $b^{\prime\prime}<b^{\prime}<b$, which implies $f(b^{\prime\prime})<f(b^{\prime})$, contradicting $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})$. If $b^{\prime}<b^{\prime\prime}<b$, we obtain the contradiction $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))>f(b^{\prime})$ analogously. Finally, if $b\leq b^{\prime\prime}$, then $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime\prime})\geq f(b)>f(b^{\prime})$, which again contradicts $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})$.

3) Let $b^{\prime}<b$ and let $\rho$ be such that $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))>f(b^{\prime})$. Towards a contradiction, assume $\mathrm{Cost}(\rho)\leq b^{\prime}$. We then obtain $f(\mathrm{Cost}(\rho))\leq f(b^{\prime})$ due to $b^{\prime}<b$ and due to $f$ being a $b$-correction function. Furthermore, due to $\mathrm{Cost}(\rho)\leq b^{\prime}$, we obtain $\mathrm{Cost}(\rho)<b$. Hence, we have $f(\mathrm{Cost}(\rho))=\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))$ due to the third property from the definition of $b$-reducibility. Since we furthermore have $f(\mathrm{Cost}(\rho))\leq f(b^{\prime})$ as argued above. This, in turn, directly implies $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\leq f(b^{\prime})$, which contradicts the assumption $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))>f(b^{\prime})$.

4) Let $\rho$ be such that $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\geq f(b)$. Towards a contradiction assume $\mathrm{Cost}(\rho)=b^{\prime}<b$. We again have $f(b^{\prime})=\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))$. However, we obtain $f(b^{\prime})<f(b)$ due to $f$ being a $b$-correction function. This contradicts $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})\geq f(b)$. ∎

These properties of correction functions when used in quantitative reductions enable us to state and prove the main result of this section, which establishes quantitative reductions as the quantitative counterpart of qualitative reductions: If $\mathcal{G}\leq^{b+1}_{\mathcal{M},f}\mathcal{G}^{\prime}$, then all plays of cost at most $b$ in $\mathcal{G}$ are “tracked” precisely in $\mathcal{G}^{\prime}$. Hence, as long as the cost of a strategy in $\mathcal{G}$ is at most $b$, it is possible to construct a strategy in $\mathcal{G}^{\prime}$ with cost at most $f(b)$. This holds true for both players.

If a strategy has cost greater than $b$, however, we do not have a direct correspondence between costs of plays in $\mathcal{G}$ and $\mathcal{G}^{\prime}$ anymore. If, however, $b$ additionally is a cap of $\mathcal{G}$, and if $\mathcal{G}$ is determined, then we can still show that Player $1$ has a strategy of infinite cost in $\mathcal{G}$ if he has a strategy of cost greater than $f(b)$ in $\mathcal{G}^{\prime}$.

Theorem 3.1

Let $\mathcal{G}$ and $\mathcal{G}^{\prime}$ be determined quantitative games with $\mathcal{G}\leq^{b+1}_{\mathcal{M},f}\mathcal{G}^{\prime}$ for some $b$, $\mathcal{M}$, and $f$, where $b\in\mathbb{N}$ is a cap of $\mathcal{G}$.

Let $b^{\prime}<b+1$. Player $i$ has a strategy $\sigma^{\prime}$ in $\mathcal{G}^{\prime}$ with $\mathrm{Cost}^{\prime}(\sigma^{\prime})=f(b^{\prime})$ if and only if they have a strategy $\sigma$ in $\mathcal{G}$ with $\mathrm{Cost}(\sigma)=b^{\prime}$. 2. 2.

If Player $1$ has a strategy $\tau^{\prime}$ in $\mathcal{G}^{\prime}$ with $\mathrm{Cost}^{\prime}(\tau^{\prime})\geq f(b+1)$, then he has a strategy $\tau$ in $\mathcal{G}$ with $\mathrm{Cost}(\tau)=\infty$.

Proof

1) We first show the direction from left to right. To this end, let $\sigma^{\prime}$ be a strategy for Player $i$ in $\mathcal{G}^{\prime}$ with $\mathrm{Cost}^{\prime}(\sigma^{\prime})=f(b^{\prime})$ for some $b^{\prime}\leq b$. We define the strategy $\sigma$ for Player $i$ in $\mathcal{G}$ for all play prefixes $\pi$ ending in a vertex in $V_{i}$ via $\sigma(\pi)=v$ if $\sigma^{\prime}(\mathrm{ext}(\pi))=(v,m)$ for some $m\in M$ and claim $\mathrm{Cost}(\sigma)=b^{\prime}$. To this end, we first show $\mathrm{Cost}(\sigma)\leq b^{\prime}$ for the case $i=0$ and $\mathrm{Cost}(\sigma)\geq b^{\prime}$ for the case $i=1$.

Let $\rho$ be an infinite play consistent with $\sigma$. A straightforward induction shows that $\rho^{\prime}=\mathrm{ext}(\rho)$ is consistent with $\sigma^{\prime}$. If $i=0$, i.e., if $\sigma$ is a strategy for Player [math], then $\mathrm{Cost}^{\prime}(\rho^{\prime})=\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\leq\mathrm{Cost}^{\prime}(\sigma^{\prime})=f(b^{\prime})$. Since we furthermore have $b^{\prime}<b+1$ by assumption and since $f$ is a $b+1$-correction function, we obtain $\mathrm{Cost}(\rho)\leq b^{\prime}$, due to Lemma 1.1 and Lemma 1.2. Since we picked $\rho$ arbitrarily from the plays consistent with $\sigma$, this in turn implies $\mathrm{Cost}(\sigma)\leq b^{\prime}$. If, however $i=1$, we directly obtain $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\geq f(b^{\prime})$ due to $\mathrm{Cost}(\sigma)\geq f(b^{\prime})$. Hence, we furthermore obtain $\mathrm{Cost}(\rho)\geq b^{\prime}$ due to Lemma 1.2 and Lemma 1.3. Since we again picked $\rho$ arbitrarily from the plays consistent with $\sigma$, this in turn implies $\mathrm{Cost}(\sigma)\geq b^{\prime}$. It remains to show $\mathrm{Cost}(\sigma)\geq b^{\prime}$ for the case $i=0$ and $\mathrm{Cost}(\sigma)\leq b^{\prime}$ for the case $i=1$.

First, since $b^{\prime}<b+1<\infty$, we obtain $f(b^{\prime})<\infty$: If $f(b^{\prime})=\infty$, we obtain $f(b^{\prime}+1)=\infty$, which contradicts strict monotonicity of $f$ up to and including $b+1\geq b^{\prime}+1$. Since $\mathrm{Cost}^{\prime}(\sigma^{\prime})=f(b^{\prime})<\infty$, there exists a play $\rho^{\prime}$ that is consistent with $\sigma^{\prime}$ such that $\mathrm{Cost}^{\prime}(\rho^{\prime})=f(b^{\prime})$.

Further, let $\rho$ be the unique play such that $\mathrm{ext}(\rho)=\rho^{\prime}$. By induction, we obtain that $\rho$ is consistent with $\sigma$. Additionally, we have $\mathrm{Cost}(\rho)=b^{\prime}$ due to $\mathrm{Cost}^{\prime}(\rho^{\prime})=\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})$ and Lemma 1.2. Hence, $\mathrm{Cost}(\sigma)\geq b^{\prime}$ if $i=0$, and $\mathrm{Cost}(\sigma)\leq b^{\prime}$ if $i=1$, which concludes the direction from left to right.

In order to show the inverse direction of the statement, let $\sigma$ be a strategy in $\mathcal{G}$ with $\mathrm{Cost}(\sigma)=b^{\prime}<b+1$. We define the strategy $\sigma^{\prime}$ for Player $i$ in $\mathcal{G}^{\prime}$ for all play prefixes $\mathrm{ext}(\pi)=(v_{0},m_{0})\cdots(v_{j},m_{j})$ ending in a vertex in $V_{i}\times M$ as $\sigma^{\prime}(\mathrm{ext}(\pi))=(v,\mathrm{Upd}(m_{j},v))$ if $\sigma(\pi)=v$ and claim $\mathrm{Cost}^{\prime}(\sigma^{\prime})=f(b^{\prime})$.

Let $\mathrm{ext}(\rho)$ be a play consistent with $\sigma^{\prime}$. A straightforward induction yields that $\rho$ is consistent with $\sigma$, hence, if $i=0$, then $\mathrm{Cost}(\rho)\leq b^{\prime}$ and thus $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\leq f(b^{\prime})$ due to $b^{\prime}<b+1$. Dually, if $i=1$, then $\mathrm{Cost}(\rho)\geq b^{\prime}$ and $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\geq f(b^{\prime})$. Hence, we obtain $\mathrm{Cost}^{\prime}(\sigma^{\prime})\leq f(b^{\prime})$ if $i=0$ as well as $\mathrm{Cost}^{\prime}(\sigma^{\prime})\geq f(b^{\prime})$ if $i=1$. It remains to show $\mathrm{Cost}^{\prime}(\sigma^{\prime})\geq f(b^{\prime})$ and $\mathrm{Cost}^{\prime}(\sigma^{\prime})\leq f(b^{\prime})$ in the former and latter case, respectively.

Now let $\rho$ be a play consistent with $\sigma$ such that $\mathrm{Cost}(\rho)=b^{\prime}$. Since $b^{\prime}<\infty$, such a play exists. Via another straightforward induction we obtain that $\mathrm{ext}(\rho)$ is consistent with $\sigma^{\prime}$. As $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=f(b^{\prime})$, we furthermore obtain $\mathrm{Cost}^{\prime}(\sigma^{\prime})\geq f(b^{\prime})$ if $i=0$ and $\mathrm{Cost}^{\prime}(\sigma^{\prime})\leq f(b^{\prime})$ if $i=1$, which concludes the proof of this statement.

2) Let $\tau^{\prime}$ be a strategy for Player $1$ in $\mathcal{G}^{\prime}$ with $\mathrm{Cost}^{\prime}(\tau^{\prime})\geq f(b+1)$. We define the strategy $\tau$ for Player $1$ in $\mathcal{G}$ via $\tau(\pi)=v$ if $\tau^{\prime}(\mathrm{ext}(\pi))=(v,m)$ for all play prefixes $\pi$ in $\mathcal{G}$. Let $\rho$ be a play consistent with $\tau$ and define $\rho^{\prime}=\mathrm{ext}(\rho)$. A straightforward induction yields that $\rho^{\prime}$ is consistent with $\tau^{\prime}$. Since $\mathrm{Cost}^{\prime}(\tau^{\prime})\geq f(b+1)$, we obtain $\mathrm{Cost}^{\prime}(\rho^{\prime})\geq f(b+1)$. Then, we obtain $\mathrm{Cost}(\rho)\geq b+1$ due to Lemma 1.4. Since we picked $\rho$ arbitrarily from the plays consistent with $\tau$, we directly obtain $\mathrm{Cost}(\tau)\geq b+1$. Since $b$ is a cap of $\mathcal{G}$ and due to determinacy of $\mathcal{G}$, this implies that there exists a strategy $\tau^{\prime\prime}$ for Player $1$ in $\mathcal{G}$ such that $\mathrm{Cost}(\tau^{\prime\prime})=\infty$. ∎

We proved Theorem 3.1 by constructing optimal strategies for Player [math] in $\mathcal{G}$ from optimal strategies for her in $\mathcal{G}^{\prime}$. These strategies use the set of all play prefixes of $\mathcal{G}^{\prime}$ as memory states and may thus be of infinite size. If Player [math] can achieve a certain cost in $\mathcal{G}^{\prime}$ using a finite-state strategy, however, then she can achieve the corresponding cost in $\mathcal{G}$ with a finite-state strategy as well.

Theorem 3.2

Let $\mathcal{G}$ and $\mathcal{G}^{\prime}$ be quantitative games such that $\mathcal{G}\leq^{b}_{\mathcal{M}_{1},f}\mathcal{G}^{\prime}$ for some $b$, $\mathcal{M}_{1}$, and $f$ and let either $b^{\prime}<b$ or $b^{\prime}=b=\infty$. If Player $i$ has a finite-state strategy $\sigma^{\prime}$ with $\mathrm{Cost}^{\prime}(\sigma^{\prime})=f(b^{\prime})$ in $\mathcal{G}^{\prime}$ that is implemented by $\mathcal{M}_{2}$, then she has a finite-state strategy $\sigma$ with $\mathrm{Cost}(\sigma)=b^{\prime}$ in $\mathcal{G}$ that is implemented by $\mathcal{M}_{1}\times\mathcal{M}_{2}$.

Proof

Let $\mathcal{G}=(\mathcal{A},\mathrm{Cost})$, $\mathcal{G}^{\prime}=(\mathcal{A}^{\prime},\mathrm{Cost}^{\prime})$, $\mathcal{M}_{1}=(M_{1},m^{1}_{I},\mathrm{Upd}_{1})$, and $\mathcal{M}_{2}=(M_{2},m^{2}_{I},\mathrm{Upd}_{2})$ such that $\sigma^{\prime}$ is implemented by $\mathcal{M}_{2}$ with the next-move function $\mathrm{Nxt}^{\prime}\colon(V\times M_{1})\times M_{2}\rightarrow(V\times M_{1})$. We define $\mathrm{Nxt}(v,(m_{1},m_{2}))=v^{*}$ if $\mathrm{Nxt}^{\prime}((v,m_{1}),m_{2})=(v^{*},\mathrm{Upd}_{1}(m_{1},v^{*}))$. We moreover define $\sigma$ as the strategy that is implemented by $\mathcal{M}_{1}\times\mathcal{M}_{2}$ with the next-move function $\mathrm{Nxt}$.

Let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play consistent with $\sigma$, let

[TABLE]

be its extension with respect to $\mathcal{M}_{1}\times\mathcal{M}_{2}$, and let $j\in\mathbb{N}$ be such that $v_{j}\in V_{i}$. We obtain $v_{j+1}=\sigma(v_{0}\cdots v_{j})=\mathrm{Nxt}(v_{j},(m_{1}^{j},m_{2}^{j}))$. Due to the definition of $\mathrm{Nxt}$, this implies $\mathrm{Nxt}^{\prime}((v_{j},m_{1}^{j}),m_{2}^{j})=(v_{j+1},m_{1}^{j+1})$, where $m_{1}^{j+1}=\mathrm{Upd}_{1}(m_{1}^{j},v_{j+1})$ due to the construction of $\mathcal{A}\times\mathcal{M}_{1}$. Hence, $\mathrm{ext}_{\mathcal{M}_{1}}(\rho)$ is consistent with $\sigma^{\prime}$, i.e., $\mathrm{Cost}^{\prime}(\mathrm{ext}_{\mathcal{M}_{1}}(\rho))\leq f(b^{\prime})$, which in turn implies $\mathrm{Cost}(\rho)\leq b^{\prime}$ for $i=0$ due to Lemma 1.1 and Lemma 1.2, and $\mathrm{Cost}^{\prime}(\mathrm{ext}_{\mathcal{M}_{1}}(\rho))\geq f(b^{\prime})$ and $\mathrm{Cost}(\rho)\geq b^{\prime}$ for $i=1$.

Due to similar reasoning, for each play $\mathrm{ext}_{\mathcal{M}_{1}}(\rho)$ consistent with $\sigma^{\prime}$, the play $\rho$ is consistent with $\sigma$. If $i=1$ or $b^{\prime}<\infty$, this concludes the proof. If, however, $i=0$ and $b^{\prime}=\infty$, then we furthermore obtain that $b=\infty$ and that $f$ is a strictly monotonic function with $f(\infty)=\infty$. Hence, if there exists a play $\mathrm{ext}_{\mathcal{M}_{1}}(\rho)$ consistent with $\sigma^{\prime}$ with $\mathrm{Cost}^{\prime}(\mathrm{ext}_{\mathcal{M}_{1}}(\rho))=\infty$, then $\mathrm{Cost}(\rho)=\infty$ and, hence, $\mathrm{Cost}(\sigma)=\infty$. If, however, the costs of the plays consistent with $\sigma^{\prime}$ diverges, then the cost of the plays consistent with $\sigma$ diverges as well and we obtain $\mathrm{Cost}(\sigma)=\infty$. ∎

Theorem 3.1 and Theorem 3.2 show that quantitative reductions indeed exhibit properties analogous to those of qualitative reductions in the quantitative setting. Recall that in addition to retaining winning plays and to allowing the implementation of finite-state strategies, qualitative reductions furthermore are transitive: If $\mathcal{G}$, $\mathcal{G}^{\prime}$, and $\mathcal{G}^{\prime\prime}$ are qualitative games such that $\mathcal{G}\leq\mathcal{G}^{\prime}$, and such that $\mathcal{G}^{\prime}\leq\mathcal{G}^{\prime\prime}$, then $\mathcal{G}\leq\mathcal{G}^{\prime\prime}$. We now show that quantitative reductions are transitive as well.

Theorem 3.3

Let $\mathcal{G}_{1},\mathcal{G}_{2},\mathcal{G}_{3}$ be quantitative games such that $\mathcal{G}_{1}\leq^{b_{1}}_{\mathcal{M}_{1},f_{1}}\mathcal{G}_{2}$ and $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{M}_{2},f_{2}}\mathcal{G}_{3}$ for some $b_{1},b_{2}\in\mathbb{N}_{\infty}$, some memory structures $\mathcal{M}_{1},\mathcal{M}_{2}$, and some $b_{1}$- and $b_{2}$-correction functions $f_{1}$ and $f_{2}$, respectively.

Then, we have $\mathcal{G}_{1}\leq^{b}_{\mathcal{M},f}\mathcal{G}_{3}$, where $\mathcal{M}=\mathcal{M}_{1}\times\mathcal{M}_{2}$, $f=f_{2}\circ f_{1}$, and $b=b_{1}$ if $b_{2}\geq f_{1}(b_{1})$ and $b=\max\{b^{\prime}\mid f_{1}(b^{\prime})\leq b_{2}\}$ otherwise.

Proof

For each $j\in\{1,2,3\}$, let $\mathcal{G}_{j}=(\mathcal{A}_{j},\mathrm{Cost}_{j})$. Recall that in order to show $\mathcal{G}_{1}\leq^{b}_{\mathcal{M},f}\mathcal{G}_{3}$ we have to show that

• •

$\mathcal{A}_{3}=\mathcal{A}_{1}\times\mathcal{M}_{1}\times\mathcal{M}_{2}$,

• •

$f_{2}\circ f_{1}$ is a $b$-reduction function,

• •

for all plays $\rho$ of $\mathcal{A}_{1}$ with $\mathrm{Cost}_{1}(\rho)<b$ we have $\mathrm{Cost}_{3}(\mathrm{ext}_{\mathcal{M}_{1}\times\mathcal{M}_{2}}(\rho))=(f_{2}\circ f_{1})(\mathrm{Cost}_{1}(\rho))$, and

• •

for all plays $\rho$ of $\mathcal{A}_{1}$ with $\mathrm{Cost}_{1}(\rho)\geq b$ we have $\mathrm{Cost}_{3}(\mathrm{ext}_{\mathcal{M}_{1}\times\mathcal{M}_{2}}(\rho))\geq(f_{2}\circ f_{1})(b)$.

We show all these items individually.

Clearly, we have

[TABLE]

We now show that $f_{2}\circ f_{1}$ is a $b$-correction function, for $b$ defined as in the statement of the theorem. Recall that to this end we have to show that

• •

for all $x<x^{\prime}<b$ we have $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(x^{\prime})$,

• •

for all $x<b$ we have $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(b)$, and

• •

for all $x\geq b$ we have $(f_{2}\circ f_{1})(x)\geq(f_{2}\circ f_{1})(b)$.

Furthermore recall that we defined

[TABLE]

We treat both cases of this definition separately.

First, assume $b_{2}\geq f_{1}(b_{1})$. In this case we have $b=b_{1}$. We show the three items of the definition of a $b$-correction function independently.

• •

First, pick $x$ and $x^{\prime}$ such that $x<x^{\prime}<b=b_{1}$. We show $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(x^{\prime})$. Since $f_{1}$ is a $b_{1}$-correction function, we obtain $f_{1}(x)<f_{1}(x^{\prime})$, $f_{1}(x)<f_{1}(b_{1})$, and $f_{1}(x^{\prime})<f_{1}(b_{1})$. Since, furthermore, $f_{2}$ is a $b_{2}$-correction function and as $f_{1}(b_{1})\leq b_{2}$ by assumption, we moreover obtain $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(x^{\prime})$.

• •

Now pick some $x$ such that $x<b=b_{1}$. We show $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(b)$. Since $f_{1}$ is a $b_{1}$-correction function, we directly obtain $f_{1}(x)<f_{1}(b_{1})$. Since $f_{1}(b_{1})\leq b_{2}$ by assumption and since $f_{2}$ is a $b_{2}$-correction function, this directly yields $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(b_{1})=(f_{2}\circ f_{1})(b)$.

• •

Finally, pick some $x$ such that $x\geq b=b_{1}$. Then $f_{1}(x)\geq f_{1}(b_{1})$, since, again, $f_{1}$ is a $b_{1}$-correction function. If $f_{1}(x)<b_{2}$, then $(f_{2}\circ f_{1})(x)\geq(f_{2}\circ f_{1})(b_{1})$. If, however, $f_{1}(x)\geq b_{2}$, then $(f_{2}\circ f_{1})(x)\geq f_{2}(b_{2})\geq(f_{2}\circ f_{1})(b_{1})$, where the latter inequality follows from the assumption $b_{2}\geq f_{1}(b_{1})$. This concludes this part of the proof.

Now assume $b_{2}<f_{1}(b_{1})$ and let $b$ be maximal such that $f_{1}(b)\leq b_{2}$. We first argue that we have $b\leq b_{1}$ in this case. Towards a contradiction assume $b_{1}<b$. This implies $f_{1}(b_{1})\leq f_{1}(b)$ due to $f_{1}$ being a $b_{1}$-correction function. However, we have $f_{1}(b)\leq b_{2}<f_{1}(b_{1})$, where the former inequality results from the definition of $b$, while the latter one is due to our initial assumption. This directly contradicts $f_{1}(b_{1})\leq f_{1}(b)$, hence we obtain $b\leq b_{1}$.

We again show that $f_{2}\circ f_{1}$ is a $b$-correction function by showing the three items of the definition independently.

• •

First, pick $x$ and $x^{\prime}$ such that $x<x^{\prime}<b$. Since $b\leq b_{1}$ we obtain $f_{1}(x)<f_{1}(x^{\prime})<f_{1}(b)$ due to $f_{1}$ being a $b_{1}$-correction function. As $f_{1}(b)\leq b_{2}$ due to the definition of $b$, we directly obtain $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(x^{\prime})$.

• •

Now, pick $x$ such that $x<b$. We obtain $(f_{2}\circ f_{1})(x)<(f_{2}\circ f_{1})(b)$ via reasoning analogous to the previous case.

• •

Finally, pick $x$ such that $b\leq x$. We show $(f_{2}\circ f_{1})(b)\leq(f_{2}\circ f_{1})(x)$. To this end, we first observe that we have $f_{1}(b)\leq f_{1}(x)$ by leveraging different properties of $f_{1}$ being a $b_{1}$-correction function, depending on whether we have $b\leq x<b_{1}$ or $b\leq b_{1}\leq x$. The case $b_{1}<b\leq x$ is excluded due to $b\leq b_{1}$ as argued above. We furthermore obtain $(f_{2}\circ f_{1})(b)\leq(f_{2}\circ f_{1})(x)$ by similar reasoning, using different properties of $f_{2}$ being a $b_{2}$-correction function, depending on whether we have $f_{1}(b)\leq b_{2}\leq f_{1}(x)$ or $f_{1}(b)\leq f_{1}(x)<b_{2}$. Again, the case $b_{2}<f_{1}(b)\leq f_{1}(x)$ is excluded due to the definition of $b$.

Thus, we have shown that $f_{2}\circ f_{1}$ is indeed a $b$-correction function. It remains to prove the latter two conditions from the definition of $\mathcal{G}_{1}\leq^{b}_{\mathcal{M},f}\mathcal{G}_{3}$. We first aim to show that for all plays $\rho$ of $\mathcal{A}_{1}$ with $\mathrm{Cost}_{1}(\rho)<b$ we have $\mathrm{Cost}_{3}(\mathrm{ext}_{\mathcal{M}_{1}\times\mathcal{M}_{2}}(\rho))=(f_{2}\circ f_{1})(\mathrm{Cost}_{1}(\rho))$. To this end, let $\rho$ be a play of $\mathcal{A}_{1}$ with $\mathrm{Cost}_{1}(\rho)<b$. For the sake of consistency and readability, we define $\rho_{1}=\rho$, $\rho_{2}=\mathrm{ext}_{\mathcal{M}_{1}}(\rho_{1})$, and $\rho_{3}=\mathrm{ext}_{\mathcal{M}_{2}}(\rho_{2})=\mathrm{ext}_{\mathcal{M}_{1}\times\mathcal{M}_{2}}(\rho_{1})$. We again treat both cases of the definition of $b$ separately.

We again first consider the case that $b_{2}\geq f_{1}(b_{1})$. We then directly obtain $b=b_{1}$ due to the definition of $b$. This yields $\mathrm{Cost}_{1}(\rho_{1})<b_{1}$, which in turn implies $f_{1}(\mathrm{Cost}_{1}(\rho_{1}))=\mathrm{Cost}_{2}(\rho_{2})$ due to $\mathcal{G}_{1}\leq^{b_{1}}_{\mathcal{M}_{1},f_{1}}\mathcal{G}_{2}$. Furthermore, since $\mathrm{Cost}_{1}(\rho_{1})<b_{1}$ and since $f_{1}$ is a $b_{1}$-correction function we have $f_{1}(\mathrm{Cost}_{1}(\rho_{1}))<f_{1}(b_{1})$, which directly yields $\mathrm{Cost}_{2}(\rho_{2})<f_{1}(b_{1})$ via the equation above. Since $f_{1}(b_{1})\leq b_{2}$, we further obtain $\mathrm{Cost}_{2}(\rho_{2})<b_{2}$. Due to $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{M}_{2},f_{2}}\mathcal{G}_{3}$ this then implies $\mathrm{Cost}_{3}(\rho_{3})=f_{2}(\mathrm{Cost}_{2}(\rho_{2}))$. By again applying $f_{1}(\mathrm{Cost}_{1}(\rho_{1}))=\mathrm{Cost}_{2}(\rho_{2})$, we obtain the desired result of $\mathrm{Cost}_{3}(\rho_{3})=(f_{2}\circ f_{1})(\mathrm{Cost}_{1}(\rho_{1}))$.

Now consider the case that $b_{2}<f_{1}(b_{1})$. In this case, we have $b=\max\{b^{\prime}\mid f_{1}(b^{\prime})\leq b_{2}\}$ by definition of $b$. As argued above, we have $b\leq b_{1}$ in this case, which directly implies $\mathrm{Cost}_{1}(\rho_{1})<b_{1}$. Due to $\mathcal{G}_{1}\leq^{b_{1}}_{\mathcal{M}_{1},f_{1}}\mathcal{G}_{2}$ this yields $f_{1}(\mathrm{Cost}_{1}(\rho_{1}))=\mathrm{Cost}_{2}(\rho_{2})$. Moreover, we again have $f_{1}(b)\leq b_{2}$ by definition of $b$. Since $\mathcal{G}_{1}\leq^{b_{1}}_{\mathcal{M}_{1},f_{1}}\mathcal{G}_{2}$ and since $\mathrm{Cost}_{1}(\rho_{1})<b$, the latter due to our choice of $\rho_{1}$, we also obtain $f_{1}(\mathrm{Cost}_{1}(\rho_{1}))<f_{1}(b)$. Moreover, we have $f_{1}(b)\leq b_{2}$ due to the definition of $b$. Hence, we obtain $f_{1}(\mathrm{Cost}_{1}(\rho_{1}))<b_{2}$. By applying $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{M}_{2},f_{2}}\mathcal{G}_{3}$ analogously to the previous case, we obtain the desired result of $\mathrm{Cost}_{3}(\rho_{3})=(f_{2}\circ f_{1})(\mathrm{Cost}_{1}(\rho_{1}))$.

It remains to show the final item in the definition of $b$-reducibility, i.e., that we indeed have $\mathrm{Cost}_{3}(\mathrm{ext}_{\mathcal{M}_{1}\times\mathcal{M}_{2}}(\rho))\geq(f_{2}\circ f_{1})(b)$ for all plays $\rho$ of $\mathcal{A}_{1}$ with $\mathrm{Cost}_{1}(\rho)\geq b$. To this end, let $\rho$ be a play of $\mathcal{A}_{1}$ with $\mathrm{Cost}_{1}(\rho)\geq b$. For the sake of brevity and consistency we again define $\rho_{1}=\rho$, $\rho_{2}=\mathrm{ext}_{\mathcal{M}_{1}}(\rho)$, and $\rho_{3}=\mathrm{ext}_{\mathcal{M}_{2}}(\rho_{2})=\mathrm{ext}_{\mathcal{M}_{1}\times\mathcal{M}_{2}}(\rho_{1})$. We again treat the two cases from the definition of $b$ separately.

First, assume $b_{2}\geq f_{1}(b_{1})$. We directly obtain $b=b_{1}$ by definition of $b$, which in turn implies $\mathrm{Cost}_{2}(\rho_{2})\geq f_{1}(b_{1})$ due to $\mathcal{G}_{1}\leq^{b_{1}}_{\mathcal{M}_{1},f_{1}}\mathcal{G}_{2}$. If $b_{2}>\mathrm{Cost}_{2}(\rho_{2})$, then we directly obtain $f_{2}(\mathrm{Cost}_{2}(\rho_{2}))\geq(f_{2}\circ f_{1})(b_{1})$ since $f_{2}$ is a $b_{2}$-correction function. Since we have $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{M}_{2},f_{2}}\mathcal{G}_{3}$, we moreover obtain $f_{2}(\mathrm{Cost}_{2}(\rho_{2}))=\mathrm{Cost}_{3}(\rho_{3})$, which in turn yields $\mathrm{Cost}_{3}(\rho_{3})\geq(f_{2}\circ f_{1})(b_{1})=(f_{2}\circ f_{1})(b)$. If, however, $\mathrm{Cost}_{2}(\rho_{2})\geq b_{2}$, then we obtain $\mathrm{Cost}_{3}(\rho_{3})\geq f_{2}(b_{2})\geq(f_{2}\circ f_{1})(b_{1})=(f_{2}\circ f_{1})(b)$, where the former inequality is implied by $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{M}_{2},f_{2}}\mathcal{G}_{3}$ while we obtain the latter due to $f_{2}$ being a $b_{2}$-correction function and due to $b_{2}\geq f_{1}(b_{1})$.

Now consider the case $b_{2}<f_{1}(b_{1})$. Here, we again distinguish two sub-cases. If $\mathrm{Cost}_{1}(\rho_{1})\geq b_{1}$, then we obtain $\mathrm{Cost}_{2}(\rho_{2})\geq f_{1}(b_{1})>b_{2}\geq f_{1}(b)$. The three inequalities result from $\mathcal{G}_{1}\leq^{b_{1}}_{\mathcal{M}_{1},f_{1}}\mathcal{G}_{2}$, from the assumption above, and from the definition of $b$, respectively. We furthermore obtain $\mathrm{Cost}_{3}(\rho_{3})\geq f_{2}(b_{2})\geq(f_{2}\circ f_{1})(b)$, where the former inequality is due to $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{M}_{2},f_{2}}\mathcal{G}_{3}$ and $\mathrm{Cost}_{2}(\rho_{2})>b_{2}$, while the latter one results from $f_{2}$ being a $b_{2}$-correction function and from $b_{2}\geq f_{1}(b)$.

It remains to consider the case $b_{1}>\mathrm{Cost}_{1}(\rho_{1})$. In this case, we directly obtain $\mathrm{Cost}_{2}(\rho_{2})=f_{1}(\mathrm{Cost}_{1}(\rho_{1}))\geq f_{1}(b)$. The former equality is due to $\mathcal{G}_{1}\leq^{b_{1}}_{\mathcal{M}_{1},f_{1}}\mathcal{G}_{2}$, while the latter results from the assumption $\mathrm{Cost}_{1}(\rho_{1})\geq b$ and the fact that $f_{1}$ is a $b_{1}$-correction function. We again distinguish two cases based on the relation of $b_{2}$ to $f_{1}(b)$ and $\mathrm{Cost}_{2}(\rho_{2})$: Either we have $\mathrm{Cost}_{2}(\rho_{2})\geq b_{2}\geq f_{1}(b)$, or we have $b_{2}>\mathrm{Cost}_{2}(\rho_{2})\geq f_{1}(b)$. In the former case, we obtain $\mathrm{Cost}_{3}(\rho_{3})\geq f_{2}(b_{2})\geq(f_{2}\circ f_{1})(b)$, where the former and latter inequality are due to $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{M}_{2},f_{2}}\mathcal{G}_{3}$ and due to $f_{2}$ being a $b_{2}$-reduction function, respectively. In the latter case, we similarly obtain $f_{2}(\mathrm{Cost}_{2}(\rho_{2}))=\mathrm{Cost}_{3}(\rho_{3})\geq(f_{2}\circ f_{1})(b)$, where the former equality again results from $\mathcal{G}_{2}\leq^{b_{2}}_{\mathcal{G}_{2},f_{2}}\mathcal{G}_{3}$, while the latter inequality is again due to $f_{2}$ being a $b_{2}$-correction function. ∎

By using quantitative reductions we are able to structure the space of quantitative games similarly to that of qualitative games. While for qualitative games, there exist direct solutions to a number of well-studied winning conditions, for quantitative games, no such direct solutions for the threshold problems exist to the best of our knowledge. Instead, the threshold problem for quantitative games is usually solved by reducing the quantitative game to a qualitative game for a fixed bound $b$.

Hence, there does not yet exist a “foundation” of the space of quantitative winning conditions analogous to that of the space of qualitative winning conditions, i.e., there is no canonical simple class of quantitative games that provides a natural target for quantitative reductions. In the following section, we provide such a foundation in the form of vertex-ranked games.

4 Vertex-Ranked Games

We introduce two very simple kinds of quantitative games, which we call vertex-ranked games. In such games, the cost of a play is determined solely by a qualitative winning condition and a ranking of the vertices of the arena by natural numbers. We show that solving the threshold problem for either kind of game is possible with only a polynomial overhead over solving the underlying qualitative game.

Furthermore, we show that the memory structures implementing winning strategies for either player only incur a polynomial overhead in comparison to the memory structures implementing winning strategies for the underlying conditions. Finally, we briefly discuss the optimization problem for such games, i.e., the problem of determining the minimal $b$ such that Player [math] has a strategy of cost at most $b$ in such a game. We argue that determining such $b$ incurs only a polynomial overhead over solving the underlying qualitative game.

Let $\mathcal{A}$ be an arena with vertex set $V$, let $\mathrm{Win}\subseteq(V^{\prime})^{\omega}$ be a qualitative winning condition, and let $\mathrm{rk}\colon V\rightarrow\mathbb{N}$ be a ranking function on vertices. We define the quantitative vertex-ranked $\sup$-condition

[TABLE]

as well as its prefix-independent version, the vertex-ranked $\limsup$-condition

[TABLE]

A vertex-ranked $\sup$- or $\limsup$-game $\mathcal{G}=(\mathcal{A},{\textsc{Rank}^{X}}(\mathrm{Win},\mathrm{rk}))$ with $X\in\{\sup,\lim\}$ consists of an arena $\mathcal{A}$ with vertex set $V$, a qualitative winning condition $\mathrm{Win}$, and a vertex-ranking function $\mathrm{rk}\colon V\rightarrow\mathbb{N}$.

If $\mathcal{G}_{X}=(\mathcal{A},{\textsc{Rank}^{X}}(\mathrm{Win},\mathrm{rk}))$ is a vertex-ranked $\sup$- or $\limsup$-game, we call the game $(\mathcal{A},\mathrm{Win})$ the qualitative game corresponding to $\mathcal{G}_{X}$. Moreover, if $\mathcal{G}_{\sup}$ is a vertex-ranked $\sup$-game, we denote the vertex-ranked $\limsup$-game with the same arena, winning condition, and rank function by $\mathcal{G}_{\lim}$ and vice versa. In either case, we denote the corresponding qualitative game by $\mathcal{G}$.

Before showing how to solve vertex-ranked $\sup$- and $\limsup$-games, we argue that these games allow straightforward adaptations of qualitative winning conditions to quantitative ones. This is witnessed by the following theorem.

Theorem 4.1

Let $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ and $\mathcal{G}^{\prime}=(\mathcal{A}^{\prime},\mathrm{Win}^{\prime})$ be qualitative games and let $\mathcal{M}$ be a memory structure such that $\mathcal{G}\leq_{\mathcal{M}}\mathcal{G}^{\prime}$. Moreover, let $\mathrm{rk}$ be a ranking function on vertices of $\mathcal{G}$ and let $b$ be the maximal rank assigned to a vertex of $\mathcal{G}$ by $\mathrm{rk}$. Then, $\mathcal{G}_{\sup}\leq^{b+1}_{\mathcal{M}}\mathcal{G}_{\sup}^{\prime}$, where $\mathcal{G}_{\sup}=(\mathcal{A},{\textsc{Rank}^{\sup}}(\mathrm{Win},\mathrm{rk}))$ and $\mathcal{G}_{\sup}^{\prime}=(\mathcal{A}^{\prime},{\textsc{Rank}^{\sup}}(\mathrm{Win}^{\prime},\mathrm{rk}^{\prime}))$ with $\mathrm{rk}^{\prime}(v,m)=\mathrm{rk}(v)$.

Proof

Clearly, we have $\mathcal{A}^{\prime}=\mathcal{A}\times\mathcal{M}$ due to $\mathcal{G}\leq\mathcal{G}^{\prime}$. Moreover, as argued above, $\text{cap}_{b+1}$ is a $b+1$-correction function. Hence, it remains to show that the latter two conditions in the definition of a quantitative reduction are satisfied.

To this end, let $\rho$ be a play in $\mathcal{A}$. If the cost of $\rho$ is less than $b+1$, then we obtain $\rho\in\mathrm{Win}$ by definition of $b$ and by definition of the vertex-ranked $\sup$-condition. This, in turn, implies $\mathrm{ext}(\rho)\in\mathrm{Win}^{\prime}$ due to $\mathcal{G}\leq\mathcal{G}^{\prime}$. Hence, we obtain

[TABLE]

If, however, the cost of $\rho$ is at least $b+1$, then we have $\rho\notin\mathrm{Win}$, again due to the definition of $b$, which implies both ${\textsc{Rank}^{\sup}}(\mathrm{Win},\mathrm{rk})(\rho)=\infty$ as well as $\mathrm{ext}(\rho)\notin\mathrm{Win}$ due to $\mathcal{G}\leq\mathcal{G}^{\prime}$. Hence, we obtain

[TABLE]

which concludes the proof of the fourth condition of quantitative reductions. ∎

Clearly, the above proof can be adapted in a very straightforward way to show the analogous result for the case of vertex-ranked $\limsup$-games.

Remark 1

Let $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ and $\mathcal{G}^{\prime}=(\mathcal{A}^{\prime},\mathrm{Win}^{\prime})$ be qualitative games and let $\mathcal{M}$ be a memory structure such that $\mathcal{G}\leq_{\mathcal{M}}\mathcal{G}^{\prime}$. Moreover, let $\mathrm{rk}$ be a ranking function on vertices of $\mathcal{G}$ and let $b$ be the maximal rank assigned to a vertex of $\mathcal{G}$ by $\mathrm{rk}$. Then, $\mathcal{G}_{\lim}\leq^{b+1}_{\mathcal{M}}\mathcal{G}_{\lim}^{\prime}$, where $\mathcal{G}_{\lim}=(\mathcal{A},{\textsc{Rank}^{\lim}}(\mathrm{Win},\mathrm{rk}))$ and $\mathcal{G}_{\lim}^{\prime}=(\mathcal{A}^{\prime},{\textsc{Rank}^{\lim}}(\mathrm{Win}^{\prime},\mathrm{rk}^{\prime}))$ with $\mathrm{rk}^{\prime}(v,m)=\mathrm{rk}(v)$.

The remainder of this section is dedicated to providing bounds on the complexity of solving vertex-ranked games with respect to some given bound. In particular, we show that vertex-ranked $\sup$-games can be solved with only an additive linear blowup compared to the complexity of solving the corresponding qualitative games. Vertex-ranked $\limsup$-games, on the other hand, can be solved while incurring only a polynomial blowup compared to solving the corresponding qualitative games.

4.1 Solving Vertex-Ranked $\sup$-Games

We begin by observing that solving vertex-ranked $\sup$-games is at least as hard as solving the underlying qualitative games, since the former subsumes the latter. This is due to the fact that Player [math] has a winning strategy in $(\mathcal{A},\mathrm{Win})$ if and only if she has a strategy with cost at most zero in $(\mathcal{A},{\textsc{Rank}^{\sup}}(\mathrm{Win},\mathrm{rk}))$, where $\mathrm{rk}$ is the constant function assigning zero to every vertex.

We now turn our attention to finding an upper bound for the complexity of the threshold problem for vertex-ranked $\sup$-games. To achieve a general treatment of such games, we first introduce some notation. Let $\mathfrak{G}$ be a class of qualitative games. We define the extension of $\mathfrak{G}$ to vertex-ranked $\sup$-games as

[TABLE]

We first show that we can use a decision procedure solving games from $\mathfrak{G}$ to solve games from ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ with respect to a given $b$. To this end, we remove all vertices from which Player $1$ can enforce a visit to a vertex of rank greater than $b$ and proclaim that Player [math] wins the quantitative game with respect to $b$ if and only if she wins the qualitative game corresponding to the resulting quantitative game. To ensure that we are able to solve the resulting qualitative game, we assume some closure properties of $\mathfrak{G}$. To this end, we first introduce some notation.

Let $\mathcal{G}$ be a qualitative or quantitative game with vertex set $V$. For each $v\in V$, we write $\mathcal{G}_{v}$ to denote the game $\mathcal{G}$ with its initial vertex replaced by $v$. All other components, i.e., the structure of the arena and the cost-function, remain unchanged. Let $\mathcal{A}=(V,V_{0},V_{1},E,v_{I})$ and $\mathcal{A}^{\prime}=(V^{\prime},V^{\prime}_{0},V^{\prime}_{1},E^{\prime},v^{\prime}_{I})$ be arenas. We say that $\mathcal{A}^{\prime}$ is a sub-arena of $\mathcal{A}$ if $V^{\prime}\subseteq V$, $V^{\prime}_{0}\subseteq V_{0}$, $V^{\prime}_{1}\subseteq V_{1}$, $E^{\prime}\subseteq E$, and $v_{I}=v^{\prime}_{I}$ and write $\mathcal{A}^{\prime}\sqsubseteq\mathcal{A}$ in this case.

We call a class of qualitative (or quantitative) games $\mathfrak{G}$ proper if

• •

for each $(\mathcal{A},\mathrm{Win})$ (or $(\mathcal{A},\mathrm{Cost})$) in $\mathfrak{G}$ and each sub-arena $\mathcal{A}^{\prime}\sqsubseteq\mathcal{A}$ the game $(\mathcal{A}^{\prime},\mathrm{Win}^{\prime})$ (or $(\mathcal{A}^{\prime},\mathrm{Cost}^{\prime})$), where $\mathrm{Win}^{\prime}$ (or $\mathrm{Cost}^{\prime}$) is the restriction of $\mathrm{Win}$ (or $\mathrm{Cost}$) to plays from $\mathcal{A}^{\prime}$, is a member of $\mathfrak{G}$ as well, if

• •

for each game $\mathcal{G}\in\mathfrak{G}$ and each vertex $v$ of $\mathcal{G}$ we have $\mathcal{G}_{v}\in\mathfrak{G}$, if

• •

all games in $\mathfrak{G}$ are determined, and if

• •

all $\mathcal{G}\in\mathfrak{G}$ are finitely representable.

Intuitively, the first condition ensures that games obtained by removing vertices or edges from games in $\mathfrak{G}$ are members of $\mathfrak{G}$ as well, whereas the latter three conditions are very weak technical requirements. In particular the requirement that all games included in the class must be finitely representable serves mainly to enable us to talk about the size of a game.

Using this notion of proper classes of games, we are now able to formulate the main result of this section regarding vertex-ranked $\sup$-games.

Theorem 4.2

Let $\mathfrak{G}$ be a proper class of qualitative games $\mathcal{G}$ that can be solved in time $t(|\mathcal{G}|)$ and space $s(|\mathcal{G}|)$, where $t$ and $s$ are monotonic functions.

Then, the following problem can be solved in time $\mathcal{O}(n)+t(|\mathcal{G}|)$ and space $\mathcal{O}(n)+s(|\mathcal{G}|)$: “Given some game $\mathcal{G}_{\sup}\in{\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ with $n$ vertices and some bound $b\in\mathbb{N}$, does Player [math] win $\mathcal{G}_{\sup}$ with respect to $b$?”

Intuitively, in order to prove Theorem 4.2, we show that Player [math] wins $\mathcal{G}_{\sup}\in{\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ with respect to some bound $b$ if and only if

• •

Player $1$ cannot enforce a visit to vertices of rank greater than $b$ from $v_{I}$, and if

• •

she is able to win the game $\mathcal{G}_{\sup}$ without visiting any vertices from which Player $1$ is able to enforce a visit to a vertex of rank greater than $b$.

We formalize the idea of removing vertices from which one player can enforce a visit to some set of vertices by first recalling the attractor construction. Let $\mathcal{A}=(V,V_{0},V_{1},E,v_{I})$ be an arena with $n$ vertices and let $X\subseteq V$. We define $\mathrm{Attr}_{i}(X)=\mathrm{Attr}_{i}^{n}(X)$ inductively with $\mathrm{Attr}_{i}^{0}(X)=X$ and

[TABLE]

Intuitively, the $i$-attractor $\mathrm{Attr}_{i}(X)$ is the set of all vertices from which Player $i$ can enforce a visit to $X$. The set $\mathrm{Attr}_{i}(X)$ can be computed in linear time in $|E|$ and Player $i$ has a positional strategy $\sigma$ such that each play starting in some vertex in $\mathrm{Attr}_{i}(X)$ and consistent with $\sigma$ eventually encounters some vertex from $X$ [25]. We call $\sigma$ an attractor strategy towards $X$.

We furthermore formalize the notion of removing attractors from arenas: Let $\mathcal{A}$ be an arena with vertex set $V$, let $X\subseteq V$, and let $A=\mathrm{Attr}_{i}(X)$. If $v_{I}\notin A$, then we define

[TABLE]

which is again an arena. We lift this notation to qualitative (and quantitative) games $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ (or $(\mathcal{A},\mathrm{Cost})$) by defining $\mathcal{G}\setminus A=(\mathcal{A}\setminus A,\mathrm{Win}\cap(V\setminus A)^{\omega})$ (or $(\mathcal{A}\setminus A,\left.\mathrm{Cost}\right|_{(V\setminus A)^{\omega}})$, where $\left.\mathrm{Cost}\right|_{(V\setminus A)^{\omega}}$ denotes the restriction of $\mathrm{Cost}$ to the domain $(V\setminus A)^{\omega}$). This restriction of the winning condition and the cost fuction to vertices of $V$ is not strictly necessary due to our definition of $\mathrm{Win}\subseteq(V^{\prime})^{\omega}$ and of $\mathrm{Cost}\colon(V^{\prime})^{\omega}\rightarrow\mathbb{N}_{\infty}$, but it makes the resulting objects easier to reason about.

If $v_{I}\in A$, however, then both $\mathcal{A}\setminus A$ and $\mathcal{G}\setminus A$ are undefined. The game $\mathcal{G}\setminus A$ can be constructed in linear time and is of size at most $|\mathcal{G}|$.

As a first step towards the proof of Theorem 4.2, we show that vertex-ranked $\sup$-games can be solved by using a single attractor construction and considering the qualitative game obtained by removing the resulting attractor.

Lemma 2

Let $\mathfrak{G}$ be a proper class of qualitative games, let $\mathcal{G}_{\sup}=(\mathcal{A},{\textsc{Rank}^{\sup}}(\mathrm{Win},\mathrm{rk}))\in{\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ with vertex set $V$ and initial vertex $v_{I}$, and let $b\in\mathbb{N}$.

Player [math] has a strategy with cost at most $b$ in $\mathcal{G}_{\sup}$ if and only if $v_{I}\notin A$ and if she has a winning strategy in the qualitative game $\mathcal{G}^{\prime}=\mathcal{G}\setminus A$, where $\mathcal{G}=(\mathcal{A},\mathrm{Win})$ and $A=\mathrm{Attr}_{1}(\{v\in V\mid\mathrm{rk}(v)>b\})$.

Proof

Let $X_{b}=\{v\in V\mid\mathrm{rk}(v)>b\}$. We first show the direction from right to left, i.e., that, if $v_{I}\notin A$ and if Player [math] wins $\mathcal{G}^{\prime}$, say with strategy $\sigma^{\prime}$, then she has a strategy of cost at most $b$ in $\mathcal{G}_{\sup}$. To this end, define $\mathcal{A}^{\prime}=\mathcal{A}\setminus A$. Since $\mathcal{A}^{\prime}\sqsubseteq\mathcal{A}$, the strategy $\sigma^{\prime}$ is a strategy for Player [math] in $\mathcal{G}_{\sup}$ as well, due to Player [math] being able to keep the play inside $\mathcal{A}^{\prime}$ using $\sigma^{\prime}$. Hence, each play consistent with $\sigma^{\prime}$ in $\mathcal{G}^{\prime}$ is consistent with $\sigma^{\prime}$ in $\mathcal{G}$ as well as vice versa. Let $\rho$ be a play in $\mathcal{G}_{\sup}$ consistent with $\sigma^{\prime}$. Since $\sigma^{\prime}$ is winning for Player [math] in $\mathcal{G}^{\prime}$, we have $\rho\in\mathrm{Win}\cap(V\setminus A)^{\omega}\subseteq\mathrm{Win}$. Moreover, since $X_{b}\subseteq A$, and as $\rho$ visits only vertices occurring in $\mathcal{G}^{\prime}$, we obtain ${\textsc{Rank}^{\sup}}(\mathrm{Win},\mathrm{rk})(\rho)\leq b$ and thus $\mathrm{Cost}(\sigma^{\prime})\leq b$, which concludes this direction of the proof.

We show the other direction via contraposition: To this end, first assume $v_{I}\in A$ and let $\tau_{A}$ be an attractor strategy towards $X_{b}$ for Player $1$. We show that Player [math] does not have a strategy with cost at most $b$ in $\mathcal{G}_{\sup}$ by showing that $\tau_{A}$ has cost exceeding $b$. We obtain $\mathrm{Cost}(\tau_{A})>b$ in $\mathcal{G}_{\sup}$: By playing consistently with $\tau_{A}$, Player $1$ forces the play to eventually reach a vertex in $X_{b}$, i.e., a vertex $v$ with $\mathrm{rk}(v)>b$. Thus, $\mathrm{Cost}(\tau_{A})>b$, i.e., $\mathrm{Cost}(\sigma)>b$ for all strategies $\sigma$ of Player [math].

Now assume that Player [math] does not have a winning strategy in $\mathcal{G}^{\prime}$. Towards a contradiction, assume that she has a strategy $\sigma$ with cost at most $b$ in $\mathcal{G}_{\sup}$. We first observe that no play consistent with $\sigma$ visits any vertex from $A$. Otherwise, playing consistently with his attractor strategy towards $X_{b}$ from the first visit to $A$, Player $1$ would be able to construct a play consistent with $\sigma$, but with cost greater than $b$. Thus, $\sigma$ is a strategy for Player [math] in $\mathcal{G}^{\prime}$ and we obtain that all plays consistent with $\sigma$ in $\mathcal{A}$ are consistent with $\sigma$ in $\mathcal{A}^{\prime}$ and vice versa. Since $\mathrm{Cost}(\sigma)\leq b$, we obtain ${\textsc{Rank}^{\sup}}(\mathrm{Win},\mathrm{rk})(\rho)<\infty$, i.e., $\rho\in\mathrm{Win}$ for all plays $\rho$ consistent with $\sigma$. Thus, $\sigma$ is a winning strategy for Player [math] in $\mathcal{G}^{\prime}$, a contradiction. ∎

Using this lemma, we are able to construct a decision procedure solving games from ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ using a decision procedure solving games from $\mathfrak{G}$.

Proof (Proof of Theorem 4.2)

Since $\mathfrak{G}$ is proper, ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ is proper as well. Given the vertex-ranked $\sup$-game $\mathcal{G}_{\sup}=(\mathcal{A},{\textsc{Rank}^{\sup}}(\mathrm{Win},\mathrm{rk}))$, let $X_{b}=\{v\in V\mid\mathrm{rk}(v)>b\}$ and let $A=\mathrm{Attr}_{1}(X_{b})$. We define the decision procedure $\text{dec}_{\sup}$ deciding the given problem such that it returns false if $v_{I}\in A$. Otherwise, $\text{dec}_{\sup}$ returns true if and only if Player [math] wins $\mathcal{G}\setminus A$. Since ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ is proper and due to the assumption of the theorem, $\mathcal{G}\setminus A$ can be solved in time at most $t(|\mathcal{G}|)$ and space at most $s(|\mathcal{G}|)$. The procedure $\text{dec}_{\sup}$ indeed decides the given decision problem due to Lemma 2.

Since we can compute and remove the Player-$1$-attractor $A$ in linear time in $|\mathcal{A}|$ [25], the decision procedure $\text{dec}_{\sup}$ indeed requires time $\mathcal{O}(|\mathcal{A}|)+t(|\mathcal{G}|)$ and space $\mathcal{O}(|\mathcal{A}|)+s(|\mathcal{G}|)$. ∎

This theorem provides an upper bound on the complexity of solving vertex-ranked $\sup$-games. Intuitively, we prove Theorem 4.2 by showing that, for any vertex-ranked $\sup$-game $\mathcal{G}_{\sup}$, a winning strategy for Player [math] in $\mathcal{G}$ that never moves to the Player $1$-attractor towards vertices of rank greater than $b$ has cost at most $b$. Thus, an upper bound on the size of winning strategies for Player [math] for games from $\mathfrak{G}$ provides an upper bound for strategies of finite cost in ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ as well. Moreover, if the decision procedure deciding $\mathfrak{G}$ constructs winning strategies for one or both players, we can adapt the decision procedure deciding ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ to construct strategies of cost at most (greater than) $b$ for Player [math] (Player $1$) as well.

Corollary 1

Let $\mathfrak{G}_{\sup}$ be a proper class of vertex-ranked $\sup$-games and let $\mathcal{G}_{\sup}\in\mathfrak{G}_{\sup}$. If $\sigma$ is a finite-state winning strategy for Player $i$ in $\mathcal{G}$, then Player $i$ has a finite-state winning strategy $\sigma_{\sup}$ in $\mathcal{G}_{\sup}$ with $|\sigma_{\sup}|\in\mathcal{O}(|\sigma|)$. Furthermore, if $\sigma$ is effectively constructible, then $\sigma_{\sup}$ is effectively constructible.

Finally, the procedure constructed in the proof of Theorem 4.2 enables us to solve the optimization problem for vertex-ranked $\sup$-games from ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$: Recall that if Player [math] wins $\mathcal{G}_{\sup}$ with respect to some $b$, she wins it with respect to all $b^{\prime}\geq b$ as well. Hence, using a binary search, $\log(M)$ invocations of the decision procedure from the proof of Theorem 4.2 suffice to determine the minimal $b$ such that Player [math] wins $\mathcal{G}_{\sup}$ with respect to $b$, where $M$ denotes the number of ranks assigned to vertices of $\mathcal{G}_{\sup}$ by its ranking function. Hence, it is possible to determine the minimal such $b$ in time $\mathcal{O}(\log(M)(n+t(|\mathcal{G}|)))$ and space $\mathcal{O}(M)+s(|\mathcal{G}|)$.

4.2 Solving Vertex-Ranked $\limsup$-Games

We now turn our attention to solving vertex-ranked $\limsup$-games. Solving these games is again at least as hard as solving their corresponding qualitative games, due to the same reasoning as for vertex-ranked $\sup$-games. Thus, we again only provide upper bounds on the complexity of solving such games. To this end, given some class $\mathfrak{G}$ of games, we define the corresponding class of vertex-ranked $\limsup$-games

[TABLE]

We identify two criteria on classes of qualitative games $\mathfrak{G}$, each of which is sufficient for quantitative games in ${\mathfrak{G}}^{\textsc{rnk}}_{\lim}$ to be solvable with respect to some given $b$. More precisely, we provide decision procedures for ${\mathfrak{G}}^{\textsc{rnk}}_{\lim}$ for the case that

• •

games from $\mathfrak{G}$ can be solved in conjunction with coBüchi-conditions, and for the case that

• •

the winner of a play $\rho$ in a game from $\mathfrak{G}$ depends only on an infinite suffix of $\rho$.

The latter condition is commonly referred to as prefix-independence, which we formally define later in this section.

In order to show the former case, fix some class of games $\mathfrak{G}$ and let $\mathcal{G}_{\lim}=(\mathcal{A},{\textsc{Rank}^{\lim}}(\mathrm{Win},\mathrm{rk}))\in{\mathfrak{G}}^{\textsc{rnk}}_{\lim}$ be a vertex-ranked $\limsup$-game with vertex set $V$. Furthermore, recall that a play in $\mathrm{Win}$ has cost at most $b$ in $\mathcal{G}_{\lim}$ if it visits vertices of rank greater than $b$ only finitely often.

In the qualitative case, the behavior of visiting a certain set of vertices only finitely often is formalized by the qualitative co-Büchi condition

[TABLE]

where $\inf(\rho)$ denotes the set of vertices occurring infinitely often in $\rho$. Clearly, Player [math] has a strategy of cost at most $b$ in $\mathcal{G}_{\lim}$ if and only if she wins $(\mathcal{A},\mathrm{Win}\cap\textsc{CoBüchi}(\{v\in V\mid\mathrm{rk}(v)>b\}))$. This observation gives rise to the following remark.

Remark 2

Let $\mathfrak{G}$ be a class of qualitative games such that the games in $\{(\mathcal{A},\mathrm{Win}\cap\textsc{CoBüchi}(F))\mid(\mathcal{A},\mathrm{Win})\in\mathfrak{G},F\subseteq V,V\text{ is vertex set of }\mathcal{A}\}$ can be solved in time $t(|\mathcal{G}|,|F|)$ and space $s(|\mathcal{G}|,|F|)$, where $t$ and $s$ are monotonic functions.

Then, the following problem can be solved in time $t(|\mathcal{G}_{\lim}|,n)$ and space $s(|\mathcal{G}_{\lim}|,n)$: “Given some game $\mathcal{G}_{\lim}\in{\mathfrak{G}}^{\textsc{rnk}}_{\lim}$ with $n$ vertices as well as some bound $b\in\mathbb{N}$, does Player [math] win $\mathcal{G}_{\lim}$ with respect to $b$?”

In this case, we solve vertex-ranked $\limsup$-games via a decision procedure for solving qualitative games as-is. Such a procedure trivially exists if the winning conditions of games from $\mathfrak{G}$ are closed under intersection with co-Büchi conditions. Thus, we obtain solvability of a wide range of classes of vertex-ranked $\limsup$-games, e.g., co-Büchi-, parity-, Muller-, Streett- and Rabin games.

We now turn our attention to the latter case described above: We consider classes ${\mathfrak{G}}^{\textsc{rnk}}_{\lim}$ where a play is only determined to be winning or losing in a game from $\mathfrak{G}$ due to some infinite suffix. Formally, we say that a qualitative winning condition $\mathrm{Win}\subseteq V^{\omega}$ is prefix-independent if for all infinite plays $\rho\in V^{\omega}$ and all play prefixes $\pi\in V^{*}$, we have $\rho\in\mathrm{Win}$ if and only if $\pi\rho\in\mathrm{Win}$. A qualitative game is prefix-independent if its winning condition is prefix-independent. A class of games is prefix-independent if every game in the class is prefix-independent. This notion allows us to formalize the claim made in the second bullet point above.

Theorem 4.3

Let $\mathfrak{G}$ be a proper prefix-independent class of qualitative games where each $\mathcal{G}\in\mathfrak{G}$ can be solved in time $t(|\mathcal{G}|)$ and space $s(|\mathcal{G}|)$, where $t$ and $s$ are monotonic functions.

Then, the following problem can be solved in time $\mathcal{O}(n^{3}+n^{2}\cdot t(|\mathcal{G}_{\lim}|))$ and space $\mathcal{O}(n+s(|\mathcal{G}_{\lim}|))$: “Given some game $\mathcal{G}_{\lim}\in{\mathfrak{G}}^{\textsc{rnk}}_{\lim}$ with $n$ vertices and some bound $b\in\mathbb{N}$, does Player [math] win $\mathcal{G}_{\lim}$ with respect to $b$?”

Let $\mathfrak{G}$ be a proper prefix-independent class of games and let $\mathcal{G}_{\lim}\in{\mathfrak{G}}^{\textsc{rnk}}_{\lim}$. Moreover, let $b\in\mathbb{N}$. Intuitively, in order to solve the $b$-threshold problem for $\mathcal{G}_{\lim}$, we adapt the classic algorithm for solving prefix-independent qualitative games (cf., e.g., the work by Chatterjee, Henzinger, and Piterman [13]). Thereby, we repeatedly compute the set of vertices from which Player [math] has a strategy of cost at most $b$ in the corresponding vertex-ranked $\sup$-game  $\mathcal{G}_{\sup}$ and remove their [math]-attractor from the game similarly to the construction of a decision procedure for vertex-ranked $\sup$-games in the proof of Theorem 4.2. We claim that Player [math] has a strategy with cost at most $b$ in $\mathcal{G}_{\lim}$ if and only if $v_{I}$ was removed during that above construction.

In order to prove Theorem 4.3, we first show that, if Player [math] does not win a $\sup$-game from any vertex, then she also does not win the corresponding $\limsup$-game from any vertex. Recall that for a qualitative or quantitative game $\mathcal{G}$ with vertex set $V$ we write $\mathcal{G}_{v}$ to denote the game $\mathcal{G}$ with its initial vertex replaced by $v\in V$. All other components, i.e., the structure of the arena and the cost-function, remain unchanged. We write $\mathrm{W}^{b}_{i}(\mathcal{G})$ to denote the set of all vertices $v$ such that Player $i$ has a strategy of cost at most $b$, if $i=0$, or greater than $b$, if $i=1$, in $\mathcal{G}_{v}$.

Lemma 3

Let $\mathcal{G}_{\lim}=(\mathcal{A},{\textsc{Rank}^{\lim}}(\mathrm{Win},\mathrm{rk}))$ be a vertex-ranked $\limsup$-game with vertex set $V$ such that $\mathrm{Win}$ is prefix-independent and such that for each $v\in V$ the vertex-ranked $\sup$-game $(\mathcal{G}_{\sup})_{v}$ is determined. If $\mathrm{W}^{b}_{0}(\mathcal{G}_{\sup})=\emptyset$, then $\mathrm{W}^{b}_{0}(\mathcal{G}_{\lim})=\emptyset$.

Proof

Let $V$ be the vertex set of $\mathcal{G}_{\sup}$ and $\mathcal{G}_{\lim}$. Since $\mathrm{W}^{b}_{0}(\mathcal{G}_{\sup})=\emptyset$ and since for all $v\in V$ the game $(\mathcal{G}_{\sup})_{v}$ is determined, we obtain $\mathrm{W}^{b}_{1}(\mathcal{G}_{\sup})=V$. For each $v\in V$, let $\tau^{\prime}_{v}$ be a strategy for Player $1$ in $(\mathcal{G}_{\sup})_{v}$ with cost greater than $b$. We now define a single strategy $\tau$ for Player $1$ in $\mathcal{G}_{\lim}$ with cost greater than $b$. For each $\pi=v_{0}\cdots v_{j}\in V^{*}$ we define $\tau(\pi)=\tau^{\prime}_{v_{k}}(v_{k}\cdots v_{j})$, where $k=\max\{k^{\prime}\mid\mathrm{rk}(v_{k^{\prime}-1})>b\}$, with $\max\emptyset=0$. We claim that $\tau$ has cost greater than $b$ in all $(\mathcal{G}_{\lim})_{v}$. Since the cost-function $\mathrm{Cost}$ is identical in all $(\mathcal{G}_{\lim})_{v}$ this claim is formalized as $\mathrm{Cost}(\tau)>b$.

Let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play of $\mathcal{G}_{v}$ consistent with $\tau$. If there are infinitely many positions $j$ with $\mathrm{rk}(v_{j})>b$, then $\mathrm{Cost}(\rho)>b$. Thus, assume the opposite and let $j$ be the maximal position with $\mathrm{rk}(v_{j})>b$. Then the suffix $\rho^{\prime}=v_{j+1}v_{j+2}v_{j+3}\cdots$ of $\rho$ is consistent with $\tau^{\prime}_{v_{j+1}}$. Since $\rho^{\prime}$ does not encounter any vertices of rank greater than $b$, while $\mathrm{Cost}(\rho^{\prime})>b$ due to $\rho^{\prime}$ being consistent with a strategy of cost greater than $b$, we obtain $\rho^{\prime}\notin\mathrm{Win}$. This implies $\rho\notin\mathrm{Win}$ due to prefix-independence of $\mathrm{Win}$. Hence, $\mathrm{Cost}(\rho)=\infty$, which, together with the statement above, implies $\mathrm{Cost}(\tau)>b$. ∎

We are now able to prove Theorem 4.3 using Lemma 3 as a building block for showing the correctness of the approach outlined above.

Proof (Proof of Theorem 4.3)

Given $\mathcal{G}_{\lim}=(\mathcal{A},{\textsc{Rank}^{\lim}}(\mathrm{Win},\mathrm{rk}))$ with vertex set $V$ of size $n$, we define $\mathcal{G}_{0}=\mathcal{G}_{\sup}$, as well as $X_{j}=\mathrm{W}^{b}_{0}(\mathcal{G}_{j})$, $A_{j}=\mathrm{Attr}_{0}(X_{j})$, which is computed in the arena of $\mathcal{G}_{j}$, and $\mathcal{G}_{j+1}=\mathcal{G}_{j}\setminus A_{j}$ for all $j\in\mathbb{N}$. As we only remove vertices from the games $\mathcal{G}_{j}$, we obtain $\mathcal{G}_{j+1}\sqsubseteq\mathcal{G}_{j}$. Thus, the series of games stabilizes at $j=n$ at the latest, i.e., $\mathcal{G}_{j}=\mathcal{G}_{n}$ for all $j\geq n$. We define $A=\bigcup_{j\leq n}A_{j}$ and $\mathcal{G}^{\prime}=\mathcal{G}_{n}$ and claim that Player [math] has a strategy with cost at most $b$ in $\mathcal{G}$ if and only if $v_{I}\in A$. We first argue that this suffices to show the desired result.

First note that since $\mathfrak{G}$ is proper, ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$ is proper as well. Thus, Theorem 4.2 is applicable to ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$. Let $\text{dec}_{\sup}$ be the decision procedure deciding whether or not Player [math] has a strategy with cost at most $b$ in games from ${\mathfrak{G}}^{\textsc{rnk}}_{\sup}$, as constructed in the proof of that theorem. The decision procedure $\text{dec}_{\sup}$ can be easily modified to return $W^{b}_{0}(\mathcal{G}_{j})$ instead of a yes/no-answer by applying it to each $(\mathcal{G}_{j})_{v}$ individually. This, however, is only possible since we assume $\mathfrak{G}$ to be proper, as the second condition of the definition of a proper family of games allows us to solve each $(\mathcal{G}_{j})_{v}$. This modified procedure $\text{dec}_{\sup}^{\prime}$ runs in time at most $\mathcal{O}(n^{2}+n\cdot t(|\mathcal{G}|))$ and space $\mathcal{O}(n)+s(|\mathcal{G}|)$, where $t(|\mathcal{G}|)$ and $s(|\mathcal{G}|)$ are the time and space required to solve $\mathcal{G}$, respectively.

For $j\in\{0,\dots,n\}$, the decision procedure $\text{dec}_{\lim}$ first computes $\mathcal{G}_{j}$ in linear time in $n$ and reusing the space used for solving $\mathcal{G}_{j-1}$. It then computes $X_{j}$ requiring a single call to the modified $\text{dec}_{\sup}$. It subsequently computes $A_{j}$ in time $\mathcal{O}(n)$ and space $\mathcal{O}(n)$. Finally, it returns false if and only if $v_{I}$ is in the arena of $\mathcal{G}_{n}$. In total, we obtain a runtime of $\text{dec}_{\lim}$ of $\mathcal{O}(n^{3}+n^{2}\cdot t(|\mathcal{G}|))$. The only additional memory required by $\text{dec}_{\lim}$ is that for storing the sets $X_{j}$ and $A_{j}$, the size of which is bounded from above by $n$. The games $\mathcal{G}_{j}$ can be stored by reusing the memory occupied by $\mathcal{G}$, due to $\mathcal{G}_{j}\sqsubseteq\mathcal{G}_{j-1}$. Hence, the procedure $\text{dec}_{\lim}$ requires space $\mathcal{O}(n)+s(|\mathcal{G}|)$.

It remains to show that Player [math] indeed has a strategy with cost at most $b$ in $\mathcal{G}$ if and only if $v_{I}\notin\mathcal{A}_{n}$, i.e., if $v_{I}\in A$. To this end, first assume $v_{I}\in A$ and note that we have $A_{j}\supseteq X_{j}$. However, for each two $j\neq j^{\prime}$, we have $A_{j}\cap A_{j^{\prime}}=\emptyset$ and, in particular, $X_{j}\cap X_{j^{\prime}}=\emptyset$. Hence, for each $v\in A$ there exists a unique $j$ such that $v\in A_{j}$.

We define the strategy $\sigma$ for Player [math] in $\mathcal{G}$ inductively such that any play consistent with $\sigma$ only descends through the $X_{j}$. Formally, we construct $\sigma$ such that it satisfies the following invariant:

Let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play consistent with $\sigma$ and let $k\in\mathbb{N}$. If $v_{k}\in A_{j}\setminus X_{j}$, then $v_{k+1}\in\bigcup_{j^{\prime}\leq j}A_{j^{\prime}}\cup X_{j^{\prime}}$. Moreover, if $v_{k}\in(A_{j}\setminus X_{j})\cap V_{0}$, then the move to $v_{k+1}$ is the move prescribed by the attractor strategy of Player [math] towards $X_{j}$. If $v_{k}\in X_{j}$, then $v_{k+1}\in X_{j}\cup\bigcup_{j^{\prime}<j}A_{j^{\prime}}\cup X_{j^{\prime}}$.

Clearly, this invariant holds true for $\pi=v_{I}$. Thus, let $\pi=v_{0}\cdots v_{k}$ be a play prefix consistent with $\sigma$. If $v_{k}\in V_{1}$, let $v^{*}$ be an arbitrary successor of $v_{k}$ in $\mathcal{G}$ and assume towards a contradiction that $\pi v^{*}$ violates the invariant. If $v_{k}\in A_{j}\setminus X_{j}$, then in $\mathcal{G}_{j}$ there exists an edge from $v_{k}$ leading to some vertex $v^{*}\notin A_{j}$, a contradiction to the definition of the attractor. If, however, $v_{k}\in X_{j}$ and $v^{*}\notin X_{j}\cup\bigcup_{j^{\prime}<j}A_{j^{\prime}}\cup X_{j^{\prime}}$, then Player $1$ has a strategy $\tau$ in $(\mathcal{G}_{j})_{v^{*}}$ with cost greater than $b$. Thus, a play that begins in $v_{k}$, moves to $v^{*}$ and is consistent with $\tau$ afterwards has cost greater $b$, i.e., Player [math] does not have a strategy with cost at most $b$ in $(\mathcal{G}_{j})_{v_{k}}$, a contradiction to $v_{k}\in X_{j}=\mathrm{W}^{b}_{0}(\mathcal{G}_{j})$. Hence, $\pi v^{*}$ satisfies the invariant for each successor $v^{*}$ of $v_{k}\in V_{1}$.

Now assume $v_{k}\in V_{0}$ and first let $v_{0}\in A_{j}\cup X_{j}$ for some $j\in\mathbb{N}$. Let $\sigma^{A}_{j}$ be an attractor strategy for Player [math] towards $X_{j}$. If $v_{k}\in A_{j}\setminus X_{j}$, we define $\sigma(\pi)=\sigma^{A}_{j}(v_{k})$, which satisfies the invariant due to the definition of the attractor strategy. If, however, $v_{k}\in X_{j}$, let $k^{\prime}$ be minimal such that $v_{k^{\prime\prime}}\in X_{j}$ for all $k^{\prime\prime}$ with $k^{\prime}\leq k^{\prime\prime}\leq k$. Moreover, let $\sigma^{v}_{j}$ be a strategy for Player [math] such that every play consistent with $\sigma^{v}_{j}$ in $\mathcal{G}_{j}$ with initial vertex $v$ has cost at most $b$. Such a strategy exists due to $X_{j}=\mathrm{W}^{b}_{0}(\mathcal{G}_{j})$. We define $\sigma(\pi)=\sigma^{v_{k^{\prime}}}_{j}(v_{k^{\prime}}\cdots v_{k})$, which satisfies the invariant to similar reasoning as above.

In order to show $\mathrm{Cost}(\sigma)\leq b$, let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play consistent with $\sigma$. Due to the invariant of $\sigma$ and since $v_{0}\in A$, the play $\rho$ descends through the $A_{j}$ and the $X_{j}$, i.e., once it encounters some $X_{j}$, it never moves to any $A_{j^{\prime}}\setminus X_{j^{\prime}}$ with $j^{\prime}\geq j$ nor to any $X_{j^{\prime}}$ with $j^{\prime}>j$. Also, $\rho$ stabilizes in some $X_{j}$, i.e., there exists a $k\in\mathbb{N}$ such that $v_{k^{\prime}}\in X_{j}$ for all $k^{\prime}\geq k$, as $\sigma$ prescribes moves according to the attractor strategy towards $X_{j}$ when in $A_{j}\setminus X_{j}$. Moreover, due to the definition of $\sigma$, the suffix $\rho^{\prime}=v_{k}v_{k+1}v_{k+2}\cdots$ is consistent with $\sigma^{v_{k}}_{j}$, i.e., we obtain $\rho^{\prime}\in\mathrm{Win}$ and that the maximal vertex-rank encountered in $\rho$ is at most $b$. As $\mathrm{Win}$ is prefix-independent, we obtain $\rho\in\mathrm{Win}$ as well as $\limsup_{k\rightarrow\infty}\mathrm{rk}(v_{k})\leq b$. Hence, ${\textsc{Rank}^{\lim}}(\mathrm{Win},\mathrm{rk})(\rho)\leq b$, which concludes this direction of the proof.

Now assume $v_{I}\notin A$ and consider $\mathcal{G}^{\prime}$ with vertex set $V\setminus A$. Since the construction of the $\mathcal{G}_{j}$ stabilized, we have $A_{j}=X_{j}=W^{b}_{0}(\mathcal{G}^{\prime})=\emptyset$, i.e., Player $1$ has a strategy with cost greater than $b$ from any starting vertex in $\mathcal{G}^{\prime}$. Due to Lemma 3, this implies that he has such a strategy from every vertex in $\mathcal{G}_{\sup}\setminus A$, call it $\tau$. Note that there exists no Player-[math]-vertex in $V\setminus A$ that has an outgoing edge leading into $A$, as this would contradict the definition of the Player-[math]-attractors $A_{j}$. Hence, $\tau$ is a strategy for Player $1$ in $\mathcal{G}$ as well and we retain $\mathrm{Cost}(\tau)>b$. ∎

Intuitively, we prove Theorem 4.3 by constructing a strategy $\sigma$ for Player [math] by “stitching together” the attractor-strategies towards her winning regions in the decreasing vertex-ranked $\sup$-games and the winning strategies for her in the respective vertex-ranked $\sup$-games. As each play consistent with that strategy descends down the hierarchy of $\sup$-games thus constructed, we can reuse the memory states of the winning strategies in these games when implementing $\sigma$. Thus, a monotonic upper bound on the size of strategies with cost at most $b$ in $\mathcal{G}_{\sup}$ is an upper bound on the size of such strategies in $\mathcal{G}_{\lim}$ as well.

Corollary 2

Let $\mathfrak{G}$ be a proper prefix-independent class of qualitative games such that, if Player [math] wins $\mathcal{G}$, then she has a finite-state winning strategy of size at most $m(|\mathcal{G}|)$, where $m$ is a monotonic function.

If Player [math] wins $\mathcal{G}_{\lim}\in{\mathfrak{G}}^{\textsc{rnk}}_{\lim}$, then she has a finite-state winning strategy $\sigma_{\lim}$ with $|\sigma_{\lim}|\in\mathcal{O}(m(|\mathcal{G}_{\lim}|))$ in $\mathcal{G}_{\lim}$. Furthermore, if winning strategies for Player [math] in the games in $\mathfrak{G}$ are effectively constructible, then $\sigma_{\lim}$ is effectively constructible.

Moreover, in order to find the optimal $b$ such that Player [math] wins $\mathcal{G}_{\lim}$ with respect to $b$, we can again employ a binary search analogously to the case of vertex-ranked $\sup$-games. Thus, we can determine the optimal such $b$ in time $\mathcal{O}(\log(M)(n^{3}+n^{2}\cdot t(|\mathcal{G}_{\lim}|)))$ and space $\mathcal{O}(n+s(|\mathcal{G}_{\lim}|))$, where $M$ again denotes the number of ranks assigned to vertices in a given vertex-ranked $\limsup$-game.

Having thus defined both quantitative reductions and a canonical target for such reductions, we now give examples of how to solve quantitative games using this tools.

5 Applications

In this section, we give examples of how to use quantitative reductions and vertex-ranked games to solve quantitative games. First, in Section 5.1, we formally introduce a quantitative variant of request-response games, which we call request-response games with costs, and show how to solve such games using quantitative reductions and vertex-ranked sup-request-response games. Second, in Section 5.2, we recall the definition of quantitative Muller games due to McNaughton [21] and show how to reduce such games to vertex-ranked safety games via quantitative reductions. Finally, in Section 5.3, we show that vertex-ranked games are useful in their own right, by showing how to use them to synthesize controllers that are resilient against disturbances.

5.1 Reducing Request-Response Games with Costs to Vertex-Ranked Request-Response Games

Recall that a play satisfies the qualitative request-response condition if every request that is opened is eventually answered. We extend this condition to a quantitative one by equipping the edges of the arena with costs and measuring the maximal cost incurred between opening and answering a request.

Fix some arena $\mathcal{A}$ with vertex set $V$ and set $E$ of edges. Formally, the qualitative request-response condition $\textsc{ReqRes}(\Gamma)$ consists of a family of so-called request-response pairs $\Gamma=(Q_{c},P_{c})_{c\in[d]}$, where  $d\in\mathbb{N}$, $d>0$, and where $Q_{c},P_{c}\subseteq V$ for all $c\in[d]$. Player [math] wins a play according to this condition if each visit to some vertex from $Q_{c}$ is answered by some later visit to a vertex from $P_{c}$, i.e., we define

[TABLE]

We say that a visit to a vertex from $Q_{c}$ opens a request for condition $c$ and that the first visit to a vertex from $P_{c}$ afterwards answers the request for that condition.

Proposition 1 ([28])

Request-response games with $n$ vertices and $d$ request-response pairs can be solved in time $\mathcal{O}(n^{2}d^{2}2^{d})$.

Furthermore, let $\mathcal{G}$ be a request-response game with $d$ request-response pairs. If Player [math] has a winning strategy in $\mathcal{G}$, then she has a finite-state winning strategy of size at most $d2^{d}$.

We extend this qualitative winning condition to a quantitative one using families of cost functions $\mathrm{Cost}=(\mathrm{Cost}_{c})_{c\in[d]}$, where $\mathrm{Cost}_{c}\colon E\rightarrow\mathbb{N}$ for each $c\in[d]$ and lift the cost functions $\mathrm{Cost}_{c}$ to play infixes $\pi$ in $\mathcal{A}$ by adding up the costs along $\pi$. The cost-of-response for a request for condition $c$ at position $j$ is then defined as

[TABLE]

with $\min\emptyset=\infty$, which naturally extends to the (total) cost-of-response

[TABLE]

Finally, we define the request-response condition with costs as

[TABLE]

i.e., this condition measures the maximal cost incurred by any request in $\rho$.

We call a game $\mathcal{G}=(\mathcal{A},\textsc{CostReqRes}(\Gamma,\mathrm{Cost}))$ a request-response game with costs. We denote the largest cost assigned to any edge by $W$. As we assume the functions $\mathrm{Cost}_{c}$ to be given in binary encoding, the largest cost $W$ assigned to an edge may be exponential in the size of $\mathcal{G}$.

If all $\mathrm{Cost}_{c}$ assign zero to every edge, then the request-response condition with costs coincides with the qualitative request-response condition. In general, however, the request-response condition with costs is a strengthening of the classic request-response condition: If some play $\rho$ has finite cost according to the condition with costs, then it is winning for Player [math] according to the qualitative condition, but not vice versa.

Remark 3

Let $\mathcal{G}=(\mathcal{A},\textsc{CostReqRes}(\Gamma,\mathrm{Cost}))$ be a request-response game with costs. If a strategy $\sigma$ for Player [math] in $\mathcal{G}$ has finite cost, then $\sigma$ is a winning strategy for Player [math] in the qualitative game $(\mathcal{A},\textsc{ReqRes}(\Gamma))$.

This remark together with a detour via qualitative request-response games yield a cap for request-response games with costs.

Lemma 4

Let $\mathcal{G}$ be a request-response game with costs with $n$ vertices, $d$ request-response pairs, and largest cost of an edge $W$. If Player [math] has a strategy with finite cost in $\mathcal{G}$, then she also has a strategy with cost at most $d2^{d}nW$.

Proof

Let $\mathcal{G}=(\mathcal{A},\textsc{CostReqRes}(\Gamma,\mathrm{Cost}))$ and let $\mathcal{G}^{\prime}=(\mathcal{A},\textsc{ReqRes}(\Gamma))$ be a qualitative request-response game obtained by disregarding the cost functions of $\mathcal{G}$. Moreover, let $\sigma$ be a strategy with finite cost for $\mathcal{G}$. Due to Remark 3, the strategy $\sigma$ is winning for Player [math] in $\mathcal{G}^{\prime}$ as well, hence Player [math] wins $\mathcal{G}^{\prime}$. Thus, due to Proposition 1, she has a winning strategy $\sigma^{\prime}$ of size at most $d2^{d}$ in $\mathcal{G}^{\prime}$. Let $\sigma^{\prime}$ be implemented by the memory structure $\mathcal{M}$ and let $b=d2^{d}nW$. We show $\textsc{CostReqRes}(\Gamma,\mathrm{Cost})(\sigma^{\prime})\leq b$.

Let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play consistent with $\sigma^{\prime}$ and assume towards a contradiction $\textsc{CostReqRes}(\Gamma,\mathrm{Cost})(\rho)>b$. Then there exist $c\in[d]$ and $j\in\mathbb{N}$ such that $\textsc{ReqResCor}_{c}(\rho,j)>b$. As each edge has cost at most $W$, the request for condition $c$ opened at position $j$ is not answered for at least $d2^{d}n$ steps, i.e., we obtain $v_{j^{\prime}}\notin P_{c}$ for all $j^{\prime}$ with $j\leq j^{\prime}\leq j+d2^{d}n$. Let $\mathrm{ext}(\rho)=(v_{0},m_{0})(v_{1},m_{1})(v_{2},m_{2})\cdots$. Since $|\mathcal{M}|\leq d2^{d}$, there exists a vertex repetition on the play infix $(v_{j},m_{j})\cdots(v_{j+d2^{d}n},m_{j+d2^{d}n})$ of $\mathrm{ext}(\rho)$, say at positions $k$ and $k^{\prime}$ with $j\leq k<k^{\prime}\leq j+d2^{d}n$. Thus, the play $\rho^{\prime}=v_{0}\cdots v_{k}(v_{k+1}\cdots v_{k^{\prime}})^{\omega}$ is consistent with $\sigma^{\prime}$.

In $\rho^{\prime}$, however, a request for condition $c$ is opened at position $j\leq k$. Since we have $j\leq k^{\prime}\leq j+d2^{d}n$, this request is not answered in the play infix $v_{j}\cdots v_{k}\cdots v_{k^{\prime}}$, i.e., it is never answered. Hence, $\rho^{\prime}\notin\textsc{ReqRes}(\Gamma)$, which contradicts $\sigma^{\prime}$ being a winning strategy for Player [math] in $\mathcal{G}^{\prime}$. ∎

Having obtained a cap for request-response games with costs, we can now turn to the main result of this section: Request-response games with costs are reducible to vertex-ranked $\sup$-request-response games. In order to show this, we use a memory structure that keeps track of the costs incurred by the requests open at each point in the play [30].

Lemma 5

Let $\mathcal{G}$ be a request-response game with costs with $n$ vertices, $d$ request-response pairs, and highest cost of an edge $W$. Then $\mathcal{G}\leq^{b+1}_{\mathcal{M}}\mathcal{G}^{\prime}$ for $b=d2^{d}nW$, some memory structure $\mathcal{M}$ of size $\mathcal{O}(2nb^{d})$, and a vertex-ranked $\sup$-request-response game $\mathcal{G}^{\prime}$ with $d$ request-response pairs.

Proof

Let $\mathcal{G}=(\mathcal{A},\textsc{CostReqRes}(\Gamma,\mathrm{Cost}))$ with initial vertex $v_{I}$. Recall that $b$ is a cap of $\mathcal{G}$ due to Lemma 4. We first define the memory structure $\mathcal{M}$. Intuitively, we use it to keep track of the currently open requests and the costs they have incurred up to the cap $b$. Once the cost of a single request incurs a cost greater than $b$, the memory structure raises a Boolean flag, which indicates that Player $1$ can unbound the cost of that request.

Let $r\colon[d]\rightarrow\{\bot\}\cup[b+1]=\{\bot,0,\dots,b\}$ be a function mapping conditions $c$ to the cost $r(c)\in[b+1]$ they have incurred so far, or to $r(c)=\bot$ if no request for that condition is pending. We call such a function a request-function and denote the set of all request functions by $R$. We define the initial request function $r_{I}$ such that $r_{I}(c)=0$ if $v_{I}\in Q_{c}$ and $r_{I}(c)=\bot$ otherwise. In order to be able to access the current vertex during the update of the memory structure, we store it in the memory structure as well. By accessing the current vertex together with the vertex that we move to, we are thus able to obtain the cost of the traversed edge. Finally, we store a flag that indicates whether or not the bound $b$ has been exceeded. Hence, we define the set of memory states $M=V\times R\times\{0,1\}$ with the initial memory state $m_{I}=(v_{I},r_{I},0)$.

We define the update function $\mathrm{Upd}((v,r,f),v^{\prime})=(v^{\prime},r^{\prime},f^{\prime})$ by performing the following steps in order:

• •

For each $c\in[d]$, if $v\in P_{c}$, set $r^{\prime}(c)=\bot$. Otherwise, set $r^{\prime}(c)=r(c)$.

• •

For each $c\in[d]$, if $r^{\prime}(c)\neq\bot$, set $r^{\prime}(c)=r^{\prime}(c)+\mathrm{Cost}_{c}((v,v^{\prime}))$.

• •

Now, if there exists a condition $c$ such that $r^{\prime}(c)>b$, then set $r^{\prime}(c)=\bot$ for all $c$ and set $f^{\prime}=1$. Otherwise, set $f^{\prime}=f$.

• •

For each $c\in[d]$, if $v^{\prime}\in Q_{c}$, set $r^{\prime}(c)$ to $\max\{r^{\prime}(c),0\}$ where $\max\{\bot,0\}=0$.

Note that we replicate the current vertex $v$ in the memory state in order to be able to access it in the update of the memory state during the move to $v^{\prime}$, thereby attaining access to the traversed edge $(v,v^{\prime})$.

We obtain $\mathcal{M}=(M,m_{I},\mathrm{Upd})$. Clearly, we have $|\mathcal{M}|\in\mathcal{O}(2nb^{d})$, i.e., $\mathcal{M}$ is of exponential size in $d$, but only of polynomial size in $n$ and $W$.

Using this definition, we obtain that if $\textsc{CostReqRes}(\Gamma,\mathrm{Cost})(\rho)\leq b$, then the extended play $\mathrm{ext}(\rho)$ remains in vertices of the form $(v,v,r,0)$. Dually, if $\textsc{CostReqRes}(\Gamma,\mathrm{Cost})(\rho)>b$, then $\mathrm{ext}(\rho)$ eventually moves to vertices of the form $(v,v,r,1)$ and remains there ad infinitum.

Let $\Gamma=(Q_{c},P_{c})_{c\in[d]}$. It remains to define the vertex-ranking function $\mathrm{rk}\colon V\times M\rightarrow\mathbb{N}$, as well as the family of request-response pairs $\Gamma^{\prime}$ for $\mathcal{G}^{\prime}$. We define the former as

[TABLE]

and the latter as

[TABLE]

Note that $\rho\in\textsc{ReqRes}(\Gamma)$ if and only if $\mathrm{ext}(\rho)\in\textsc{ReqRes}(\Gamma^{\prime})$.

We first argue that the ranking functions included in the memory state indeed contain information about the cost incurred so far by open requests as long as the cost of the play does not exceed $b$. In order to do so, let $\rho=v_{0}v_{1}v_{2}\cdots$ be some play in $\mathcal{G}$ with $\textsc{CostReqRes}(\Gamma,\mathrm{Cost})(\rho)\leq b$ and let $\mathrm{ext}(\rho)=(v_{0},v_{0},r_{0},f_{0})(v_{1},v_{1},r_{1},f_{1})(v_{2},v_{2},r_{2},f_{2})\cdots$ be its extension. Intuitively, since the cost of $\rho$ does not exceed the bound $b$, the flags $f_{j}$ are not raised and the request functions track the cost of all requests precisely.

More formally if, for some $c\in[d]$ and some $j\in\mathbb{N}$ with $v_{j}\in Q_{c}$, we have $\textsc{ReqResCor}_{c}(\rho,j)=b^{\prime}$, then $r_{j^{\prime}}(c)=b^{\prime}$, where $j^{\prime}\geq j$ is the earliest position at which the request for $c$ opened at position $j$ is answered. Dually, if $r_{j^{\prime}}(c)=b^{\prime}$ for some $j^{\prime}\in\mathbb{N}$, some $b^{\prime}\in\mathbb{N}$, and some $c\in[d]$, then $\textsc{ReqResCor}_{c}(\rho,j)\geq b^{\prime}$, where $j\leq j^{\prime}$ is the earliest position at which the request for condition $c$ is opened without being answered prior to position $j^{\prime}$. In particular, if $r_{j^{\prime}}(c)=b^{\prime}$ with $j^{\prime}$, $b^{\prime}$, and $c$ as above and we additionally have $v_{j^{\prime}}\in P_{c}$, then $\textsc{ReqResCor}_{c}(\rho,j)=b^{\prime}$.

We define $\mathcal{G}^{\prime}=(\mathcal{A}\times\mathcal{M},{\textsc{Rank}^{\sup}}(\textsc{ReqRes}(\Gamma^{\prime}),\mathrm{rk}))$. Moreover, since $\Gamma^{\prime}$ is the extension of $\Gamma$ to the vertices of $\mathcal{A}\times\mathcal{M}$, the game $\mathcal{G}^{\prime}$ contains $d$ many request-response pairs.

It remains to show $\mathcal{G}\leq^{b+1}_{\mathcal{M}}\mathcal{G}^{\prime}$. Recall that, since we do not name a $(b+1)$-correction function explicitly, we implicitly use the $(b+1)$-correction-function $\text{cap}_{b+1}$. Clearly, the first and second condition of the definition of a quantitative reduction hold true, i.e., the arena of $\mathcal{G}^{\prime}$ is $\mathcal{A}\times\mathcal{M}$ and $\text{cap}_{b+1}$ is a $(b+1)$-correction function. It remains to show the two latter conditions. To this end, let $\rho=v_{0}v_{1}v_{2}\cdots\in V^{\omega}$ be a play in $\mathcal{G}$ and let $\mathrm{ext}(\rho)=(v_{0},v_{0},r_{0},f_{0})(v_{1},v_{1},r_{1},f_{1})(v_{2},v_{2},r_{2},f_{2})\cdots$ be its unique extended play in $\mathcal{G}^{\prime}$. We use the shorthands $\mathrm{Cost}_{\mathcal{G}}=\textsc{CostReqRes}(\Gamma,\mathrm{Cost})$ as well as $\mathrm{Cost}_{\mathcal{G}^{\prime}}={\textsc{Rank}^{\sup}}(\textsc{ReqRes}(\Gamma^{\prime}),\mathrm{rk})$.

We first show $\mathrm{Cost}_{\mathcal{G}}(\rho)=\mathrm{Cost}_{\mathcal{G}^{\prime}}(\mathrm{ext}(\rho))$ for all $\rho$ with $\mathrm{Cost}_{\mathcal{G}}(\rho)<b+1$. Let $\mathrm{Cost}_{\mathcal{G}}(\rho)=b^{\prime}<b+1$ and note that this implies $\rho\in\textsc{ReqRes}(\Gamma)$ and $\mathrm{ext}(\rho)\in\textsc{ReqRes}(\Gamma^{\prime})$ as well as $f_{j}=0$ for all $j\in\mathbb{N}$. As argued above, we obtain $\mathrm{rk}(v_{j},v_{j},r_{j},f_{j})\leq b^{\prime}$ for all $j$, which implies $\mathrm{Cost}_{\mathcal{G}^{\prime}}(\mathrm{ext}(\rho))\leq b^{\prime}$. Moreover, let $c\in[d]$ and $j\in\mathbb{N}$ with $v_{j}\in Q_{c}$ such that $\textsc{ReqResCor}_{c}(\rho,j)=b^{\prime}$. Since $b^{\prime}<\infty$, such $c$ and $j$ exist. The play $\mathrm{ext}(\rho)$ visits a vertex of rank $b^{\prime}$ at the position at which the request for condition $c$ opened at position $j$ is answered for the first time. Thus, $\mathrm{Cost}_{\mathcal{G}^{\prime}}(\mathrm{ext}(\rho))\geq b^{\prime}$, which concludes this part of the proof.

It remains to show that $\mathrm{Cost}_{\mathcal{G}^{\prime}}(\mathrm{ext}(\rho))\geq\text{cap}_{b+1}(b+1)=b+1$ holds true for all $\rho$ with $\mathrm{Cost}_{\mathcal{G}}(\rho)\geq b+1$. To this end, let $\mathrm{Cost}_{\mathcal{G}}(\rho)=b^{\prime}\geq b+1$. As argued above, the extended play $\mathrm{ext}(\rho)$ eventually moves to vertices of the form $(v,v,r,1)$ and remains there. Hence, $\mathrm{Cost}_{\mathcal{G}^{\prime}}(\mathrm{ext}(\rho))=b+1$ if $\rho\in\textsc{ReqRes}(\Gamma)$, i.e., if $\mathrm{ext}(\rho)\in\textsc{ReqRes}(\Gamma^{\prime})$. If, however, $\rho\notin\textsc{ReqRes}(\Gamma)$, then $\mathrm{ext}(\rho)\notin\textsc{ReqRes}(\Gamma^{\prime})$ and hence, $\mathrm{Cost}_{\mathcal{G}^{\prime}}(\rho)=\infty>b+1$. ∎

Thus, in order to solve a request-response game with costs with respect to some $b$, it suffices to solve a vertex-ranked $\sup$-request-response game with respect to $b$. This, in turn, can be done by reducing the problem to that of solving a request-response game as shown in Theorem 4.2. Using this reduction together with the framework of quality-preserving reductions, we are able to provide an upper bound on the complexity of solving request-response games with costs with respect to some bound $b$.

Theorem 5.1

The following decision problem is in ExpTime: “Given some request-response game with costs $\mathcal{G}$ and some bound $b\in\mathbb{N}$, does Player [math] have a strategy $\sigma$ with $\mathrm{Cost}(\sigma)\leq b$ in $\mathcal{G}$?”

Proof

Let $\mathcal{G}$ contain $n$ vertices, $d$ request-response pairs, and let $W$ be the largest cost assigned to any edge. We first construct the vertex-ranked $\sup$-request-response game $\mathcal{G}^{\prime}$ from $\mathcal{G}$ as shown in Lemma 5. Recall that $\mathcal{G}^{\prime}$ contains $\mathcal{O}(n(d2^{d}nW)^{d})$ vertices and $d$ request-response pairs. Due to the instantiation of Theorem 4.2 with the decision procedure for qualitative request-response games from Proposition 1, the game $\mathcal{G}^{\prime}$ can be solved with respect to $b$ in time

[TABLE]

Due to $W^{2d}\in\mathcal{O}((2^{|\mathcal{G}|})^{|\mathcal{G}|})=\mathcal{O}(2^{|\mathcal{G}|^{2}})$, this is exponential in the description length of $\mathcal{G}$. ∎

Moreover, solving request-response games is known to be ExpTime-hard [12]. Thus, solving quantitative request-response games with costs via quantitative reductions is asymptotically optimal.

Furthermore, by leveraging our results on the sizes of memory structures in vertex-ranked $\sup$-games we obtain an upper bound on the size of strategies with a given cost in request-response games with costs.

Lemma 6

Let $\mathcal{G}$ be a request-response game with costs with $n$ vertices, $d$ request-response pairs, and largest cost of an edge $W$. If Player [math] has a strategy in $\mathcal{G}$ with finite cost, then she also has a strategy in $\mathcal{G}$ with finite cost of size at most $\mathcal{O}(nb^{d}d2^{d})$, where $b=d2^{d}nW$.

Proof

Let $\sigma$ be a strategy for Player [math] in $\mathcal{G}$ with finite cost. Due to Lemma 4, Player [math] has a strategy $\sigma^{\prime}$ in $\mathcal{G}$ with cost at most $d2^{d}nW$. Let $\mathcal{G}^{\prime}_{\sup}$ be the vertex-ranked $\sup$-request-response game constructed in the proof of Lemma 5 and recall that $\mathcal{G}^{\prime}_{\sup}$ has $d$ request-response pairs as well.

Due to Theorem 3.1, and since $b$ is a cap of $\mathcal{G}$ due to Lemma 4, Player [math] has a strategy $\sigma^{\prime}_{\sup}$ with cost at most $d2^{d}nW$ in $\mathcal{G}^{\prime}_{\sup}$. Let $\mathcal{G}^{\prime}$ be the qualitative request-response game corresponding to $\mathcal{G}^{\prime}_{\sup}$, i.e., the game played in the same arena as $\mathcal{G}^{\prime}_{\sup}$ in which a play is winning for Player [math] if and only if it has finite cost in $\mathcal{G}^{\prime}_{\sup}$.

Clearly, the strategy $\sigma^{\prime}_{\sup}$ is winning for Player [math] in $\mathcal{G}^{\prime}$ as well. By applying Proposition 1 we obtain that Player [math] has a winning strategy of size at most $d2^{d}$ in $\mathcal{G}^{\prime}$. By furthermore applying Corollary 1 and Theorem 3.2, we obtain that Player [math] has a strategy of finite cost of size $\mathcal{O}(2nb^{d}d2^{d})=\mathcal{O}(nb^{d}d2^{d})$. ∎

Finally, the optimization problem of finding the minimal $b^{\prime}$ such that Player [math] wins a request-response game with costs $\mathcal{G}$ with respect to $b^{\prime}$ can be solved in exponential time as well. Recall that if Player [math] wins $\mathcal{G}$ with respect to some $b^{\prime}$, then she also wins it with respect to all $b^{\prime\prime}\geq b^{\prime}$. Since we can assume $b^{\prime}\leq b=d2^{d}nW$, we can perform a binary search for $b^{\prime}$ on the interval $\{0,\dots,b\}$. Hence, the optimal $b^{\prime}$ can be found in time $\mathcal{O}(\log(b)(n^{2}b^{2d}d^{2}2^{d}))$.

5.2 Reducing Quantitative Muller Games to Vertex-Ranked Safety Games

Having shown how our framework can be used to find optimal strategies in request-response games with costs in a structured and modular way, we now show how it can be used to greatly simplify existing methods for finding such strategies. To this end, we show how to reduce quantitative Muller games to vertex-ranked safety games, i.e., vertex-ranked games in which it is the aim of Player [math] to avoid a certain set of undesirable vertices. In order to do so, we leverage techniques introduced by Neider, Rabinovich, and Zimmermann [23].

Let $\mathcal{A}$ be some arena with vertex set $V$ and recall that the qualitative Muller condition is defined via a partition of $2^{V}$ into $({\mathcal{F}}_{0},{\mathcal{F}}_{1})$ as

[TABLE]

where $\inf(\rho)$ denotes the set of vertices that are visited infinitely often by $\rho$. Thus, Player $i$ wins $\rho$ if and only if $\inf(\rho)\in{\mathcal{F}}_{i}$.

McNaughton introduced a quantitative characterization of the Muller condition by assigning a score to each prefix of a play and each subset of the set of vertices [21]. In order to characterize the set of vertices visited infinitely often during a play, the score of a subset $F$ measures how often $F$ has been visited completely without leaving it. For a play $\rho$, the limit inferior of the score of $\inf(\rho)$ tends towards infinity, while the limit inferior of the score for all other sets is zero [21].

Formally, for any set $F\subseteq V$ with $F\neq\emptyset$, the score $\text{Score}_{F}(\pi)$ is defined inductively using an accumulator that stores the vertices of $F$ that have already been visited, as follows:

[TABLE]

We generalize the score-function to families ${\mathcal{F}}$ of subsets of vertices, i.e., ${\mathcal{F}}\subseteq 2^{V}$, by defining $\text{Score}_{\mathcal{F}}(\pi)=\max_{F\in{\mathcal{F}}}(\text{Score}_{F}(\pi))$ and to infinite plays by defining $\text{Score}_{\mathcal{F}}(v_{0}v_{1}v_{2}\cdots)=\sup_{j\rightarrow\infty}\text{Score}_{\mathcal{F}}(v_{0}\cdots v_{j})$. This definition inspires the quantitative Muller condition, which is defined as

[TABLE]

We obtain a cap for such games via leveraging a result by Fearnley and Zimmermann [17].

Lemma 7

Let $\mathcal{G}=(\mathcal{A},\mathrm{Cost})$ be a quantitative Muller game. If Player [math] has a strategy $\sigma$ with finite cost in $\mathcal{G}$, then she has a strategy $\sigma^{\prime}$ with $\mathrm{Cost}(\sigma^{\prime})\leq 2$.

Proof

Let $\mathcal{G}=(\mathcal{A},\textsc{QuantMuller}({\mathcal{F}}_{0},{\mathcal{F}}_{1}))$. Since $\mathrm{Cost}(\sigma)<\infty$, for every play $\rho$ consistent with $\sigma$ and every prefix $\pi$ of $\rho$, we have that there exists an upper bound on $\text{Score}_{F}(\pi)$ for all $F\in{\mathcal{F}}_{1}$. Moreover, as the score of $\inf(\rho)$ tends towards $\infty$, this implies $\inf(\rho)\in{\mathcal{F}}_{0}$, i.e., $\sigma$ is a winning strategy for the qualitative Muller game $\mathcal{G}^{\prime}=(\mathcal{A},\textsc{Muller}({\mathcal{F}}_{0},{\mathcal{F}}_{1}))$.

It is known that, since Player [math] wins $\mathcal{G}^{\prime}$, she has a strategy $\sigma^{\prime}$ with $\text{Score}_{{\mathcal{F}}_{1}}(\pi)\leq 2$ for all prefixes $\pi$ of all plays consistent with $\sigma^{\prime}$ [17]. Thus, we directly obtain $\textsc{QuantMuller}({\mathcal{F}}_{0},{\mathcal{F}}_{1})(\sigma^{\prime})\leq 2$. ∎

We now show how to reduce quantitative Muller games to vertex-ranked $\sup$-safety games based on previous work by Neider, Rabinovich, and Zimmermann [23]. Recall that a safety game is a very simple qualitative game, in which it is Player [math]’s goal to avoid a certain set of undesirable vertices. Formally, the safety condition is defined via a set $U\subseteq V$ as

[TABLE]

In order to construct the safety game, we define an equivalence relation over play prefixes, such that two play prefixes are equivalent if they have the same accumulator and the same score with respect to all $F\in{\mathcal{F}}_{1}$. The constructed safety game uses as vertices representatives of the equivalence classes of all play prefixes that have a cost of at most $2$ for all $F\in{\mathcal{F}}_{1}$. Moreover, it mimics play prefixes $\pi$ of cost at most $2$ in the Muller game by moving to some vertex $\pi^{\prime}$ such that the score and the accumulator are equal in $\pi$ and $\pi^{\prime}$ for all $F\in{\mathcal{F}}_{1}$. We show how to lift this qualitative construction to the setting of quantitative games by providing a quantitative reduction from quantitative Muller games to vertex-ranked $\sup$-safety games.

Lemma 8

Let $\mathcal{G}$ be a quantitative Muller game with $n$ vertices. There exists a memory structure $\mathcal{M}$ of size at most $(n!)^{3}$ and a vertex-ranked $\sup$-safety game $\mathcal{G}^{\prime}$ such that $\mathcal{G}\leq^{3}_{\mathcal{M}}\mathcal{G}^{\prime}$.

Proof

Let $\mathcal{G}=(\mathcal{A},\mathrm{Cost})$ with $\mathrm{Cost}=\textsc{QuantMuller}({\mathcal{F}}_{0},{\mathcal{F}}_{1})$. We say that two play prefixes $\pi$ and $\pi^{\prime}$ are ${\mathcal{F}}_{1}$-equivalent if they end in the same vertex and if, for each $F\in{\mathcal{F}}_{1}$, we have $\text{Acc}_{F}(\pi)=\text{Acc}_{F}(\pi^{\prime})$ and $\text{Score}_{F}(\pi)=\text{Score}_{F}(\pi^{\prime})$. In this case, we write $\pi\approx_{{\mathcal{F}}_{1}}\pi^{\prime}$. For each play prefix $\pi$, we denote the ${\mathcal{F}}_{1}$-equivalence-class of $\pi$ by $[\pi]_{\approx_{{\mathcal{F}}_{1}}}=\{\pi^{\prime}\in V^{*}\mid\pi\approx_{{\mathcal{F}}_{1}}\pi^{\prime}\}$. Furthermore, for each set $\Pi\subseteq V^{*}$ of play prefixes we define the $\approx_{{\mathcal{F}}_{1}}$-quotient of $\Pi$ as ({\Pi}\big{/}\approx_{{\mathcal{F}}_{1}})=\{[\pi]_{\approx_{{\mathcal{F}}_{1}}}\mid\pi\in\Pi\}. For the sake of readability, we omit the index ${\mathcal{F}}_{1}$ of the score-function and the index $\approx_{{\mathcal{F}}_{1}}$ of the equivalence class for the remainder of this proof wherever possible without introducing ambiguity.

Let $\mathrm{Plays}_{\leq 2}=\{\pi\in V^{*}\mid\text{Score}_{{\mathcal{F}}_{1}}(\pi)\leq 2\}$ be the set of play prefixes whose score is at most two. We define the set of memory states M=\left({\mathrm{Plays}_{\leq 2}}\big{/}\approx\right)\cup\{\bot\}, the initial memory state $m_{I}=[v_{I}]$, and the update function $\mathrm{Upd}$ as $\mathrm{Upd}(\bot,v)=\bot$,  $\mathrm{Upd}(\pi,v)=[\pi v]$ if $\text{Score}(\pi v)\leq 2$ and $\mathrm{Upd}(\pi,v)=\bot$ otherwise. We obtain |M|\in\mathcal{O}(|{{\mathrm{Plays}_{\leq 2}}\big{/}\approx}|). Since |{\mathrm{Plays}_{\leq 2}}\big{/}\approx|\leq(n!)^{3} due to Neider, Rabinovich, and Zimmermann [23], the memory structure $\mathcal{M}$ is of size at most $(n!)^{3}$ as well.

A straightforward induction shows that this memory structure tracks the score of a play precisely as long as it does not exceed the value two on any prefix. More formally, it satisfies the following invariant:

Let $\pi=v_{0}\cdots v_{j}$ be a play prefix in $\mathcal{G}$ such that $\text{Score}(v_{0}\cdots v_{k})\leq 2$ for all $k$ with $0\leq k\leq j$. Moreover, let $\mathrm{Upd}^{+}(\pi)=\pi^{\prime}$. Then $\pi\approx\pi^{\prime}$.

Recall $\mathrm{Safety}(U)=\{v_{0}v_{1}v_{2}\cdots\in V^{\omega}\mid\forall j\in\mathbb{N}.\,v_{j}\notin U\}$. We define the vertex-ranked $\sup$-safety game $\mathcal{G}^{\prime}=(\mathcal{A}\times\mathcal{M},{\textsc{Rank}^{\sup}}(\mathrm{Safety}(V\times\{\bot\}),\mathrm{rk}))$, with $\mathrm{rk}(v,\pi)=\text{Score}(\pi)$ for all $\pi\in\mathrm{Plays}_{\leq 2}$, and $\mathrm{rk}(v,\bot)=3$.

Let $\mathrm{Cost}^{\prime}={\textsc{Rank}^{\sup}}(\mathrm{Safety}(V\times\{\bot\}),\mathrm{rk})$. Clearly, the first two items of the definition of $\mathcal{G}\leq^{3}_{\mathcal{M}}\mathcal{G}^{\prime}$ hold true. It remains to show $\mathrm{Cost}(\rho)=\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))$ for all $\rho$ with $\mathrm{Cost}(\rho)<3$ and $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))\geq 3$ for all other $\rho$.

First, let $\rho=v_{0}v_{1}v_{2}\cdots$ be some play with $\mathrm{Cost}(\rho)\leq 2$ and let $\mathrm{ext}(\rho)=(v_{0},m_{0})(v_{1},m_{1})(v_{2},m_{2})\cdots$. Then $\text{Score}(v_{0}\cdots v_{j})\leq 2$ for all $j\in\mathbb{N}$. Thus, due to the invariant above and the definition of $\mathrm{rk}$, we obtain $\mathrm{rk}(v_{j},m_{j})=\text{Score}(v_{0}\cdots v_{j})$ for all $j\in\mathbb{N}$, which implies $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=\mathrm{Cost}(\rho)$.

Towards a proof of the latter statement, let $\rho=v_{0}v_{1}v_{2}\cdots$ be a play with $\mathrm{Cost}(\rho)\geq 3$ and let $j$ be the minimal position such that $\mathrm{Cost}(v_{0}\cdots v_{j})=3$. Since $\mathrm{Cost}(v_{0}\cdots v_{j})=\text{Score}_{F}(v_{0}\cdots v_{j})$ for some $F\in{\mathcal{F}}_{1}$ and since the score is at most incremented by one during each step, we obtain $\text{Score}_{F}(v_{0}\cdots v_{j-1})=2$,  $\text{Acc}_{F}(v_{0}\cdots v_{j-1})=F\setminus\{v_{j}\}$, and $v_{j}\in F$. Let $\mathrm{Upd}^{+}(v_{0}\cdots v_{j-1})=\pi^{\prime}$. Due to the invariant we obtain $\text{Score}_{F}(\pi^{\prime})=2$ and $\text{Acc}_{F}(\pi^{\prime})=F\setminus\{v_{j}\}$. Thus, $\text{Score}_{F}(\pi^{\prime}v_{j})=3$, hence $\mathrm{ext}(v_{0}\cdots v_{j})=(v_{0},m_{I})\cdots(v_{j},\bot)$, which implies $\mathrm{ext}(\rho)\notin\mathrm{Safety}(V\times\{\bot\})$, which in turn yields $\mathrm{Cost}^{\prime}(\mathrm{ext}(\rho))=\infty>3$. ∎

Thus, in order to solve a quantitative Muller game with respect to some $b$, it suffices to solve a vertex-ranked $\sup$-safety game $\mathcal{G}^{\prime}$ with respect to $b$. Recall that this is only constructive if Player [math] wins $\mathcal{G}^{\prime}$ with respect to $b<3$, i.e., only in this case are we able to construct a strategy with cost at most $b$ for her in $\mathcal{G}$. Otherwise, Theorem 3.1 yields that there exists a strategy of cost $\infty$ for Player $1$ in $\mathcal{G}$, but we cannot construct such a strategy from his strategy of cost greater than two in $\mathcal{G}^{\prime}$. This is consistent with results of Neider et al. [23] and with the fact that Muller conditions are in a higher level of the Borel hierarchy than safety conditions. Hence, qualitative Muller games cannot be reduced to safety games.

We can, however, solve the resulting vertex-ranked $\sup$-safety game with respect to a given bound by solving a qualitative safety game as shown in Theorem 4.2. Using this reduction together with the framework of quality-preserving reductions, we obtain an upper bound on the complexity of solving quantitative Muller games with respect to some bound $b$.

Theorem 5.2

The following problem can be solved in time $\mathcal{O}((n!)^{3})$: “Given some quantitative Muller game $\mathcal{G}$ with $n$ vertices and some bound $b\in\mathbb{N}$, does Player [math] win $\mathcal{G}$ with respect to $b$?”

Proof

Given $\mathcal{G}$, we first construct the vertex-ranked $\sup$-safety game $\mathcal{G}^{\prime}$ as shown in Lemma 8. Recall that $\mathcal{G}^{\prime}$ contains at most $(n!)^{3}$ vertices. Due to Theorem 4.2 and the fact that safety games can be solved in linear time in the number of vertices, $\mathcal{G}^{\prime}$ can indeed be solved in time at most $\mathcal{O}((n!)^{3})$ with respect to a given bound $b$. ∎

Analogously to the reasoning leading to Corollary 1 on Page 1 and to Corollary 2 on Page 2, we are now also able to provide an upper bound on the size of strategies for Player [math] in quantitative Muller games. Since both players have positional winning strategies in safety games, an application of Theorem 3.2 to Lemma 8 yields that if Player [math] has a strategy with cost at most three in a quantitative Muller game $\mathcal{G}$ with $n$ vertices, then she also has a strategy in $\mathcal{G}$ with the same cost and of size at most exponential in $n$.

Moreover, we can bound the complexity of the optimization problem for quantitative Muller games as follows: Finding the minimal $b$ such that Player [math] has a strategy of cost at most $b$ in $\mathcal{G}$ requires solving at most three safety games of size in $\mathcal{O}((n!)^{3})$. Thus, the optimization problem for quantitative Muller games can be solved in factorial time.

5.3 Fault Resilient Strategies for Safety Games

We now demonstrate the flexibility and versatility of vertex-ranked games in their own right. To this end, we consider the problem of synthesizing a controller for a reactive system that is embedded into some environment. This setting is typically modeled as an infinite game in which Player [math] and Player $1$ take the roles of the controller and of the environment, respectively. Here, we consider safety games, i.e., we assume that the specification for the controller is given as a game in which it is the aim of Player [math] to keep the play inside a safe subset of the vertices.

Dallal, Neider, and Tabuada [14] argue that this setting is not sufficiently expressive to correctly model a real-world scenario, since it assumes that Player [math] can accurately predict the effect of her actions on the state of the system. In a realistic setting, in contrast, faults may occur, i.e., an action chosen by a controller may be executed incorrectly, or it may not be executed at all.

In order to model such faults, Dallal, Neider, and Tabuada introduce arenas with faults $\mathcal{A}_{F}=(V,V_{0},V_{1},E,F,v_{I})$, which consist of an arena without faults $(V,V_{0},V_{1},E,v_{I})$ and a set of faults $F\subseteq V_{0}\times V$. In such an arena, whenever it is the turn of Player [math], say at vertex $v$, a fault $(v,v^{\prime})\in F$ may occur, resulting in the play continuing in vertex $v^{\prime}$ instead of that chosen by Player [math]. Moreover, Dallal et al. consider safety conditions, i.e., qualitative winning conditions of the form $\mathrm{Safety}(U)=\{v_{0}v_{1}v_{2}\cdots\mid\forall j\in\mathbb{N}.\,v_{j}\notin U\}$ for some $U\subseteq V$. Hence, it is the aim of Player [math] to keep the play outside the “unsafe” set of vertices $U$. If the play enters the set $U$, it is declared winning for Player $1$. The task at hand is to compute a fault-resilient strategy for Player [math] that forces the play to remain inside $V\setminus U$ and that can “tolerate” as many faults as possible.

Safety games without faults are solved by a simple attractor construction: As soon as the play enters $W_{1}=\mathrm{Attr}_{1}(U)$, Player $1$ can play consistently with his attractor strategy towards $U$ in order to win the play. Thus, it is the aim of Player [math] to keep the play inside $W_{0}=V\setminus W_{1}$.

Dallal, Neider, and Tabuada solve the problem of computing fault-resilient strategies for safety games by adapting the classic algorithm for solving safety games to this setting. In doing so, they obtain a value $\mathrm{val}(v)$ for each vertex $v$ that denotes the minimal number of faults that need to occur in order for the play to reach $W_{1}$, if Player [math] plays well. Furthermore, they show that $\mathrm{val}$ can be computed in polynomial time in $|V|$. Finally, due to the existence of positional winning strategies for both players in safety games, they obtain $\mathrm{val}(v)\in[n]\cup\{\infty\}$ for all $v\in V$. Then, a fault-resilient strategy for Player [math] is one that maximizes the minimal value $\mathrm{val}(v)$ witnessed during any play. Dallal, Neider, and Tabuada construct such a strategy on the fly during the computation of $\mathrm{val}(v)$ [14].

This task can, however, easily be reframed as a vertex-ranked game in the arena $\mathcal{A}=(V,V_{0},V_{1},E,v_{I})$, which we obtain from $\mathcal{A}_{F}$ by omitting the faults. In that game, we assign to each vertex the rank $\mathrm{rk}(v)=|V|-\mathrm{val}(v)$ if $\mathrm{val}(v)\in[n]$ and $\mathrm{rk}(v)=0$ otherwise, i.e., if $\mathrm{val}(v)=\infty$. Then, Player [math] has a strategy with cost at most $b$ in $\mathcal{G}^{\prime}=(\mathcal{A},{\textsc{Rank}^{\sup}}(\mathrm{Safety}(U),\mathrm{rk}))$ if and only if she has a winning strategy in the original safety game with faults that tolerates at least $|V|-b$ faults.

This formulation as a vertex-ranked game enables further study of games in arenas with faults. Here, we require the winning condition to be a safety condition in order to compute $\mathrm{val}(v)$. In recent work, we have shown how to compute this value for more complex qualitative winning conditions [24]. If $\mathrm{val}(v)$ is effectively computable for a given qualitative winning condition, one can easily obtain fault-resilient strategies by formulating the task as a vertex-ranked game as demonstrated.

Finally, the formulation as a vertex-ranked game yields a method to compute eventually-fault-resilient strategies, i.e., strategies that are resilient to a large number of faults after a finite “start-up” phase. In order to obtain such strategies, it suffices to view the resulting vertex-ranked games as a $\limsup$-game instead of a $\sup$-game and to solve it optimally as described in Section 4.2.

6 Conclusion

In this work, we have lifted the concept of reductions, which has yielded a multitude of results in the area of qualitative games, to quantitative games. We have shown that this novel concept exhibits the same useful properties for quantitative games as it does for qualitative ones and that it furthermore retains the quality of strategies.

Additionally, we have provided two very general types of quantitative games that serve as targets for quantitative reductions, namely vertex-ranked $\sup$ games and vertex-ranked $\limsup$-games. For both kinds of games we have shown a polynomial overhead on the complexity of solving them with respect to some bound, on the memory necessary to achieve a given cost, and on the complexity of determining the optimal cost that either player can ensure.

Finally, we have demonstrated the versatility of these tools by using them to solve quantitative request-response games and quantitative Muller games and by showing how to solve the problem of computing fault-resilient strategies in safety games via vertex-ranked games. This last formulation enables a general study of games with faults, even in the presence of more complex winning conditions than the safety condition considered by Dallal et al. [14] and in this work. We are currently investigating how to leverage vertex-ranked games for the synthesis of fault-resistant strategies in parity games.

Further research continues in two additional directions: Firstly, while the framework of quantitative reductions and vertex-ranked games yields upper bounds on the complexity of solving quantitative games, it does not directly yield lower bounds on the complexity of the problems under investigation. Consider, for example, the threshold problem for parity games with costs, which is PSpace-complete [30]. It is possible to reduce this problem to that of solving a vertex-ranked parity game of exponential size and linearly many colors similarly to the reduction presented in this work, which yields an ExpTime-algorithm. It remains open how to use quantitative reductions to obtain an algorithm for this problem that only requires polynomial space.

Secondly, another goal for future work is the establishment of an analogue to the Borel hierarchy for quantitative winning conditions. In the qualitative case, this hierarchy establishes clear boundaries for reductions between infinite games, i.e., a game whose winning condition is in one level of the Borel hierarchy cannot be reduced to one with a winning condition in a lower level. Also, each game with a winning condition in the hierarchy is known to be determined [20]. To the best of our knowledge, it is open how to define such a hierarchy for quantitative winning conditions which exhibit similar properties.

Acknowledgements

I would like to thank Martin Zimmermann for many fruitful discussions. Furthermore, I would like to thank the anonymous reviewers for their thorough reviews and constructive comments.