text:
\section{Adaptive Strategies}\label{adaptive strategy}
In this section, we start by presenting a motivating example, a game in which classical strategies for Player~$0$ are not necessarily optimal (in an intuitive sense). We then formalize this intuition by introducing adaptive strategies and give a doubly-exponential time algorithm to compute such strategies.

\paragraph*{Motivating Example.}\label{sec: Motivating adaptive}
Consider the arena given in \autoref{fig:motivate adaptive}
(where Player~$0$'s vertices are shown as circles and Player~$1$'s vertices are shown as squares) with the $\mathrm{rLTL}$ specification~$\varphi =\Boxdot p$.

\begin{figure}[t!]
	\centering
	\begin{tikzpicture}
		\node[player0, label={below:$\{ p \}$}] (0) at (0, 0) {$0$};
		\node[player1, label={below:$\{  \}$}] (1) at (1.5, 0) {$1$};
		\node[player0, label={below:$\{  \}$}] (4) at (3, 0) {$4$};
		\node[player1, label={below:$\{ p \}$}] (5) at (4.5, 0) {$5$};
		\node[player1, label={below:$\{ p \}$}] (2) at (-1.5, 0) {$2$};
		\node[player0, label={below:$\{  \}$}] (3) at (-3, 0) {$3$};

		\path[->] (0) edge (1) edge (2);
		\path[->] (1) edge (4) edge[bend right =40] (2);
		\path[->] (4) edge (5) edge[bend left=60] (0);
		\path[->] (5) edge[loop right] ();
		\path[->] (2) edge[bend left=20] (3);
		\path[->] (3) edge[bend left=20] (2);

	\end{tikzpicture}
	\caption{First motivating example for adaptive strategies}
	\label{fig:motivate adaptive}
\end{figure}

Suppose the token is initially placed at vertex~$0$. Considering Player~$1$ plays optimally, the token would eventually reach vertex~$2$, from which the best possible scenario for Player~$0$ is to enforce a play where $p$ holds at infinitely many positions. As the classical problem only considers the worst-case analysis, a classical strategy for Player~$0$ is to try to visit vertex~$2$ infinitely often. That can be done by moving the token along one of the following edges every time the token reaches Player~$0$'s vertices: $\{0\rightarrow 1; 3\rightarrow 2; 4\rightarrow 0\}$. Note that the move $4\rightarrow 0$ is irrelevant in this worst-case analysis, as vertex~$4$ is never reached if Player~$1$ plays optimally.

Suppose Player~$1$ makes a bad move by moving along $1\rightarrow 4$. Then, Player~$0$ can force the play to eventually just stay at vertex~$5$, and hence, $p$ holds almost always. However, the above classical strategy for Player~$0$ moves the play back to vertex~$0$, from which $p$ might not hold almost always. Therefore, a better strategy for Player~$0$ is to move along $4\rightarrow 5$ if the token reaches vertex~$4$ to get a play where $p$ holds almost always; otherwise, enforce a play where $p$ holds at infinitely many positions as earlier by moving along $0\rightarrow 1$ and then $3\rightarrow 2$ repeatedly.

In the worst case, i.e., if Player~$1$ does not make a bad move by reaching vertex~$4$, both strategies yield value~$0011$.
However, if Player~$1$ does make a bad move by reaching vertex~$4$, the second strategy achieves value~$0111$ on some plays, while the second one does not.
So, in the worst case analysis, both strategies are equally good, but if we assume that Player~$1$ is not necessarily antagonistic, then the second strategy is better as it is able to exploit the bad move by Player~$1$.
We call such a strategy \textit{adaptive} as it adapts its moves to achieve the best possible outcome after each bad move of the opponent. We will formalize this shortly.

\begin{figure}[b!]
	\centering
	\begin{tikzpicture}
		\node[player1, label={below:$\{ r\}$}] (0) at (0, 0) {$0$};
		\node[player1, label={below:$\{ q,r \}$}] (1) at (1.5, 0) {$1$};
		\node[player1, label={below:$\{ r\}$}] (2) at (3, 0) {$2$};
		\node[player0, label={below:$\{ p,r \}$}] (3) at (4.5, 0) {$3$};
		\node[player1, label={below:$\{ r \}$}] (4) at (6,0) {$4$};

		\path[->] (0) edge (1) edge[bend left=40] (2);
		\path[->] (1) edge (2);
		\path[->] (2) edge[bend left=20] (3);
		\path[->] (3) edge[bend left=20] (2) edge(4);
		\path[->] (4) edge[loop right] ();

	\end{tikzpicture}
	\caption{Second motivating example for adaptive strategies}
	\label{fig:motivate adaptive2}
\end{figure}

To illustrate the notion of adaptive strategies, consider another game with the arena shown in \autoref{fig:motivate adaptive2} and with $\mathrm{rLTL}$ specification $\varphi' = (\Xdot \neg q \Rightarrow \Boxdot p)\wedge (\Xdot q \Rightarrow \Boxdot r)$.
In this example, Player~$1$ has only two strategies starting from vertex~$0$: one moving the token along $0\rightarrow 1$ and one moving the token along $0\rightarrow 2$.

The best truth value Player~$0$ can enforce in this game is $0011$.
This is because Player~$1$ can move along the edge~$0\rightarrow 2$, which satisfies the second implication with value~$1111$ (as $q$ does not occur), but also satisfies the premise of the first implication with value~$1111$.
Hence, the value of the whole formula is the value of the subformula~$\Boxdot p$.
The best value Player~$0$ can achieve for it is indeed $0011$ by looping between vertices~$3$ and $2$.
His only other choice, i.e., to move to $4$ eventually, only results in the value~$0001$.

However, if Player~$1$ does not take the edge~$0\rightarrow 2$ but instead moves to vertex~$2$ via vertex~$1$, Player~$0$ can gain from this \emph{bad move} by instead moving to vertex~$4$.
In that case, the formula is satisfied with truth value~$1111$.
Thus, a strategy that adapts to the bad move by the opponent can achieve a better value than one that does not, if she does make a bad move.

\subsection{Definitions}
Recall that a $(\sigma,\mathtt{p})$-play for a strategy~$\sigma$ for Player~$i$ and a play prefix~$\mathtt{p}$ (not necessarily consistent with $\sigma$) is an extension of $\mathtt{p}$ by $\sigma$, i.e., Player~$i$ uses the strategy~$\sigma$ to extend the play prefix~$p$ he had not control over, while still taking the prefix~$\mathtt{p}$ into account when making his decisions.
We say that a strategy $\sigma$ for Player~$0$ \textit{enforces} a truth value of $b$ from a play prefix~$\mathtt{p}$, if we have $\mathcal{V}(\rho) \geq b$ for every $(\sigma, \mathtt{p})$-play~$\rho$.
Similarly, we say a strategy $\tau$ for Player~$1$ enforces a truth value of $b$ from a play prefix~$\mathtt{p}$, if we have $\mathcal{V}(\rho) \leq b$ for every $(\tau, \mathtt{p})$-play~$\rho$.
This conforms to our intuition that Player~$0$ tries to maximize the truth value while Player~$1$ tries to minimize it.
Moreover, we say Player~$i$ can enforce a value $b$ from some prefix~$\mathtt{p}$ if he has a strategy that enforces $b$ from $\mathtt{p}$.

\begin{remark}
Let $\mathtt{p}$ be a play prefix. If Player~$0$ can enforce value~$b_0$ from $\mathtt{p}$ and Player~$1$ can enforce value~$b_1$ from $\mathtt{p}$ then $b_0 \le  b_1$	.
\end{remark}

For example, consider the game given in \autoref{fig:motivate adaptive} with the $\mathrm{rLTL}$ specification~$\Boxdot p$. Using the analysis given in Section~\ref{sec: Motivating adaptive}, we can see that Player~$0$ can enforce $0111$ and $0011$ from prefixes $014$ and $012$, respectively, by moving the token along $\{0\rightarrow 1, 4\rightarrow 5, 3\rightarrow 2\}$. It is easy to check that these are the best values Player~$0$ can enforce from those prefixes as Player~$1$ can enforce the same values from these prefixes.

We are interested in a strategy that enforces the best possible value from each play prefix. This is formalized as follows.

\begin{definition}[Adaptive Strategies]\label{def:adaptive}
	In an $\mathrm{rLTL}$ game, a strategy $\sigma_0$ for Player~$0$ is \textit{adaptive} if from any play prefix~$\mathtt{p}$, no strategy for Player~$0$ enforces a better truth value than $\sigma_0$,
	that is, if some strategy $\sigma$ for Player~$0$ enforces a truth value of $b$ from $\mathtt{p}$, then $\sigma_0$ also enforces the value $b$ from $\mathtt{p}$.
\end{definition}

Note that $\mathtt{p}$ is not required to be consistent with $\sigma_0$ in the above definition, i.e., an adaptive strategy achieves the best possible outcome from every possible play prefix (even for those it had no control over when they are constructed).
Also, let us mention that a dual notion can be defined for Player~$1$.

\subsection{Computing Adaptive Strategies}\label{solving rLTL games}
Now, to synthesize an adaptive strategy, we need to monitor the bad moves of the opponent at runtime by keeping track of the best value that can be enforced from the current play prefix.
To do that, using the idea of automata-based runtime verification~\cite{runtime_verif}, we construct multiple parity automata to monitor the bad moves of the opponent and then we synthesize adaptive strategies by using a reduction to parity games (see \cite{Automata_Book} for definitions).

Given an $\mathrm{rLTL}$ game $\mathcal{G} = (\mathcal{A}, \varphi)$ with $\mathcal{A} = (V,E,\lambda)$, we proceed as follows:
\begin{enumerate}
	\item We construct a generalized (non-deterministic) B\"uchi automata $\mathcal{A}^b$ such that $L(\mathcal{A}^b) =\{w \in  (2^\mathcal{P})^{\omega} \mid \mathcal{V}(w, \varphi) \geq b\}$ for all $b\in \mathbb{B}_4$.

	\item We determinize each $\mathcal{A}^b$ to obtain a deterministic parity automaton~$\mathcal{C}^b$ with the same language.

	\item For each $b$, we construct a parity game $\mathcal{G}^b$ by taking the product of the arena~$\mathcal{A}$ and the parity automaton~$\mathcal{C}^b$.

	\item We solve the above parity games~$\mathcal{G}^b$~\cite{calude}, yielding, for each truth value~$b$, a finite-state  strategy for the original game~$\mathcal{G}$ with value~$b$ (if one exists).

	\item We combine all these winning strategies for Player~$0$ computed in the last step to obtain an adaptive strategy $\sigma$ for Player~$0$.

\end{enumerate}

Let us now explain each step in more detail.

\paragraph{Step 1.} We construct the generalized non-deterministic B\"uchi automata $\mathcal{A}^b$ such that $L(\mathcal{A}^b) =\{w \in  (2^\mathcal{P})^{\omega} \mid \mathcal{V}(w, \varphi) \geq b\}$ for all $b\in \mathbb{B}_4$. By \autoref{thm:rLTL-Buchi}, the automaton $\mathcal{A}^b$ has $n = 2^{O(\lvert\varphi\rvert)}$ states and $k = O(\lvert\varphi\rvert)$ accepting sets.

\paragraph{Step 2.} We determinize each $\mathcal{A}^b$ to get a deterministic parity automaton $\mathcal{C}^b = (Q^b, 2^\mathcal{P},q_0^b,\delta^b,\Omega^b)$ with $O(2^{O(n \log n )})$ states and $2n$ colors~\cite{Buchi-Parity}.

\paragraph{Step 3.} We construct the (unlabelled) product arena~$\mathcal{A}^b = (V^b,E^b)$ of the arena~$\mathcal{A} = (V,E,\lambda)$ and the parity automaton $\mathcal{C}^b$ such that $V^b = V \times Q^b$, $V_i^b = V_i \times Q^b$ for $i \in \set{0,1}$, and
\[((v,q),(v',q'))\in E^b \text{ if and only if } (v,v')\in E \text{ and } \delta^b(q, \lambda(v)) = q'.\]
The function $\bar{\Omega}^b$ assigns colors to the vertices such that $\bar{\Omega}^b(v,q) = \Omega^b(q)$.
The desired parity games are the $\mathcal{G}^b = (\mathcal{A}^b, \bar{\Omega}^b)$ with $b \in \mathbb{B}_4$.

It is easy to verify that Player~$0$ wins a play $\rho' = (v_0, q^b_0)(v_1, q^b_1)\cdots$ in $\mathcal{G}^b$ if and only if the value of the play $\rho = v_0v_1\cdots$ in $\mathcal{G}$ is at least $b$. Furthermore, given a path $\rho = v_0v_1\cdots v_k$ in $\mathcal{A}$, there is a unique path of the form $\rho' = (v_0, q_0^b)(v_1, q_1^b)\cdots (v_k,q_k^b)$ in $\mathcal{A}^b$, that is when $q^b_{i+1} = \delta^b(q_i^b,v_i)$ for all $0\leq i \leq k-1$.

Since winning a play in $\mathcal{G}^b$ is equivalent to the corresponding play in $\mathcal{G}$ satisfying $\varphi$ with truth value $b$ or greater, we can characterize the enforcement of $b$ in $\mathcal{G}$ by the winning region of Player~$0$ in $\mathcal{G}^b$, i.e., the set of vertices from which Player~$0$ has a winning strategy.
This can easily be shown by simulating a winning strategy from $(v,q)$ to extend the play prefix~$\mathtt{p} $ and vice versa.

\begin{remark}
\label{remark_enforcementcharac}
Fix a play prefix~$\mathtt{p}$ in the rLTL game~$\mathcal{G}$, and let $(v,q^b)$ be the last vertex of the corresponding play in the parity game~$\mathcal{G}^b$ for some $b$.
Then, Player~$0$ can enforce~$b$ from $\mathtt{p}$ if and only if $(v,q^b)$ is in his winning region of $\mathcal{G}^b$.
\end{remark}

\paragraph{Step 4.} We solve the resulting parity games $\mathcal{G}^b$ and determine the winning regions~$\win{\mathcal{G}^b}$ of Player~$0$ and  uniform memoryless winning strategies~$\sigma^{b}$ for Player~$0$ that are winning from every vertex in the corresponding winning region. The parity games have $n_p = \abs{V} \cdot 2^{O(n \log n )}$ vertices and $k_p = O(2n)$ colors. Since $k_p < \lg(n_p)$, these can be solved in time $O(n_p^5)$~\cite{calude}.

\paragraph{Step 5.} Consider the extended $\mathrm{rLTL}$ game $\mathcal{G}' = (\mathcal{A}',\varphi)$, where $\mathcal{A}' = (V', E', \lambda')$  with $V' = V \times Q^{0000} \times \cdots \times Q^{1111}$, \begin{multline*}
	E' = \bigl\{ \left((v_1,q_1^{0000}, \ldots, q_1^{1111}),(v_2,q_2^{0000}, \ldots, q_2^{1111})\right) \mid \\
(v_1,v_2)\in E \text{ and } \delta^{b}(q_1^b, \lambda(v)) = q_2^b \text{ for all }b\in \mathbb{B}_4 \bigr\},
\end{multline*}
	and $\lambda'$ such that $\lambda'(v,q^{0000},\ldots,q^{1111}) = \lambda(v)$ for all $v\in V$ and $ q^b\in Q^b$.

It is easy to see that there is a one to one correspondence between the plays in both games $\mathcal{G}$ and $\mathcal{G}'$. Besides that, the $\mathrm{rLTL}$ specification is also the same in both games. Therefore, computing an adaptive strategy in the game $\mathcal{G}$ is equivalent to computing one in the game $\mathcal{G}'$. Now using the analysis given in Step~$3$, we have the following in the $\mathrm{rLTL}$ game $\mathcal{G}'$:
\begin{itemize}
	\item[\textbullet] A vertex~$v'$ is in $\enfMore{b} = \{(v,q^{0000},\ldots,q^{1111})\in V'\mid (v,q^b)\in \win{\mathcal{G}^{b}}\}$ if and only if Player~$0$ can enforce $b$ from every play prefix in $\mathcal{G}'$ ending in~$v'$.

	\item[\textbullet] Using these sets, we now define the set~$\enfExact{b}$ of vertices from which the maximum value Player~$0$ can enforce is $b$.
	Formally, this set is given by
	\[
	\enfExact{b} = \begin{cases}
 	\enfMore{1111} &\text{if $b =1111$,} \\
 	\enfMore{b}\setminus \enfMore{b+1} &\text{if $b < 1111$},
 \end{cases}\]
where $b+1$ is the smallest value bigger than~$b<1111$. Note that the sets~$\enfExact{b}$ form a partition of the vertex set of $\mathcal{G}'$.
\end{itemize}

Furthermore, it is easy to see that if a play $\rho$ satisfies a parity objective then every play sharing a suffix with $\rho$ also satisfies the parity objective. Since the game $\mathcal{G}'$ is a product of parity games and since we have characterized the enforcement of truth values via the membership in the winning regions of the parity games (see Remark~\ref{remark_enforcementcharac}), the next remark follows.

\begin{remark}\label{remark: two prefix same ending}
	In the $\mathrm{rLTL}$ game $\mathcal{G}'$, for two play prefixes $\mathtt{p}_1,\mathtt{p}_2$ ending in the same vertex, the following holds: if a memoryless strategy~$\sigma$ for Player~$0$ enforces a truth value $b$ from $\mathtt{p}_1$, then it also enforces the value $b$ from $\mathtt{p}_2$.
\end{remark}

Then, we can see that if the token stays in $\enfExact{b}$ for some $b$, then Player~$0$ can simulate the strategy $\sigma^b$ for $\mathcal{G}^b$ to enforce the value $b$ in $\mathcal{G}'$. Therefore, we obtain a memoryless adaptive strategy $\sigma$ for Player~$0$ in the game $\mathcal{G}'$ as follows: for any vertex~$(v,q^{0000},\ldots,q^{1111})$ in $\enfExact{b}$, we define $\sigma(v,q^{0000},\ldots,q^{1111})$ to be the unique successor of $(v,q^{0000},\ldots,q^{1111})$ in $\mathcal{G}'$ that corresponds to the successor~$\sigma^b(v,q^b)$ of $(v,q^b)$ in $\mathcal{G}^b$.
Thus, $\sigma$ simulates the strategy $\sigma^b$ for the largest $b$ such that the value $b$ can be enforced (which is exactly what $\sigma^b$ does from such a prefix).
Hence, it is an adaptive strategy for Player~$0$ in $\mathcal{G}'$.

Finally, using the strategy $\sigma$, one can compute a corresponding strategy in the game $\mathcal{G}$ with memory $Q^{0000}\times Q^{0001} \times \cdots \times Q^{1111}$, which is used to simulate the positional strategy~$\sigma$.
The resulting finite-state strategy is an adaptive strategy for Player~$0$ in $\mathcal{G}$.

Note that the adaptive strategy in $\mathcal{G}$ is of doubly-exponential size in $|V|$ and $\lvert\varphi\rvert$.
This upper bound is tight,  since there is a doubly-exponential lower bound on the size of winning strategies strategies for $\mathrm{LTL}$ games~\cite{LTL_synthesis_memory}, which can be lifted to $\mathrm{rLTL}$ games.

Similarly, one can compute an adaptive strategy for Player~$1$.
Hence, an adaptive strategy for both players in an $\mathrm{rLTL}$ game can be computed in time $O(n_p^5)$, which is doubly-exponential in the size of the formula.

\begin{theorem}
	Given an $\mathrm{rLTL}$ game, an adaptive strategy of a player can be computed in doubly-exponential time. Moreover, each player has an adaptive strategy with doubly-exponential memory size.
\end{theorem}

Note that adaptive strategies enforce the best possible value from the given prefix.
This value can be obtained at runtime as follows: Given a play prefix~$\mathtt{p}$ ending in some vertex~$v$, let $(q^{0000},\ldots, q^{1111})$ be the state of the automaton implementing the adaptive finite-state strategy computed above is in after the prefix~$\mathtt{p}$.
Note that this state has to be tracked to determine the next move the strategy prescribes at prefix~$\mathtt{p}$ (in case $v \in V_0$).
Then, there is a unique~$b$ such that $(v, q^{0000},\ldots, q^{1111}) \in \enfExact{b}$.
Then, the value currently enforced by the adaptive strategy is $b$, which, by construction, is the maximal one that can be enforced from $\mathtt{p}$.

\section{Combining Adaptive Strategies}

Let us begin by introducing a  useful preliminary result:
in many of the constructions presented below, we need to combine several strategies into a new one while maintaining adaptiveness.
The following lemma will be useful to prove this.

\begin{lemma}\label{lem:follow adaptive is adaptive}
Let $\sigma$ be a strategy for Player~$0$ in $\mathcal{G}'$ such that for all play prefixes~$\mathtt{p}$ and all $(\sigma,\mathtt{p})$-plays~$\rho$, the following are both satisfied:
\begin{itemize}
\item $\rho$ does not contain a bad move of Player~$0$ after the play prefix~$\mathtt{p}$.
\item There is an adaptive strategy~$\sigma_\rho$ such that $\rho$ is a $(\sigma_\rho,\mathtt{p}')$-play for some prefix~$\mathtt{p}'$ of $\rho$.
\end{itemize}
Then, $\sigma$ is adaptive.
\end{lemma}
\begin{proof}
Towards a contradiction, suppose $\sigma$ is a strategy for Player~$0$ in $\mathcal{G}'$ satisfying the given properties, but is not adaptive.
Then, by definition, for some play prefix~$\mathtt{p}$, there exists some strategy $\sigma'$ that enforces some value~$b$ from $\mathtt{p}$, but $\sigma$ does not.
That means there exists a $(\sigma,\mathtt{p})$-play~$\rho$ which has a value strictly less than $b$.
By the given properties, there exists an adaptive strategy $\sigma_\rho$ such that $\rho$ is a $(\sigma_\rho, \mathtt{p}')$-play for some prefix~$\mathtt{p}'$ of $\rho$.
Since both $\mathtt{p}$ and $\mathtt{p}'$ are prefixes of $\rho$, one has to be the prefix of the other.
If $\mathtt{p}'$ is a prefix of $\mathtt{p}$, then $\rho$ is also a $(\sigma_\rho,\mathtt{p})$-play.
As $\sigma_\rho$ is adaptive, it enforces value~$b$ from $\mathtt{p}$, i.e., we have derived a contradiction to $\mathcal{V}(\rho) < b$.

Now, assume that $\mathtt{p}$ is a prefix of $\mathtt{p}'$.
Since $\sigma'$ enforces value $b$ from $\mathtt{p}$ and Player~$0$ does not make a bad move after prefix~$\mathtt{p}$ in the play $\rho$, Player~$0$ can still enforce value~$b$ from $\mathtt{p}'$. Then, by the definition of adaptive strategies, $\sigma_\rho$ enforces the value $b$ from $\mathtt{p}'$ (in particular for the $(\sigma_\rho,\mathtt{p}')$-play~$\rho$), i.e., we have again derived a contradiction to $\mathcal{V}(\rho) < b$.
\end{proof}

\section{Proof of Lemma~\ref{lem:strongly ad if and only if e(p) is summaryMax(v)}}
We use the following properties to simplify the proof.
\begin{remark}
\label{remark:stronglyadaptivestrat}
\hfill
\begin{enumerate}
\item \label{remark:stronglyadaptivestrat:charac} Let $\sigma$ be an adaptive strategy for Player~$0$. Then, $\sigma$ is strongly adaptive if and only if $\stratsummary{\sigma}{\mathtt{p}} = \mathrm{smry}(\mathtt{p})$  for every play prefix $\mathtt{p}$.

\item \label{remark:stronglyadaptivestrat:simplific} Let $\sigma$ be an adaptive strategy for Player~$0$  and $\mathtt{p}$ a play prefix. Then, $\stratsummary{\sigma}{\mathtt{p}} = \mathrm{smry}(\mathtt{p})$ if and only if $\stratsummary{\sigma}{\mathtt{p}} \ge_{\lex} \mathrm{smry}(\mathtt{p})$.

\item \label{remark:stronglyadaptivestrat:optimumrealized} Let $\mathtt{p}$ be a play prefix. Then, there is a strategy $\sigma$ for Player~$0$ such that $\stratsummary{\sigma}{\mathtt{p}} = \mathrm{smry}(\mathtt{p})$.

\end{enumerate}
\end{remark}

Now, let us prove Lemma~\ref{lem:strongly ad if and only if e(p) is summaryMax(v)}. Recall that we need to prove that a strategy $\sigma$ for Player~$0$ in the game $\mathcal{G}'$ is strongly adaptive if and only if for every play prefix~$\mathtt{p}$ ending in vertex~$v$, it holds that $\stratsummary{\sigma}{\mathtt{p}}) = \mathrm{smry}(v)$.

\begin{proof}
By Remark~\ref{remark:stronglyadaptivestrat}.\ref{remark:stronglyadaptivestrat:charac}, a strategy $\sigma$ for Player~$0$ is strongly adaptive if and only if $\stratsummary{\sigma}{\mathtt{p}}= \mathrm{smry}(\mathtt{p})$ for every play prefix~$\mathtt{p}$. Hence, it is enough to show that for any two prefixes $\mathtt{p}_1$ and $\mathtt{p}_2$ ending in the same vertex, it holds that $\mathrm{smry}(\mathtt{p}_1) = \mathrm{smry}(\mathtt{p}_2)$.
The result then follows by picking $\mathtt{p}_1 = \mathtt{p}$ and $\mathtt{p}_2 = v$.

Suppose, towards a contradiction, and without loss of generality, $\mathrm{smry}(\mathtt{p}_1) <_{\lex} \mathrm{smry}(\mathtt{p}_2)$. Let $\sigma_i$ for $i\in \{1,2\}$ be an adaptive strategy that maximizes the summary from $\mathtt{p}_i$ over all strategies. Then, we define the strategy $\sigma'$ for Player~$0$ defined as
\[
\sigma'(\mathtt{p}) = \begin{cases}
 	\sigma_2(\mathtt{p}_2\mathtt{p}') & \text{ if $\mathtt{p} = \mathtt{p}_1\mathtt{p}'$ for some (possibly empty) $\mathtt{p}'$}\\
 	\sigma_1(\mathtt{p}) &\text{ otherwise.}
 \end{cases}
\]
Applying Lemma~\ref{lem:follow adaptive is adaptive} shows that $\sigma'$ is adaptive. Hence, $\stratsummary{\sigma'}{\mathtt{p}_1} = \stratsummary{\sigma_2}{\mathtt{p}_2}$ in the game $\mathcal{G}'$, as $\sigma'$ behaves after the prefix $\mathtt{p}_1$ like $\sigma_2$ does after the prefix~$\mathtt{p}_2$.
Thus, it holds that
\[\stratsummary{\sigma'}{\mathtt{p}_1} = \stratsummary{\sigma_2}{\mathtt{p}_2} = \mathrm{smry}(\mathtt{p}_2) >_{\lex} \mathrm{smry}(\mathtt{p}_1) = \stratsummary{\sigma_1}{\mathtt{p}_1},\] which contradicts the maximality of $\sigma_1$.
\end{proof}

\section{Proof of Lemma~\ref{lem:characterization}}

Recall that we need to prove that in the game $\mathcal{G}'$, for some summary ${s}$ and for some vertex~$v$, we have $v\in \smrExact{{s}}$ if and only if $v \not \in \smrMore{{s}}$ and there is an ${s}$-witness from $v$.

\begin{proof}
Fix some ${s} = (b_0, \ldots, b_k,\blank,\ldots,\blank)\in \mathcal{S}$ throughout the proof.

Suppose a vertex~$v \notin \smrMore{{s}}$ has an ${s}$-witness~$\sigma$.
We show that $v$ is in $\smrExact{{s}}$.

Observe that $v\not \in \smrMore{{s}}$ implies $\mathrm{smry}(v) \le_{\lex} {s}$. Furthermore, since $\sigma$ is enforcing, every $(\sigma,v)$-play containing no bad move of Player~$1$ has value at least $b_0$. Hence, the maximum value Player~$0$ enforces from $v$ is at least $b_0$. Therefore, we obtain
	\begin{equation}\label{eqn:lemChar}
	(b_0,\bot,\bot,\bot,\bot)\leq_{lex} \mathrm{smry}(v) \leq_{lex} {s}.
	\end{equation}
If $ k = 0 $, i.e., ${s} = (b_0, \blank,\ldots,\blank)$ then we are done.

So, suppose $k > 0$.
For every play prefix $\mathtt{p}'$ ending in $v'\in \smrMore{{s}}$, let $\sigma_{\mathtt{p}'}$ be an adaptive strategy such that $\stratsummary{\sigma_{\mathtt{p}'}}{\mathtt{p}'} = \mathrm{smry}(\mathtt{p}') = \mathrm{smry}(v')$ (the second equality follows from Lemma~\ref{lem:strongly ad if and only if e(p) is summaryMax(v)}).
By Remark~\ref{remark:stronglyadaptivestrat}.\ref{remark:stronglyadaptivestrat:optimumrealized}, such a strategy always exists.

We combine these $\sigma_{\mathtt{p}'}$ into a strategy $\sigma_v$ as follows:
for any play prefix~$\mathtt{p}$, $\sigma_v(\mathtt{p}) = \sigma(\mathtt{p})$ if $\mathtt{p}$ does not contain any vertex in $\smrMore{{s}}$.
Otherwise, $\sigma_v(\mathtt{p}) = \sigma_{\mathtt{p}'}(\mathtt{p})$, where $\mathtt{p}'$ is the minimal prefix of $\mathtt{p}$ containing a vertex of $\smrMore{{s}}$, i.e., no strict prefix of $\mathtt{p}'$ contains a vertex in $\smrMore{{s}}$.
Note that the sets $\smrExact{{s}}$ and $\smrMore{{s}}$ are disjoint, so this is well-defined.
We call $\sigma_v$ the continuation of $\sigma$ with $(\sigma_{\mathtt{p}'})_{\mathtt{p}'}$.

Note that $\sigma_v$ does not make a bad move (of Player~$0$) in any $(\sigma_v, v)$-play, as $\sigma$ enforces~$b_0$ (the largest value that can be enforced from $v$ due to $v \notin \smrEMore{{s}}$) and every bad move of Player~$1$ leading to $\sigma_v$ simulating an adaptive strategy, which does not make any bad move either.
Hence, $\sigma_v$ is also adaptive by Lemma~\ref{lem:follow adaptive is adaptive}.

We claim that $\stratsummary{\sigma_v}{v} \ge_{\lex} {s}$. This equality implies $\mathrm{smry}(v) \ge_{\lex} \stratsummary{\sigma_v}{v} \ge_{\lex} {s}$.
Then, we have $\mathrm{smry}(v) = {s}$, as we have already argued $\mathrm{smry}(v) \le_{\lex} {s}$.

So, let us prove $\stratsummary{\sigma_v}{v} \ge_{\lex} {s}$.
To this end, we show that $\playsummary{\sigma_v}{v}{\rho} \ge_{\lex} {s}$ for every $(\sigma_v,v)$-uncovered play~$\rho$.
Fix such a play.

As $k > 0$ and due to $\sigma$ being enabling, there is a $(\sigma_v,v)$-play~$\rho_B$ in which Player~$1$ makes at least one bad move.
Due to Remark~\ref{remark:leftshiftSummary}, we can pick $\rho_B$ such that $\playsummary{\sigma_v}{v}{\rho_B} = {s}$.
Hence, if $\rho$ does not contain any bad moves by Player~$1$ (which implies $\playsummary{\sigma_v}{v}{\rho} = (b_0, \blank,\ldots,\blank)$) then $\rho$ is covered by $\rho_B$.
This contradicts our choice of $\rho$.
Thus, we can assume that $\rho$ contains at least one bad move of Player~$1$.
Now, by definition of $\sigma_v$, the play~$\rho$ is consistent with $\sigma$ up to the first bad move of Player~$1$.

As $\sigma$ is enforcing, any play~$\rho' \in \bmfree{\sigma}{v}$ is winning w.r.t.\ the parity condition of $\mathcal{G}^{b_0}$.
Hence, the value of $\rho'$ is at least $b_0$.
Thus, $\rho'$ never visits the vertex set~$\enfExact{b_0'}$ for some truth value $b_0'< b_0$.
Note that by Equation~(\ref{eqn:lemChar}), $v\in \enfExact{b_0}$ as the maximal value Player~$0$ can enforce is $b_0$. Hence, $\rho$ starts in $\enfExact{b_0}$ and it leaves $\enfExact{b_0}$ only when Player~$1$ makes a bad move, which leads to $\enfEMore{b_0}$.
More precisely, the first bad move of Player~$1$ in $\rho$ is a move from some vertex~$v_p$ in $\mathrm{pre}(\smrExact{{s}^\star})$ for some ${s}^\star \in \mathcal{S}$ such that the first entry of ${s}^\star$ is strictly greater than $b_0$.

As $\sigma$ is evading,  there are two cases: either ${s}^\star \ge_{\lex} \leftshift{{s}}$ or ${s}^\star$ is a strict prefix of $\leftshift{{s}}$.
In the second case, by Remark~\ref{remark:leftshiftSummary}, $\rho$ is covered by the play~$\rho_B$, which again contradicts our choice of $\rho$.
In the first case, after the first bad move, the play reaches a vertex~$v^\star$ in $\smrExact{{s}^\star}$.
Let $\mathtt{p}^\star$ be the prefix of $\rho$ ending in this vertex $v^\star$. Thus, $\rho$ is a $(\sigma_{\mathtt{p}^\star},\mathtt{p}^\star)$-play by construction.
There are two subcases:
either $\rho$ is an $(\sigma_{\mathtt{p}^\star},\mathtt{p}^\star)$-uncovered play and \[\playsummary{\sigma_{\mathtt{p}^\star}}{\mathtt{p}^\star}{\rho}\ge_{\lex} \stratsummary{\sigma_{\mathtt{p}^\star}}{\mathtt{p}^\star} = \mathrm{smry}(v^\star)={s}^\star \ge_{\lex} \leftshift{{s}}\] or
$\rho$ is a $(\sigma_{\mathtt{p}^\star},\mathtt{p}^\star)$-covered play and $\playsummary{\sigma_{\mathtt{p}^\star}}{\mathtt{p}^\star}{\rho}$ is a strict prefix of $\playsummary{\sigma_{\mathtt{p}^\star}}{\mathtt{p}^\star}{\rho'}$ for some $(\sigma_{\mathtt{p}^\star},\mathtt{p}^\star)$-play~$\rho'$.

In the second subcase, due to Remark~\ref{remark:leftshiftSummary}, $\rho$ is also a $(\sigma_v,v)$-covered play such that $\playsummary{\sigma_v}{v}{\rho}$ is a strict prefix of $\playsummary{\sigma_v}{v}{\rho'}$, which again contradicts our choice of $\rho$.
In the first subcase, we obtain $\playsummary{\sigma_v}{v}{\rho} \ge {s}$ by Remark~\ref{remark:leftshiftSummary}, which completes the first direction of the proof.

For the other direction, suppose a vertex~$v$ belongs to $\smrExact{{s}}$.
By definition, $\smrExact{{s}} \cap \smrMore{{s}} = \emptyset$, which implies $v \notin \smrMore{{s}}$.
By Remark~\ref{remark:stronglyadaptivestrat}.\ref{remark:stronglyadaptivestrat:optimumrealized}, there exists a strategy~$\sigma$ such that $\stratsummary{\sigma}{v} = {s}$.

It remains to be shown that there is an ${s}$-witness from $v$.
We actually prove a more general result, which will be useful later on: If for some play prefix~$\mathtt{p}$, there exists a strategy~$\sigma$ such that $\stratsummary{\sigma}{\mathtt{p}} = {s}$, then $\sigma$ is an ${s}$-witness from $\mathtt{p}$, i.e., we show the result for arbitrary play prefixes~$\mathtt{p}$.

So, assume we have a strategy~$\sigma$ such that $\stratsummary{\sigma}{\mathtt{p}}  = {s}$.
Hence, there is an $(\sigma, \mathtt{p})$-uncovered play~$\rho_m$ with $\playsummary{\sigma}{\mathtt{p}}{\rho_m} = {s}$ and $\playsummary{\sigma}{\mathtt{p}}{\rho} \ge_{\lex} {s}$ for every $(\sigma, \mathtt{p})$-uncovered play~$\rho$.
We show that the set~$\bmfree{\sigma}{\mathtt{p}}$ of $(\sigma,\mathtt{p})$-plays without bad moves of Player~$1$ after $\mathtt{p}$ satisfies the three properties of an ${s}$-witness.

The Enforcing property is satisfied by the fact that $\sigma$ enforces the truth value~$b_0$ from $\mathtt{p}$ (as it enforces the first entry of ${s}$ due to $\stratsummary{\sigma}{\mathtt{p}}= {s}$), which implies that the parity condition of $\mathcal{G}^{b_0}$ is satisfied.

Now, assume $k>0$. Then, $\rho_m$ must contain a bad move by Player~$1$.
Note that the prefix~$\mathtt{p}'$ of $\rho_m$ ending at the position before the first bad move ends in $\mathrm{pre}\big( \smrExact{\leftshift{{s}}}\big)$.
So, there is also a play in $\bmfree{\sigma}{\mathtt{p}}$ that visits this set, but does not contain any bad move by Player~$1$, i.e., an extension of $\mathtt{p}'$ where Player~$0$ uses $\sigma$ and Player~$1$ uses an adaptive strategy for her (which does not make any bad moves).
Thus, $\sigma$ satisfies the Enabling property.

To conclude, assume towards a contradiction, that there is a play in $\bmfree{\sigma}{\mathtt{p}}$ that visits $\mathrm{pre}\big(\smrExact{{s}'}\big)$ for some summary ${s}' = (b_0',\ldots, b_{k'}',\blank,\ldots,\blank) \in \evade{{s}}$, i.e., $\sigma$ does not satisfy the Evading property.
Then, there is a play prefix~$\mathtt{p}'$ extending $\mathtt{p}$ and consistent with $\sigma$ that ends in a vertex~$v'$ such that $\mathrm{smry}(\mathtt{p}') = \mathrm{smry}(v') = {s}'$ (recall Lemma~\ref{lem:strongly ad if and only if e(p) is summaryMax(v)}).

Then, $\stratsummary{\sigma}{\mathtt{p}'} \le_{\lex} {s}'$.
Hence, by Remark~\ref{remark:existenceofplaysummary}, there exists a $(\sigma, \mathtt{p}')$-uncovered play~$\rho'$ with $\playsummary{\sigma}{\mathtt{p}'}{\rho'} \le_{\lex} {s}'$.
Note that $\rho'$ is also a $(\sigma, \mathtt{p})$-play, as $\mathtt{p}'$ is a $(\sigma,\mathtt{p})$-play prefix by construction.
Due to Remark~\ref{remark:leftshiftSummary}, $\playsummary{\sigma}{\mathtt{p}}{\rho'} \le_{\lex} (b_0, b_0',\ldots,  b_{k'}',\blank,\ldots,\blank ) <_{\lex} {s}$.
This is a contradiction to $\playsummary{\sigma}{\mathtt{p}}{\rho} \ge_{\lex} {s}$ for every $(\sigma,\mathtt{p})$-uncovered play~$\rho$.
\end{proof}

\section{Proof of Lemma~\ref{lemma:algoforsummary}}
The following remark shows how the maximal summary of a vertex is related to its successor. We use this remark in the next proofs.
\begin{remark}\label{remark:successor}
Let $v \in \smrExact{{s}}$ for ${s} <_{\lex} (1111,\blank,\ldots,\blank)$.
If $v \in V_0'$ then
\begin{itemize}
	\item $v$ has no successor in $\smrMore{{s}'}$.
	\item $v$ has at least one successor in $\smrExact{{s}}$,
\end{itemize}
If $v \in V_1'$ then:
\begin{itemize}
	\item If $v$ has a successor in $\smrExact{{s}'}$ for some ${s}'<_{\lex} {s}$ then ${s}'$ is a strict prefix of~${s}$.
	\item If $v$ has a successor in $\smrExact{{s}'}$ for some ${s}'>_{\lex} {s}$ then neither of ${s}$ and $\leftshift{{s}}$ is a strict prefix of~${s}'$.
	\item If $v$ does not have a successor in $\smrExact{{s}}$, then it has at least one successor in $\smrExact{\leftshift{{s}}}$.
\end{itemize}
\end{remark}

Now, we give the proof for Lemma~\ref{lemma:algoforsummary}. Recall that we need to prove the our algorithm correctly computes the sets~$\smrExact{{s}}$.

\begin{proof}
As argued earlier, the claim is trivially true for the largest summary, as we have $\smrExact{(1111,\blank,\ldots,\blank)} = \enfExact{1111}$.

Assuming we already have computed $\smrExact{{s}'}$ for every ${s}' >_{\lex} {s}$, suppose $U$ is the vertex set computed by the algorithm in that situation.
We claim $U = \smrExact{{s}}$.

First, we show $U\subseteq \smrExact{{s}}$ by showing that each vertex~$v\in U$ satisfies the characterization given in Lemma~\ref{lem:characterization}. Suppose $v$ is a vertex in $U$. Excluding $\smrMore{{s}}$ in Step~\ref{item:algo1:3} ensures that $v\not \in \smrMore{{s}}$, the first part of the characterization.

If $k = 0$, then since $v\in \enfMore{b_0}$, any adaptive strategy $\sigma$ for Player~$0$ enforces $b_0$ from $v$. Hence, $\sigma$ is enforcing.
Thus, $v\in \smrExact{{s}}$, as the other two properties of an ${s}$-witness are trivially satisfied in this case.

If $k > 0$, then by Step~\ref{item:algo1:4}, there is a path $v_0 v_1\cdots v_k$ from $v=v_0$ to some $v_k \in \mathrm{pre}\big(\smrExact{\leftshift{{s}}}\big)$ in the arena restricted to $\win{{{s}}}$.
Let $\sigma({{s}})$ be the winning strategy for Player~$0$ computed in Step~\ref{item:algo1:4} and let $\sigma_0$ be an adaptive strategy for Player~$0$ in the game $\mathcal{G}'$. For $v'\in \smrMore{{s}}$, let $\sigma_{v'}$ be the adaptive strategy that maximizes the summary of $v'$ over all adaptive strategies.  Now consider the strategy $\sigma$ such that
\begin{equation*}
\sigma(\mathtt{p}) =
\begin{cases}
	v_{i+1} &\text{if } \mathtt{p} = v_0v_1\cdots v_i \text{ ending in a Player~$0$ vertex},\\
	\sigma({{s}})(\mathtt{p}) & \text{$\mathtt{p}$ is a play prefix in }\win{{{s}}} \text{ but not a prefix of $v_0 v_1\cdots v_k$},\\
	\sigma_{v'}(v'\mathtt{p}'') &\text{if } \mathtt{p} = \mathtt{p}'v'\mathtt{p}'' \text{ for some play prefix~$\mathtt{p}'$ in }\win{{{s}}},\\
	&\qquad\quad\text{$v'\in \smrMore{{s}}$, and play prefix~$\mathtt{p}''$},\\
	\sigma_0(\mathtt{p}) & \text{otherwise.}
\end{cases}
\end{equation*}
Note that $\sigma$ never makes a bad move and eventually follows an adaptive strategy by construction. Hence, it is also adaptive by Lemma~\ref{lem:follow adaptive is adaptive}.
Let $\rho$ be a  $(\sigma, \mathtt{p})$-play from a play prefix~$\mathtt{p}$ in $\win{{s}}$. If $\rho$ stays in $\win{{{s}}}\subseteq \enfExact{b_0}$, then it eventually follows $\sigma({{s}})$ and has value at least $b_0$. If not, it follows some strategy $\sigma_{v'}$ for some $v'\in \smrMore{{s}}$ which has value at least $b_0$ by construction. Hence, $\sigma$ satisfies the Enforcing property.

Moreover, the exists a $(\sigma,v)$-play~$v_0 v_1\cdots v_k \cdots$ (formed by Player~$0$ using $\sigma$ after $v_0 \cdots v_k$ and Player~$1$ using an adaptive strategy after the prefix) showing that $\sigma$ satisfies the Enabling property.

 Furthermore, by removing $\bigcup_{{s}'\in \evade{{s}}} \reach{\smrExact{{s}'}}$ in Step~\ref{item:algo1:3}, it is also ensured that $\sigma$ satisfies the Evading property. Hence, $\sigma$ is an ${s}$-witness from $v$, which implies $v\in \smrExact{{s}}$.

For the other direction, we show that $\smrExact{{s}} \subseteq U$ by showing that if a vertex~$v$ satisfies the characterization given in Lemma~\ref{lem:characterization}, then $v\in U$.

Note that since $U\subseteq \smrExact{{s}}$, the subgraph $\mathcal{A}_{{s}}$ does not have terminal vertices by Remark~\ref{remark:successor}.
Also, we have $v\not \in \smrMore{{s}}$ by the first item of the characterization. Furthermore, there is an ${s}$-witness~$\sigma$ from $v$.

Hence, by the Enforcing property, $\sigma$ enforces $b_0$ from $v$. Hence, $v\in \enfMore{b_0}$. If $k =0$, then $U = \enfMore{b_0}\setminus \smrMore{{s}}$. Thus, $v\in U$ as required.

Now suppose $k > 0$.
If $v\in \reach{\smrExact{{s}'}}$ for some ${s}'\in \evade{{s}}$, then Player~$1$ has a strategy $\tau$ that forces the token to reach $\smrExact{{s}'}$ from $v$ while only visits vertices in $\enfExact{b_0}$.
Hence, there is a $(\sigma,v)$-play $\rho$ that visits $\mathrm{pre}(\smrExact{{s}'})$ with ${s}'\in \evade{{s}}$.
Hence, there also exists a $(\sigma,v)$-play containing no bad move of Player~$1$ that visiting $\mathrm{pre}(\smrExact{{s}'})$.
This contradicts $\sigma$ being evading. Hence, $v\not \in \bigcup_{{s}'\in \evade{{s}}} \reach{\smrExact{{s}'}}$. Therefore, we obtain $v\in \smrExact{{s}}$.

Now, as $\sigma$ is enabling, there exists a $(\sigma,v)$-play $\rho$ containing no bad move of Player~$1$ that visits $\mathrm{pre}(\smrExact{\leftshift{{s}}})$.
As $\sigma$ is evading, $\rho$ does not visit $\reach{\smrExact{{s}'}}$ for any ${s}'\in \evade{{s}}$.
 Furthermore, by $\sigma$ being enforcing, since $\rho$ does not contain any bad move of Player~$1$, it stays in the vertex set $\win{{{s}}}$. Hence, $\mathrm{pre}(\smrExact{\leftshift{{s}}})$ is reachable from $v$ in the graph restricted to $\win{{{s}}}$. Therefore, $v\in U$.
\end{proof}

\section{Proof of Lemma~\ref{lem:characterizationStronglyad}}

Recall that we need to prove that in the game $\mathcal{G}'$, a strategy~$\sigma$ is strongly adaptive if and only if it is a $\mathrm{smry}(\mathtt{p})$-witness from every play prefix $\mathtt{p}$.

\begin{proof}
First, consider a strategy~$\sigma$ that is a $\mathrm{smry}(\mathtt{p})$-witness from every play prefix $\mathtt{p}$.
Note that $\sigma$ is adaptive by the Enforcing property.
Now we show by induction over summaries~${s} \in \mathcal{S}$, from largest to smallest, that $\stratsummary{\sigma}{\mathtt{p}} \ge_{\lex} {s}$ for every play prefix~$\mathtt{p}$ ending in $\smrExact{{s}}$, which implies that $\sigma$ is strongly adaptive.

So, for the induction start, we have to consider~${s} = (1111,\blank,\ldots,\blank)$, the maximal summary.
So, let $\rho$ be a $(\sigma, \mathtt{p})$-play such that $\mathtt{p}$ ends in $\smrExact{{s}}$.
Note that $\rho$ cannot contain a bad move after the prefix~$\mathtt{p}$, as $1111$ is the maximal truth value, i.e., $\rho \in \bmfree{\sigma}{\mathtt{p}}$.
Hence, $\rho$ satisfies the parity condition of $\mathcal{G}^{1111}$ due to the Enforcing property, i.e., $\rho$ has value~$1111$.
Thus, we have $\stratsummary{\sigma}{\mathtt{p}} = {s}$ as required.

For the induction step, we consider some~${s} <_{\lex} (1111, \blank,\ldots,\blank)$.
The induction hypothesis yields that $\stratsummary{\sigma}{\mathtt{p}} \ge_{\lex} {s}^\star$ for every play prefix~$\mathtt{p}$ ending in $\smrExact{{s}^\star}$ for some ${s}^\star >_{\lex} {s}$.
Hence, we have $\stratsummary{\sigma}{\mathtt{p}'} = \mathrm{smry}(\mathtt{p}') = \mathrm{smry}(v')$ (the last equality follows from Lemma~\ref{lem:strongly ad if and only if e(p) is summaryMax(v)}) for every play prefix $\mathtt{p}'$, where $v'\in \smrMore{{s}}$ is the last vertex of $\mathtt{p}'$.

Now, let $\sigma_{\mathtt{p}'} = \sigma$ for every play prefix~$\mathtt{p}'$ ending in $\smrEMore{{s}}$, and let $\sigma'$ be the continuation of $\sigma$ with $(\sigma_{\mathtt{p}'})_{\mathtt{p}'}$.
Then, we have $\mathrm{smry}(\sigma',\mathtt{p}) \ge_{\lex} {s}$ using the same reasoning as in the proof of Lemma~\ref{lem:characterization} (note that $\sigma$ satisfies exactly the properties required for that reasoning).
The desired result follows by noticing that $\sigma'$ is equal to $\sigma$.

For the other direction, let $\sigma$ be a strongly adaptive strategy.
We need to show that $\sigma$ is a $\mathrm{smry}(\mathtt{p})$ witness from every play prefix~$\mathtt{p}$.

Due to $\sigma$ being strongly adaptive, we have $\stratsummary{\sigma}{\mathtt{p}} = \mathrm{smry}(\mathtt{p})$ for every play prefix~$\mathtt{p}$.
Hence, by the argument presented in the second direction of the proof of Lemma~\ref{lem:characterization}, we conclude that $\sigma$ is indeed a $\mathrm{smry}(\mathtt{p})$-witness from every $\mathtt{p}$.
\end{proof}

\section{Proof Lemma~\ref{lemma:gracioustostronglyad}}
We use the following remarks in the proof.

\begin{remark}\label{remark:qnewWinning}
Any play in $\mathcal{G}_{{s}}$ containing $v_{\mathrm{new}}$ is both $S_{{s}}$ and $W_{{s}}$-winning.
\end{remark}

\begin{remark}
Let ${s}\in \mathcal{S}$ and $v$ be a terminal vertex in the game $\mathcal{G}'$ restricted $\smrExact{{s}}$. Then, $v$ satisfies the following:
\begin{itemize}
\item $v\in V_1'$.
\item $v$ has no successor in $\smrExact{{s}}$.
\item $v$ has a successor in $\smrExact{\leftshift{{s}}}$.
\end{itemize}
\end{remark}

\begin{remark}\label{remark:stratsuccessor}
Suppose $\sigma$ is a strategy of Player~$0$ in $\mathcal{G}'$ that never makes a move from a play prefix ending in $\smrExact{{s}}$ to a vertex in $\smrLess{{s}}$ for some ${s}\in \mathcal{S}$.
Let $\mathtt{p}$ be a play prefix in $\mathcal{G}'$  ending in $\smrExact{{s}}$ and $\rho$ be a $(\sigma,\mathtt{p})$-play in $\mathcal{G}'$.
If $\rho$ visits a vertex $v'\in \smrExact{{s}'}$ after~$\mathtt{p}$ for some ${s}'\in \mathcal{S}$, then one the following holds:
		\begin{itemize}
		\item ${s} = {s}'$.
		\item ${s}'>_{\lex}{s}$ such that ${s}$ is not a strict prefix of ${s}'$.
		\item ${s}'$ is a strict prefix of ${s}$.
		\end{itemize}
Moreover, since there are only finitely many summaries and $\rho$ can not return to the same set $\smrExact{{s}'}$ after leaving the set, it holds that $\rho$ has a suffix staying in $\smrExact{{s}'}$ forever for some ${s}'\in \mathcal{S}$ satisfying one of the above.
\end{remark}

Let us now prove the lemma.
Recall that we need to show that there exists a strongly adaptive strategy in $\mathcal{G}'$ if and only if there exists a uniformly gracious strategy in every obliging game $\mathcal{G}_{{s}}$.
Moreover, given a uniformly gracious strategy with finite memory in each obliging game $\mathcal{G}_{{s}}$, one can effectively combine these into a strongly adaptive strategy with finite memory in $\mathcal{G}'$.

\begin{proof}
First, assume there exists a strongly adaptive strategy $\sigma$ in the game~$\mathcal{G}'$. Let ${s} = (b_0,\ldots,b_k,\blank,\ldots,\blank)\in \mathcal{S}$. We show that $\sigma$ is a uniformly gracious strategy in the obliging game~$\mathcal{G}_{{s}}$.

Let $\rho$ be a $(\sigma,\mathtt{p})$-play in $\mathcal{G}_{{s}}$ for some play prefix $\mathtt{p}$ ending in $\smrExact{{s}}$.
We show that $\rho$ satisfies the strong winning condition and that there is a $(\sigma,\mathtt{p})$-play~$\rho'$ that satisfies the weak condition.
This implies that $\sigma$ is uniformly gracious.

If $\rho$ contains~$v_{\mathrm{new}}$, then it is both $S_{{s}}$ and $W_{{s}}$-winning by Remark~\ref{remark:qnewWinning}, i.e., we can use $\rho' = \rho$ to finish the argument.

So, now suppose $\rho$ does not contain the vertex $v_{\mathrm{new}}$. Then, $\rho$ is also a $(\sigma,\mathtt{p})$-play in the game $\mathcal{G}'$.  Since $\sigma$ is enforcing, $\rho$ satisfies the parity condition of $\mathcal{G}^{b_0}$, which implies it also $S_{{s}}$-winning.
If $k = 0$, then the weak condition is satisfied by every play, i.e., we  can again use $\rho' = \rho $ to finish the argument.

Otherwise, i.e., if $k > 0$, by the Enabling property, there exists a $(\sigma,\mathtt{p})$-play~$\rho'$ in $\mathcal{G}'$ that visits $\mathrm{pre}(\leftshift{{s}})$. Let $\mathtt{p}'$ be the minimal prefix of $\rho$ containing a vertex in  $\mathrm{pre}(\leftshift{{s}})$ after $\mathtt{p}$. We claim that all vertices between $\mathtt{p}$ to $\mathtt{p}'$ are in $\smrExact{{s}}$. This implies that $\mathtt{p}'$ is also a $(\sigma,\mathtt{p})$-play prefix in $\mathcal{G}_{{s}}$.
Then, by iterating this argument ad infinitum, we obtain a $(\sigma,\mathtt{p})$-play in $\mathcal{G}_{{s}}$ that visits $\mathrm{pre}(\leftshift{{s}})$ infinitely often. This play satisfies the weak condition.

Now, we only need to prove that all vertices between $\mathtt{p}$ to $\mathtt{p}'$ are in $\smrExact{{s}}$. Let $v$ be a vertex in $\mathtt{p}'$ after $\mathtt{p}$. First, note that a strongly adaptive strategy does not make a move from a play prefix $\mathtt{p}_1$ ending in $\smrExact{{s}_1}$ to a vertex $v_1$ in $\smrLess{{s}_1}$.
If it would then every $(\sigma,\mathtt{p}_1)$-uncovered play is also a $(\sigma,\mathtt{p}_1 v_1)$-uncovered play and vice versa.
This implies that $\stratsummary{\sigma}{\mathtt{p}_1}$ and $\stratsummary{\sigma}{\mathtt{p}_1 v_1}$ are equal, as they are obtained by minimizing over the same set of plays.
This contradicts the assumption that $v_1\in \smrLess{{s}}$. Hence, by Remark~\ref{remark:stratsuccessor}, $v\in \smrExact{{s}'}$ for some ${s}'\in \mathcal{S}$ such that ${s}'\ge_{\lex} {s}$ or ${s}'$ is a strict prefix of ${s}$.

Due to Remark~\ref{remark:existenceofplaysummary}, $\mathtt{p}'$ can be extended to a $(\sigma,\mathtt{p})$-uncovered play $\rho^\star$ satisfying $\playsummary{\sigma}{\mathtt{p}}{\rho^\star} = {s}$.  Since Player~$1$ makes $k > 0$ bad moves after $\mathtt{p}'$ in $\rho^\star$ (as $\mathtt{p}'$ is the minimal extension of $\mathtt{p}$ visiting a vertex where Player~$1$ can make a bad move), we also have $\playsummary{\sigma}{\mathtt{p}_v}{\rho^\star} = {s}$ for the prefix $\mathtt{p}_v$ of $\mathtt{p}'$ ending in $v$.
Recall that either ${s}'\ge_{\lex} {s}$ or ${s}'$ is a strict prefix of ${s}$. We show that both ${s}'>_{\lex} {s}$ and ${s}'$ being a strict prefix of ${s}$ lead to a contradiction, leaving us only with the conclusion  ${s}' = {s}$ as required.

First, assume we have ${s}'>_{\lex} {s}$.
Since $\stratsummary{\sigma}{\mathtt{p}_v} = {s}'$, every $(\sigma, \mathtt{p}_v)$-uncovered play~$\rho''$ satisfies $\playsummary{\sigma}{\mathtt{p}_v}{\rho''} \ge_{\lex} {s}'$. But the $(\sigma, \mathtt{p}_v)$-play $\rho^\star$ has summary~${s} <_{\lex} {s}'$.
We show that $\rho^\star$ is $(\sigma, \mathtt{p}_v)$-uncovered, which yields the desired contradiction.
If $\rho^\star$ is $(\sigma,\mathtt{p}_v)$-covered by another $(\sigma,\mathtt{p}_v)$-play $\rho''$, then $\rho^\star$ is also $(\sigma,\mathtt{p})$-covered by $\rho''$, which contradicts the assumption that $\rho^\star$ is $(\sigma, \mathtt{p})$-uncovered.

Finally, assume ${s}'$ is a strict prefix of ${s}$. By definition, $\stratsummary{\sigma}{\mathtt{p}_v} = {s}'$ implies that there is some $(\sigma, \mathtt{p}_v)$-uncovered play~$\rho''$ with $\playsummary{\sigma}{\mathtt{p}_v}{\rho''} =  {s}'$. However, $\rho^\star$ is also a $(\sigma, \mathtt{p}_v)$-play and it covers $\rho''$, as ${s}'$, the summary of $\rho''$, is a strict prefix of ${s}$, the  summary of $\rho^\star$.

For the other direction, assume there is a uniformly gracious strategy~$\sigma_{{s}}$ for every game $\mathcal{G}_{{s}}$.
Let $\sigma$ be the strategy obtained by combining all strategies~$\sigma_{{s}}$ as follows: for any play prefix~$\mathtt{p}$ ending in $\smrExact{{s}}$, we have $\sigma(\mathtt{p}) = \sigma_{{s}}(\mathtt{p}')$, where $\mathtt{p}'$ is the longest suffix of $\mathtt{p}$ which is a $\sigma_{{s}}$-play in $\mathcal{G}_{{s}}$.
It remains to show that, for every play prefix~$\mathtt{p}$ ending in $\smrExact{{s}}$ for some ${s} = (b_0,\ldots,b_k,\blank,\ldots,\blank) \in \mathcal{S}$, $\sigma$ is an ${s}$-witness from $\mathtt{p}$. This implies that $\sigma$ is strongly adaptive by Lemma~\ref{lem:characterizationStronglyad}.

First, we show that $\sigma$ satisfies the Enabling property.
If $k = 0$ then the property is satisfied trivially.
If not, then let $\mathtt{p}'$ be the longest suffix of $\mathtt{p}$ which is a $\sigma_{{s}}$-play in $\mathcal{G}_{{s}}$.
Then, every $(\sigma,\mathtt{p})$-play that stays in $\smrExact{{s}}$ follows $\sigma_{{s}}$, i.e., it has a suffix that is a $(\sigma_{{s}},\mathtt{p}')$-play.
Since, $\sigma_{{s}}$ is uniformly gracious, there exists a  $(\sigma_{{s}},\mathtt{p}')$-play $\rho^\star$ in $\mathcal{G}_{{s}}$ that is $W_{{s}}$-winning, i.e., $\rho^\star$ visits $\mathrm{pre}(\leftshift{{s}})\cup \{v_{\mathrm{new}}\}$ infinitely often.
Note that by Remark~\ref{remark:qnewWinning}, every predecessor of $v_{\mathrm{new}}$ also belongs to $\mathrm{pre}(\leftshift{{s}})$.
Hence, $\rho^\star$ visits $\mathrm{pre}(\leftshift{{s}})$ at least once.
Let $\mathtt{p}'\mathtt{p}^\star$ be a prefix of $\rho^\star$ ending in $\mathrm{pre}(\leftshift{{s}})$.
Then, there exists a $(\sigma,\mathtt{p}\p^\star)$-play which is also a $(\sigma,\mathtt{p})$-play satisfying the Enabling property, i.e., one in which Player~$1$ does not make a bad move.

Now, given a play $\rho\in \bmfree{\sigma}{\mathtt{p}}$ containing no bad move of Player~$1$ after $\mathtt{p}$, we show that $\rho$ satisfies the Enforcing and the Evading property.

Note that by construction, $\sigma$ never makes a move from a play prefix ending in $\smrExact{{s}}$ to a vertex in $\smrLess{{s}}$. Hence, by Remark~\ref{remark:stratsuccessor}, $\rho$ has a suffix that stays in $\smrExact{{s}'}$ forever for some ${s}' = (b_0',\ldots,b_{k'}',\blank,\ldots,\blank)\in \mathcal{S}$ such that ${s}'\ge_{\lex}{s}$ or ${s}'$ is a strict prefix of ${s}$. In any case, $b_0'\geq b_0$. Furthermore, $\rho$ has a suffix that is a $\sigma_{{s}'}$-play which is $S_{{s}'}$-winning. Hence, it has value at least $b_0'$. Therefore, $\rho$ satisfies the Enforcing property.

Now, suppose $\rho$ does not satisfy the Evading property and visits some vertex $v\in \mathrm{pre}(\smrExact{{s}^\star})$ for some ${s}^\star=(b_0^\star,\ldots,b_{k^\star}^\star,\blank,\ldots,\blank)\in \evade{{s}}$.
Suppose $v\in \smrExact{{s}'}$ for ${s}' = (b_0',\ldots,b_{k'}',\blank,\ldots,\blank)\in \mathcal{S}$.
We claim that ${s}^\star \in \evade{{s}'}$.

Step~\ref{item:algo1:3} of the algorithm to compute $\smrExact{{s}}$ and its proof of correctness imply that $\reach{V_{{s}^\star}}$ and $V_{{s}'}$ are disjoint.
Hence, the facts that $v$ is a vertex of Player~$1$ (since there exists a bad move from $v$ to $\smrExact{{s}^\star}$) and $v \in \mathrm{pre}(\smrExact{{s}^\star})$, which implies $v \in \reach{\smrExact{{s}^\star}}$, yield the desired contradiction.

Now, we only need to prove ${s}^\star \in \evade{{s}'}$ to conclude the proof. First, note that since $\rho$ does not contain a bad move of Player~$1$ after $\mathtt{p}$, we have $b_0' = b_0$, which implies $b_0^\star>b_0'$. To prove the other two conditions, we consider two cases derived as follows: By Remark~\ref{remark:stratsuccessor}, it holds that ${s}'\ge_{\lex}{s}$ or ${s}'$ is a strict prefix of ${s}$.

If ${s}'\ge_{\lex}{s}$, then ${s}^\star <_{\lex} \leftshift{{s}} \le_{\lex} \leftshift{{s}'}$ (as $b_0 = b_0'$). Furthermore, if ${s}^\star$ is a strict prefix of $\leftshift{{s}'}\ge_{\lex}\leftshift{{s}}$, then either ${s}^\star \ge_{\lex} \leftshift{{s}}$ or ${s}^\star$ is a strict prefix of $\leftshift{{s}}$. This contradicts the fact that ${s}^\star <_{\lex} \leftshift{{s}}$ and ${s}^\star$ not being a strict prefix of $\leftshift{{s}}$.

If ${s}'$ is a strict prefix of ${s}$, then ${s}^\star$ is not a strict prefix of ${s}'$ (as it is not a strict prefix of ${s}$). Furthermore, since ${s}^\star <_{\lex} \leftshift{{s}}$, either ${s}^\star <_{\lex} \leftshift{{s}'}$ or $\leftshift{{s}'}$ is a strict prefix of ${s}^\star$.
The second case never holds by Remark~\ref{remark:successor}.
Therefore, the claim is proved.
\end{proof}

\section{Conclusion}

We argued that in a reactive system, in addition to correctness, we also need to ensure robustness.
To this end, we introduced adaptive strategies for $\mathrm{rLTL}$ games that satisfy the specification to a higher degree when the environment is not antagonistic. We also presented a stronger version of adaptive strategies that additionally maximizes the opportunities for the opponent to make bad choices. Finally, we showed that both adaptive and strongly adaptive strategies can be computed in doubly-exponential time. As we know that the classical $\mathrm{LTL}$ and $\mathrm{rLTL}$ synthesis algorithms also take doubly-exponential time, we conclude that adaptive and strongly adaptive strategies are not harder to compute.

\section{Introduction}
\label{section1}

Formal methods have focused on the paradigm of correctness-by-construction, i.e., ensuring that systems are guaranteed to meet their design specifications.
While correctness is necessary, it has widely been acknowledged that this property alone is insufficient for a good design when a reactive system interacts with an ever-changing, uncontrolled environment.
To illustrate this point, consider a typical correctness specification $\varphi \Rightarrow \psi$ of a reactive system, where $\varphi$ is an environment assumption and $\psi$ the system's desired guarantee.
Thus, if the environment violates $\varphi$, the entire implication becomes vacuously true, regardless of whether the system satisfies $\psi$.
In other words, if the assumption about the environment is violated, the system may behave arbitrarily.
This behavior is clearly undesirable as modeling any reasonably complex environment accurately and exhaustively is exceptionally challenging, if not impossible.

The example above shows that reactive systems must not only be correct but should also be \emph{robust} to unexpected environment behavior.
The notion of robustness we use in this paper is inspired by concepts from control theory~\cite{DBLP:journals/tecs/MajumdarRT13,DBLP:conf/hybrid/SamuelMSN20,DBLP:conf/cdc/SamuelMSN20,DBLP:journals/tac/TabuadaCRM14} and requires that deviations from the environment assumptions result in at most proportional violations of the system guarantee.
More precisely, ``minor'' violations of the environment assumption should only cause ``minor'' violations of the system guarantee, while ``major'' violations of the environment assumption allow for ``major`` violations of the system guarantee.

To capture different degrees of violation (or satisfaction) of a specification, we rely on a many-valued extension of Linear Temporal Logic~(LTL)~\cite{LTL}, named \emph{robust Linear Temporal Logic~(rLTL)}, which has recently been introduced by Tabuada and Neider~\cite{DBLP:conf/csl/TabuadaN16}.
The basic idea of this logic can best be illustrated by considering the prototypical environment assumption $\varphi \coloneqq \Box p$ (``always~$p$''), which demands that the environment ensures that an atomic proposition~$p$ holds at every step during its interaction with the system.
Clearly, $\varphi$ is violated even if $p$ does not hold at a single step, which is a ``minor'' violation. However, the classical Boolean semantics of LTL cannot distinguish between this case and the case where $p$ does not hold at any position, which is a ``major'' violation.
To distinguish these (and more) degrees of violations, $\mathrm{rLTL}$ adopts a five-valued semantics with truth values $\mathbb B_4 = \{ 1111, 0111, 0011, 0001, 0000\}$. The set~$\mathbb B_4$ is ordered according to $1111 > 0111 > 0011 > 0001 > 0000$, where $1111 $ is interpreted as $\mathit{true}$ and all other values as increasing shades of $\mathit{false}$.
In case of the formula $\varphi$, for instance, the interpretation of these five truth values is as follows: $\varphi$ evaluates to $1111$ if the environment ensures $p$ at every step of the interaction, $\varphi$ evaluates to $0111$ if $p$ holds almost always, $\varphi$ evaluates to $0011$ if $p$ holds infinitely often, $\varphi$ evaluates to $0001$ if $p$ holds at least once, and $\varphi$ evaluates to $0000$ if $p$ never holds.
The semantics of $\mathrm{rLTL}$ is then set up so that $\varphi \Rightarrow \psi$ evaluates to $1111$ if any violation of the environment assumption $\varphi$ causes at most a proportional violation of the system guarantee $\psi$ (i.e., if $\varphi$ evaluates to truth value $b \in \mathbb B_4$, then $\psi$ must evaluate to a truth value $b' \geq b$).

Here, we are interested in the synthesis problem for $\mathrm{rLTL}$ specifications. As usual, we model such a synthesis problem as an infinite-duration two-player game.
Since we study $\mathrm{rLTL}$ synthesis, we consider games with $\mathrm{rLTL}$ winning conditions, so-called $\mathrm{rLTL}$ games.

$\mathrm{rLTL}$ games with a Boolean notion of winning strategy for the system player have already been studied by Tabuada and Neider~\cite{DBLP:conf/csl/TabuadaN16}. In their setting, the objective for the system player is as follows: given a truth value $b \in \mathbb B_4$, he must react to the actions of the environment player in such a way that the specification is satisfied with a value of at least $b$.
As for $\omega$-regular games, a winning strategy for the system player can immediately be implemented in hardware or software.
This implementation then results in a reactive system that is guaranteed to satisfy the given specification with at least a given truth value $b \in \mathbb B_4$, regardless of how the environment acts.

While $\mathrm{rLTL}$ games provide an elegant approach to robustness-by-construction synthesis, the Boolean notion of winning strategies that Tabuada and Neider adopt has a substantial drawback: it does not incentivize the system player to satisfy the specification with a value better than $b$, even if the environment player allows this.
Of course, one can (and should) statically search for the largest $b \in \mathbb B_4$ such that the system player can win the game.
However, this traditional worst-case view does not account for many practical situations where the environment is not antagonistic, e.g., in the presence of intermittent disturbances or noise, or when the environment cannot be modeled entirely~\cite{DBLP:conf/cdc/DallalNT16,DBLP:conf/hybrid/EhlersT14,DBLP:conf/mfcs/NeiderT020,DBLP:conf/csl/NeiderW018,DBLP:conf/hybrid/TopcuOLM12}.
In such situations, the system player should exploit the environment's ``bad'' moves, i.e., actions that permit the system player to achieve a value greater than $b$, and adapt its strategy at runtime.

We present two novel synthesis algorithms for $\mathrm{rLTL}$ specifications that ensure that the resulting systems are \emph{robust by construction} (in addition to being correct by construction).
These are based on two refined non-Boolean notions of strategies for $\mathrm{rLTL}$ games which both optimize the satisfaction of the specification.

The first notion, named \emph{adaptive strategies}, uses automata-based runtime verification techniques~\cite{runtime_verif} to monitor plays, detect bad moves of the environment, and adapt the actions of the system player to optimize the satisfaction of the winning condition.
The second notion, named \emph{strongly adaptive strategies}, is an extension of the first one that, in addition to being adaptive, also seeks to maximize the opportunity for the environment player to make bad moves.
We show that both types of strategies can be computed using methods from automata theory and result in effective synthesis algorithms for reactive systems that are robust by construction and adapt to the environment at runtime.

After recapitulating $\mathrm{rLTL}$ in Section~\ref{section2}, we introduce adaptive strategies in Section~\ref{adaptive strategy} and show that one can compute such strategies in $\mathrm{rLTL}$ games in doubly-exponential time by reducing the problem to solving parity games~\cite{calude}.
In Section~\ref{sec:strongly-adaptive}, we then turn to strongly adaptive strategies.
It turns out that this type of strategy does not always exist, which we demonstrate through an example.
Nevertheless, we give a doubly-exponential time algorithm that decides whether a strongly adaptive strategy exists, and, if this is the case, computes one. Our algorithm is based on reductions to a series of parity and obliging games~\cite{Obliging}.
As the $\mathrm{LTL}$ synthesis problem is 2EXPTIME-complete~\cite{LTL_synthesis}, which is a special case of the problems we consider here, computing both types of adaptive strategies is 2EXPTIME-complete as well.
Furthermore, the size of the (strongly) adaptive strategies our algorithms compute is at most doubly exponential, matching the corresponding lower bound for $\mathrm{LTL}$ games, demonstrating that this bound is tight.
Thus, our results show that adaptive robust-by-construction synthesis is asymptotically not harder than classical $\mathrm{LTL}$ synthesis.

All proofs omitted due to space restrictions can be found in the appendix.

\section{Preliminaries}\label{section2}
In this section, we describe the syntax and semantics of Robust $\mathrm{LTL}$ and how it is different from classical $\mathrm{LTL}$. Moreover, we discuss some important results on $\mathrm{rLTL}$ and introduce games with $\mathrm{rLTL}$ specifications.

\paragraph{Robust Linear Temporal Logic.}
We assume that the reader is familiar with Linear Temporal Logic~\cite{LTL}. We fix a finite non-empty set $\mathcal{P}$ of atomic propositions. The syntax of $\mathrm{rLTL}$ is similar to that of $\mathrm{LTL}$ with the only difference being the use of dotted temporal operators in order to distinguish them from $\mathrm{LTL}$ operators. More precisely, $\mathrm{rLTL}$ formulas are inductively defined as follows:

\begin{itemize}
	\item each $p\in \mathcal{P}$ is an $\mathrm{rLTL}$ formula, and
	\item if $\varphi$ and $\psi$ are $\mathrm{rLTL}$ formulas, so are $\neg \varphi$, $\varphi \vee \psi$, $\varphi \wedge \psi$, $\varphi \Rightarrow \psi$, $\Xdot \varphi$ (``next''), $\Boxdot \varphi$ (``always''), $\Diamonddot \varphi$ (``eventually''), $\varphi\Rdot \psi$ (``release'') and $\varphi\Udot \psi$ (``until'').
\end{itemize}

As already discussed, $\mathrm{rLTL}$ uses the set~$\mathbb{B}_4 = \{1111,0111,0011,0001,0000\}$ of truth values, which are ordered as follows:
\[1111>0111>0011>0001>0000.\]
Intuitively, $1111$ corresponds to ``true'', and the other four values correspond to different degrees of ``false''.

The $\mathrm{rLTL}$ semantics is a mapping $\mathcal{V}$, called \emph{valuation}, that maps an infinite word $\alpha \in (2^{\mathcal{P}})^{\omega}$ and an $\mathrm{rLTL}$ formula $\varphi$ to an element of $\mathbb{B}_4$.
Before we define the semantics, we need to introduce some useful notation.
Let $\alpha = \alpha_0\alpha_1\cdots \in (2^{\mathcal{P}})^{\omega}$ be an infinite word. For $i\in \mathbb{N}$, let $\alpha_{i\ldots} = \alpha_i\alpha_{i+1}\cdots$ be the (infinite) suffix of $\alpha$ starting at position~$i$. Also, for $1\leq k \leq 4$, we let $V_k(\alpha, \varphi)$ denote the $k$-th entry of  $\mathcal{V}(\alpha, \varphi)$, i.e., $\mathcal{V}(\alpha, \varphi) = V_1(\alpha, \varphi) V_2(\alpha, \varphi) V_3(\alpha, \varphi) V_4(\alpha, \varphi)$.
Now, $V$ is defined inductively as follows, where the semantics of Boolean connectives relies on \textit{da Costa algebras}~\cite{da_costa}:
\begin{align*}
	\mathcal{V}(\alpha, p) & = \begin{cases} 0000 & \text{if $p\not \in \alpha_0$} \\ 1111 & \text{if $p \in \alpha_0$} \end{cases} &
	%
	\mathcal{V}(\alpha, \lnot \varphi) & = \begin{cases} 0000 & \text{if $\mathcal{V}(\alpha, \varphi) = 1111$} \\ 1111 & \text{otherwise} \end{cases} \\

	\mathcal{V}(\alpha, \varphi \lor \psi) & = \max{\bigl\{ \mathcal{V}(\alpha, \varphi), \mathcal{V}(\alpha, \psi) \bigr\}} &
	\mathcal{V}(\alpha, \varphi \Rightarrow \psi) & = \begin{cases} 1111 & \text{if $\mathcal{V}(\alpha, \varphi)\leq \mathcal{V}(\alpha, \psi)$} \\ \mathcal{V}(\alpha, \psi) & \text{otherwise} \end{cases} \\

	\mathcal{V}(\alpha, \varphi \land \psi) & = \min{\bigl\{ \mathcal{V}(\alpha, \varphi), \mathcal{V}(\alpha, \psi)\bigr\}} &
	%
	\mathcal{V}(\alpha,\Xdot \varphi) & = \mathcal{V}(\alpha_{1\ldots}, \varphi) \\

	\mathcal{V}(\alpha,\Boxdot \varphi) & = \parbox{0pt}{$\displaystyle \left(\inf_{i\geq 0} V_1(\alpha_{i\ldots}, \varphi), \adjustlimits \sup_{j\geq 0} \inf_{i\geq j} V_2(\alpha_{i\ldots}, \varphi), \adjustlimits \inf_{j\geq 0} \sup_{i\geq j} V_3(\alpha_{i\ldots}, \varphi), \sup_{i\geq 0} V_4(\alpha_{i\ldots}, \varphi)\right)$} \\

	\mathcal{V}(\alpha,\Diamonddot \varphi) & = \parbox{0pt}{$\displaystyle \left(\sup_{i\geq 0} V_1(\alpha_{i\ldots}, \varphi), \sup_{i\geq 0} V_2(\alpha_{i\ldots}, \varphi), \sup_{i\geq 0} V_3(\alpha_{i\ldots}, \varphi), \sup_{i\geq 0} V_4(\alpha_{i\ldots}, \varphi)\right)$}
\end{align*}
The semantics for the temporal operators $\Udot$ and $\Rdot$ can be generalized similarly.
We refer the reader to Tabuada and Neider~\cite{DBLP:conf/csl/TabuadaN16} for more details.

\begin{example}
We can see that for the formula $\Boxdot p$, the valuation $\mathcal{V}(\alpha,\Boxdot p)$ can be expressed in terms of the $\mathrm{LTL}$ valuation function~$W$ by
\[\mathcal{V}(\alpha,\Boxdot p) = W(\alpha,\Box p) W(\alpha, \Diamond \Box p) W(\alpha,\Box \Diamond p) W(\alpha,\Diamond p).\]
This evaluates to different values in $\mathbb{B}_4$ distinguishing various degrees of violations as seen in Section~\ref{section1}.
\end{example}

\begin{example}
Now let us see how the $\mathrm{rLTL}$ semantics for a specification of the form $\varphi\Rightarrow\psi$ captures robustness. Consider an instance where the environment assumption $\varphi$ is $\Boxdot p$ and the system guarantee $\psi$ is $\Boxdot q$ and assume the specification $\Boxdot p \Rightarrow \Boxdot q$ evaluates to $1111$ for some infinite word. Let us see how the system behaves in response to various degrees of violation of the environment assumption.
\begin{itemize}
	\item If $p$ holds at all positions, then $\Boxdot p$ evaluates to $1111$. Hence, by the semantics of implication, $\Boxdot q$ also evaluates to $1111$, which means $q$ holds at all positions. Therefore, the desired behavior of the system is retained when the environment assumption holds with no violation.

	\item If $p$ holds eventually always but not always (a minor violation of $\Boxdot p$), then $\Boxdot p$ evaluates to $0111$. Hence, $\Boxdot q$ evaluates to $0111$ or higher, meaning that $q$ also needs to hold eventually always.

	\item Similarly, if $p$ holds at infinitely (finitely) many positions, then $q$ needs to hold at infinitely (finitely) many positions.
\end{itemize}
Hence, the semantics of $\Boxdot p \Rightarrow \Boxdot q$ captures the robustness property as desired. Furthermore, if $\Boxdot p \Rightarrow \Boxdot q$ evaluates to $b<1111$, then $\Boxdot p$ evaluates to a higher value than $b$, whereas $\Boxdot q$ evaluates to $b$. So, the desired system guarantee is not satisfied. However, the value of $\Boxdot p \Rightarrow \Boxdot q$ still describes which weakened guarantee follows from the environment assumption.

\end{example}

\paragraph{From rLTL to B\"uchi Automata.}
Given an $\mathrm{LTL}$ formula $\varphi$, a generalized B\"uchi automaton (see \cite{Buchi-Parity} for a definition) with $O(2^{\lvert\varphi\rvert})$ states and $O(\lvert\varphi\rvert)$ accepting sets can be constructed that recognizes the infinite words satisfying $\varphi$~\cite{LTL_Buchi}. Using a similar method, Tabuada and Neider obtained the following result.

\begin{theorem}[\cite{DBLP:conf/csl/TabuadaN16}]\label{thm:rLTL-Buchi}
	Given an $\mathrm{rLTL}$ formula $\varphi$ and a set of truth values $B\subseteq \mathbb{B}_4$, one can construct a generalized B\"uchi automaton $\mathcal{A}$ with $2^{O(\lvert\varphi\rvert)}$ states and $O(\lvert\varphi\rvert)$ accepting sets that recognizes the infinite words on which the value of $\varphi$ belongs to $B$, i.e., $L(\mathcal{A}) = \{w\in (2^{\mathcal{P}})^{\omega}\mid \mathcal{V}(\alpha,\varphi) \in B\}$.
\end{theorem}

\paragraph{rLTL Games.}

\label{section3}

We consider infinite-duration two-player games over finite graphs with $\mathrm{rLTL}$ specifications. Here, we assume basic familiarity with games on graphs.
Formally, an $\mathrm{rLTL}$ game $\mathcal{G} = (\mathcal{A}, \varphi)$ consists of
	\begin{enumerate*}[label=(\roman*)]
		\item a finite, directed, labelled arena $\mathcal{A} = (V,E,\lambda)$ with $V = V_0 \mathbin{\mathaccent\cdot\cup} V_1$, an edge relation~$E \subseteq V \times V$, and a labelling function $\lambda \colon V \rightarrow 2^{\mathcal{P}}$, and
		\item an $\mathrm{rLTL}$ formula $\varphi$ over $\mathcal{P}$.
	\end{enumerate*}
The game is played by two players, Player~$0$ and Player~$1$, who construct a \textit{play} $\rho = v_0v_1\cdots \in V^\omega$ by moving a token along the edges of the arena. A~play $\rho = v_0v_1\cdots $ induces an infinite word $\lambda(\rho) = \lambda(v_0)\lambda(v_1)\cdots \in (2^{\mathcal{P}})^{\omega}$, and the \textit{value} of the play, denoted by $\mathcal{V}(\rho)$, is the value of the formula $\varphi$ on $\lambda(\rho)$. Player~$0$'s objective is to maximize this value, while Player~$1$'s objective is to minimize it.

\paragraph*{Strategies.}
A \textit{play prefix} is a finite, nonempty path $\mathtt{p}\in V^*$ in the arena.
Then, a \textit{strategy} for Player~$i$, $i\in \{0,1\}$, is a function $\sigma\colon V^*V_i \rightarrow V$ mapping each play prefix~$\mathtt{p}$ ending in a vertex in $V_i$ to one of its successors.
Intuitively, a strategy prescribes Player~$i$'s next move depending on the play prefix constructed so far.

A strategy $\sigma$ is \textit{memoryless} if it only depends on the last vertex, i.e., for any prefix~$\mathtt{p}$ ending in vertex~$v$, it holds that $\sigma(\mathtt{p}) = \sigma(v)$. Moreover, we say a strategy has \textit{memory size} $m$ if there exists a finite state machine with output with $m$ states computing the strategy (see Grädel et al.~\cite{Automata_Book} for more details).

Next we define the plays that are consistent with a given strategy for Player~$i$.
Typically, this means that the token is placed at some initial vertex and then, whenever a vertex of Player~$i$ is reached, then Player~$i$ uses the move prescribed by the strategy for the current play prefix to extend this prefix.
Note that the strategy does not have control over the initial placement of the token.

Here we will use a more general notion, inspired by previous work in optimal strategies for Muller games~\cite{FJ}: the initial prefix over which the strategy does not have control over might be longer than just the initial vertex.
This means strategies are also applicable to prefixes that where not constructed according to the strategy.
However, crucially, the strategy still gets access to that prefix and therefore can base its decisions on the prefix it had no control over.
This generality will turn out to be useful both when defining adaptive strategies and when combining strategies to obtain adaptive strategies.

Formally, for a play prefix~$\mathtt{p}=v_0v_1\cdots v_n$ and a strategy $\sigma$ for Player~$i$, a play~$\rho$ is a $(\sigma, \mathtt{p})$-play if $\rho =\mathtt{p} v_{n+1}v_{n+2}\cdots$ with $v_{k+1} = \sigma(v_0v_1\cdots v_k)$ for all $v_k\in V_i$ with $k\geq n$. Note that the prefix~$\mathtt{p}$ is arbitrary here, i.e., it might not have been constructed following the strategy~$\sigma$.
Moreover, a $(\sigma,\mathtt{p})$-play prefix $\mathtt{p}\p'$ is a prefix of a $(\sigma,\mathtt{p})$-play.
We say that a play~$\rho$ starting in some vertex~$v$ is consistent with $\sigma$, if it is a $(\sigma, v)$-play (which is the classical notion of consistency).
Finally, a play prefix~$\mathtt{p}$ is consistent with $\sigma$ if it is the prefix of some play that is consistent with $\sigma$.

In the paper introducing $\mathrm{rLTL}$~\cite{DBLP:conf/csl/TabuadaN16}, Tabuada and Neider gave a doubly-exponential time algorithm that solves the classical $\mathrm{rLTL}$ synthesis problem, which is equivalent to solving the following problem.
\begin{problem}
	Given an $\mathrm{rLTL}$ game $\mathcal{G}$, an initial vertex~$v_0$ and a truth value~$b\in \mathbb{B}_4$, compute a strategy $\sigma$ (if one exists at all) for Player~$0$ such that every $(\sigma,v_0)$-play has value at least $b$.
\end{problem}

Note that Tabuada and Neider were interested in strategies for Player~$0$ that enforce the value~$b$ from $v_0$, i.e., strategies such that every consistent play starting in the given initial vertex has at least value~$b$.
In contrast, we will compute strategies that are improvements in two dimensions:
\begin{enumerate*}[label=(\roman*)]
\item they enforce the optimal value rather than a given one, and
\item they do so from every possible play prefix, even if they did not have control over the prefix.
\end{enumerate*}

\section{Strongly Adaptive Strategies}
\label{sec:strongly-adaptive}

In the previous section, we have argued the importance of adaptive strategies and proved that in every rLTL game both players have an adaptive strategy.
Intuitively, such a strategy exploits bad moves of the opponent to always enforce the best truth value possible after a given prefix.
However, such a strategy does not necessarily seek out opportunities for the opponent to make bad moves.
We argue that this property implies that some adaptive strategies are more desirable than others, which leads us to the notion of strongly adaptive strategies.

In this section, we define strongly adaptive strategies, which are based on a fine-grained analysis of the possibilities a strategy gives the opponent to make bad moves and the resulting outcomes of such bad moves.
We show that strongly adaptive strategies do not exist in every rLTL game.
This is in stark contrast to adaptive strategies, which always exists.
Nevertheless, we give a doubly-exponential time algorithm that decides whether a strongly adaptive strategy exists and, if yes, computes one.

\subsection{Bad Moves}\label{sec:bad moves}
We already have used the notion of bad moves in Section~\ref{adaptive strategy} in an intuitive, but informal, way.
Formally, we say a play~$\rho = v_0v_1 \cdots$ contains a bad move of Player~$i$ at position~$j>0$ if the player can enforce some value $b$ from the prefix~$v_0 \cdots v_{j-1}$ but can no longer enforce the value~$b$ from the prefix~$v_0\cdots v_{j}$.
Note that the position~$j$ is the target of the bad move.
Moreover, note that moving from $v_0 \cdots v_{j-1}$ to $v_{j}$ can only be a bad move for Player~$i$ if it is Player~$i$'s turn at $v_{j-1}$.
Also, there must be some other edge from $v_{j-1}$ to a vertex~$v\not = v_{j}$ so that he can still enforce $b$ from $v_0 \cdots v_{j-1} v$.

For the example given in \autoref{fig:motivate adaptive}, we know that Player~$1$ can enforce the value $0011$ from $01$ (by moving the token from $01$ to $2$).
Suppose he moves the token from $01$ to $4$ instead.
Then, Player~$0$ can enforce $0111$ by visiting vertex~$5$.
Hence Player~$1$ can no longer enforce $0011$ from $014$.
Therefore, the move from prefix~$01$ to vertex~$4$ made by Player~$1$ is bad.

Note that if Player~$1$ makes a bad move from a play prefix~$\mathtt{p}$ to vertex~$v$, then the maximum value Player~$0$ can enforce from $\mathtt{p} v$ is strictly larger than the maximum value he can enforce from $\mathtt{p}$.
Hence, if the maximum value Player~$0$ can enforce from a play prefix is $1111$, then Player~$1$ can not make any bad move from that prefix.
Moreover, since the maximum value Player~$0$ can enforce from any play prefix can increase at most four times, assuming Player~$0$ does not make any bad move. Thus, Player~$1$ can make at most four bad moves against an adaptive strategy because such a strategy does not make any bad moves.

\begin{remark}
\label{remark:badmoves}
Let $\sigma$ be an adaptive strategy and $\mathtt{p}$ a play prefix (not necessarily consistent with $\sigma$). Then, every $(\sigma,\mathtt{p})$-play~$\rho = v_0v_1 \cdots$ contains at most four bad moves of Player~$1$ after $\mathtt{p}$.
Also, if there is no bad move by Player~$1$ at positions~$j_0, j_0+1, \ldots, j_1$ in $\rho$, then $\sigma$ enforces the same truth values from every prefix of the form~$v_0 \cdots v_{j}$ with $j_0-1 \le j < j_1$.
\end{remark}

Our next example shows that an adaptive strategy does not actively seek out opportunities for the opponent to make bad moves, it just exploits those made.

\subsection{Motivating Example}\label{sec:motivate strongly}
Recall the example given in \autoref{fig:motivate adaptive}.
The strategy for Player~$0$ given by $\{\mbox{$0\rightarrow 1$}; 3\rightarrow 2; 4\rightarrow 5\}$ is adaptive: if Player~$1$ makes a bad move by moving from $1$ to $4$, then moving from $4$ to $5$ improves the value of the play to $0111$.
Such an improvement can only be enforced after the bad move.

Another adaptive strategy for Player~$0$ is to move along $0\rightarrow 2$ directly in his first move and then move along $3\rightarrow 2$ every time.
Then, the token can never reach vertex~$1$.
Hence, Player~$1$ can never make a bad move.
However, it also means that there can not be a play with value $0111$.
By contrast, if Player~$0$ moves along $0\rightarrow 1$, there is a chance of getting such plays (when Player~$1$ makes a bad move of $1\rightarrow 4$).
Therefore, using the earlier strategy of moving the token along $0\rightarrow 1$, Player~$0$ might be able to enforce $0111$ at some point, but he can never achieve the value~$0111$ when moving directly to vertex~$2$.

Similarly, in many games, a player may have two (or more) optimal choices to move the token from some prefix. In such situations, that player should compare the bad moves his opponent can make in both choices and determine the choice in which he can enforce the best value after a bad move has been made by the opponent. To capture this, we refine the notion of adaptive strategies by introducing strongly adaptive strategies, which are, in a sense to be formalized below, the best adaptive strategies.

\subsection{Definitions}

In this section, we introduce the necessary machinery to define strongly adaptive strategies for Player~$0$.
Throughout this section, we are concerned with ranking adaptive strategies according to the number of bad moves they allow the opponent to make, and on the effect these moves have.
As the number of bad moves in one play is bounded by four, this results in at most five truth values, i.e., the one that is enforced before the first bad move, and the ones after each bad move.
If Player~$1$ makes less than four bad moves, we use the symbol~$\bot \notin \mathbb{B}_4$ to signify~this.

A summary is a five-tuple~$(b_0, \ldots, b_k,\blank,\ldots,\blank) \in (\mathbb{B}_4 \cup \set{\bot})^5$ such that $\bot \neq b_0 < b_1 < \cdots < b_k$.
The set of all summaries is denoted by $\mathcal{S}$.

Fix an adaptive strategy~$\sigma$ for Player~$0$, a play prefix~$\mathtt{p}$ not necessarily consistent with $\sigma$, and a $(\sigma,\mathtt{p})$-play~$\rho$, and let $0 \le k \le 4$ be the number of bad moves by Player~$1$ after $\mathtt{p}$.
Define $\mathtt{p}_0 = \mathtt{p}$ and let $\mathtt{p}_{j}$, for $1 \le j \le k$, be the prefix of $\rho$ ending at the position of the $j$-th bad move.
Due to Remark~\ref{remark:badmoves}, these prefixes contain information about all possible truth vales that are enforced by Player~$0$ from prefixes of $\rho$.
We employ summaries to capture the values a given \emph{strategy}~$\sigma$ enforces from these prefixes.
Formally, for $0 \le j \le k$, let $b_j$ be the maximal value that $\sigma$ enforces from $\mathtt{p}_j$.
As $\sigma$ is adaptive, these values are strictly increasing.
So, we can define the summary
$\playsummary{\sigma}{\mathtt{p}}{\rho} = (b_0, \ldots, b_k, \blank,\ldots,\blank)$.
Intuitively, the summary collects all information about which truth values the strategy~$\sigma$  enforces after each bad move has been made.
If there are less than four bad moves in $\rho$ after $\mathtt{p}$, then we fill the summary with $\bot$'s to obtain a vector of length five.

We will use such summaries to compare strategies.
To do so, we compare summaries in lexicographic order~$\le_{\lex}$ with $\bot$ being the smallest element.
In other words, we prefer larger truth values of smaller ones and prefer the opportunity for a bad move over the impossibility of a bad move.

\begin{example}
\label{example:summaries}
Consider again the game in Figure~\ref{fig:motivate adaptive}.
Let $\sigma_1$ be the memoryless Player~$0$ strategy always making the moves~$\set{0 \rightarrow 1, 3\rightarrow 2, 4\rightarrow 5 }$.
Then,
 \[\playsummary{\sigma_1}{0}{0145^\omega} = \playsummary{\sigma_1}{01}{0145^\omega} = (0011,0111,\bot,\bot,\bot)\]
and $\playsummary{\sigma_1}{014}{0145^\omega} = (0111,\bot,\bot,\bot,\bot)$ because the play~$0145^\omega$ does not contain a bad move of Player~$1$ after $014$.
In addition, $\playsummary{\sigma_1}{\mathtt{p}}{01(23)^\omega} = (0011,\bot,\bot,\bot,\bot)$ for every prefix~$\mathtt{p}$ of $01(23)^\omega$, as the play does not contain any bad move of Player~$1$.

Let $\sigma_2$ now be the memoryless Player~$0$ strategy given by $\set{0 \rightarrow 2, {3\rightarrow 2}, {4\rightarrow 5} }$.
Then, we have $\playsummary{\sigma_2}{\mathtt{p}}{0(23)^\omega} = (0011,\bot,\bot,\bot,\bot)$ for every prefix~$\mathtt{p}$ of  $0(23)^\omega$ because the play does not contain bad moves of Player~$1$.
\end{example}

We continue by listing some simple properties of summaries that are useful later on.
Consider the prefixes $0$, $01$, $014$ of $0145^\omega$ in Example~\ref{example:summaries}. The former two have the same summary~${s}$, while the summary of the latter is obtained by shifting ${s}$ to the left. Note that moving from from $01$ to $4$ is a bad move of Player~$1$, while moving from $0$ to $1$ is not.
By inspecting the definition of play summaries, it is clear that extending plays by bad moves corresponds to a left shift, while Remark~\ref{remark:badmoves} implies that the absence of bad moves keeps summaries stable.

To formalize this, we use the following notation:
for ${s} = (b_0, \ldots, b_k, \blank,\ldots,\blank) \in \mathcal{S}$ with $k>0$ let $\leftshift{{s}} = (b_1, \ldots, b_k, \blank,\ldots,\blank)  \in \mathcal{S}$, i.e., we shift ${s}$ to the left and fill the last entry with a $\bot$.
As entries in summaries are strictly increasing, we have $\leftshift{{s}} >_{\lex} {s}$ for every ${s}$ with at least two non-$\bot$ entries.

\begin{remark}
\label{remark:playsummaryevolution}
Let $\sigma$ be an adaptive strategy for Player~$0$, let $\mathtt{p}$ be a play prefix, and let $\rho = v_0 v_1 \cdots$ be a $(\sigma, \mathtt{p})$-play. Further, let $n = |\mathtt{p}|$, i.e., $v_{n-1}$ is the last vertex of $\mathtt{p}$, and note that $\rho$ is also a $(\sigma, \mathtt{p} v_n)$-play.

If $\rho$ has a bad move at position~$n$, then $\playsummary{\sigma}{ \mathtt{p} v_n}{ \rho} = \leftshift{\playsummary{\sigma}{ \mathtt{p}}{ \rho}}$ (reflecting the fact that $\rho$ has one bad move less after $\mathtt{p} v_n$ than after $\mathtt{p}$), otherwise we have $\playsummary{\sigma}{ \mathtt{p} v_n}{ \rho} = \playsummary{\sigma}{ \mathtt{p}}{ \rho}$.
Note that we have kept $\sigma$ and $\rho$ fixed and just added a vertex to the prefix we consider.
\end{remark}

As seen above, a bad move shifts the summary to the left.
The following remark shows a dual result, allowing us to determine the summary of a play prefix of length one from the summary of play prefix up to the first bad move.
In Example~\ref{example:summaries}, note that the strategy~$\sigma_1$ (using the edges $\set{0 \rightarrow 1, 3\rightarrow 2, 4\rightarrow 5 }$) enforces value~$0011$ from $0$,  i.e., the first entry of $\playsummary{\sigma_1}{0}{0145^\omega}$ is $0011$.
The play~$0145^\omega$ has its first bad move of Player~$1$ at position~$2$, and the corresponding summary is~$\playsummary{\sigma_1}{014}{0145^\omega} = (0111,\bot,\bot,\bot,\bot)$.
Hence, $\playsummary{\sigma_1}{0}{0145^\omega}$ must be the ``concatenation''~$(0011,0111,\bot,\bot,\bot)$ of $0011$ and $(0111,\bot,\bot,\bot,\bot)$ (with the last $\bot$ removed).
In general, we have the following property.

\begin{remark}\label{remark:leftshiftSummary}
Let ${s} = (b_0,\ldots, b_k,\blank,\ldots,\blank) \in \mathcal{S}$ with $k>0$ and let $v$ be a vertex.
Let $\sigma$ be an adaptive strategy such that $b_0$ is the maximal value that $\sigma$ enforces from $v$
and let $\rho$ be a $(\sigma, v)$-play with at least one bad move, and let $\mathtt{p}$ be the prefix of $\rho$ ending at the position of the first bad move.
Then, $\playsummary{\sigma}{\mathtt{p}}{\rho} = \leftshift{{s}}$ if and only if $\playsummary{\sigma}{v}{\rho} = {s}$.
\end{remark}

Again, recall Example~\ref{example:summaries}, and consider the plays~$\rho_b = 0145^\omega$ (with a bad move by Player~$1$) and $\rho_n = 01(23)^\omega$ (without a bad move), which are both $(\sigma_1,0)$-plays.
We have $\playsummary{\sigma_1}{0}{\rho_b} = (0011,0111,\bot,\bot,\bot)$ and $\playsummary{\sigma_1}{0}{\rho_n} = (0011,\bot,\bot,\bot,\bot)$.
Disregarding the $\bot$'s the summary of $\rho_n$ can be seen as a strict prefix of the summary of $\rho_b$.
Note that $(0011,\bot,\bot,\bot,\bot) <_{\lex} (0011,0111,\bot,\bot,\bot)$.

In general, fix a strategy~$\sigma$, a play prefix~$\mathtt{p}$, and a $(\sigma,\mathtt{p})$-play~$\rho$ with $\playsummary{\sigma}{\mathtt{p}}{\rho} = (b_0, \ldots,b_k,\blank,\ldots,\blank)$. Then, for every $k' < k$ there is a $(\sigma, \mathtt{p})$-play~$\rho'$ with $\playsummary{\sigma}{\mathtt{p}}{\rho'} = (b_0, \ldots,b_{k'},\blank,\ldots,\blank)$, i.e., any play where Player~$1$ stops making bad moves after the first $k'$ ones (recall that making bad moves is a choice).

To formalize this, we say that a summary~$(b_0, \ldots, b_k, \blank,\ldots,\blank)$ is a strict prefix of a summary~$(b_0', \ldots, b_{k'}', \blank,\ldots,\blank)$ if $k < k'$ and $b_j = b_j'$ for all $0\le j \le k$, i.e., we only consider non-$\bot$ entries.
Now, fix $(\sigma,\mathtt{p})$-plays $\rho, \rho'$.
We say that $\rho$ is $(\sigma, \mathtt{p})$-covered by $\rho'$ if $\playsummary{\sigma}{\mathtt{p}}{\rho}$ is a strict prefix of $\playsummary{\sigma}{\mathtt{p}}{\rho'}$.
Also, we say that $\rho$ is a $(\sigma, \mathtt{p})$-uncovered play if there is no $(\sigma,\mathtt{p})$-play~$\rho'$ that covers it.
When $\sigma$ and $\mathtt{p}$ are clear from context, we drop them and say that a play is uncovered.
In the example, $\rho_n$ is $(\sigma_1, 0)$-covered  by $\rho_b$, which is $(\sigma_1, 0)$-uncovered.

Now, we lift summaries from plays to strategies by defining~$\stratsummary{\sigma}{\mathtt{p}}$ as the lexicographical minimum over all $\playsummary{\sigma}{\mathtt{p}}{\rho}$ where $\rho$ ranges over $(\sigma, \mathtt{p})$-uncovered plays.
Note that if $\rho$ $(\sigma, \mathtt{p})$-covers $\rho'$, then the summary of $\rho$ is a strict prefix of the summary of $\rho'$ and, therefore, strictly smaller.
Our definition of $\stratsummary{\sigma}{\mathtt{p}}$ discards such plays when computing the minimum, but the information is not lost as it appears as a prefix of a covering play.

In the running example, we have $\stratsummary{\sigma_1}{0} = (0011,0111,\bot,\bot,\bot)$ and $\stratsummary{\sigma_2}{0} = (0011,\bot,\bot,\bot,\bot)$.

\begin{remark}\label{remark:existenceofplaysummary}
Let $\sigma$ be an adaptive strategy for Player~$0$ and let $\mathtt{p}$ be a play prefix. If $\stratsummary{\sigma}{\mathtt{p}} = {s}$ for some ${s}\in \mathcal{S}$, then there exists a $(\sigma,\mathtt{p})$-uncovered play $\rho$ such that $\playsummary{\sigma}{\mathtt{p}}{\rho} = {s}$.
\end{remark}

Finally, we are ready to formalize our intuitive notion of strongly adaptive strategies, i.e., adaptive strategies that seek out opportunities for the opponent to make bad moves.
Recall that summaries record the possibility, and the effect, of Player~$1$ making bad moves.
So, we intuitively say a strategy is strongly adaptive if it maximizes the summaries globally.

Recall that a strategy is adaptive if the value it enforces from any possible play prefix is as large as the value any other strategy enforces from that prefix.
Analogously, a strategy is strongly adaptive if its summary for every play prefix is as good as the summary from the play prefix for any other strategy.

\begin{definition}
An adaptive strategy~$\sigma_0$ is strongly adaptive if $\stratsummary{\sigma_0}{\mathtt{p}}\ge_{\lex} \stratsummary{\sigma}{\mathtt{p}}$ for every adaptive strategy~$\sigma$ and every play prefix~$\mathtt{p}$.
\end{definition}

For every play prefix~$\mathtt{p}$, let $\mathrm{smry}(\mathtt{p})$ denote the lexicographical maximum of $\stratsummary{\sigma}{\mathtt{p}}$ over all adaptive strategies $\sigma$ for Player~$0$ in the game $\mathcal{G}$, i.e.,
\[\mathrm{smry}(\mathtt{p}) = \max_{\sigma} \stratsummary{\sigma}{\mathtt{p}},\]
where $\sigma$ ranges over all adaptive strategies for Player~$0$.

Note that every strongly adaptive strategy is adaptive by definition, and the first entry of $\mathrm{smry}(\mathtt{p})$ is equal to the maximal value that can be enforced from $\mathtt{p}$. However, as argued above, not every adaptive strategy is strongly adaptive.

\subsection{Existence of Strongly Adaptive Strategies}

While strongly adaptive strategies generalize adaptive strategies, there is a catch in the definition: The former may not always exist, whereas the latter always do.
For instance, consider the graph given in \autoref{fig:no strongly ex} with initial vertex~$0$ and the formula~$\varphi = \Boxdot p$. It is clear that Player~$0$ can enforce $0011$ from any play prefix in $0(10)^*$ by eventually moving to vertex~$3$. And if at some point, Player~$1$ makes the bad move~$1\rightarrow 2$, then Player~$0$ enforces $0111$ as the token stays at vertex~$2$ forever.
However, any adaptive strategy for Player~$0$ has to eventually visit vertex~$3$, unless Player~$1$ makes a bad move prior.

Note that Player~$1$ can only make a bad move at vertex~$1$, so visiting $1$ once more when at vertex $0$ instead of moving to vertex~$3$ gives her another chance to make a bad move.
So, to optimize the enforced value under one bad move, Player~$1$ should stay in the loop between $0$ and $1$ forever.
However, this is not the optimal behavior if no bad move occurs, as looping yields a value of $0000$, which is smaller than the value $0011$ that is achieved by eventually moving to $3$.

Formally, for $n\ge 0$, let $\sigma_n$ be the strategy such that $\sigma_n(0(10)^{n'}) = 1$ for all $n' < n$ and $\sigma_n(0(10)^{n'}) = 3$ for all $n' \ge n$, i.e., $\sigma_n$ gives Player~$1$ $n$ chances to make a bad move and then moves to $3$, thereby preventing him from making a bad move.
Note that each of the $\sigma_n$ is adaptive, but $\sigma_{n+1}$ gives Player~$0$ more opportunities to make a bad move than $\sigma_{n}$, namely for the prefix~$0(10)^{n}$.

Fix some $n$.
There are only two $(\sigma_{n+1},0(10)^{n})$-plays, i.e., $0(10)^{n}10(34)^\omega$ (Player~$1$ does not make a bad move) and $0(10)^{n}12^\omega$ (Player~$1$ makes a bad move).
Then, $\playsummary{\sigma_{n+1}}{0(10)^{n}}{0(10)^{n}10(34)^\omega} = (0011,\bot,\bot,\bot,\bot)$ as well as $\playsummary{\sigma_{n+1}}{0(10)^{n}}{0(10)^{n}12^\omega} = (0011,0111,\bot,\bot,\bot)$.
Hence, we conclude $\stratsummary{\sigma_{n+1}}{0(10)^{n}} = (0011,0111,\bot,\bot,\bot)$, as the former is covered by the latter.

Towards a contradiction assume there is a strongly adaptive strategy $\sigma$.
By definition, we have
\begin{equation}
\label{eq}
	\stratsummary{\sigma}{0(10)^{n}} \ge_{\lex} \stratsummary{\sigma_{n+1}}{0(10)^{n}}  = (0011,0111,\bot,\bot,\bot)
\end{equation} for every $n$.
As we have $\stratsummary{\sigma}{0(10)^{n}} <_{\lex} (1111,\bot,\bot,\bot,\bot)$ ($p$ does not hold at vertex~$0$), $\sigma$ must give Player~$1$ the chance to make at least one bad move after the prefix~$0(10)^{n}$.
So, we must have $\sigma(0(10)^{n}) = 1$, as Player~$1$ can only make a bad move at vertex $1$.

Thus, the play~$(01)^\omega$ (with value~$0000$) is a $(\sigma, 0(10)^{n})$-play for every $n$, i.e., $\sigma$ only enforces $0000$ from every such prefix.
Hence, the first entry of $\stratsummary{\sigma}{0(10)^{n}}$ is $0000$ for every $n$.
This contradicts Inequality~(\ref{eq}).
Therefore, $\sigma$ is not strongly adaptive, i.e., Player~$0$ does not have a strongly adaptive strategy in the game.

\begin{figure}[t!]
	\centering
	\begin{tikzpicture}
		\node[player0, label={below:$\{ \}$}] (0) at (0, 0) {$0$};
		\node[player1, label={below:$\{ \}$}] (1) at (1.5, 0) {$1$};
		\node[player1, label={below:$\{ p\}$}] (2) at (3, 0) {$2$};
		\node[player1, label={below:$\{\}$}] (3) at (-1.5,0) {$3$};
		\node[player1, label={below:$\{ p\}$}] (4) at (-3,0) {$4$};

		\path[->] (0) edge (3) edge[bend left=20] (1);
		\path[->] (1) edge (2) edge[bend left=20] (0);
		\path[->] (2) edge[loop right] ();
		\path[->] (3) edge[bend left=20] (4);
		\path[->] (4) edge[bend left=20] (3);
	\end{tikzpicture}
	\caption{An $\mathrm{rLTL}$ game with no strongly adaptive strategy}
	\label{fig:no strongly ex}
\end{figure}

As strongly adaptive strategies do not necessarily exist, we are interested in the following problem.
\begin{problem}\label{problem 2}
	Given an $\mathrm{rLTL}$ game, determine whether a strongly adaptive strategy for Player~$0$ exists and, if yes, compute one.
\end{problem}

\subsection{Computing Strongly Adaptive Strategies}
We solve Problem \ref{problem 2} for an $\mathrm{rLTL}$ game $\mathcal{G} = (\mathcal{A},\varphi)$ by constructing the parity games $\mathcal{G}^b$ for each $b$ and the extended game $\mathcal{G}' = (\mathcal{A}',\varphi)$ as in the algorithm given in Section~\ref{solving rLTL games}.
Recall that Player~$0$ wins $\mathcal{G}^b$ if and only if he can enforce $b$ in $\mathcal{G}$ and that $\mathcal{G}'$ is the product of the $\mathcal{G}^b$.
As we have described in Step~$5$ of that algorithm, it is easy to see that solving Problem \ref{problem 2} for the game $\mathcal{G}$ is equivalent to solving the problem for game $\mathcal{G}'$. Hence, from now on, we only consider $\mathcal{G}'$ and show properties for the game $\mathcal{G}'$, which we can use later to compute a strongly adaptive strategy in $\mathcal{G}$. This strategy can then be transformed into a strongly adaptive strategy for $\mathcal{G}$.
In the following, it is often useful to focus on one truth value by equipping $\mathcal{G}'$ with the parity condition of $\mathcal C_b$ for some $b$: a vertex~$(v,q_{1111}, \ldots, q_{0000})$ has the color that $q_b$ has in $\mathcal C_b$.
Thus, $\mathcal{G}'$ equipped with the parity condition of $\mathcal{G}^b$ is equivalent to $\mathcal{G}^b$.

To decide whether a strongly adaptive strategy exists, we proceed as follows:
\begin{enumerate}
	\item We first give a characterization of the vertices~$v$ of $\mathcal{G}'$ with $\mathrm{smry}(v)={s}$ that only uses summaries that are larger than ${s}$. This allows us to compute $\mathrm{smry}(v)$ for every vertex $v$ by induction over the summaries.
	\item Using the decomposition of $\mathcal{G}'$ into regions with the same summary and the characterization we construct a series of obliging games~\cite{Obliging}. In an obliging game, Player~$0$ has a strong winning condition that has to be satisfied on every play and a weak winning condition that must be satisfiable if Player~$1$ cooperates. In our case, the strong winning condition requires Player~$0$ to always enforce the best value that is currently possible and the weak condition requires Player~$1$ to have a chance to make a bad move (if the summary encodes that this is still possible), i.e., whenever possible, Player~$1$ is given the chance to make a bad move.
	\item Finally, if  Player~$1$ has in all obliging games a strategy satisfying both the strong and the weak condition, then these can be turned effectively into a strongly adaptive strategy, otherwise there is no such strategy.
\end{enumerate}

We first provide a useful lemma showing that a strategy in $\mathcal{G}'$ is strongly adaptive if and only if its summary is history independent, i.e., only depends on the last vertex.

\begin{lemma}\label{lem:strongly ad if and only if e(p) is summaryMax(v)}
A strategy $\sigma$ for Player~$0$ in $\mathcal{G}'$ is strongly adaptive if and only if for every play prefix~$\mathtt{p}$ ending in vertex~$v$, it holds that $\stratsummary{\sigma}{\mathtt{p}}) = \mathrm{smry}(v)$.
\end{lemma}

As computed in Section~\ref{solving rLTL games}, let $\enfExact{b}$ be the set of vertices in $\mathcal{G}'$ from which the maximum value Player~$0$ can enforce is~$b$.
Furthermore, for a summary ${s} \in \mathcal{S}$, let $\smrEMore{{s}}$ denote the set of vertices $v$ in $\mathcal{G}'$ for which $\mathrm{smry}(v) \ge_{\lex} {s}$.
Let $\smrExact{{s}}$, $\smrMore{{s}}$, and $\smrLess{{s}}$ be defined similarly.

\begin{remark}
Let ${s} = (b_0, \ldots, b_k,\blank,\ldots,\blank)$. Then, $\smrExact{{s}} \subseteq \enfExact{b_0}$.
\end{remark}

For a vertex set $F$, let $\mathrm{pre}(F)$ denote the set of vertices from which there is an edge to $F$.
Maybe surprisingly, we do not distinguish between vertices of Player~$0$ and Player~$1$, but we will only apply $\mathrm{pre}(F)$ when it is Player~$1$'s turn.

Next, we characterize the sets $\smrExact{{s}}$ in terms of the existence of strategies that witness summaries.
The key aspects of this characterization is that it only refers to summaries~${s}' >_{\lex} {s}$, which will later allow us to compute these sets inductively.

Given a strategy~$\sigma$ for Player~$0$ in $\mathcal{G}'$ and a play prefix~$\mathtt{p}$, let $\bmfree{\sigma}{\mathtt{p}}$ denote the set of $(\sigma,\mathtt{p})$-plays that do not contain a bad move by Player~$1$ after $\mathtt{p}$.

\begin{definition}
Let $\sigma$ be a strategy for Player~$0$, $\mathtt{p}$ be a play prefix, and ${s} = (b_0, \ldots, b_k, \blank,\ldots,\blank)$ a summary.
We say that $\sigma$ is an ${s}$-witness from $\mathtt{p}$ if and only if it satisfies the following three properties:

		\begin{description}
			\item[Enforcing] Every play in $\bmfree{\sigma}{\mathtt{p}}$ satisfies the parity condition of the game $\mathcal{G}^{b_0}$. Thus, a witness has to enforce~$b_0$ unless Player~$1$ makes a bad move.

			\item[Enabling] If $k \ge 1$, there exists a play in $\bmfree{\sigma}{\mathtt{p}}$ that visits $\mathrm{pre}\big( \smrExact{\leftshift{{s}}}\big)$. Thus, if there is the chance to reach a vertex where Player~$1$ can make a bad move, then a witness has to visit such a vertex.
				Note that we require that the bad move leads to a vertex with summary~$\leftshift{{s}}$, which is the largest summary that can be guaranteed to be reached from $\mathtt{p}$ after a bad move.

			\item[Evading] If $k \ge 1$, then let us define $\evade{{s}}$ to be the set of summaries ${s}' = (b_0',\ldots, b_{k'}',\blank,\ldots,\blank)$ with $b_0' > b_0$, ${s}' <_{\lex} \leftshift{{s}}$, and such that ${s}'$ is not a strict prefix of $\leftshift{{s}}$. Then, no play in $\bmfree{\sigma}{\mathtt{p}}$ visits $\mathrm{pre}\big(\smrExact{{s}'}\big)$ for any ${s}'\in \evade{{s}}$.
			Thus, a witness can never reach a vertex where Player~$1$ can make a bad move to reach a summary that is worse than $\leftshift{{s}}$.
		\end{description}
\end{definition}

Recall that $\leftshift{{s}} >_{\lex} {s}$ and that ${s}' \in \evade{{s}}$ implies ${s}' >_{\lex} {s}$.

\begin{lemma}\label{lem:characterization}
	In the game $\mathcal{G}'$, for some summary ${s}$ and for some vertex~$v$, we have $v\in \smrExact{{s}}$ if and only if $v \not \in \smrMore{{s}}$ and there is an ${s}$-witness from $v$.
\end{lemma}

We now give a method to compute $\smrExact{{s}}$ for each summary~${s} \in \mathcal{S}$ by induction from the largest to the smallest summary.
Since truth values in a summary are strictly increasing, $(1111,\blank,\ldots,\blank)$ is the maximal summary.
We have $\smrExact{(1111,\blank,\ldots,\blank)} = \enfExact{1111}$, which we can compute using Tabuada and Neider's result for classical rLTL games (see Section~\ref{section3}).
For the inductive step, assume that for a summary~${s} = (b_0, \ldots, b_k, \blank,\ldots,\blank)$ the sets $\smrExact{{s}'}$ are already computed for every ${s}' >_{\lex} {s}$.
The set $\smrExact{{s}}$ can then be computed using the following algorithm:

\begin{enumerate}
\item\label{item:algo1:1} If $ k = 0$, then return $ \enfMore{b_0}\setminus \smrMore{{s}} $. Here, $\enfMore{b_0}$ can again be computed using Tabuada and Neider's result for classical rLTL games.

\item\label{item:algo1:3} Now assume $k > 0$.
Let $\mathcal{A}_{{s}}$ be the subgraph of $\mathcal{A}'$ restricted to the vertex set
\[ \enfMore{b_0}\setminus \Big(\smrMore{{s}} \cup \bigcup\nolimits_{{s}'\in \evade{{s}}} \reach{\smrExact{{s}'}}\Big),\]
where $\reach{F}$ denotes the set of vertices of $\mathcal{A}'$ from which Player~$1$ can force the token to reach $F$. This set can be computed in linear time (in the number of edges of $\mathcal{A}'$) using standard methods to solve reachability games (see \cite{Automata_Book} for more details).
In the proof of correctness of the algorithm (see Lemma~\ref{lemma:algoforsummary}) we show that $\mathcal{A}_{{s}}$ does not have any terminal vertices.

Also, the sets~$\smrExact{{s}'}$ for ${s}' \in \evade{{s}}$ are already computed, because  the summaries~${s}' \in \evade{{s}}$ are all greater than ${s}$.

\item\label{item:algo1:4} Let $\win{{{s}}}$ be the winning region for Player~$0$ in the parity game with arena~$\mathcal{A}_{{s}}$ and coloring as in the game~$\mathcal{G}^{b_0}$.
Return the set of vertices in Player~$0$'s winning region~$\win{{s}}$ from which $\mathrm{pre}\big(\smrExact{\leftshift{{s}}}\big)$ is reachable in the subgraph of $\mathcal{A}'$ restricted to $\win{{{s}}}$.
\end{enumerate}

\begin{lemma}\label{lemma:algoforsummary}
The algorithm described above computes the sets~$\smrExact{{s}}$ for ${s} \in \mathcal{S}$.
\end{lemma}

Now, we give a characterization of strongly adaptive strategies in terms of summary witnesses.

\begin{lemma}\label{lem:characterizationStronglyad}
In the game $\mathcal{G}'$, a strategy~$\sigma$ is strongly adaptive if and only if it is a $\mathrm{smry}(\mathtt{p})$-witness from every play prefix $\mathtt{p}$.
\end{lemma}

Now, we show how to decide whether a strategy satisfying the condition given in Lemma~$\ref{lem:characterizationStronglyad}$ exists, i.e., a strategy that is a $\mathrm{smry}(\mathtt{p})$-witness from every play prefix~$\mathtt{p}$.
Furthermore, if such a strategy exists, we compute one.
To do so, we present a reduction to another type of game, called \textit{obliging games}. So, before describing the details of the reduction, let us recapitulate the definitions and useful results on obliging games.

Obliging games are two-player games introduced by Chatterjee et al.~\cite{Obliging}. They have two winning conditions, $S$ and $W$, called strong and weak conditions. The objective of Player~$0$ is to ensure the strong winning condition while allowing Player~$1$ to cooperate with him to additionally fulfil the weak winning condition. Formally, a strategy $\sigma$ for Player~$0$ is \textit{uniformly gracious} if it satisfies the following:
\begin{itemize}
\item for every vertex~$v$, every $(\sigma,v)$-play is $S$-winning, and
\item for every play prefix $\mathtt{p}$ consistent with  $\sigma$, there is a $W$-winning $(\sigma,\mathtt{p})$-play.
\end{itemize}
We are only interested in parity/B\"uchi obliging games (i.e., the strong condition is a parity condition, and the weak one is a B\"uchi condition). The next theorem follows directly from the results by Chatterjee et al.~\cite{Obliging}.

\begin{theorem}\label{thm: Obliging}
A parity/B\"uchi obliging game with $n$ vertices and a parity condition
with $k$ colors can be reduced to a parity game with $O(n)$ vertices and $O(k)$ colors. Moreover, if Player~$0$ has a uniformly gracious strategy in such an obliging game, he has a uniformly gracious strategy with a memory of size at most $O(k)$.
\end{theorem}

Now, coming back to our problem, we define obliging games~$\mathcal{G}_{{s}}$ (for each ${s}\in \mathcal{S}$), which are subgames of $\mathcal{G}'$, such that a uniformly gracious strategy in $\mathcal{G}_{{s}}$ satisfies the properties of an ${s}$-witness locally. In particular, the games are defined in way such that the strong condition resembles the Enforcing property, the weak condition resembles the Enabling property, and the restricted vertex set ensures that the Evading property is satisfied.

\begin{definition}
Given a summary ${s} = (b_0,\ldots,b_k,\blank,\ldots,\blank)\in \mathcal{S}$, let $\mathcal{G}_{{s}} $ be the obliging game obtained from $\mathcal{G}'$ as follows:
\begin{itemize}
\item The set of vertices $V(\mathcal{G}_{{s}})$ is the set $\smrExact{{s}}\cup \{v_{\mathrm{new}}\}$, where $v_{\mathrm{new}}$ is a new vertex that does not belong to $V'$.
\item The set of edges $E(\mathcal{G}_{{s}})$ contains the following edges:
	\begin{itemize}
	\item The edges of the game $\mathcal{G}'$ restricted to the vertex set $\smrExact{{s}}$.
	\item All edges of the form $(v,v_{\mathrm{new}})$ where $v$ is a terminal vertex in the game~$\mathcal{G}'$ restricted to $\smrExact{{s}}$.
	\item A self loop on $v_{\mathrm{new}}$.
	\end{itemize}
\item The strong condition $S_{{s}}$ is a parity condition such that the color of $v_{\mathrm{new}}$ is $0$ and color of any other vertex is same as in $\mathcal{G}^{b_0}$.
\item If $k=0$, then there is no weak condition, i.e., $W_{{s}}$ is a B\"uchi condition with $F = V(\mathcal{G}_{{s}})$. If $k>0$, then the weak condition $W_{{s}}$ is a B\"uchi condition with $F = \mathrm{pre}(\leftshift{{s}}) \cup \{v_{\mathrm{new}}\}$.
\end{itemize}
\end{definition}

The following lemma formalizes the connection between uniformly gracious strategies in the obliging games~$\mathcal{G}_{s}$ and strongly adaptive strategies in $\mathcal{G}'$.

\begin{lemma}\label{lemma:gracioustostronglyad}
There exists a strongly adaptive strategy in $\mathcal{G}'$ if and only if there exists a uniformly gracious strategy in every obliging game $\mathcal{G}_{{s}}$.
Given a uniformly gracious strategy with finite memory in each obliging game $\mathcal{G}_{{s}}$, one can effectively combine these into a strongly adaptive strategy with finite memory in $\mathcal{G}'$.
\end{lemma}

Since the game $\mathcal{G}'$ has doubly-exponential size, using \autoref{thm: Obliging}, the parity\slash{}Büchi obliging games $\mathcal{G}_{{s}}$ can be reduced to doubly-exponential-sized parity games. Once we computed a strongly adaptive strategy for $\mathcal{G}'$, it can then be reduced to a strongly adaptive strategy for the original game $\mathcal{G}$.

Moreover, note that strongly adaptive strategies also have doubly-exponential memory since the obliging games we constructed have doubly-exponential size.
By \autoref{thm: Obliging}, uniformly gracious strategies in such obliging games require memory of linear size, leading to the following result.

\begin{theorem}
Given an $\mathrm{rLTL}$ game, one can decide in doubly-exponential time whether Player~$0$ has a strongly adaptive strategy. If yes, one can compute one with doubly-exponential memory  in doubly-exponential time.
\end{theorem}

Note that by dualizing the definitions and the constructions, an analogous result for Player~$1$ can also be obtained.

redpajama_set_name: RedPajamaArXiv