3.1 Characterizing vertices of finite resilience
Our goal in this section is to characterize vertices with finite resilience in a game with prefix-independent winning condition, i.e., those vertices from which Player 0 can win even under \(k-1\) disturbances, but not under k disturbances, for some \(k \in \omega \).
To illustrate our approach, consider the parity game in Fig.
1, which is determined and has a prefix-independent winning condition. The winning region of Player 1 only contains the vertex
\(v_1\). Thus, by Lemma
1,
\(v_1\) is the only vertex with resilience zero, every other vertex has a larger resilience.
Now, consider the vertex \(v_2\), which has a disturbance edge leading into the winning region of Player 1. Due to this edge, \(v_2\) has resilience at most one. This implies, as argued above, that \(v_2\) has resilience precisely one. The unique disturbance-free play starting in \(v_1\) is consistent with every strategy for Player 0 and violates the winning condition. Due to prefix-independence, prepending the disturbance edge does not change the winner and consistency with every strategy for Player 0. Hence, this play witnesses that \(v_2\) has resilience at most one, while \(v_2\) being in Player 0’s winning region yields the matching lower bound. However, \(v_2\) is the only vertex to which this reasoning applies. Now, consider \(v_3\): from here, Player 1 can force a play to visit \(v_2\) using a standard edge. Thus, \(v_3\) has resilience one as well. Again, this is the only vertex to which this reasoning is applicable.
In particular, from \(v_4\), Player 0 can avoid reaching the vertices for which we have already determined the resilience by using the self loop. However, this comes at a steep price for her: doing so results in a losing play, as the color of \(v_4\) is odd. Thus, if she wants to have a chance at winning, she has to take a risk by moving to \(v_2\), from which she has a 1-resilient strategy, i.e., one that is winning if no more disturbances occur. For this reason, \(v_4\) has resilience one as well. The same reasoning applies to \(v_6\): Player 1 can force the play to \(v_4\) and from there Player 0 has to take a risk by moving to \(v_2\).
The vertices \(v_3\), \(v_4\), and \(v_6\) share the property that Player 1 can either enforce a play violating the winning condition or reach a vertex with already determined finite resilience. These three vertices are the only ones currently satisfying this property. They all have resilience one since Player 1 can enforce to reach a vertex of resilience one, but he cannot enforce reaching a vertex of resilience zero. Now, we can also determine the resilience of \(v_5\): the disturbance edge from \(v_5\) to \(v_3\) witnesses it being two.
Afterwards, these two arguments no longer apply to new vertices: no disturbance edge leads from a vertex
\(v \in \{ v_7, \ldots , v_{10} \} \) to some vertex whose resilience is already determined and Player 0 has a winning strategy from each such
v that additionally avoids vertices whose resilience is already determined. Thus, our reasoning cannot determine their resilience. This is consistent with our goal, as all four vertices have non-finite resilience:
\(v_7\) and
\(v_8\) have resilience
\(\omega \) and
\(v_9\) and
\(v_{10}\) have resilience
\(\omega +1\). Our reasoning here cannot distinguish these two values. We solve this problem in Sect.
3.2.
We now formalize the reasoning sketched above: starting from the vertices in Player 1’s winning region having resilience zero, we use a so-called disturbance update and a risk update to determine all vertices of finite resilience. A disturbance update computes the resilience of vertices having a disturbance edge to a vertex whose resilience is already known (such as vertices
\(v_2\) and
\(v_5\) in the example of Fig.
1). A risk update, on the other hand, determines the resilience of vertices from which either Player 1 can force a visit to a vertex with known resilience (such as vertices
\(v_3\) and
\(v_6\)) or Player 0 needs to move to such a vertex in order to avoid losing (e.g., vertex
\(v_4\)). To simplify our proofs, we describe both as monotone operators updating partial rankings mapping vertices to
\(\omega \), which might update already defined values. We show that applying these updates in alternation eventually yields a stable ranking that indeed characterizes the vertices of finite resilience.
Throughout this section, we fix a game
\(\mathcal {G}= (\mathcal {A}, \mathrm {Win})\) with
\(\mathcal {A}= (V, V_0, V_1, E, D)\) and prefix-independent
\(\mathrm {Win}\subseteq V^\omega \) satisfying the following condition: the game
\((\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(U))\) is determined for every
\(U \subseteq V\). We discuss this requirement in Sect.
4.
A ranking for
\(\mathcal {G}\) is a partial mapping
\(r :V \dashrightarrow \omega \). The domain of
r is denoted by
\(\mathrm {dom}(r)\), its image by
\(\mathrm {im}(r)\). Let
r and
\(r'\) be two rankings. We say that
\(r'\) refines
r if
\(\mathrm {dom}(r') \supseteq \mathrm {dom}(r)\) and if
\(r'(v) \le r(v)\) for all
\(v \in \mathrm {dom}(r)\). A ranking
r is sound, if we have
\(r(v) = 0\) if and only if
\(v \in \mathcal {W}_1(\mathcal {G})\) (cf. Lemma
1).
Let
r be a ranking for
\(\mathcal {G}\). We define the ranking
\(r'\) as
$$\begin{aligned} r'(v) = \min \bigl ( \{ r(v) \} \cup \{ r(v')+1 \mid v' \in \mathrm {dom}(r) \text { and } (v,v') \in D \} \bigr ), \end{aligned}$$
where
\(\{ r(v) \} = \emptyset \) if
\(v \notin \mathrm {dom}(r)\), and
\(\min \emptyset \) is undefined (causing
\(r'(v)\) to be undefined). We call
\(r'\) the
disturbance update of
r.
Again, let
r be a ranking for
\(\mathcal {G}\). For every
\(k \in \mathrm {im}(r)\) let
$$\begin{aligned} A_k = \mathcal {W}_1(\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(\{ v \in \mathrm {dom}(r) \mid r(v) \le k \})) \end{aligned}$$
be the winning region of Player 1 in the game where he either wins by reaching a vertex
v with
\(r(v) \le k\) or by violating the winning condition of
\(\mathcal {G}\). Now, define
\(r'(v) = \min \{ k \mid v \in A_k \}\), where
\(\min \emptyset \) is again undefined. We call
\(r'\) the
risk update of
r.
Let \(r_0\) be the unique sound ranking with domain \(\mathcal {W}_1(\mathcal {G})\), i.e., \(r_0\) maps exactly the vertices in Player 1’s winning region to zero, all others are undefined. Starting with \(r_0\), we inductively define a sequence of rankings \((r_j)_{j \in \omega }\) such that \(r_{j}\) for an odd (even) \(j >0\) is the disturbance (risk) update of \(r_{j-1}\), i.e., we alternate between disturbance and risk updates.
Due to refinement, the
\(r_j\) eventually stabilize, i.e., there is some
\(j_0\) such that
\(r_j = r_{j_0}\) for all
\(j \ge j_0\). Define
\(r^* = r_{j_0}\). Due to
\(r_0\) being sound and by Lemmas
2 and
3, each
\(r_j\), and
\(r^*\) in particular, is sound. If
\(v \in \mathrm {dom}(r^*)\), let
\(j_v\) be the minimal
j with
\(v \in \mathrm {dom}(r_j)\); otherwise,
\(j_v\) is undefined.
Proof
We show the following stronger result for every
\(v \in \mathrm {dom}(r^*)\):
If \(j_v\) is odd, then \(r_j(v) = \frac{j_v+1}{2}\) for every \(j \ge j_v\).
If \(j_v\) is even, then \(r_j(v) = \frac{j_v}{2}\) for every \(j \ge j_v\).
The disturbance update increases the maximal rank by at most one and the risk update does not increase the maximal rank at all. Furthermore, due to refinement, the rank of
v is set and then it cannot increase. Hence, we obtain
\(r_j(v) \le \frac{j_v+1}{2}\) and
\(r_j(v) \le \frac{j_v}{2}\) for odd and even
\(j_v\), respectively. In the remainder of the proof, we show a matching lower bound.
We say that a vertex v is updated to \(k \in \omega \) in \(r_j\) if \(r_j(v) = k\) and either \(v \notin \mathrm {dom}(r_{j-1})\) or both \(v \in \mathrm {dom}(r_{j-1})\) and \(r_{j-1}(v) \ne k\) (here, \(r_{-1}\) is the unique ranking with empty domain). Note that as part of the proof, we have to show that the second case never occurs.
Now, we show the following by induction over
j, which implies the matching lower bound.
If j is odd, then no v is updated in \(r_j\) to some \(k < \frac{j+1}{2}\).
If j is even, then no v is updated in \(r_j\) to some \(k < \frac{j}{2}\).
For
\(j = 0\), we have
\(\frac{j}{2} = 0\), and clearly, no vertex is assigned a negative rank by
\(r_0\). For
\(j = 1\) and
\(j' = 2\), we obtain
\(\frac{j+1}{2} = \frac{j'}{2} = 1\). As
\(r_0\),
\(r_1\), and
\(r_2\) are sound, neither
\(r_1\) nor
\(r_2\) update some
v to zero.
Now, let \(j > 2\) and first consider the case where j is odd. Towards a contradiction, assume that \(v \in V\) is updated in \(r_j\) to some value less than \(\frac{j+1}{2}\). Since j is odd, \(r_j\) is the disturbance update of \(r_{j-1}\). Further, as v is updated in \(r_j\), there exists some disturbance edge \((v, v') \in D\) such that \(r_j(v) = r_{j-1}(v') + 1\). Thus, \(r_{j-1}(v')< r_j(v) < \frac{j+1}{2}\), i.e., \(r_{j-1}(v') \le \frac{j+1}{2} - 2 = \frac{j-3}{2}\). First, we show \(r_{j-3}(v') = r_{j-2}(v') = r_{j-1}(v')\), i.e., the rank of \(v'\) is stable during the last two updates.
First assume towards a contradiction \(r_{j-2}(v') \ne r_{j-1}(v')\). Then, \(v'\) is updated in \(r_{j-1}\) to some rank of at most \(\frac{j-3}{2}\), which is in turn smaller than \(\frac{j-1}{2}\), violating the induction hypothesis for \(j-1\). Hence, \(r_{j-2}(v') = r_{j-1}(v')\). The same reasoning yields a contradiction to the assumption \(r_{j-3}(v') \ne r_{j-2}(v')\). Thus, we indeed obtain \(r_{j-3}(v') = r_{j-2}(v') = r_{j-1}(v')\).
Since \(r_{j-2}\) is the disturbance update of \(r_{j-3}\), we obtain \(r_{j-2}(v) \le r_{j-3}(v') + 1 = r_{j-1}(v') + 1 = r_j(v)\). Due to refinement, we obtain \(r_{j-2}(v) \ge r_{j}(v)\), i.e., altogether \(r_{j-2}(v) = r_{j-1}(v) = r_{j}(v)\). The latter equality contradicts our initial assumption, namely v being updated in \(r_j\) to \(r_j(v)\).
Now, consider the case where j is even. Again, assume towards a contradiction that \(v \in V\) is updated in \(r_j\) to some value less than \(\frac{j}{2}\). Since j is even, \(r_j\) is the risk update of \(r_{j-1}\). Further, as v is updated in \(r_j\), Player 1 wins the game \((\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(U))\) from v, where \(U = \{ v' \in \mathrm {dom}(r_{j-1}) \mid r_{j-1}(v') \le r_j(v) \}\). Hence, he has a strategy \(\tau \) such that every play starting in v and consistent with \(\tau \) either violates \(\mathrm {Win}\) or eventually visits some vertex \(v'\) with \(r_{j-1}(v') \le r_j(v)\). We claim \(r_{j-2}(v') = r_{j-1}(v')\) for all \(v' \in U\).
Towards a contradiction, assume \(r_{j-2}(v') \ne r_{j-1}(v')\) for some \(v' \in U\). Note that we have \(r_{j-1}(v') \le r_j(v) < \frac{j}{2}\). Thus, \(v'\) is updated in \(r_{j-1}\) to some value strictly less than \(\frac{j}{2}\), which contradicts the induction hypothesis for \(j-1\). Hence, we indeed obtain \(r_{j-2}(v') = r_{j-1}(v')\) for all \(v' \in U\).
Thus, there are two types of vertices \(v'\) in U: those for which \(r_{j-3}(v')\) is defined, which implies \(r_{j-3}(v') = r_{j-1}(v')\) due to the induction hypothesis and refinement, and those where \(r_{j-3}(v')\) is undefined, which implies \(r_{j-2}(v') = r_{j-1}(v')\) due to the claim above.
We claim that Player 1 wins \((\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(\{ v'' \in \mathrm {dom}(r_{j-3}) \mid r_{j-3}(v'') \le r_j(v) \}))\) from v, which implies \(r_{j-2}(v) = r_j(v)\). This contradicts v being updated in \(r_j\), our initial assumption.
To this end, we construct a strategy \(\tau '\) from v that either violates \(\mathrm {Win}\) or reaches a vertex \(v''\) with \(r_{j-3}(v'')\le r_j(v)\) as follows. From v, \(\tau '\) mimics \(\tau \) until a vertex \(v'\) in U is reached (if it is at all). If \(v'\) is of the first type, then we have \(r_{j-3}(v') = r_{j-1}(v') \le r_j(v)\). If \(v'\) is of the second type, then \(v'\) is updated in \(r_{j-2}\) to some rank \(r_{j-2}(v') = r_{j-1}(v') \le r_j(v)\). As \(r_{j-2}\) is the risk update of \(r_{j-3}\), Player 1 has a strategy \(\tau _{v'}\) from \(v'\) that either violates \(\mathrm {Win}\) or reaches a vertex \(v''\) with \(r_{j-3}(v'') \le r_{j-2}(v') \le r_j(v)\). Thus, starting in \(v'\), \(\tau '\) mimics \(\tau _{v'}\) from \(v'\) until such a vertex is reached (if it is reached at all). Thus, every play that starts in v and is consistent with \(\tau '\) either violates \(\mathrm {Win}\) (as it has a suffix that does) or reaches a vertex \(v''\) with \(r_{j-3}(v'') \le r_j(v)\), which proves our claim.\(\square \)
Lemma
4 implies that an algorithm computing the
\(r_j\) does not need to implement the definition of the two updates as presented above, but can be optimized by taking into account that a rank is never updated once set. However, for the proofs below, the definition presented above is more expedient, as it gives stronger preconditions to rely on, e.g., Lemmas
2 and
3 only hold for the definition presented above.
Also, from the proof of Lemma
4, we obtain an upper bound on the maximal rank of
\(r^*\). This in turn implies that the
\(r_j\) stabilize quickly, as
\(r_j = r_{j+1} = r_{j+2}\) implies
\(r_j = r^*\).
The main result of this section shows that \(r^*\) characterizes the resilience of vertices of finite resilience.
Proof
(1) We show \(r_\mathcal {G}(v) \le r^*(v)\) and \(r_\mathcal {G}(v) \ge r^*(v)\).
“
\(\mathbf{r }_{\varvec{\mathcal {G}}}(\mathbf{v }) \le \mathbf{r }^{\varvec{*}}(\mathbf{v })\)”: an
\(\alpha \)-resilient strategy from
v is also
\(\alpha '\)-resilient from
v for every
\(\alpha ' \le \alpha \). Thus, to prove
$$\begin{aligned} r_\mathcal {G}(v) = \sup \{ \alpha \in \omega +2 \mid \text {Player~0 has an } \alpha \hbox {-}\text {resilient strategy for }\mathcal {G}\text { from }v\} \le r^*(v) \end{aligned}$$
we just have to show that Player 0 has no
\((r^*(v)+1)\)-resilient strategy from
v. By definition, for every strategy
\(\sigma \) for Player 0, we have to show that there is a play
\(\rho \) starting in
v and consistent with
\(\sigma \) that has at most
\(r^*(v)\) disturbances and is winning for Player 1. So, fix an arbitrary strategy
\(\sigma \).
We define a play with the desired properties by constructing longer and longer finite prefixes before finally appending an infinite suffix. During the construction, we ensure that each such prefix ends in \(\mathrm {dom}(r^*)\) in order to be able to proceed with our construction.
The first prefix just contains the starting vertex (v, 0), i.e., the prefix does indeed end in \(\mathrm {dom}(r^*)\). Now, assume we have produced a prefix \(w(v',b')\) ending in some vertex \(v' \in \mathrm {dom}(r^*)\), which implies that \(j_{v'}\) is defined. We consider three cases:
If \(j_{v'} = 0\), then \(v' \in \mathcal {W}_1(\mathcal {G})\) by definition of \(r_0\), i.e., Player 1 has a winning strategy \(\tau \) from v. Thus, we extend \(w(v',b')\) by the unique disturbance-free play that starts in \(v'\) and is consistent with \(\sigma \) and \(\tau \), without its first vertex. In that case, the construction of the infinite play is complete.
Second, if \(j_{v'} > 0\) is odd, then \(v'\) received its rank \(r^*(v')\) during a disturbance update. Hence, there is some \(v''\) such that \((v',v'') \in D\) with \(r^*(v') -1 = r^*(v'') \). In this case, we extend \(w(v',b')\) by such a vertex \(v''\) to obtain the new prefix \(w(v',b')(v'',1)\), which satisfies the invariant, as \(v''\) is in \(\mathrm {dom}(r^*)\). Further, we have \(j_{v''} < j_{v'}\) as the rank of \(v''\) had to be defined in order to be considered during the disturbance update assigning a rank to \(v'\).
Finally, if \(j_{v'} > 0\) is even, then \(v'\) received its rank \(r^*(v')\) during a risk update. We claim that Player 1 has a strategy \(\tau _{v'}\) that guarantees one of the following outcomes from \(v'\): either the resulting play violates \(\mathrm {Win}\) or it encounters a vertex \(v''\) that satisfies \(r^*(v'') \le r^*(v')\) and \(j_{v''} < j_{v'}\) (which implies \(v'' \ne v'\)).
In that case, consider the unique disturbance-free play \(\rho '\) that starts in \(v'\) and is consistent with \(\sigma \) and the strategy \(\tau _{v'}\) as above. If \(\rho '\) violates \(\mathrm {Win}\), then we extend \(w(v',b')\) by \(\rho '\) without its first vertex. In that case, the construction of the infinite play is complete.
If \(\rho '\) does not violate \(\mathrm {Win}\), then we extend \(w(v',b')\) by the prefix of \(\rho '\) without its first vertex and up to (and including) the first occurrence of a vertex \(v''\) in \(\rho '\) satisfying the properties described above. Note that this again satisfies the invariant.
It remains to argue our claim:
\(v'\) was assigned its rank
\(r^*(v') = r_{j_{v'}}(v')\) because it is in Player 1’s winning region in the game with winning condition
\(\mathrm {Win}\cap \mathrm {Safety}(U)\), for
$$\begin{aligned} U = \{ v'' \in \mathrm {dom}(r_{j_{v'}-1}) \mid r_{j_{v'}-1}(v'') \le r_{j_{v'}}(v') \}. \end{aligned}$$
Hence, from
\(v'\), Player 1 has a strategy to either violate the winning condition or to reach
U. Thus,
\(r_{j_{v'}-1}(v'') = r^*(v'')\) for every
\(v'' \in \mathrm {dom}(r_{j_{v'}-1})\) yields
\(r^*(v'') \le r^*(v')\). Finally, we have
\(j_{v''} < j_{v'}\), as the rank of
\(v'\) is assigned due to vertices in
U already having ranks.
Note that only in two cases, we extend the prefix to an infinite play. In the other two cases, we just extend the prefix to a longer finite one. Thus, we first show that this construction always results in an infinite play. To this end, let \(w_0(v_0,b_0)\) and \(w_1 (v_1,b_1)\) be two of the prefixes constructed above such that \(w_1(v_1,b_1)\) is an extension of \(w_0(v_0,b_0)\). A simple induction proves \(j_{v_1} < j_{v_0}\). Hence, as the value can only decrease finitely often, at some point an infinite suffix is added. Thus, we indeed construct an infinite play.
Finally, we have to show that the resulting play has the desired properties: by construction, the play starts in v and is consistent with \(\sigma \). Furthermore, by construction, it has a disturbance-free suffix that violates \(\mathrm {Win}\). Thus, by prefix-independence, the whole play also violates \(\mathrm {Win}\). It remains to show that it has at most \(r^*(v)\) disturbances. To this end, let \(w_0(v_0,b_0)\) and \(w_1 (v_1,b_1)\) be two of the prefixes such that \(w_1 (v_1,b_1)\) is obtained by extending \(w_0(v_0,b_0)\) once. If the extension consists of taking the disturbance edge \((v_0, v_1) \in D\), then we have \(r^*(v_1) = r^*(v_0)+1\). The only other possibility is the extension consisting of a finite play prefix that is consistent with the strategy \(\tau _{v_0}\). Then, by construction, we obtain \(r^*(v_1) \le r^*(v_0)\). So, there are at most \(r^*(v)\) many disturbances in the play, as the current rank decreases with every disturbance edge and does not increase with the other type of extension, but is always non-negative.
“\(\mathbf r _{\varvec{\mathcal {G}}}(\mathbf v ) \varvec{\ge } \mathbf r ^{\varvec{*}}(\mathbf v )\)”: Here, we construct a strategy \(\sigma _{\!f}\) for Player 0 that is \(r^*(v)\)-resilient from every \(v \in \mathrm {dom}(r^*)\), i.e., from v, \(\sigma _{\!f}\) has to be winning even under \(r^*(v)-1\) disturbances. As every strategy is 0-resilient, we only have to consider those v with \(r^*(v) >0\).
The proof is based on the fact that \(r^*\) is both stable under the disturbance and under the risk update, i.e., the disturbance update and the risk update of \(r^*\) are \(r^*\), which yields the following properties. Let \((v,v') \in D\) be a disturbance edge such that \(r^*(v) > 0\). Then, we have \(r^*(v') \ge r^*(v) -1\). Also, for every \(v \in \mathrm {dom}(r^*)\) with \(r^*(v) > 0\), Player 0 has a winning strategy \(\sigma _v\) from v for the game \(\mathcal {G}_v = (\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(\{ v' \in \mathrm {dom}(r^*) \mid r^*(v') < r^*(v) \}))\) (note the strict inequality). Here, we apply determinacy of \(\mathcal {G}_v\), as the risk update is formulated in terms of Player 1’s winning region.
Now, we define \(\sigma _{\!f}\) to always mimic a strategy \(\sigma _{v_{\mathrm {cur}}}\) for some \(v_\mathrm {cur}\in \mathrm {dom}(r^*)\), which is initialized by the starting vertex. The strategy \(\sigma _{v_{\mathrm {cur}}}\) is mimicked until a consequential (w.r.t. \(\sigma _{v_\mathrm {cur}}\)) disturbance edge is taken, say by reaching \(v'\). In that case, the strategy \(\sigma _{\!f}\) discards the history of the play constructed so far, updates \(v_\mathrm {cur}\) to \(v'\), and begins mimicking \(\sigma _{v'}\). This is repeated ad infinitum.
Now, consider a play that starts in \(\mathrm {dom}(r^*)\), is consistent with \(\sigma _{\!f}\), and has less than \(r^*(v)\) disturbances. The part up to the first consequential disturbance edge (if it exists at all) is consistent with \(\sigma _v\). Now, let \((v_0, v_0')\) be the corresponding disturbance edge. Then, we have \(r^*(v_0) \ge r^*(v)\), as \(\sigma _v\) being a winning strategy for the safety condition never visits vertices with a rank smaller than \(r^*(v)\). Thus, we conclude \(r^*(v_0') \ge r^*(v_0) -1 \ge r^*(v) -1\). Similarly, the part between the first and the second consequential disturbance edge (if it exists at all) is consistent with \(\sigma _{v_0'}\). Again, if \((v_1, v_1')\) is the corresponding disturbance edge, then we have \(r^*(v_1') \ge r^*(v_1) -1 \ge r^*(v) - 2\). Continuing this reasoning shows that less than \(r^*(v)\) (consequential) disturbance edges lead to a vertex \(v'\) with \(r^*(v') > 0\), as the rank is decreased by at most one for every disturbance edge. The suffix starting in this vertex is disturbance-free and consistent with \(\sigma _{v'}\). Hence, the suffix satisfies \(\mathrm {Win}\), i.e., by prefix-independence, the whole play satisfies \(\mathrm {Win}\) as well. Thus, \(\sigma _{\!f}\) is indeed \(r^*(v)\)-resilient from every \(v \in \mathrm {dom}(r^*)\).
(2) Let \(X = V {\setminus } \mathrm {dom}(r^*)\). The disturbance update of \(r^*\) being \(r^*\) implies that every disturbance edge starting in X leads back to X. Similarly, the risk update of \(r^*\) being \(r^*\) implies \(X = \mathcal {W}_0(\mathcal {G}_X)\) for \(\mathcal {G}_X = (\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(V {\setminus } X))\). Thus, from every \(v \in X\), Player 0 has a strategy \(\sigma _v\) such that every disturbance-free play that starts in v and is consistent with \(\sigma _v\) satisfies the winning condition \(\mathrm {Win}\) and never leaves X. Using these properties, we construct a strategy \(\sigma _{\!\omega }\) that is \(\omega \)-resilient from each \(v \in X\). Thus, \(r_\mathcal {G}(v) \in \{ \omega , \omega +1 \}\).
The definition of the strategy \(\sigma _{\!\omega }\) here is similar to the one above yielding the lower bound on the resilience. Again, \(\sigma _{\!\omega }\) always mimics a strategy \(\sigma _{v_{\mathrm {cur}}}\) for some \(v_\mathrm {cur}\in X\), which is initialized by the starting vertex. The strategy \(\sigma _{v_{\mathrm {cur}}}\) is mimicked until a consequential (w.r.t. \(\sigma _{v_\mathrm {cur}}\)) disturbance edge is taken, say by reaching the vertex \(v'\). In that case, the strategy \(\sigma _{\!\omega }\) discards the history of the play constructed so far, updates \(v_\mathrm {cur}\) to \(v'\), and begins mimicking \(\sigma _{v'}\). This is repeated ad infinitum.
Due to the properties of the disturbance edges and the strategies \(\sigma _v\), such a play never leaves X, even if disturbances occur. Furthermore, if only finitely many disturbances occur, then the resulting play has a disturbance-free suffix that starts in some \(v' \in X\) and is consistent with \(\sigma _{v'}\). As \(\sigma _{v'}\) is winning from \(v'\) in \(\mathcal {G}_X\), this suffix satisfies \(\mathrm {Win}\). Hence, by prefix-independence of \(\mathrm {Win}\), the whole play also satisfies \(\mathrm {Win}\). Thus, \(\sigma _{\!\omega }\) is indeed an \(\omega \)-resilient strategy from every \(v \in X\). \(\square \)
Combining Corollary
1 and Lemma
5, we obtain an upper bound on the resilience of vertices with finite resilience.
3.3 Computing optimally resilient strategies
This section is concerned with computing the resilience and optimally resilient strategies. Here, we focus on positional and finite-state strategies, which are sufficient for the majority of winning conditions in the literature. Nevertheless, it is easy to see that our framework is also applicable to infinite-state strategies.
In the proof of Lemma
5, we construct strategies
\(\sigma _{\!f}\) and
\(\sigma _{\!\omega }\) such that
\(\sigma _{\!f}\) is
\(r_\mathcal {G}(v)\)-resilient from every
v with
\(r_\mathcal {G}(v) \in \omega \) and such that
\(\sigma _{\!\omega }\) is
\(\omega \)-resilient from every
v with
\(r_\mathcal {G}(v) \ge \omega \). Both strategies are obtained by combining winning strategies for some game
\((\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(U))\). However, even if these winning strategies are positional, the strategies
\(\sigma _{\!f}\) and
\(\sigma _{\!\omega }\) are in general not positional. Nonetheless, we show in the proof of Theorem
1 that such positional winning strategies and a positional one for
\(\mathcal {G}_\mathrm {rig}\) can be combined into a single positional optimally resilient strategy.
Recall the requirements from Sect.
3.1 for a game
\((\mathcal {A}, \mathrm {Win})\):
\(\mathrm {Win}\) is prefix-independent and the game
\(\mathcal {G}_U\) is determined for every
\(U \subseteq V\), where we write
\(\mathcal {G}_U\) for the game
\((\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(U))\) for some
\(U \subseteq V\). To prove the results of this section, we need to impose some additional effectiveness requirements: we require that each game
\(\mathcal {G}_U\) and the rigged game
\({\mathcal {G}_{\mathrm {rig}}}\) can be effectively solved. Also, we first assume that Player 0 has positional winning strategies for each of these games, which have to be effectively computable as well. We discuss the severity of these requirements in Sect.
4.
To prove this result, we refine the following standard technique that combines positional winning strategies for games with prefix-independent winning conditions.
Assume we have a positional strategy \(\sigma _v\) for every vertex v in some set \(W \subseteq V\) such that \(\sigma _v\) is winning from v. Furthermore, let \(R_v\) be the set of vertices visited by plays that start in v and are consistent with \(\sigma _v\). Also, let \(m(v) = \min _\prec \{ v' \in V \mid v \in R_{v'} \}\) for some strict total ordering \(\prec \) of W. Then, the positional strategy \(\sigma \) defined by \(\sigma (v) = \sigma _{m(v)}(v)\) is winning from each \(v \in W\), as along every play that starts in some \(v \in W\) and is consistent with \(\sigma \), the value of the function m cannot increase. Thus, after it has stabilized, the remaining suffix is consistent with some strategy \(\sigma _{v'}\). Hence, the suffix is winning for Player 0 and prefix-independence implies that the whole play is winning for her as well.
Here, we have to adapt this reasoning to respect the resilience of the vertices and to handle disturbance edges. Also, we have to pay attention to vertices of resilience \(\omega +1\), as plays starting in such vertices have to be winning under infinitely many disturbances.
Proof of Theorem 1
The effective computability of the resilience follows from the effectiveness requirements on
\(\mathcal {G}\): to compute the ranking
\(r^*\), it suffices to compute the disturbance and risk updates. The former are trivially effective while the effectiveness of the latter ones follows from our assumption. Lemma
5 shows that
\(r^*\) correctly determines the resilience of all vertices with finite resilience. Finally, by solving the rigged game, we also determine the resilience of the remaining vertices (Lemma
6). Again, this game can be solved due to our assumption.
Thus, it remains to show how to compute a positional optimally resilient strategy. To this end, we compute a positional strategy
\(\sigma _v\) for every
v satisfying the following:
Furthermore, we fix a strict linear order
\(\prec \) on
V such that
\(v \prec v'\) implies
\(r_\mathcal {G}(v) \le r_\mathcal {G}(v')\), i.e., we order the vertices by ascending resilience. For
\(v\in V\) with
\(r_\mathcal {G}(v) \ne \omega +1\), let
\(R_v\) be the set of vertices reachable via disturbance-free plays that start in
v and are consistent with
\(\sigma _v\). On the other hand, for
\(v \in V\) with
\(r_\mathcal {G}(v) = \omega +1\), let
\(R_v\) be the set of vertices reachable via plays with arbitrarily many disturbances that start in
v and are consistent with
\(\sigma _v\).
We claim \(R_v \subseteq \{ v' \in V \mid r_\mathcal {G}(v') \ge r_\mathcal {G}(v) \}\) for every \(v \in V\) (\(*\)). For v with \(r_\mathcal {G}(v) \ne \omega +1\) this follows immediately from the choice of \(\sigma _v\). Thus, let v with \(r_\mathcal {G}(v) = \omega +1\). Assume \(\sigma _v\) reaches a vertex \(v'\) of resilience \(r_\mathcal {G}(v') \ne \omega +1\). Then, there exists a play \(\rho '\) starting in \(v'\) that is consistent with \(\sigma _v\), has less than \(\omega +1\) many disturbances and is losing for Player 0. Thus, the play obtained by first taking the play prefix to \(v'\) and then appending \(\rho '\) without its first vertex yields a play starting in v, consistent with \(\sigma _v\), but losing for Player 0. This play witnesses that \(\sigma _v\) is not \((\omega +1)\)-resilient from v, which contradicts our assumption and thus concludes the proof of the claim for the case \(r_\mathcal {G}(v) = \omega + 1\).
Let \(m :V \rightarrow V\) be given as \(m(v) = \min _\prec \{ v' \in V \mid v \in R_{v'} \}\) and define the positional strategy \(\sigma \) as \(\sigma (v) = \sigma _{m(v)}(v)\). By our assumptions, \(\sigma \) can be effectively computed. It remains to show that it is optimally resilient.
To this end, we apply the following two properties of edges
\((v,v')\) that may appear during a play that is consistent with
\(\sigma \), i.e., we either have
\(v \in V_0 \) and
\(\sigma (v) = v'\) (which implies
\((v,v') \in E\)), or
\(v \in V_1\) and
\((v,v') \in E\), or
\(v \in V_0\) and
\((v,v') \in D\):
1.If \((v,v') \in E\), then we have \(r_\mathcal {G}(v) \le r_\mathcal {G}(v')\) and \(m(v) \ge m(v')\). The first property follows from minimality of m(v) and (\(*\)) while the second follows from the definition of \(R_v\).
2.If
\((v,v') \in D\), then we distinguish several subcases, which all follow immediately from the definition of resilience:
If \(r_\mathcal {G}(v) \in \omega \), then \(r_\mathcal {G}(v') \ge r_\mathcal {G}(v) -1\).
If \(r_\mathcal {G}(v) = \omega \), then \(r_\mathcal {G}(v') = \omega \), and
If \(r_\mathcal {G}(v) = \omega + 1\), then \(r_\mathcal {G}(v') = \omega + 1\) and \(m(v) \ge m(v')\) (here, the second property follows from the definition of \(R_v\) for v with \(r_\mathcal {G}(v) = \omega + 1\), which takes disturbance edges into account).
Now, consider a play
\(\rho = (v_0, b_0) (v_1, b_1) (v_2, b_2) \cdots \) that is consistent with
\(\sigma \). If
\(r_\mathcal {G}(v_0) = 0\) then we have nothing to show, as every strategy is 0-resilient from
v.
Now, assume \(r_\mathcal {G}(v_0) \in \omega {\setminus }\{ 0 \}\). We have to show that if \(\rho \) has less than \(r_\mathcal {G}(v_0)\) disturbances, then it is winning for Player 0. An inductive application of the above properties shows that in that case the last disturbance edge leads to a vertex of non-zero resilience. Furthermore, as the values \(m(v_j)\) are only decreasing afterwards, they have to stabilize at some later point. Hence, there is some suffix of \(\rho \) that starts in some \(v'\) with non-zero resilience and that is consistent with the strategy \(\sigma _{v'}\). Thus, the suffix is winning for Player 0 by the choice of \(\sigma _{v'}\) and prefix-independence implies that \(\rho \) is winning for her as well.
Next, assume \(r_\mathcal {G}(v_0) = \omega \). We have to show that if \(\rho \) has a finite number of disturbances, then it is winning for Player 0. Again, an inductive application of the above properties shows that in that case the last disturbance edge leads to a vertex of resilience \(\omega \) or \(\omega +1\). Afterwards, the values \(m(v_j)\) stabilize again. Hence, there is some suffix of \(\rho \) that starts in some \(v'\) with non-zero resilience and that is consistent with the strategy \(\sigma _{v'}\). Thus, the suffix is winning for Player 0 by the choice of \(\sigma _{v'}\) and prefix-independence implies that \(\rho \) is winning for her as well.
Finally, assume \(r_\mathcal {G}(v_0) = \omega +1\). Then, the above properties imply that \(\rho \) only visits vertices with resilience \(\omega +1\) and that the values \(m(v_j)\) eventually stabilize. Hence, there is a suffix of \(\rho \) that is consistent with some \((\omega +1)\)-resilient strategy \(\sigma _{v'}\), where \(v'\) is the first vertex of the suffix. Hence, the suffix is winning for Player 0, no matter how many disturbances occur. This again implies that \(\rho \) is winning for her as well. \(\square \)
The algorithm determining the vertices’ resilience and a positional optimally resilient strategy first computes \(r^*\) and the winner of the rigged game. This yields the resilience of \(\mathcal {G}\)’s vertices. Furthermore, the strategy is obtained by combining winning strategies for the games \(\mathcal {G}_U\) and for the rigged game as explained above.
Next, we analyze the complexity of the algorithm sketched above in some more detail. The inductive definition of the
\(r_j\) can be turned into an algorithm computing
\(r^*\) (using the results of Lemma
4 to optimize the naive implementation), which has to solve
\(\mathcal {O}(|V|)\) many games (and compute winning strategies for some of them) with winning condition
\(\mathrm {Win}\cap \mathrm {Safety}(U)\). Furthermore, the rigged game, which is of size
\(\mathcal {O}(|V|)\), has to be solved and winning strategies have to be determined. Thus, the overall complexity is in general dominated by the complexity of solving these tasks.
We explicitly state one complexity result for the important case of parity games, using the fact that each of these games is then a parity game as well. Also, we use a quasipolynomial time algorithm for solving parity games [
8,
15,
20,
22] to solve the games
\(\mathcal {G}_U\) and
\({\mathcal {G}_{\mathrm {rig}}}\).
Using similar arguments, one can also analyze games where positional strategies do not suffice. As above, assume \(\mathcal {G}\) satisfies the same assumptions on determinacy and effectiveness, but only require that Player 0 has finite-state winning strategies for each game with winning condition \((\mathcal {A}, \mathrm {Win}\cap \mathrm {Safety}(U))\) and for the rigged game \({\mathcal {G}_{\mathrm {rig}}}\). Then, one can show that she has a finite-state optimally resilient strategy. In fact, by reusing memory states, one can construct an optimally resilient strategy that it is not larger than any constituent strategy.