\section{Causality-Based Game Solving}
\label{sec:gamesolving}

\Cref{lem:slicing} in the preceding section foreshadows how subgoals can be employed in building a recursive approach for the solution of reachability games. 
Before turning to our actual algorithm, we describe a way to symbolically represent nondeterministic memoryless strategies. As discussed in \cite{FarzanK17}, there is no ideal strategy description language for the class of games we consider. Our approach allows us to describe sets of concrete strategies as defined in Section~\ref{sec:prelims} with linear arithmetic formulas.
This framework will prove convenient for \emph{strategy synthesis}, i.e., the computation of winning strategies instead of simply determining the winner of the game.


\subsection{Symbolically Represented Strategies}
We will represent strategies for both players using transition predicates $\mathfrak{S} \in \cal L(\mathcal{V} \cup \mathcal{V'})$, henceforth called \emph{symbolic strategies}, where we only require that $(\mathfrak{S} \implies (\mathit{Safe} \lor \mathit{Reach}))$ is valid.
A sequence $s_0 \ldots s_n \in S^+$ is called a \emph{play prefix} if it is a prefix of some play in $\mathcal{G}$, $(\neg \mathit{Goal})(s_j)$ holds for all $0 \leq j \leq n$, and $s_n$ is not a trap state.
We say that a play prefix $\rho = s_0 \ldots s_n$ \emph{conforms to} a symbolic reachability strategy $\mathfrak{S}$ if for all $j < n$ we have that $\mathfrak{S}(s_j,s_{j+1})$ holds whenever $s_j \in S_{\texttt{{REACH}}}$ (and analogously for safety strategies).
A play conforms to~$\mathfrak{S}$ if all its play prefixes conform to $\mathfrak{S}$.
We say that $\mathfrak{S}$ is winning for \texttt{{REACH}}{} in $s$ if all plays from $s$ that conform to $\mathfrak{S}$ are winning for \texttt{{REACH}}{}  and all play prefixes $s_0 \ldots s_n \in S^*S_{\texttt{{REACH}}{}}$ from $s$ that conform to $\mathfrak{S}$ are such that $(\mathfrak{S} \land \mathit{Reach})(s_n)$ is satisfiable (and analogously for \texttt{{SAFE}}{}).
The second condition ensures that the player cannot be forced to play a transition outside of $\mathfrak{S}$ by their opponent while the play has not reached a trap state or $\mathit{Goal}$, and in particular guarantees the existence of a concrete strategy (as defined in~\Cref{sec:prelims}) conforming to~$\mathfrak{S}$.

\begin{lemma}
  If \texttt{{REACH}}{} (\texttt{{SAFE}}{}) has a winning symbolic strategy in $s$, then \texttt{{REACH}}{} (\texttt{{SAFE}}{}) has a concrete winning strategy in $s$.
\end{lemma}
\begin{proof}
  Let $\mathfrak{S}$ by a symbolic winning strategy for \texttt{{REACH}}{}.
  Let $\sigma_R$ be any reachability strategy such that for all play prefixes $\omega s \in S^* S_{\texttt{{REACH}}}$ that conform to $\mathfrak{S}$ the formula $\mathfrak{S}(s,\sigma_R(\omega s))$ is valid. 
  Such a function is guaranteed to exist, as $(\mathfrak{S} \land \mathit{Reach})(s)$ is satisfiable for all such play prefixes by definition.
  Furthermore, $\sigma_R$ is winning as all play prefixes of plays consistent with $\sigma_R$ conform to $\mathfrak{S}$, and hence all these plays are winning by assumption. 
  The proof for \texttt{{SAFE}}{} is analogous.
  \qed
\end{proof}

This representation allows us to specify nondeterministic strategies, but classical memoryless strategies on finite arenas (specified as a function $\sigma\colon S_{\texttt{{REACH}}}\to S$ or $\S_{\texttt{{SAFE}}}\to S$) can also be represented in this form using a disjunction over formulas $\bigwedge_{v\in \mathcal{V}} (v =s(v)\land v' =\sigma(s)(v))$ for varying $s\in S$.

The following lemma shows that a necessary subgoal directly yields a symbolic strategy for \texttt{{SAFE}}{} if the subgoal is, in a certain sense, \emph{locally avoidable} by \texttt{{SAFE}}{}. It will be our main tool for synthesizing safety player strategies.
\begin{restatable}{lemma}{avoidingC}
	\label{lem:avoidingC}
	Let $C$ be a necessary subgoal for $\mathcal{G}$ and suppose that $\operatorname{Unsat}(\operatorname{Enf}(C,\mathcal{G}))$ holds.
	Then, $\mathit{Safe} \land \neg C$ is a winning symbolic strategy for $\texttt{{SAFE}}$ in $\mathcal{G}$.
\end{restatable}

\subsection{A Recursive Algorithm}


\begin{algorithm}
	\caption{$\operatorname{Reach}(\mathcal{G})$}
	\label{alg:algreach}
	\SetKwInOut{Input}{In}
	\SetKwInOut{Output}{Out}
	\Input{ reachability game $\G = \langle \init, \safe, \reach, \goal \rangle${}}
	\Output{ triple $(R, \mathfrak{S}_{\texttt{{REACH}}}, \mathfrak{S}_{\texttt{{SAFE}}})$ s.t.
		\begin{itemize}
			\item $\mathit{R}\in\cal L(\mathcal{V})$ represents the set of initial states winning for \texttt{{REACH}}{};
			\item $\mathfrak{S}_{\texttt{{REACH}}}$ is a winning symbolic reachability strategy  for states in $R$;
			\item $\mathfrak{S}_{\texttt{{SAFE}}}$ is a winning symbolic safety strategy for states in $\mathit{Init} \land \neg R$.
		\end{itemize}}
	\Begin{
		$\mathit{R} \leftarrow \mathit{Init} \land \mathit{Goal}$\\
		$\mathit{I} \leftarrow \mathit{Init} \land \lnot\mathit{Goal}$\\
		\If{$\operatorname{Unsat}(\mathit{I})$}{\KwRet{$\mathit{R}, {\normalfont \texttt{false}}, \normalfont \texttt{false}$ \label{line:ret1}}}
		$\varphi \leftarrow  \operatorname{Interpolate}(\mathit{I},\mathit{Goal})$\label{line: phi}\\
		$\mathit{C} \leftarrow \operatorname{Instantiate}(\varphi,\mathcal{G})$\label{line: subgoal}\\
		\If{$\operatorname{Unsat}(\operatorname{Enf}(\mathit{C},\mathcal{G}))$\label{line: cpre}}{\KwRet{$\mathit{R}, {\normalfont \texttt{false}},\mathit{Safe} \land \neg C$}\label{line:safety wins}}
		$\mathcal{G}_{post} \leftarrow \langle \operatorname{Post}(C)[\varp/\var], \mathit{Safe} \land \varphi, \mathit{Reach} \land \varphi, \mathit{Goal} \rangle$\label{line:gpost}\\
		$\mathit{R}_{post},\mathfrak{S}_{\texttt{{REACH}}{}}^{post}, \mathfrak{S}_{\texttt{{SAFE}}{}}^{post} \leftarrow \operatorname{Reach} \big(\mathcal{G}_{post}\big)$\label{line: recursion1}\\
		$\mathit{F} \leftarrow C \land \mathit{R}_{post}[\var/\varp]$\\
		\If{$\operatorname{Unsat}(\operatorname{Enf}(\mathit{F},\mathcal{G}))$\label{line:safeavoidsE}}{\KwRet{$\mathit{R}, {\normalfont \texttt{false}}, \mathit{Safe} \land \neg F \land (\varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})$}\label{line:thirdreturn}}
		\If{$\operatorname{Sat}((\mathit{Reach} \lor \mathit{Safe}) \land \varphi \land \lnot \varphi' \land \lnot \mathit{Goal})$\label{line:transback}}{
			$\mathit{F} \leftarrow \mathit{F} \lor \mathit{Goal} [\var/\varp]$\label{line: E2}\\
			$\varphi \leftarrow \texttt{false}$\label{line:tpostfalse}
		}
		$\mathcal{G}_{pre} \leftarrow \langle I,\mathit{Safe} \land \lnot \mathit{F},\mathit{Reach} \land \lnot \mathit{F}, \operatorname{Pre}(\operatorname{Enf}(\mathit{F},\mathcal{G}))\rangle$\label{line:gpre2}\\
		$\mathit{R}_{pre}, \mathfrak{S}_{\texttt{{REACH}}{}}^{pre}, \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre} \leftarrow \operatorname{Reach} \big(\mathcal{G}_{pre}\big)$\label{line: recursion2}\\
    \KwRet{$\mathit{R} \lor \mathit{R}_{pre}$, \label{line: last return}\\ $\qquad \quad \;\; \operatorname{combine}(\mathfrak{S}_{\texttt{{REACH}}{}}^{pre},F, \mathfrak{S}_{\texttt{{REACH}}{}}^{post})$\label{line:reachstrat}, \\$\qquad \quad \;\;(\neg \varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre}) \land (\varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})$\label{line:safetystrat}}
	}
\end{algorithm}

We now describe our algorithm which utilizes necessary subgoals to decompose and solve two-player reachability games (Algorithm~\ref{alg:algreach}).
It is incomplete in the sense that it does not return on every input (\Cref{sec:termination} discusses special cases with guaranteed termination).
If the algorithm returns on input $\mathcal{G}$, it returns a triple $(R,\mathfrak{S}_{\texttt{{REACH}}{}},\mathfrak{S}_{\texttt{{SAFE}}{}})$, where (1) $R$ is a state predicate characterizing the initial states that are winning for \texttt{{REACH}}{} in $\mathcal{G}$, (2) $\mathfrak{S}_{\texttt{{REACH}}{}}$ is a symbolic strategy for \texttt{{REACH}}{} that wins in all initial states satisfying $R$, and (3) $\mathfrak{S}_{\texttt{{SAFE}}{}}$ is a symbolic strategy for \texttt{{SAFE}}{} that wins in all initial states satisfying $\mathit{Init} \land \neg R$.
The returned safety strategy $\mathfrak{S}_{\texttt{{SAFE}}{}}$ is such that $\neg \mathfrak{S}_{\texttt{{SAFE}}{}}$ is a necessary subgoal that \texttt{{SAFE}}{} can avoid locally in the game $\mathcal{G}$ restricted to intial states $\mathit{Init} \land \neg R$ (see~\Cref{lem:avoidingC}).

Algorithm~\ref{alg:algreach} works as follows.
States satisfying $\mathit{Init}$ and $\mathit{Goal}$ are immediately winning for $\texttt{{REACH}}$ and thus always part of the returned formula $R$.
Following the discussion at the beginning of Section~\ref{sec:subgoals}, further analysis considers the game starting in the remaining initial states $I = \mathit{Init} \land \lnot \mathit{Goal}$.
If there is no such state, we may return that all initial states are winning (line~\ref{line:ret1}).
Here, \texttt{{REACH}}{} wins from $R$ without playing any move, and hence $\mathfrak{S}_{\texttt{{REACH}}{}} = \texttt{false}$ is a valid winning symbolic strategy (winning symbolic strategies are only required to provide moves in prefixes that have not seen $\mathit{Goal}$ so far).
We may choose $\mathfrak{S}_{\texttt{{SAFE}}{}}$ arbitrarily as there is no initial state winning for $\texttt{{SAFE}}{}$.

If the algorithm does not return in line~\ref{line:ret1}, a necessary subgoal $C$ between $I$ and $\mathit{Goal}$ is computed by instantiating a Craig interpolant $\varphi$ for the two predicates (lines \ref{line: phi} and \ref{line: subgoal}, see also \Cref{prop_necessary}).
We break up the remaining description of the algorithm into three parts, which correspond to the main cases that occur when splitting the game along the subgoal $C$.

\subsubsection{Case 1: \texttt{{SAFE}}{} can avoid the subgoal $C$.}
If the necessary subgoal $C$ qualifies for~\Cref{lem:avoidingC}, we can immediately conclude that \texttt{{SAFE}}{} is winning for all states statisfying $I$ (lines~\ref{line: cpre} and~\ref{line:safety wins}).
An instance of this case occurs if the interpolant describes a bottleneck in the game which is fully controlled by \texttt{{SAFE}}{}.
The winning symbolic reachability strategy is $\mathit{Safe} \land \neg C$ in this case (line~\ref{line:safety wins}), and we will assume that safety strategies returned by recursive calls of the algorithm are essentially negations of necessary subgoals that can be avoided by \texttt{{SAFE}}{}. 

If Lemma \ref{lem:avoidingC} is not applicable, we next find those transitions in $C$ that move into a winning state for the safety player.
This is achieved by analyzing the \emph{post-game} (line~\ref{line:gpost}):
\[\mathcal{G}_{post} = \langle \operatorname{Post}(C)[\varp/\var], \mathit{Safe} \land \varphi, \mathit{Reach} \land \varphi, \mathit{Goal} \rangle.\]

Its initial states are exactly the states one sees after bridging the subgoal $C$.
In order to make sure that $\mathcal{G}_{post}$ is, in some sense, easier to solve than $\mathcal{G}$, we restrict both $\mathit{Safe}$ and $\mathit{Reach}$ to $\varphi$, which is the interpolant used to compute the subgoal $C$.
This has the effect of removing all transitions in states \emph{not} satisfying~$\varphi$, making them trap states.
For the safety player this makes $\mathcal{G}_{post}$ easier to win than $\mathcal{G}$ as all plays ending in such a trap state without seeing $\mathit{Goal}$ before are winning for \texttt{{SAFE}}{} in $\mathcal{G}_{post}$.
Hence we formally have:
\begin{restatable}{lemma}{gpost}
  \label{lem:gpost}
  If $\mathfrak{S}$ is a winning symbolic reachability strategy from $s$ in $\mathcal{G}_{post}$, then $\mathfrak{S}$ is also winning from $s$ in $\mathcal{G}$.
\end{restatable}



Due to the restriction to $\varphi$, intuitively \texttt{{REACH}}{} wins from a state $s$ in $\mathcal{G}_{post}$ if they can win from $s$ in $\mathcal{G}$ \emph{while staying inside the interpolant} $\varphi$.
In other words, \texttt{{REACH}}{} must guarantee that the necessary subgoal $C$ is not visited again in the play.
Still, the set $R_{post}$, as returned in line \ref{line: recursion1} by the recursive call to Algorithm~\ref{alg:algreach} on $\mathcal{G}_{post}$, is a sufficient subgoal in $\mathcal{G}$, by the above lemma.
Furthermore, if \texttt{{SAFE}}{} can avoid all states satisfying $R_{post}$ (see line~\ref{line:safeavoidsE}), then this also implies a winning strategy from all initial states in $I$. 
The reason is that \texttt{{REACH}}{} can only win by eventually visiting a state from which they can win without leaving $\varphi$ again, as $(\mathit{Goal} \implies \varphi)$ is valid.
This is not possible if \texttt{{SAFE}}{} can avoid all states in $R_{post}$. 

In this case we construct $\mathfrak{S}_{\texttt{{SAFE}}{}}$ as follows.
We assume that $\neg \mathfrak{S}_{\texttt{{SAFE}}{}}^{post}$ is a necessary subgoal that can be locally avoided in $\mathcal{G}_{post}$ from all states satisfying $\operatorname{Post}(C)[\varp/\var] \land \neg R_{post}$, and furthermore, we know that $F := C \land R_{post}[\var/\varp]$ can be locally avoided in $\mathcal{G}$ (line~\ref{line:safeavoidsE}).
Intuitively, playing according to $\mathfrak{S}^{post}_{\texttt{{SAFE}}{}}$ in $\mathcal{G}_{post}$ yields a strategy for \texttt{{SAFE}}{} which avoids $\mathit{Goal}$ and may move back into a state satisfying $\neg \varphi$, which forces \texttt{{REACH}}{} to bridge the subgoal $C$ again in order to win.
It follows that $F \lor (\varphi \land \neg \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})$ is a necessary subgoal from $I$ that can be locally avoided by \texttt{{SAFE}}{} in $\mathcal{G}$, and the corresponding symbolic strategy is $\mathit{Safe} \land \neg F \land (\varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})$ (we additionally intersect the negated necessary subgoal with $\mathit{Safe}$ to ensure that the symbolic strategy only includes legal transitions).

\medskip
So far, the subgoal was such that \texttt{{SAFE}}{} could avoid it entirely, or at least avoid all states from which \texttt{{REACH}}{} would win when forced to remain inside the post-game.
If this is not the case, then we also need to consider the \emph{pre-game} (line~\ref{line:gpre2}):
\[\mathcal{G}_{pre} = \langle I,\mathit{Safe} \land \lnot \mathit{F},\mathit{Reach} \land \lnot \mathit{F}, \operatorname{Pre}(\operatorname{Enf}(\mathit{F},\mathcal{G}))\rangle.\]
which intuitively describes the game before bridging the interpolant $C$ for the last time.
The exact definition of $F$ will depend on whether $C$ \emph{perfectly partitions} the game or not.
In both cases $F$ will be the largest sufficient subgoal contained in a necessary subgoal, which lets us apply~\Cref{lem:slicing} to conclude that the initial winning regions of $\mathcal{G}$ and $\mathcal{G}_{pre}$ coincide.

\subsubsection{Case 2: The subgoal perfectly partitions $\mathcal{G}$.}
We say that $\varphi$ \emph{perfectly partitions} $\mathcal{G}$ if $(\mathit{Reach} \lor \mathit{Safe}) \land \varphi \land \neg \varphi' \land \neg \mathit{Goal}$ is unsatisfiable (cf. line~\ref{line:transback}).
Intuitively, this means that there is no transition that ``undoes'' the effect of the subgoal~$C$.
If this holds, then the restriction of $\mathcal{G}_{post}$ to states satisfying $\varphi$ is \emph{de facto} no longer a restriction, as no play can reach such a state anyway after passing through the subgoal.
This intuition is formalized by the following lemma.
\begin{restatable}{lemma}{perfectpartition}
  Assume that $\varphi$ \emph{perfectly partitions} $\mathcal{G}$, and let $s$ be a state satisfying $\operatorname{Post}(C)[\varp/\var]$. Then \texttt{{REACH}}{} wins from $s$ in $\mathcal{G}_{post}$ if and only if \texttt{{REACH}}{} wins from $s$ in~$\mathcal{G}$.
\end{restatable}
It follows that $F = C \land R_{post} [\var/\varp]$ is the largest sufficient subgoal included in~$C$.
By~\Cref{lem:slicing}, the same initial states are winning for \texttt{{REACH}}{} in $\mathcal{G}_{pre}$ and in~$\mathcal{G}$. 
In this case, we construct the desired safety strategy (line~\ref{line:safetystrat}) as 
\[\mathfrak{S}_{\texttt{{SAFE}}{}} = (\neg \varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre}) \land (\varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{post}),\]
where $\neg \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre/post}$ are assumed to be necessary subgoals avoidable by \texttt{{SAFE}}{} in the corresponding subgames. 
Intuitively, the combined strategy consists of following $\mathfrak{S}_{\texttt{{SAFE}}}^{pre}$ as long as one remains in the pre-game, which, by induction hypothesis, allows \texttt{{SAFE}}{} to avoid all transitions from $F$ if starting in $R_{pre}$. 
If the play crosses $C \land \neg F$, the strategy is to play according to the winning strategy of the post-game.

A symbolic strategy for \texttt{{REACH}}{} can be given by combining pre- and post-strategies as follows (line~\ref{line:reachstrat}):
\begin{align*}
  \operatorname{combine}(\mathfrak{S}_{\texttt{{REACH}}{}}^{pre},F, \mathfrak{S}_{\texttt{{REACH}}{}}^{post}) := \;\;&(\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \implies \mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \\
  \land \;\; &((\neg \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \land \operatorname{Pre}(F)) \implies F) \\
  \land \;\; &((\neg \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \land \neg \operatorname{Pre}(F)) \implies \mathfrak{S}_{\texttt{{REACH}}{}}^{pre}) \\
  \land \;\; &(\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \lor \operatorname{Pre}(F) \lor \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{pre})).
\end{align*}
This represents a nested conditional strategy that prefers the strategies of the subgames in the priority order $\mathfrak{S}_{\texttt{{REACH}}{}}^{post}, F$, and finally $\mathfrak{S}_{\texttt{{REACH}}{}}^{pre}$.
The reason for this order is that the winning condition in the post-game coincides with the global winning objective (to reach $\mathit{Goal}$), while in the pre-game \texttt{{REACH}}{} tries to reach a winning state in the post-game.
The set $F$ is exactly the bridge between these two.
The last condition makes sure that the strategy only includes transitions of states in which it is winning.

\subsubsection{Case 3: The subgoal does not perfectly partition $\mathcal{G}$.}

If $\operatorname{Sat}((\mathit{Reach} \lor \mathit{Safe}) \land \varphi \land \lnot \varphi' \land \neg \mathit{Goal})$ is true in line~\ref{line:transback}, we can no longer assume that $F$ is the largest sufficient subgoal in $C$.
The reason is that \texttt{{SAFE}}{} may win in $\mathcal{G}_{post}$ by moving out of the subgame, but if this move leads to a winning state for \texttt{{REACH}}{} in $\mathcal{G}$, then such a strategy is winning in $\mathcal{G}_{post}$, but not in $\mathcal{G}$.
So we can only assume that $F$ is sufficient (this follows by~\Cref{lem:gpost}).
In order to apply~\Cref{lem:slicing} we extend~$F$ by all transitions that move directly into $\mathit{Goal}$ (line~\ref{line: E2}). 
This immediately yields a necessary and sufficient subgoal, and so again~\Cref{lem:slicing} applies to $\mathcal{G}_{pre}$ (line~\ref{line:gpre2}).
We could have also added $\mathit{Goal}$-states to $F$ in Case 2, but we have observed that not doing so improves the performance of our procedure considerably. 

The reachability strategy is composed of $\mathfrak{S}_{\texttt{{REACH}}{}}^{pre}, F$, and $\mathfrak{S}_{\texttt{{REACH}}{}}^{post}$ exactly as in Case 2 (line~\ref{line:reachstrat}).
As all transitions in $F$ are losing for \texttt{{SAFE}}{}, and these are the only ones that are removed in $\mathcal{G}_{pre}$, essentially \texttt{{SAFE}}{} can play using the same strategies in $\mathcal{G}$ and $\mathcal{G}_{pre}$.
We implement this by setting $\varphi$ to $\texttt{false}$ (line~\ref{line:tpostfalse}), in which case $\mathfrak{S}_{\texttt{{SAFE}}}$ (line~\ref{line:safetystrat}) equals 
$(\texttt{true} \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre}) \land (\texttt{false} \implies \mathfrak{S}_{\texttt{{SAFE}}}^{post}) \equiv \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre}$.

\medskip
Finally, we formally state the partial correctness of the algorithm, using the ideas outlined above. 
The proof can be found in the appendix.

\begin{restatable}[Partial correctness]{theorem}{partialcorrectness}
  \label{thm:partcorr}
  If $\operatorname{Reach}(\mathcal{G})$ returns $(R,\mathfrak{S}_{\texttt{{REACH}}{}},\mathfrak{S}_{\texttt{{SAFE}}{}})$, then
  \begin{itemize}
  \item $R$ characterizes the set of initial states that are winning for $\texttt{{REACH}}{}$ in $\mathcal{G}$,
  \item $\mathfrak{S}_{\texttt{{REACH}}{}}$ is a winning symbolic reachability strategy from $R$,
  \item $\mathfrak{S}_{\texttt{{SAFE}}{}}$ is a winning symbolic safety strategy from $\mathit{Init} \land \neg R$.
  \end{itemize}
\end{restatable}

\begin{remark}[Simulating the attractor]
  \label{rem:attractor}
	Note that Craig interpolants are by no means unique. If we choose the interpolation function so that $\operatorname{Interpolate}(I,\mathit{Goal})$ always returns $\mathit{Goal}$ (this is a valid interpolant), Algorithm~\ref{alg:algreach} essentially simulates the attractor.
  In this case the subgoal $C$ (line~\ref{line: subgoal}) contains exactly the transitions that move directly into $\mathit{Goal}$.
  All states in $\operatorname{Post}(C)[\varp/\var]$ are then winning for \texttt{{REACH}}{} and hence $R_{post}$ would be equivalent to $\operatorname{Post}(C)[\varp/\var]$, which implies that $C \equiv F$ holds in this case.
  The new goal states in $\mathcal{G}_{pre}$ are set to $\operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G}))$, which are exactly the states in $\operatorname{Pre}(C)$ that either are controlled by \texttt{{REACH}}{}, or such that all their transitions are included in $F$.
  Hence the set $\operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G}))$ is exactly the classical controlled predecessor.
\end{remark}

One effect of slicing the game along general subgoals is that the initial predicate of the post-game (which describes all states satisfying the post-condition of the subgoal) may be satisfied by many states that do not necessarily need to be considered in order to decide who wins from the initial states of $\mathcal{G}$ (for example, because they are not reachable from any initial state, or cannot reach $\mathit{Goal}$).
This can be a drawback if the (superfluous) size of the subgames makes them hard to solve.
Notably, this is in general less of an issue for approaches based on unrolling of the transition relation: 
The method of solving increasingly large step-bounded games~\cite{FarzanK17} will only consider states that are reachable from $\mathit{Init}$, while backwards fixpoint computations will not explore states that do not reach $\mathit{Goal}$.
 A way of coping with this is to provide additional information on the domains of variables, whenever this is available (we discuss the effect of bounding variable domains in \Cref{sec:experiments}).
Indeed, in the case where all variable domains are finite, Algorithm~\ref{alg:algreach} is guaranteed to terminate, as shown in the next subsection.

\subsection{Special Cases with Guaranteed Termination}
\label{sec:termination}

Deciding the winner in the types of games we consider is generally undecidable (see~\cite{FarzanK17} for the case that $\cal L$ is linear real arithmetic).
Since Algorithm \ref{alg:algreach} returns a correct result whenever it terminates, this implies that it cannot always terminate.
In this section, we give two important cases in which we can prove termination. 
The proofs can be found in the appendix.

\begin{restatable}{theorem}{terminationfinite}
  If the domains of all variables in $\mathcal{G}$ are finite, then $\operatorname{Reach}(\mathcal{G})$ terminates.
\end{restatable}

\begin{remark}[Time complexity]
  The termination argument given in the appendix yields a single-exponential upper bound on the runtime of the algorithm, where the input size is measured in the number of concrete transitions of the game.
  This is because in both recursive calls the subgames may be ``almost'' as large as the input -- they are only guaranteed to have at least one concrete transition less.
\end{remark}

We now show that, under certain assumptions, our algorithm also terminates for games that have a finite bisimulation quotient.
To this end, we first clarify what bisimilarity means in our setting.
A relation $R \subseteq S \times S$ over the states of $\mathcal{G}$ is called a \emph{bisimulation} on $\mathcal{G}$, if
\begin{itemize}
	\item for all $(s_1,s_2) \in R$ the formulas $\mathit{Goal}(s_1) \iff \mathit{Goal}(s_2)$, $\mathit{Init}(s_1) \iff \mathit{Init}(s_2)$ and $\mathbf{r}(s_1) \iff \mathbf{r}(s_2)$ are valid (recall that $\mathbf{r}$ holds exactly in states controlled by \texttt{{REACH}}{}).
\item for all $(s_1,s_2) \in R$ and $s_1' \in S$ such that $(\mathit{Safe} \lor \mathit{Reach})(s_1,s_1')$ holds, there exists $s_2' \in S$ such that $(\mathit{Safe} \lor \mathit{Reach})(s_2,s_2')$ holds, and $(s_1',s_2') \in R$.
\item for all $(s_1,s_2) \in R$ and $s_2' \in S$ such that $(\mathit{Safe} \lor \mathit{Reach})(s_2,s_2')$ holds, there exists $s_1' \in S$ such that $(\mathit{Safe} \lor \mathit{Reach})(s_1,s_1')$ holds, and $(s_1',s_2') \in R$.
\end{itemize}
We say that $s_1$ and $s_2$ are \emph{bisimilar} (denoted by $s_1 \sim s_2$) if there exists a bisimulation $R$ such that $(s_1,s_2) \in R$.
Bisimilarity is an equivalence relation, and it is the coarsest bisimulation on $\mathcal{G}$.
The equivalence classes are called \emph{bisimulation classes}.
As the winning region of any player can be expressed in the $\mu$-calculus~\cite{Zappe01} and the $\mu$-calculus is invariant under bisimulation~\cite{BradfieldS07}, it follows that bisimilar states are won by the same player.
\begin{lemma}
  \label{lem:bisimpreservesreach}
  Let $R$ be a bisimulation on $\mathcal{G}$.
  If $(s_1, s_2) \in R$, then \texttt{{REACH}}{} wins from $s_1$ in $\mathcal{G}$ if and only if \texttt{{REACH}}{} wins from $s_2$ in $\mathcal{G}$.
\end{lemma}

We will assume that for each bisimulation class $S_i$ there exists a formula $\psi_i \in \cal L(\mathcal{V})$ that \emph{defines} $S_i$, formally: 
For all $s \in S$, $\psi_i(s)$ holds if and only if $s \in S_i$.
Furthermore, we will assume that the interpolation procedure \emph{respects}~$\sim$, formally: $\operatorname{Interpolate}(\varphi,\psi)$ is equivalent to a disjunction of formulas $\psi_i$.
Such an interpolant exists if $\psi$ or $\varphi$ already satisfy this assumption.

\begin{restatable}{theorem}{terminationbisim}
  Let $\mathcal{G}$ be a reachability game with finite bisimulation quotient under $\sim$ and assume that all bisimulation classes of $\mathcal{G}$ are definable in $\cal L$.
  Furthermore, assume that $\operatorname{Interpolate}$ respects $\sim$.
  Then, $\operatorname{Reach}(\mathcal{G})$ terminates.
\end{restatable}


\section*{Appendix}

\avoidingC*
\begin{proof}
	We first show that all plays that conform to the symbolic safety strategy $\mathit{Safe} \land \neg C$ are winning for \texttt{{SAFE}}{}.
	Let $\rho = s_0s_1 \ldots$ be such a play and assume, for contradiction, that $n \in \mathbb{N}$ exist such that $\mathit{Goal}(s_n)$ is valid, and let $n$ be the least such $n$.
	From $\operatorname{Unsat}(\operatorname{Enf}(C,\mathcal{G}))$ it follows that all states in $\operatorname{Pre}(C)$ are under the control of \texttt{{SAFE}}{}, and hence $C(s_j,s_{j+1})$ can only be true if $s_j \in S_{\texttt{{SAFE}}}$.
	But as $\rho$ conforms to $\mathit{Safe} \land \neg C$, it follows that all play prefixes of $\rho$ conform to $\mathit{Safe} \land \neg C$, in particular, for all $j < n$ the formula $\neg C(s_j,s_{j+1})$ must hold.
  This is in contradiction to the fact that $C$ is a necessary subgoal.
	
	Now we show that if $\pi = s_0 \ldots s_n \in S^*S_{\texttt{{SAFE}}}$ is a play prefix that conforms to $\mathit{Safe} \land \neg C$, then $\operatorname{Pre}(\mathit{Safe} \land \neg C)(s_n)$ holds.
	As $\pi$ is a play prefix and $s_n \in S_{\texttt{{SAFE}}}$, $\mathit{Safe}(s_n)$ is satisfiable.
	From $\operatorname{Unsat}(\operatorname{Enf}(C,\mathcal{G}))$ it follows that if $(\mathit{Safe} \land C)(s_j)$ is satisfiable, then so is $(\mathit{Safe} \land \neg C)(s_j)$, which concludes the proof.

	\qed
\end{proof}


\gpost*
\begin{proof}
	First, we observe that $\mathfrak{S} \implies ((\mathit{Safe} \lor \mathit{Reach}) \land \varphi)$ is valid by assumption, and hence so is $\mathfrak{S} \implies (\mathit{Safe} \lor \mathit{Reach})$.
	We show that all plays of $\mathcal{G}$ that conform to $\mathfrak{S}$ are winning for \texttt{{REACH}}{}.
	Let $\rho = s_0 s_1 \ldots$ be such a play, and assume for contradiction that it is winning for \texttt{{SAFE}}{}.
	As playing according to $\mathfrak{S}$ is winning for \texttt{{REACH}}{} in $\mathcal{G}_{post}$, the play needs to see a transition that is not included in $\mathcal{G}_{post}$.
	Such a transition can only be played by \texttt{{SAFE}}{}, as \texttt{{REACH}}{} plays according to $\mathfrak{S}$, and $\mathfrak{S} \implies ((\mathit{Safe} \lor \mathit{Reach}) \land \varphi)$ is valid.
	This can only happen if there exists $i \in \mathbb{N}$ such that $(\mathit{Safe}\land \lnot\varphi)(s_i, s_{i+1})$ holds, or in other words, $\mathit{Safe}(s_i, s_{i+1})$ and $\lnot\varphi(s_i)$. Let $i$ be the first such index. Then $s_i$ does not have any outgoing transitions in $\mathcal{G}_{post}$, meaning that $s_0\ldots s_i$ is a finite play in $\mathcal{G}_{post}$, and hence there must exist $0\leq j\leq i$ such that $\mathit{Goal}(s_j)$ is satisfied.
	Otherwise, the play would be winning for \texttt{{SAFE}}{} in $\mathcal{G}_{post}$, contradicting the assumption.
	Hence, $\rho$ is winning for \texttt{{REACH}}{}.
	
	It remains to show that any play prefix $s_0 \ldots s_n \in S^*S_{\texttt{{REACH}}}$ that conforms to $\mathfrak{S}$ is such that $(\mathfrak{S} \land \mathit{Reach})(s_n)$ is satisfiable.
  If the play prefix remains inside $\mathcal{G}_{post}$, then this follows from the fact that for all such prefixes $(\mathfrak{S} \land \mathit{Reach}(s_n) \land \varphi)(s_n)$ is satisfiable by assumption, as $\mathfrak{S}$ is winning for \texttt{{REACH}}{} in $\mathcal{G}_{post}$.
  Otherwise, the play prefix corresponds to a play that conforms to $\mathfrak{S}$ and is loosing for $\texttt{{REACH}}{}$ in $\mathcal{G}_{post}$.
  But such a play does not exist by assumption that $\mathfrak{S}$ is a winning reachability strategy for $\texttt{{REACH}}{}$ in $\mathcal{G}_{post}$.
	\qed
\end{proof}


\perfectpartition*
\begin{proof}
  \Cref{lem:gpost} can be adapted slightly to show that if \texttt{{REACH}}{} has \emph{any} (not necessarily expressable as a symbolic strategy) winning strategy from $s$ in $\mathcal{G}_{post}$, then they have a winning stratey from $s$ in $\mathcal{G}$. 

	Hence, it is enough to prove the backward direction. Let us assume that there is a reachability player strategy $\sigma_R$ that is winning from $s$ in $\mathcal{G}$, and, for contradiction, a safety player strategy $\sigma_S$ that is winning from $s$ in $\mathcal{G}_{post}$. Consider strategy $\sigma'_S$ such that $\sigma_{\mathit{S}}'(\omega s') = \sigma_{\mathit{S}}(\omega s')$ if $(\mathit{Safe} \land \varphi)(s')$ is satisfiable, and else $\sigma_{\mathit{S}}'(\omega s') = \sigma_{\mathit{S}}''(\omega s')$, where $\sigma_{\mathit{S}}''$ is an arbitrary safety player strategy in $\mathcal{G}$. There exists a unique play $\rho = s_0s_1\ldots$ in $\mathcal{G}$ consistent with both $\sigma_R$ and $\sigma'_S$ with $s_0 = s$.  Since s satisfies $\operatorname{Post}(C)[\mathcal{V}'/\mathcal{V}]$, we know that $\varphi(s_0)$ is valid (i.e., $\rho$ starts in $\mathcal{G}_{post}$), and since $\varphi$ perfectly partitions $\mathcal{G}$, we know that there is no $0 \leq i$ such that $\left((\mathit{Reach} \lor \mathit{Safe}) \land \varphi \land \neg \varphi'\right)(s_i, s_{i+1})$ holds. It follows that for all $0 \leq j$ we have that $\varphi(s_j)$ holds (i.e., $\rho$ stays in $\mathcal{G}_{post}$). Hence, $\rho$ is a play in $\mathcal{G}_{post}$ consistent with $\sigma_S$ and $\sigma_R$ (considered as a strategy in $\mathcal{G}_{post}$). Since $\sigma_R$ is winning in $\mathcal{G}$, there must exist some $n\in\mathbb{N}$ such that $\mathit{Goal}(s_n)$ is valid. This is a contradiction with $\sigma_S$ being a winning strategy in $\mathcal{G}_{post}$.
	\qed



\end{proof}



\begin{lemma}
	\label{lem:unsat_sum}
	Let $T,F$ be transition predicates such that $\operatorname{Unsat}(\operatorname{Pre}(T)\land\operatorname{Pre}(F))$ holds. Suppose that $\mathcal{G}_T$ and $\mathcal{G}_F$ are games such that  $\operatorname{Unsat}(\operatorname{Enf}(T,\mathcal{G}_T))$ and $\operatorname{Unsat}(\operatorname{Enf}(F,\mathcal{G}_F))$ both evaluate to true, and we have 
	\begin{gather*}
	T \implies (\mathit{Safe}_T \lor \mathit{Reach}_T) \implies (\mathit{Safe} \lor \mathit{Reach}),\\
	F \implies (\mathit{Safe}_F \lor \mathit{Reach}_F) \implies (\mathit{Safe} \lor \mathit{Reach}).
	\end{gather*}
	Then it follows that $\operatorname{Unsat}(\operatorname{Enf}(T \lor F,\mathcal{G}))$ is also true.
\end{lemma}
\begin{proof}
	We proceed by contradiction. Suppose there were $s,v \in \S$ such that $\operatorname{Enf}(T \lor F,\mathcal{G})(s,v)$ holds. It follows that $(T \lor F)(s,v)$ must hold. Since we have $\operatorname{Unsat}(\operatorname{Pre}(T)\land\operatorname{Pre}(F))$, two cases may occur: either (1) $\operatorname{Pre}(T)(s)$ holds, or (2) $\operatorname{Pre}(F)(s)$ holds, but not both. Since they work completely symmetrically, we give the argument only for case (2).
	
	So we know that $F(s,v)$ holds and $T(s,v)$ does not. As $F \implies (\mathit{Safe}_F \lor Reach_F)$, we know $(\mathit{Safe}_F \lor Reach_F)(s,v)$ holds. The only way we can still have $\operatorname{Unsat}(\operatorname{Enf}(F,\mathcal{G}_F))$ is if there is some $s'$ such that $\big(\mathit{Safe}_F(s,s')\land\lnot F(s,s')\big)$ holds. However, as $(\mathit{Safe}_F \lor \mathit{Reach}_F) \implies (\mathit{Safe} \lor \mathit{Reach})$, then also $\big(\mathit{Safe}(s,s')\land\lnot F(s,s')\big)$, which is a contradiction to the fact that $\operatorname{Enf}(F \lor T,\mathcal{G})(s,v)$ holds. 
	\qed
\end{proof}

\partialcorrectness*
\begin{proof}
	We show by induction on the recursion depth that if $\operatorname{Reach}(\mathcal{G})$ returns $(R,\mathfrak{S}_{\texttt{{REACH}}{}},\mathfrak{S}_{\texttt{{SAFE}}{}})$, where $R \in \cal L(\mathcal{V})$, $\mathfrak{S}_{\texttt{{REACH}}}$ and $\mathfrak{S}_{\texttt{{SAFE}}}$ are symbolic strategies for \texttt{{REACH}}{}/\texttt{{SAFE}}{} respectively, and
	\begin{enumerate}
		\item[(a)] $\mathfrak{S}_{\texttt{{REACH}}{}}$  is a winning strategy for \texttt{{REACH}}{} from all states satisfying $R \lor \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}})$,
		\item[(b)] $\lnot \mathfrak{S}_{\texttt{{SAFE}}{}}$  is a necessary subgoal in $\mathcal{G}^I = \langle \mathit{Init} \land \lnot \mathit{R}, \mathit{Safe}, \mathit{Reach}, \mathit{Goal} \rangle$, and
		\item[(c)] if $\mathit{Init} \land \neg R$ is satisfiable, then $\operatorname{Unsat}(\operatorname{Enf}(\lnot \mathfrak{S}_{\texttt{{SAFE}}{}},\mathcal{G}))$ holds.
	\end{enumerate}
	Note that the last condition is equivalent to $\operatorname{Unsat}(\operatorname{Enf}(\lnot \mathfrak{S}_{\texttt{{SAFE}}{}},\mathcal{G}^I))$ as $\operatorname{Enf}$ does not take initial states into account. Properties (b) and (c) ensure, in view of \Cref{lem:avoidingC}, that $\mathfrak{S}_{\texttt{{SAFE}}{}}$ is indeed a winning symbolic strategy from all initial states of $\mathcal{G}^I$ (provided that $\mathfrak{S}_{\texttt{{SAFE}}} \implies (\mathit{Safe} \lor \mathit{Reach})$ holds, which we will show is the case). Together, these properties ensure that $R$ characterizes the set of initial states that are winning for $\texttt{{REACH}}$ in $\mathcal{G}$. We distinguish the five cases that can occur when the algorithm terminates (there are four \textbf{return} statements, the last of which depends on the \textbf{if} statement in line~\ref{line:transback}).
	
	\medskip
	{\it Case 1:  $\operatorname{Reach}(\mathcal{G})$ returns in line~\ref{line:ret1}}. Then the formula $(\mathit{Init} \implies \mathit{Goal})$ is valid, which means that all initial states are goal states.
	The algorithm returns $R = \mathit{Init}\land\mathit{Goal}$, which in this case is equivalent to $\mathit{Init}$.
	Trivially, any strategy is winning for \texttt{{REACH}}{} for all initial states.
  Then, $\mathfrak{S}_{\texttt{{REACH}}} = \texttt{false}$ is a winning symbolic strategy for any state satisfying $R$.
  This is because clearly any play starting in $R$ is winning for \texttt{{REACH}}{}, and we only need to show that \texttt{{REACH}}{} has a move satisfying $\mathfrak{S}_{\texttt{{REACH}}}$ in a play prefix, which by definition has not seen $\mathit{Goal}$ already.
  In this case, there is no such play prefix that we need to cover.
  Observe also that $\operatorname{Pre}(\texttt{false}) \equiv \texttt{false}$, which is required to show (a).

 As $\mathcal{G}^I$ has no initial states, one can choose $\mathfrak{S}_{\texttt{{SAFE}}{}}$ arbitrarily, as anything qualifies as necessary subgoal if $I \equiv \texttt{false}$, in which case (c) is also directly satisfied. So the properties (a)--(c) above are satisfied.
	
	\medskip
	{\it Case 2:  $\operatorname{Reach}(\mathcal{G})$ returns in line~\ref{line:safety wins}}. Then $\operatorname{Enf}(C,\mathcal{G})$ is unsatisfiable, where $C$ is the instantiation of the interpolant $\varphi$ (lines~\ref{line: phi} and \ref{line: subgoal}). 
 	\Cref{prop_necessary} states that $C$ is a necessary subgoal in $\mathcal{G}^I$. Since $\operatorname{Enf}(C,\mathcal{G})$ is unsatisfiable, \Cref{lem:avoidingC} states that $\mathfrak{S}_{\texttt{{SAFE}}{}} = \mathit{Safe} \land \lnot C$ is a winning symbolic strategy for $\texttt{{SAFE}}$ in $\mathcal{G}^I$. For \texttt{{REACH}}{}, we have the same argument as in Case 1. We conclude that the properties (a)--(c) above are satisfied.
	
	\medskip
	{\it Case 3:  $\operatorname{Reach}(\mathcal{G})$ returns in line~\ref{line:thirdreturn}}. By induction hypothesis we assume that the recursive call in line~\ref{line: recursion1} returned a tuple $(R_{post}, \mathfrak{S}_{\texttt{{REACH}}{}}^{post}, \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})$ satisfying properties (a)--(c) above for $\mathcal{G}_{post}$. We now show these properties in $\mathcal{G}$ for $R = \mathit{Init}\land\mathit{Goal}$, $\mathfrak{S}_{\texttt{{REACH}}{}} = \texttt{false}$, and $\mathfrak{S}_{\texttt{{SAFE}}{}} = \mathit{Safe} \land \neg F  \land (\varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})$, where $F= C \land \mathit{R}_{post}[\var/\varp]$.
	
	As in the previous cases, property (a) is satisfied. In order to prove (b) let $\rho = s_0 s_1 \ldots$ be a play such that $(\mathit{Init}\land\lnot R)(s_0)$ and $\mathit{Goal}(s_n)$ hold for some $n \in \mathbb{N}$. As $C$ is a necessary subgoal in $\mathcal{G}$, there exists $m \in \mathbb{N}$ with $m < n$ such that $C(s_m,s_{m+1})$ holds. Take $m$ to be the last index with this property.  If $F(s_m,s_{m+1})$ holds, then also $(F  \lor (\varphi \land \lnot\mathfrak{S}_{\texttt{{SAFE}}{}}^{post}))(s_m,s_{m+1})$, which implies $\lnot\mathfrak{S}_{\texttt{{SAFE}}{}}(s_m, s_{m+1})$. If $\lnot F(s_m,s_{m+1})$ holds, then $(\operatorname{Post}(C)[\varp/\var] \land \lnot R_{post})(s_{k+1})$ holds. By induction hypothesis, all winning plays for $\texttt{{REACH}}$ in $\mathcal{G}_{post}$ starting in $\lnot R_{post}$ have some $n > j > m$ such that $\lnot\mathfrak{S}_{\texttt{{SAFE}}{}}^{post}(s_j,s_{j+1})$ holds.
  Furthermore, by construction of $\mathcal{G}_{post}$, all states $s_j$ with $n > j > m$ satisfy $\varphi$.
  Hence $\varphi \land \lnot\mathfrak{S}^{post}_{\texttt{{SAFE}}{}}(s_j,s_{j+1})$ holds, which implies that $\lnot \mathfrak{S}_{\texttt{{SAFE}}}(s_j,s_{j+1})$ holds. We conclude that $\lnot\mathfrak{S}_{\texttt{{SAFE}}{}}$ is a necessary subgoal in $\mathcal{G}^I$.
	
	We now show (c). Since we return in  line~\ref{line:thirdreturn}, we have $\operatorname{Unsat}(\operatorname{Enf}(F,\mathcal{G}))$ and, by induction hypothesis, $\operatorname{Unsat}(\operatorname{Enf}(\lnot\mathfrak{S}_{\texttt{{SAFE}}{}}^{post},\mathcal{G}_{post}))$.
  As the transition relation of $\mathcal{G}_{post}$ is restricted to $\varphi$, this implies $\operatorname{Unsat}(\operatorname{Enf}(\varphi \land \lnot\mathfrak{S}_{\texttt{{SAFE}}{}}^{post},\mathcal{G}_{post}))$.
 We also have $F \implies \lnot \varphi$ and $(\varphi \land \lnot\mathfrak{S}_{\texttt{{SAFE}}{}}^{post}) \implies \varphi$. As $(\mathit{Safe}_{post} \lor \mathit{Reach}_{post}) \implies (\mathit{Safe} \lor \mathit{Reach})$ holds, we can apply \Cref{lem:unsat_sum} to conclude $\operatorname{Unsat}(\operatorname{Enf}(F  \lor (\varphi\land\lnot\mathfrak{S}_{\texttt{{SAFE}}{}}^{post})),\mathcal{G})$, which implies $\operatorname{Unsat}(\operatorname{Enf}(\neg \mathit{Safe} \lor F  \lor (\varphi\land\lnot\mathfrak{S}_{\texttt{{SAFE}}{}}^{post})),\mathcal{G}) = \operatorname{Unsat}(\operatorname{Enf}(\lnot\mathfrak{S}_{\texttt{{SAFE}}{}}),\mathcal{G}))$.
		
	\medskip
	{\it Case 4:  $\operatorname{Reach}(\mathcal{G})$ returns in line~\ref{line: last return} and the {\upshape\textbf{if}} statement in line~\ref{line:transback} is false}.
	By induction hypothesis we assume that the recursive calls in lines~\ref{line: recursion1} and \ref{line: recursion2} returned tuples $(R_{post}, \mathfrak{S}_{\texttt{{REACH}}{}}^{post}, \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})$ and $(R_{pre}, \mathfrak{S}_{\texttt{{REACH}}{}}^{pre}, \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre})$ satisfying properties (a)--(c) above for $\mathcal{G}_{post}$ and $\mathcal{G}_{pre}$. We now show these properties in $\mathcal{G}$ for $R\lor R_{pre}$, and 
	\begin{align*}
		\mathfrak{S}_{\texttt{{REACH}}{}} &=  \;\;(\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \implies \mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \\
  & \land \;\; ((\neg \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \land \operatorname{Pre}(F)) \implies F) \\
  & \land \;\; ((\neg \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \land \neg \operatorname{Pre}(F)) \implies \mathfrak{S}_{\texttt{{REACH}}{}}^{pre}) \\
    & \land \;\; (\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{post}) \lor \operatorname{Pre}(F) \lor \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}{}}^{pre})) \\
		\mathfrak{S}_{\texttt{{SAFE}}{}} &= (\neg \varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre}) \land (\varphi \implies \mathfrak{S}_{\texttt{{SAFE}}{}}^{post}),
	\end{align*} 
	with $F= C \land \mathit{R}_{post}[\var/\varp]$.

We first show that (a) $\mathfrak{S}_{\texttt{{REACH}}{}}$ is winning for \texttt{{REACH}}{} from states satisfying $R\lor R_{pre} \lor \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}})$. For states in $R$ this is trivial, so let  $\rho = s_0 s_1 \ldots$ be a play in $\mathcal{G}$ conforming to $\mathfrak{S}_{\texttt{{REACH}}{}}$ such that $R_{pre}(s_0)$ holds.
  Our first claim is that if there exists $k \in \mathbb{N}$ such that $\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{post})(s_k)$ holds, then $\rho$ must be winning for \texttt{{REACH}}{}.
  This is due to the fact that $\mathfrak{S}_{\texttt{{REACH}}}^{post}$ is winning in $\mathcal{G}_{post}$ from all states satisfying $\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{post})$, which allows us to use~\Cref{lem:gpost}.
  To argue that $\mathfrak{S}_{\texttt{{REACH}}}^{post}$ keeps playing according to $\mathfrak{S}_{\texttt{{REACH}}}^{post}$ once such a state is reached, we observe that if a symbolic reachability strategy $\mathfrak{S}$ wins from $s$, then $\operatorname{Pre}(\mathfrak{S})$ holds in any state in $S_{\texttt{{REACH}}}$ reachable from $s$ via a play prefix conforming to $\mathfrak{S}$, by definition.
  
  Now we show that such a position $k$ must exist.
  First, for $j \in \mathbb{N}$ such that $(\neg \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{post}) \land \operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G})))(s_j)$ holds, the transition $(s_j,s_{j+1})$ must satisfy $F$.
  This is because if $s_j \in S_{\texttt{{SAFE}}}$, then all outgoing transitions from $s_j$ satisfy $F$.
  Otherwise, it follows by the fact that $\rho$ conforms to $\mathfrak{S}_{\texttt{{REACH}}}$.
  As $\operatorname{Post}(F) \equiv R_{post}[\var/\varp]$ and $\mathfrak{S}_{\texttt{{REACH}}}^{pos}$ wins from all states satisfying $R_{post}$ by assumption, it follows that $s_{j+1}$ satisfies $\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{post})$.

  As long as $\rho$ visits only states satisfying $(\neg \operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G})) \land \neg \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{post}))$, the strategy $\mathfrak{S}_{\texttt{{REACH}}}$ prescribes to play according to $\mathfrak{S}_{\texttt{{REACH}}}^{pre}$.
  By assumption, this strategy is winning for \texttt{{REACH}}{} in $\mathcal{G}_{pre}$, and hence the play $\rho$ eventually visits a state in $\operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G}))$.
  As above, the play is guaranteed to stay in $\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{pre})$ until that position.

  The above argument also shows that $\mathfrak{S}_{\texttt{{REACH}}}$ is winning for all states satisfying $\operatorname{Pre}(F) \lor \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{post}) \lor \operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}}^{pre})$, which is implied by $\operatorname{Pre}(\mathfrak{S}_{\texttt{{REACH}}})$.
  Also, $\mathfrak{S}_{\texttt{{REACH}}} \implies (\mathit{Reach} \lor \mathit{Safe})$ is valid, as the corresponding statements hold for the pre- and post-strategies, and $F \implies (\mathit{Safe} \lor \mathit{Reach})$ is valid.



	

	 

	
	Next we show that (b) $\lnot \mathfrak{S}_{\texttt{{SAFE}}{}}$  is a necessary subgoal in $\mathcal{G}^I$.
	No player can play back from $\mathcal{G}_{post}$ to $\mathcal{G}_{pre}$ without $\texttt{{REACH}}$ having already won in $\mathcal{G}_{post}$. We first show that under this condition,
  \[\neg \mathfrak{S}_{\texttt{{SAFE}}} = (\neg \varphi \land \neg \mathfrak{S}_{\texttt{{SAFE}}{}}^{pre}) \lor (\varphi \land \neg \mathfrak{S}_{\texttt{{SAFE}}{}}^{post})\]
  qualifies as a necessary subgoal in $\mathcal{G}^I$. For this, consider the necessary subgoal $C$.
  For any play $\rho = s_0 s_1 \ldots$ with $n \in \mathbb{N}$ such that $\mathit{Goal}(s_n)$ there is some $k \in \mathbb{N}$ with $k < n$ and $C(s_k,s_{k+1})$. As $F$ characterizes a subset of $C$, we check two cases: Either (1) $\lnot F(s_k,s_{k+1})$ or (2) $F(s_k,s_{k+1})$. In case (1), we have $\lnot R_{post}(s_{k+1})$ and because of our assumption that no transition of the game satisfies $\varphi \land \neg \varphi'$, for all $j \in \mathbb{N}$ with $k < j < n: \varphi(s_j)$. It follows by induction hypothesis that there is some $l \in \mathbb{N}$ such that $\neg \mathfrak{S}_{\texttt{{SAFE}}}^{post}(s_l,s_{l+1})$.
  In case (2) we use that $\mathfrak{S}_{\texttt{{SAFE}}}^{pre}$ plays only moves available in $\mathcal{G}_{pre}$, and hence $\mathfrak{S}_{\texttt{{SAFE}}}^{pre} \implies \neg F$ is valid.
  Furthermore $F \implies \neg \varphi$, as $F$ characterizes a subset of the subgoal $C$.
  Hence we can conclude that $F \implies (\neg \varphi \land \neg \mathfrak{S}_{\texttt{{SAFE}}}^{pre})$ is valid.
  It follows that $\neg \mathfrak{S}_{\texttt{{SAFE}}}$ qualifies as necessary subgoal.

  Finally we show (c) that $\operatorname{Unsat}(\operatorname{Enf}(\neg \mathfrak{S}_{\texttt{{SAFE}}},\mathcal{G}))$ holds.
  We have $(\mathit{Safe}_{pre} \lor \mathit{Reach}_{pre}) \implies (\mathit{Safe} \lor \mathit{Reach})$ and $(\mathit{Safe}_{post} \lor \mathit{Reach}_{post}) \implies (\mathit{Safe} \lor \mathit{Reach})$. As $\operatorname{Pre}(\neg \varphi \land \neg \mathfrak{S}_{\texttt{{SAFE}}}^{pre}) \land \operatorname{Pre}(\varphi \land \neg \mathfrak{S}_{\texttt{{SAFE}}}^{post})$ is cleary unsatisfiable, we can again apply Lemma \ref{lem:unsat_sum} to infer $\operatorname{Unsat}(\operatorname{Enf}(\neg \mathfrak{S}_{\texttt{{SAFE}}},\mathcal{G}))$.
  This uses that any transitions reachable in $\mathcal{G}_{post}$ has to satisfy $\varphi$ in this case.
	
	\medskip
	{\it Case 5:  $\operatorname{Reach}(\mathcal{G})$ returns in line~\ref{line: last return} and the {\upshape\textbf{if}} statement in line~\ref{line:transback} is true}. 

	We  assume that both recursive calls terminated and, by induction, returned triples $(R_{post},\mathfrak{S}_{\texttt{{REACH}}}^{post},\mathfrak{S}_{\texttt{{SAFE}}}^{post})$ and $(R_{pre},\mathfrak{S}_{\texttt{{REACH}}}^{pre},\mathfrak{S}_{\texttt{{SAFE}}}^{pre})$ satisfying (a)-(c).

  (a) is shown exactly as in Case 4.

	For (b) we first observe that by setting $\varphi$ to $\texttt{false}$ (see line~\ref{line:tpostfalse}) in this case we get $\mathfrak{S}_{\texttt{{SAFE}}} = \mathfrak{S}_{\texttt{{SAFE}}}^{pre}$.
  We show that $\neg \mathfrak{S}_{\texttt{{SAFE}}} = \neg \mathfrak{S}_{\texttt{{SAFE}}}^{pre}$ is a necessary subgoal in $\mathcal{G}_I$.
  The transition predicate $F$ in line~\ref{line: recursion1} is a sufficient subgoal by induction hypothesis, but due to the restriction on the post-game, we cannot conclude that states in $\operatorname{Post}(C)$ that are not in $\operatorname{Post}(F)$ are winning for \texttt{{SAFE}}{}.
	By adding all transitions to $\mathit{Goal}$ (line~\ref{line: E2}) we get that $F$ in line~\ref{line: recursion2} is a necessary and sufficient subgoal (clearly, any winning play must go through $\mathit{Goal} [\var/\varp]$).
	As we have ensured that $F$ is necessary, we know for all plays $\rho = s_0 s_1 \ldots$ with some $n \in \mathbb{N}$ such that $\mathit{Goal}(s_n)$ there is some $k \in \mathbb{N}$ with $k < n$ and $F(s_k,s_{k+1})$. As in Case 4 we may conclude that $F \implies \neg \mathfrak{S}_{\texttt{{SAFE}}}^{pre}$.
It follows that $\neg \mathfrak{S}_{\texttt{{SAFE}}}$ is a necessary subgoal in $\mathcal{G}_I$.

For (c) we observe that $\operatorname{Unsat}(\operatorname{Pre}(\operatorname{Enf}(\neg \mathfrak{S}_{\texttt{{SAFE}}}^{pre},\mathcal{G}_{pre})))$ holds by induction hypothesis, which directly implies $\operatorname{Unsat}(\operatorname{Pre}(\operatorname{Enf}(\neg \mathfrak{S}_{\texttt{{SAFE}}}^{pre},\mathcal{G})))$. This concludes the argument for the final case, and the proof is complete.
	\qed

\end{proof}


\terminationfinite*
\begin{proof}
	We denote by $\operatorname{size}(\mathcal{G})$ the number of concrete transitions of $\mathcal{G}$, formally: $\operatorname{size}(\mathcal{G}) = |\{ (s,s') \in S \times S \mid (\mathit{Safe} \lor \mathit{Reach})(s,s') \text{ is valid}\}|$.
	If the domains of all variables are finite, then so is $\operatorname{size}(\mathcal{G})$.
	We assume that this is the case and show that the subgames on which $\operatorname{Reach}(\mathcal{G})$ recurses are strictly smaller in this measure.
	This is enough to guarantee termination.
	
	The first subgame is constructed in line~\ref{line:gpost} and takes the form:
	\[\mathcal{G}_{post} = \langle \operatorname{Post}(\mathit{C})[\varp/\var],\mathit{Safe} \land \varphi, \mathit{Reach} \land \varphi, \mathit{Goal} \rangle.\]
	The important restriction of this game is that both safety and reachability player transitions have the additional precondition $\varphi$.
	We may assume that $\operatorname{Enf}(C,\mathcal{G})$ is satisfiable, as otherwise the algorithm does not reach line~\ref{line:gpost}.
	Then, in particular, $C$ is satisfiable, by the definition of $\operatorname{Enf}(C,\mathcal{G})$.
	But $C = \operatorname{Instantiate}(\varphi,\mathcal{G}) = (\mathit{Safe} \lor \mathit{Reach}) \land \neg \varphi \land \varphi'$, which means that there exist states $s,s'$ such that $ (\mathit{Safe} \lor \mathit{Reach})(s,s')$, $\neg \varphi(s)$, and $\varphi(s')$ are all valid. 
	This transition from $s$ to $s'$ in $\mathcal{G}$ is excluded in $\mathcal{G}_{post}$, and as no new transitions are included, it follows that $\operatorname{size}(\mathcal{G}_{post}) < \operatorname{size}(\mathcal{G})$.
	
	The second subgame is constructed in line~\ref{line:gpre2} and takes the form:
	\[\mathcal{G}_{pre} = \langle I,\mathit{Safe} \land \lnot F,\mathit{Reach} \land \lnot F, \operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G}))\rangle.\]
  We may assume that $F \land (\mathit{Safe} \lor \mathit{Reach})$ is satisfiable, as otherwise the algorithm would not have moved past line~\ref{line:safeavoidsE}.
  Observe that if $F$ is changed in line~\ref{line: E2} then it is only extended and hence satisfiability is preserved.
  As no transition satisfying $F$ exists in $\mathcal{G}_{pre}$ it follows that $\operatorname{size}(\mathcal{G}_{pre}) < \operatorname{size}(\mathcal{G})$.
  This concludes the proof.
	\qed
\end{proof}

\terminationbisim*
\begin{proof}
	Let $S_1,\ldots,S_n$ be the bisimulation classes of $\mathcal{G}$, and $\psi_1, \ldots, \psi_n \in \cal L(\mathcal{V})$ be the formulas that define them.
	We define
	\[\operatorname{size}(\mathcal{G}) = |\{(S_i,S_j) \mid (\mathit{Safe} \lor \mathit{Reach}) \land \psi_i \land \psi_j' \text{ is satisfiable} \}|,\]
	which equals the number of transitions in the bisimulation quotient of $\mathcal{G}$ under $\sim$.
	Our aim is to show that $\operatorname{Reach}(\cdot)$ terminates for all subgames that are considered in any recursive call of $\operatorname{Reach}(\mathcal{G})$.
	
	To this end, we show that $\operatorname{Reach}(\mathcal{G})$ terminates for all reachability games $\mathcal{G} = \langle \mathit{Init}, \mathit{Safe}, \mathit{Reach}, \mathit{Goal} \rangle$ such that
	\begin{itemize}
	\item $\operatorname{size}(\mathcal{G})$ is finite,
  \item the relation $\sim$ is a bisimulation on $\mathcal{G}$, and
	\item $\mathit{Goal}$ is equivalent to a disjunction of formulas $\psi_i$.
	\end{itemize}
	We show this by induction on $\operatorname{size}(\mathcal{G})$.
	
	Let $\mathcal{G} = \langle \mathit{Init}, \mathit{Safe}, \mathit{Reach}, \mathit{Goal} \rangle$ satisfy these conditions, and assume that $\operatorname{size}(\mathcal{G}) = 0$.
	Then it follows that $\mathit{Safe} \lor \mathit{Reach}$ is unsatisfiable.
	This is because if any $(s_1,s_2)$ would satisfy $\mathit{Safe} \lor \mathit{Reach}$, then in particular $(\mathit{Safe} \lor \mathit{Reach}) \land \psi_i \land \psi_j'$ would be satisfied by $(s_1,s_2)$, where we assume $s_1 \in \S_i$ and $s_2 \in \S_j$.
	It follows that $\operatorname{Unsat}(\operatorname{Enf}(C,\mathcal{G}))$ in line~\ref{line: cpre} is true, as $\operatorname{Enf}(C,\mathcal{G}) \implies (\mathit{Safe} \lor \mathit{Reach})$ is valid for any $C$.
	But then Algorithm~\ref{alg:algreach} terminates on input $\mathcal{G}$.
	
	Now suppose that we have $\mathcal{G}$ with $\operatorname{size}(\mathcal{G}) > 0$.
	If the algorithm does not return in lines~\ref{line:ret1} or~\ref{line:safety wins}, we have to consider the first subgame
	\[\mathcal{G}_{post} = \langle \operatorname{Post}(C)[\varp/\var], \mathit{Safe} \land \varphi, \mathit{Reach} \land \varphi, \mathit{Goal} \rangle,\]
	which is constructed in line~\ref{line:gpost}.
	We may assume that for some $I \subseteq \{1,\ldots,n\}$ we have $\varphi \equiv \bigvee_{i \in I} \psi_i$, due to our assumption on the function $\operatorname{Interpolate}$.
	Hence the effect of restricting all transitions to $\varphi$ is to remove all transitions in states not in $\bigcup \{S_i \mid i \in I\}$, which are exactly the states in $\bigcup \{S_i \mid i \in \{1,\ldots,n\} \setminus I\}$.
	It is clear that $\sim$ is still a bisimulation in the resulting game, and that the goal states are preserved.
	To see that $\operatorname{size}(\mathcal{G}_{post}) < \operatorname{size}(\mathcal{G})$ we may assume that $\operatorname{Unsat}(\operatorname{Enf}(C,\mathcal{G}))$ is false, otherwise we would have returned in line~\ref{line:safety wins}.
	Then, in particular, there is a transition in $\mathcal{G}$ satisfying $\neg \varphi$, which means that there is a pair $S_i,S_j$ such that $(\mathit{Safe} \lor \mathit{Reach}) \land \neg \varphi \land \psi_i \land \psi_j'$ is satisfiable.
	This is cleary unsatisfiable when replacing $(\mathit{Safe} \lor \mathit{Reach})$ by $(\mathit{Safe} \lor \mathit{Reach}) \land \varphi$.
	Hence, $\operatorname{size}(\mathcal{G}_{post}) < \operatorname{size}(\mathcal{G})$.
	As a result, we can apply the induction hypothesis to conclude that the recursive call $\operatorname{Reach}(\mathcal{G}_{post})$ in line~\ref{line: recursion1} terminates.
	
	Now let us consider the second subgame $\mathcal{G}_{pre}$, as constructed in line~\ref{line:gpre2}.
	First, we observe that $F \equiv (\mathit{Safe} \lor \mathit{Reach}) \land \neg \varphi \land \varphi' \land R_{post}[\var/\varp]$, where $R_{post}$ is a state predicate characterizing the initial winning states of $\mathcal{G}_{post}$ (this uses~\Cref{thm:partcorr}).
	As $\sim$ is a bisimulation on $\mathcal{G}_{post}$, it follows by~\Cref{lem:bisimpreservesreach} that $R_{post}$ is equivalent to a disjunction of formulas $\psi_i$.
	As a consequence, we can equivalently write $F$ as $\phi_1 \land (\phi_2[\var/\varp])$ for two formulas $\phi_1,\phi_2 \in \cal L(\mathcal{V})$ that are both equivalent to disjunctions of $\psi_i$.
	By~\Cref{lem:preenfbisim} it follows that $\operatorname{Pre}(\operatorname{Enf}(E,\mathcal{G}))$ is also equivalent to a disjunction of $\psi_i$.
	
	Restricting transitions to $\neg F$ in $\mathcal{G}_{pre}$ has the effect of removing all transitions from states in $\bigcup\{S_i \mid \psi_i \implies \phi_1 \text{ is valid}\}$ to states in $\bigcup\{S_i \mid \psi_i \implies \phi_2  \text{ is valid}\}$.
	It is clear that $\sim$ is still a bisimulation in the resulting game.
	Furthermore, as $\operatorname{Enf}(F,\mathcal{G})$ is satisfiable, there is at least one such transition in $\mathcal{G}$.
	It follows that $\operatorname{size}(\mathcal{G}_{pre}) < \operatorname{size}(\mathcal{G})$ and hence the algorithm terminates by induction hypothesis.
	\qed
\end{proof}

\begin{lemma}
	\label{lem:preenfbisim}
	Let $\sim$ be a bisimulation on $\mathcal{G}$ which is also an equivalence relation, and $S_1,\ldots, S_n$ be its equivalence classes.
	Assume that $S_1,\ldots, S_n$ are defined by $\psi_1,\ldots, \psi_n \in \cal L(\mathcal{V})$.
	Let $\phi_1 \land (\phi_2[\var/\varp]) \in \cal L(\mathcal{V} \cup \mathcal{V'})$ be such that both $\phi_1,\phi_2$ are equivalent to disjunctions of formulas $\psi_i$.
	
	Then, $\operatorname{Pre}(\operatorname{Enf}(\phi_1 \land (\phi_2[\var/\varp]),\mathcal{G}))$ is equivalent to a disjunction of formulas $\psi_i$.
\end{lemma}
\begin{proof}
	We show that if there exists a state in $S_i$ that satisfies $\operatorname{Pre}(\operatorname{Enf}(\phi_1 \land (\phi_2[\var/\varp]),\mathcal{G}))$, then so do all states in $S_i$.
	Let $s_1 \in S_i$ be such that $\operatorname{Pre}(\operatorname{Enf}(\phi_1 \land (\phi_2[\var/\varp]),\mathcal{G}))(s_1)$ is valid.
	
	We make a case distinction on whether $s_1 \in S_{\texttt{{REACH}}}$ holds.
	If so, then there exists a state $q_1$ such that $(\mathit{Reach} \land \phi_1 \land (\phi_2[\var/\varp]))(s_1,q_1)$ is valid.
	In particular, $\phi_1(s_1)$ and $\phi_2(q_1)$ are both valid.
	Assuming that $q_1 \in S_j$ holds, both $\psi_i \implies \phi_1$ and $\psi_j \implies \phi_2$ are valid, as both $\phi_1$ and $\phi_2$ are equivalent to disjunctions of $\psi$-formulas (which have pairwise disjoint sets of models).
	Now take any other state $s_2 \in S_i$.
	As $s_1 \sim s_2$ and $\mathit{Reach}(s_1,q_1)$ is valid, there exists a state $q_2 \in S_j$ such that $\mathit{Reach}(s_2,q_2)$ is valid.
	Furthermore, as $\psi_i(s_2)$ and $\psi_j(q_2)$ are both valid, so is $(\mathit{Reach} \land \phi_1 \land (\phi_2[\var/\varp]))(s_2,q_2)$.
	Hence, $\operatorname{Pre}(\operatorname{Enf}(\phi_1 \land (\phi_2[\var/\varp]),\mathcal{G}))(s_2)$ is valid.
	
	Now assume that $s_1 \in S_{\texttt{{SAFE}}}$.
	Then, for all states $q_1$ such that $\mathit{Safe}(s_1,q_1)$ is valid, $(\phi_1 \land (\phi_2[\var/\varp]))(s_1,q_1)$ holds.
	Whenever this is the case, and $q_1 \in S_j$ holds, it follows that $\psi_j \implies \phi_2$ is valid.

	Now take any other state $s_2 \in S_i$ and assume, for contradiction, that there exists a $q_2$ such that $\mathit{Safe}(s_2,q_2)$ is valid, but not $(\phi_1 \land (\phi_2[\var/\varp]))(s_2,q_2)$.
	Assuming $q_2 \in S_j$, we have that $\psi_j \land \phi_2$ is unsatisfiable.
	As $s_1 \sim s_2$ holds, we find $q_1$ such that $\mathit{Safe}(s_1,q_1) \land \psi_j(q_1)$ is valid.
  By the previous reasoning, this would imply that $\psi_j \implies \phi_2$ is valid.
	This is a contradiction as $\psi_j$ is satisfiable.
	\qed
\end{proof}

\section{Conclusion}
Our work is a step towards the fully automated synthesis of software. 
It targets symbolically represented reachability games which are expressive enough to model a variety of problems, from common game benchmarks to program synthesis problems. 
The presented approach exploits causal information in the form of \emph{subgoals}, which are parts of the game that the reachability player needs to pass through in order to win.
Having computed a subgoal, which can be done using Craig interpolation, the game is split along the subgoal and solved recursively.
At the same time, the algorithm infers a structured symbolic strategy for the winning player.
The evaluation of our prototype implementation \textsc{CabPy} shows that our approach is practically applicable and scales much better than previously available tools on several benchmarks.  
While termination is only guaranteed for games with finite bisimulation quotient, the experiments demonstrate that several infinite games can be solved as well.

This work opens up several interesting questions for further research.
One concerns the quality of the returned strategies.
Due to its compositional nature, at first sight it seems that our approach is not well-suited to handle global optimization criteria, such as reaching the goal in fewest possible steps.
On the other hand, the returned strategies often involve only a few key decisions and we believe that therefore the strategies are often very sparse, although this has to be further investigated.
We also plan to automatically extract deterministic strategies from the symbolic ones~\cite{Bloem,Ehlers} we currently consider.

Another question regards the computation of subgoals. 
The performance of our algorithm is highly influenced by which interpolant is returned by the solver.
In particular this affects the number of subgames that have to be solved, and how complex they are.
We believe that template-based interpolation \cite{template_interpolation} could be a promising candidate to explore with the goal to compute good interpolants. 
This could be combined with the possibility for the user to provide templates or expressive interpolants directly, thereby benefiting from the user's domain knowledge.
	
	
	
	
	
	
	

\section{Motivating Example} \label{sec:motivation}

Consider the scenario that an expensive painting is displayed in a large exhibition room of a museum.
It is secured with an alarm system that is controlled via a control panel on the opposite side of the room.
A security guard is sleeping at the control panel and occasionally wakes up to check whether the alarm is still armed.
To steal the painting, a thief first needs to disable the alarm and then reach the painting before the alarm has been reactivated. We model this scenario as a two-player game between a safety player (the guard) and a reachability player (the thief) in the theory of linear arithmetic.
The moves of both players, their initial positions, and the goal condition are described by the formulas:


\iffalse
\begin{figure}[t]
	\centering
	\scalebox{0.4}{
		\begin{tikzpicture}[node distance=2cm]
		\node(mona) at (10,5){\def\svgwidth{1cm}\input{monalisa_color.pdf_tex}};
		\node(thief) at (0,0){\def\svgwidth{1.15cm}\input{thief_color.pdf_tex}};
		\node(guard) at (0,10){\def\svgwidth{2cm}\input{guard2_color.pdf_tex}};
		\draw[step=2.0,black,thin] (-0.5,-0.5) grid (10.5,10.5);
		\node(guard) at (-1,0.0){$0$};
		\node(guard) at (0,-1){$0$};
		\node(guard) at (10.0,-1){$10$};
		\node(guard) at (-1,10.0){$10$};
		\end{tikzpicture}}
	\caption{The Mona Lisa problem. The painting is secured with an alarm the thief has to disable first in order to remain undetected. The sleeping guard will occasionally wake up to check whether the alarm is still on.}
	\label{exp_monalisa_pic}
\end{figure}
\fi


\begin{align*}
\mathit{Init} &\equiv && \lnot \mathbf{r} \land x = 0 \land y = 0 \land p = 0 \land a = 1 \land t = 0, &&&\\
\mathit{Guard} &\equiv &&\neg\mathbf{r} \land \mathbf{r}' \land x' = x \land y' = y \land p' = p  &&&\\
& &&\land ((t' = t - 1 \land a' = a)\lor (t \leq 0 \land t' = 2)),&&&(\text{sleep or wake up})\\
\mathit{Thief} &\equiv &&  \mathbf{r} \land \neg\mathbf{r}' \land t' = t \\
	&&&\land x + 1 \ge x' \ge x - 1 \land y + 1 \ge y' \ge y - 1&&&(\text{move})\\
& &&\land (x' \neq 0 \lor y' \neq 10 \implies a' = a)&&&(\text{alarm off})\\
& &&\land (x' \neq 10 \lor y' \neq 5 \lor a = 1 \implies p' = p),&&&(\text{steal})\\
\mathit{Goal} &\equiv && \lnot \mathbf{r} \land p = 1. &&&
\end{align*} 

The thief's position in the room is modeled by two coordinates $x,y \in \mathbb{R}$ with initial value $(0,0)$, and with every transition the thief can move some bounded distance. 
Note that we use primed variables to represent the value of variables after taking a transition.
The control panel is located at $(0,10)$ and the painting at $(10,5)$. 
The status of the alarm and the painting are described by two boolean variables $a,p \in \{0,1\}$. 
The guard wakes up every two time units, modeled by the variable $t \in \mathbb{R}$. 
The variables $x,y$ are bounded to the interval $[0,10]$ and $t$ to $[0,2]$. 
The boolean variable \textbf{r} encodes who makes the next move. 
In the presented configuration, the thief needs more time to move from the control panel to the painting than the guard will sleep. 
It follows that there is a winning strategy for the guard, namely, to always reactivate the alarm upon waking up.

Although it is intuitively fairly easy to come up with this strategy for the guard, it is surprisingly hard for game solving tools to find it. The main obstacle is the infinite state space of this game.
Our approach for solving games represented in this logical way imitates \emph{causal reasoning}: 
Humans observe that in order for the thief to steal the painting (i.e., the effect $p=1$), a transition must have been taken whose source state does not satisfy the pre-condition of (steal) while the target state does.  
Part of this cause is the condition $a=0$, i.e., the alarm is off. Recursively, in order for the effect $a=0$ to happen, a transition setting $a$ from $1$ to $0$ must have occurred, and so on. 

Our approach captures these cause-effect relationships through the notion of \emph{necessary subgoals}, which are essential milestones that the reachability player has to transition through in order to achieve their goal.
The first necessary subgoal corresponding to the intuitive description above is
$$C_1 = (\mathit{Guard} \lor \mathit{Thief}) \land p \neq 1 \land p' = 1.$$
In this case, it easy to see that $C_1$ is also a \emph{sufficient subgoal}, meaning that all successor states of $C_1$ are winning for the thief. Therefore, it is enough to solve the game with the modified objective to reach those predecessor states of $C_1$ from which the thief can \emph{enforce} $C_1$ being the next move (even if it is not their turn). Doing so recursively produces the necessary subgoal
$$C_2 = (\mathit{Guard} \lor \mathit{Thief}) \land a \neq 0 \land a' = 0,$$
meaning that some transition must have caused the effect that the alarm is disabled. However, $C_2$ is \emph{not} sufficient which can be seen by recursively solving the game spanning from successor states of $C_2$ to $C_1$. This computation has an important caveat: After passing through $C_2$, it may happen that $a$ is reset to $1$ at a later point (in this particular case, this constitutes precisely the winning strategy of the safety player), which means that there is no canonical way to slice the game along this subgoal into smaller parts. Hence the recursive call solves the game from $C_2$ to $C_1$ \emph{subject to} the bold assumption that any move from $a = 0$ to $a' = 1$ is winning for the guard. This generally underapproximates the winning states of the thief. Remarkably, we show that this approximation is enough to build winning strategies for \emph{both} players from their respective winning regions. In this case, it allows us to infer that moving through $C_2$ is always a losing move for the thief. However, at the same time, any play reaching $\mathit{Goal}$ has to move through $C_2$. It follows that the thief loses the global game.

We evaluated our method on several configurations of this game, which we call \emph{Mona Lisa}. The results in Section \ref{sec:experiments} support our conjecture that the room size has little influence on the time our technique needs to solve the game.

\section{Case Studies}
\label{sec:experiments}

In this section we evaluate our approach on a number of case studies. 
Our prototype \textsc{CabPy}{}\footnote[2]{The source code of \textsc{CabPy}{} and our experimental data are both available at \url{https://github.com/reactive-systems/cabpy}. We provide a virtual machine image with \textsc{CabPy}{} already installed for reproducing our evaluation~\cite{VM}.} is written in Python and implements the game solving part of the presented algorithm. 
Extending it to returning a symbolic strategy using the ideas outlined above is straightforward.
We compared our prototype with \textsc{SimSynth} \cite{FarzanK17}, the only other readily available tool for solving linear arithmetic games. 
The evaluation was carried out with Ubuntu 20.04,  a 4-core Intel\textsuperscript{\textregistered} Core\texttrademark~i5 2.30GHz processor, as well as 8GB of memory. \textsc{CabPy}{} uses the PySMT~\cite{pysmt2015} library as an interface to the MathSAT5~\cite{mathsat5} and Z3~\cite{z3solver} SMT solvers.
On all benchmarks, the timeout was set to 10 minutes. In addition to the winner, we report the runtime and the number of subgames our algorithm visits. Both may vary with different SMT solvers or in different environments.
\subsection{Game of Nim}

Game of Nim is a classic game from the literature \cite{Bouton1901} and played on a number of heaps of stones. Both players take turns of choosing a single heap and removing at least one stone from it. We consider the version where the player that removes the last stone wins. Our results are shown in \Cref{exp_nim}. In instances with three heaps or more we bounded the domains of the variables in the instance description, by specifying that no heap exceeds its initial size and does not go below zero.

Following the discussion in \Cref{sec:termination}, we need to bound the domains to ensure the termination of our tool on these instances.
Remarkably, bounding the variables was not necessary for instances with only two heaps, where our tool \textsc{CabPy}{} scales to considerably larger instances than \textsc{SimSynth}.
We did not add the same constraints to the input of \textsc{SimSynth}{}, as for \textsc{SimSynth}{} this resulted in longer runtimes rather than shorter.
In Game of Nim, there are no natural necessary subgoals that the safety player can locally control.

The results (see~\Cref{exp_nim}) demonstrate that our approach is not completely dependent on finding the right interpolants and is in particular also competitive when the reachability player wins the game. We suspect that \textsc{SimSynth}{} performs worse in these cases because the safety player has a large range of possible moves in most states, and inferring the win of the reachability player requires the tool to backtrack and try our all of them.

\begin{figure}[tbp]
	\centering
	{\def\arraystretch{1.1}\tabcolsep=5pt
    \small
		\begin{tabular}{|c|c|c|c|c|}
			\hline
			& \multicolumn{2}{c|}{\textsc{CabPy}} & \textsc{SimSynth} & \\
			\hline
			Heaps & Subgames & Time(s) &Time(s) & Winner\\
			\hline
			(4,4) & 19 & 1.50 & 10.44 & $\texttt{{REACH}}$\\
			(4,5) & 23 & 1.92 & 12.74 & $\texttt{{SAFE}}$\\
			(5,5) & 23 & 1.99 & 85.75 & $\texttt{{REACH}}$\\
			(5,6) & 27 & 2.90 & 91.66 & $\texttt{{SAFE}}$\\
			(6,6) & 28 & 3.04 & Timeout & $\texttt{{REACH}}$\\
			(6,7) & 31 & 3.76 & Timeout & $\texttt{{SAFE}}$\\
			(20,20) & 88 & 94.85 & Timeout & $\texttt{{REACH}}$\\
			(20,21) & 94 & 113.04 & Timeout & $\texttt{{SAFE}}$\\
			(30,30) & 128 & 364.13 & Timeout & $\texttt{{REACH}}$\\
			(30,31) & 135 & 404.02 & Timeout & $\texttt{{SAFE}}$\\\hline
			(3,3,3)b & 23 & 13.63 & 2.85 & $\texttt{{SAFE}}$\\
			(1,4,5)b & 32 & 7.00 & 289.85 & $\texttt{{REACH}}$\\
			(4,4,4)b & 33 & 50.55 & 24.39 & $\texttt{{SAFE}}$\\
			(2,4,6)b & 38 & 19.77 & Timeout & $\texttt{{REACH}}$\\
			(5,5,5)b & 33 & 127.89 & 162.50 & $\texttt{{SAFE}}$\\
			(3,5,6)b & 40 & 86.56 & Timeout & $\texttt{{REACH}}$\\\hline
			(2,2,2,2)b & 39 & 84.79 & 213.79 & $\texttt{{REACH}}$\\
			(2,2,2,3)b & 41 & 102.01 & Timeout & $\texttt{{SAFE}}$\\
			\hline
	\end{tabular}}
	\caption{Experimental results for the Game of Nim. The notation $(h_1,\ldots, h_n)$ denotes the instance played on $n$ heaps, each of which consists of $h_i$ stones. Instances marked with b indicate that the variable domains were explicitly bounded in the input for \textsc{CabPy}{}.}
	\label{exp_nim}
\end{figure}


\begin{figure}[tbp]
	\centering
	{\def\arraystretch{1.1}\tabcolsep=5pt
    \small
		\begin{tabular}{|c|c|c|c|c|}
			\hline
			& \multicolumn{2}{c|}{\textsc{CabPy}} & \textsc{SimSynth} & \\
			\hline
			$r$ & Subgames & Time(s) &Time(s) & Winner\\
			\hline
			10 & 10 & 0.57 & 3.93 & $\texttt{{SAFE}}$\\
			20 & 20 & 1.23 & 20.48 & $\texttt{{SAFE}}$\\
			40 & 40 & 3.42 & 121.96 & $\texttt{{SAFE}}$\\
			60 & 60 & 7.36 & Timeout & $\texttt{{SAFE}}$\\
			80 & 80 & 17.72 & Timeout & $\texttt{{SAFE}}$\\
			100 & 100 & 26.36 & Timeout & $\texttt{{SAFE}}$\\
			\hline
	\end{tabular}}
	\caption{Experimental results for the Corridor game. The safety player controls the door between rooms $r-1$ and $r$.}
	\label{exp_corridor}
\end{figure}

\subsection{Corridor}

We now consider an example that demonstrates the potential of our method in case the game structure contains natural bottlenecks. Consider a corridor of $100$ rooms arranged in sequence, i.e., each room $i$ with $0 \leq i < 100$ is connected to room $i+1$ with a door. The objective of the reachability player is to reach room 100 and they are free to choose valid values from $\mathbb{R}^2$ for the position in each room at every other turn. The safety player controls some door to a room $r \leq 100$. Naturally, a winning strategy is to prevent the reachability player from passing that door, which is a natural bottleneck and necessary subgoal on the way to the last room.

 The experimental results are summarized in Figure \ref{exp_corridor}. We evaluated several versions of this game, increasing the length from the start to the controlled door. The results confirm that our causal synthesis algorithm finds the trivial strategy of closing the door quickly. This is because Craig interpolation focuses the subgoals on the room number variable while ignoring the movement in the rooms in between, as can be seen by the number of considered subgames. \textsc{SimSynth}, which tries to generalize a strategy obtained from a step-bounded game, struggles because the tool solves the games that happen between each of the doors before reaching the controlled one.

\subsection{Mona Lisa}

The game described in Section \ref{sec:motivation} between a thief and a security guard is very well suited to further assess the strength and limitations of both our approach as well as of \textsc{SimSynth}{}. We ran several experiments with this scenario, scaling the size of the room and the sleep time of the guard, as well as trying a scenario where the guard does not sleep at all. Scaling the size of the room makes it harder for \textsc{SimSynth}{} to solve this game with a forward unrolling approach, while our approach extracts the necessary subgoals irrespective of the room size. However, scaling the guard's sleep time makes it harder to solve the subgame between the two necessary subgoals, while it only has a minor effect on the length of the unrolling needed to stabilize the play in a safe region, as done by \textsc{SimSynth}.

 The results in Figure \ref{exp_monalisa} support this conjecture. The size of the room has \emph{almost no effect at all} on both the runtime of \textsc{CabPy}{} and the number of considered subgames. However, as the results for a sleep value of 4 show, the employed combination of quantifier elimination and interpolation introduces some instability in the produced formulas. This means we may get different Craig interpolants and slice the game with more or less subgoals. Therefore, we see a lot of potential in optimizing the interplay between the employed tools for quantifier elimination and interpolation. The phenomenon of the runtime being sensitive to these small changes in values is also seen with \textsc{SimSynth}, where a longer sleep time sometimes means a faster execution.

\begin{figure}[tbp]
	\centering
    {\def\arraystretch{1.1}\tabcolsep=5pt
      \small
		\begin{tabular}{|c|c|c|c|c|c|}
			\hline
			&  & \multicolumn{2}{c|}{\textsc{CabPy}} & \textsc{SimSynth} & \\
			\hline
			Size & Sleep & Subgames & Time(s) & Time(s) & Winner\\
			\hline
			$10\times10$ & - & 7 & 0.61 & 4.79 & $\texttt{{SAFE}}$\\
			$20\times20$ & - & 7 & 0.60 & 25.26 & $\texttt{{SAFE}}$\\
			$40\times40$ & - & 7 & 0.61 & 157.62 & $\texttt{{SAFE}}$\\
			\hline
			$10\times10$ & 1 & 10 & 4.22 & 20.31 & $\texttt{{SAFE}}$\\
			$20\times20$ & 1 & 11 & 4.34 & 36.44 & $\texttt{{SAFE}}$\\
			$40\times40$ & 1 & 11 & 4.65 & 226.14 & $\texttt{{SAFE}}$\\
			\hline
			$10\times10$ & 2 & 13 & 5.88 & 7.40 & $\texttt{{SAFE}}$\\
			$20\times20$ & 2 & 14 & 5.98 & 60.00 & $\texttt{{SAFE}}$\\
			$40\times40$ & 2 & 13 & 5.92 & 270.48 & $\texttt{{SAFE}}$\\
			\hline
			$10\times10$ & 3 & 18 & 26.58 & 13.94 & $\texttt{{SAFE}}$\\
			$20\times20$ & 3 & 17 & 26.19 & 115.53 & $\texttt{{SAFE}}$\\
			$40\times40$ & 3 & 18 & 27.85 & 290.12 & $\texttt{{SAFE}}$\\
			\hline
			$10\times10$ & 4 & 30 & 175.27 & 13.96 & $\texttt{{SAFE}}$\\
			$20\times20$ & 4 & 22 & 204.79 & 60.08 & $\texttt{{SAFE}}$\\
			$40\times40$ & 4 & 27 & 123.95 & 319.47 & $\texttt{{SAFE}}$\\
			\hline
	\end{tabular}}
	\caption{Experimental results for the Mona Lisa game.}
	\label{exp_monalisa}
\end{figure}

\subsection{Program Synthesis}

Lastly, we study two benchmarks that are directly related to program synthesis. 
The first problem is to synthesize a controller for a thermostat by filling out an incomplete program, as described in \cite{BeyeneCPR14}. A range of possible initial values of the room temperature $c$ is given, e.g., $20.8 \leq c \leq 23.5$, together with the temperature dynamics which depend on whether the heater is on (variable $o \in \mathbb{B}$).
The objective for $\texttt{{SAFE}}$ is to control the value of $o$ in every round such that $c$ stays between $20$ and $25$. This is a common benchmark for program synthesis tools and both \textsc{CabPy}{} and \textsc{SimSynth}{} solve it quickly.
The other problem relates to Lamport's bakery algorithm\cite{Lamport1974}. We consider two processes using this protocol to ensure mutually exclusive access to a shared resource. The game describes the task of synthesizing a scheduler that violates the mutual exclusion. This essentially is a model checking problem, and we study it to see how well the tools can infer a safety invariant that is out of control of the safety player. For our approach, this makes no difference, as both players may play through a subgoal and the framework is well suited to find a safety invariant. The forward unrolling approach of \textsc{SimSynth}, however, seems to explore the whole state space before inferring safety, and fails to find an invariant before a timeout. 

\begin{figure}[tbp]
	\centering
	{\def\arraystretch{1.1}\tabcolsep=5pt
    \small
		\begin{tabular}{|c|c|c|c|c|}
			\hline
			& \multicolumn{2}{c|}{\textsc{CabPy}} & \textsc{SimSynth} & \\
			\hline
			Name & Subgames & Time(s) &Time(s) & Winner\\
			\hline
			Thermostat & 6 & 0.44 & 0.39 & $\texttt{{SAFE}}$ \\
			Bakery & 46 & 18.25 & Timeout & $\texttt{{SAFE}}$ \\
			\hline
	\end{tabular}}
	\caption{Experimental results for program synthesis problems.}
	\label{exp_synth}
\end{figure}




\section{Introduction}
Two-player games are a fundamental model in logic and verification due to their connection to a wide range of topics such as decision procedures, synthesis and control~\cite{Harding05,Alur15,Alur16,BLOEM2012911,BLOEM20073,6225075}. 
Algorithmic techniques for \emph{finite-state} two-player games have been studied extensively for many acceptance conditions~\cite{GraedelTW2002}.
For \emph{infinite-state} games most problems are directly undecidable. 
However, infinite state spaces occur naturally in domains like software synthesis~\cite{RyzhykCKLH09} and cyber-physical systems~\cite{JessenRLD07}, and hence handling such games is of great interest. 
An elegant classification of infinite-state games that can be algorithmically handled, depending on the acceptance condition of the game, was given in~\cite{deAlfaroHM2001}.
The authors assume a symbolic encoding of the game in a very general form.
More recently, incomplete procedures for solving infinite-state two-player games specified using logical constraints were studied~\cite{BeyeneCPR14,FarzanK17}.
While~\cite{BeyeneCPR14} is based on automated theorem-proving for Horn formulas and handles a wide class of acceptance conditions, the work in~\cite{FarzanK17} focusses on reachability games specified in the theory of linear arithmetic, and uses sophisticated decision procedures for that theory.

In this paper, we present a novel technique for solving logically represented reachability games based on the notion of \emph{subgoals}.
A \emph{necessary} subgoal is a transition predicate that is satisfied at least once on every play that reaches the overall goal.
It represents an intermediate target that the reachability player must reach in order to win. Subgoals open up game solving to the study of cause-effect relationships in the form of counterfactual reasoning~\cite{counterfactual}: If a cause (the subgoal) had not occurred, then the effect (reaching the goal) would not have happened.
Thus for the safety player, a necessary subgoal provides a chance to win the game based on local information:
If they control all states satisfying the pre-condition of the subgoal, then any strategy that in these states picks a transition outside of the subgoal is  winning. 
Finding such a necessary subgoal may let us conclude that the safety player wins without ever having to unroll the transition relation.

On the other hand, passing through a necessary subgoal is in general not enough for the reachability player to win. We call a subgoal \emph{sufficient} if indeed the reachability player has a winning strategy from every state satisfying the post-condition of the subgoal.
Dual to the description in the preceding paragraph, sufficient subgoals provide a chance for the reachability player to win the global game as they must merely reach this intermediate target. The two properties differ in one key aspect: While necessity of a subgoal only considers the paths of the game arena, for sufficiency the game structure is crucial.  

We show how Craig interpolants can be used to compute necessary subgoals, making our methods applicable to games represented by any logic that supports interpolation. In contrast, determining whether a subgoal is sufficient requires a partial solution of the given game. This motivates the following recursive approach. We slice the game along a necessary subgoal into two parts, the pre-game and the post-game.
In order to guarantee these games to be smaller, we solve the post-game under the assumption that the considered subgoal was bridged \emph{for the last time}.
We conclude that the safety player wins the overall game if they can avoid all initial states of the post-game that are winning for the reachability player.
Otherwise, the pre-game is solved subject to the winning condition given by the sufficient subgoal consisting of these states. 
This approach does not only determine which player wins from each initial state, but also computes symbolically represented winning strategies with a causal structure. 
Winning safety player strategies induce necessary subgoals that the reachability player cannot pass, which constitutes a cause for their loss. Winning reachability player strategies represent a sequence of sufficient subgoals that will be passed, providing an explanation for the win.

The Python-based implementation \textsc{CabPy}{} of our approach was used to compare its performance to \textsc{SimSynth} \cite{FarzanK17}, which is, to the best of our knowledge, the only other available tool for solving linear arithmetic reachability games. Our experiments demonstrate that our algorithm is competitive in many case studies. We can also confirm the expectation that our approach heavily benefits from qualitatively expressive Craig interpolants. It is noteworthy that like \textsc{SimSynth}{} our approach is fully automated and does not require any input in the form of hints or templates. 
Our contributions are summarized as follows:
\begin{itemize}[topsep=0.5ex]
	\item We introduce the concept of \emph{necessary} and \emph{sufficient subgoals} and show how Craig interpolation can be used to compute necessary subgoals (\Cref{sec:subgoals}).
	\item We describe an algorithm for solving logically represented two-player reachability games using these concepts.
    We also discuss how to compute representations of winning strategies in our approach (\Cref{sec:gamesolving}).
	\item We evaluate our approach experimentally through our Python-based tool \textsc{CabPy}, demonstrating a competitive performance compared to the previously available tool \textsc{SimSynth}{} on various case studies (\Cref{sec:experiments}).
\end{itemize}

\textbf{Related Work. } 
The problem of solving linear arithmetic games is addressed in~\cite{FarzanK17} using an approach that relies on a dedicated decision procedure for quantified linear arithmetic formulas, together with a method to generalize safety strategies from truncated versions of the game  that end after a prescribed number of rounds.
Other approaches for solving infinite-state games include deductive methods that compute the winning regions of both players using proof rules~\cite{BeyeneCPR14}, 
predicate abstraction where an abstract controlled predecessor operation is used on the abstract game representation~\cite{WalkerR14}, 
and symbolic BDD-based exploration of the state space~\cite{Edelkamp2002}. 
Additional techniques are available for finite-state games, e.g., generalizing winning runs into a winning strategy for one of the players~\cite{NarodytskaLBRW14}. 

Our notion of subgoal is related to the concept of landmarks as used in planning~\cite{HoffmannPS11}. Landmarks are milestones that must be true on every successful plan, and they can be used to decompose a planning task into smaller sub-tasks. 
Landmarks have also been used in a game setting to prevent the opponent from reaching their goal using counter-planning~\cite{PozancoEFB18}. 
Whenever a planning task is unsolvable, one method to find out why is checking hierarchical abstractions for solvability and finding the components causing the problem~\cite{SreedharanSSK19}. 

Causality-based approaches have also been used for model checking of multi-threaded concurrent programs~\cite{DBLP:conf/concur/KupriyanovF13,DBLP:conf/cav/KupriyanovF14}. 
In our approach, we use Craig interpolation to compute the subgoals. 
Interpolation has already been used in similar contexts before, for example to extract winning strategies from game trees~\cite{EenLNR15} or to compute new predicates to refine the game abstractions~\cite{SlicingAbstractions}. 
In ~\cite{FarzanK17}, interpolation is used to synthesize concrete winning strategies from so called \emph{winning strategy skeletons}, which describe a set of strategies of which at least one is winning.



\section{Preliminaries}
\label{sec:prelims}
We consider two-player reachability games defined by formulas in a given logic $\cal L$.
We let $\cal L(\mathcal{V})$ be the $\cal L$-formulas over a finite set of variables $\mathcal{V}$, also called \emph{state predicates} in the following.
We call $\mathcal{V'} = \{\mathit{v'} \mid \mathit{v} \in \mathcal{V}\}$ the set of \emph{primed variables}, which are used to represent the value of variables after taking a transition.
Transitions are expressed by formulas in the set $\cal L(\mathcal{V} \cup \mathcal{V'})$, called \emph{transition predicates}.
For some formula $\varphi \in \cal L(\mathcal{V})$, we denote the substitution of all variables by their primed variant by $\varphi[\var/\varp]$. Similarly, we define $\varphi[\varp/\var]$.

For our algorithm we will require the satisfiability problem of $\cal L$-formulas to be decidable and \emph{Craig interpolants} \cite{Craig1957} to exist for any two mutually unsatisfiable formulas.
Formally, we assume there is a function $\operatorname{Sat} : \cal L(\mathcal{V}) \to \mathbb{B}$ that checks the satisfiability of some formula $\varphi \in \cal L(\mathcal{V})$ and an unsatisfiability check $\operatorname{Unsat} : \cal L(\mathcal{V}) \rightarrow \mathbb{B}$. 
For interpolation, we assume that there is a function $\operatorname{Interpolate} : \cal L(\mathcal{V}) \times \cal L(\mathcal{V}) \to \cal L(\mathcal{V})$ computing a \emph{Craig interpolant} for mutually unsatisfiable formulas: If $\varphi ,\psi \in \cal L(\mathcal{V})$ are such that $\operatorname{Unsat}(\varphi\land\psi)$ holds, then $\psi \implies \operatorname{Interpolate}(\varphi,\psi)$ is valid, $\operatorname{Interpolate}(\varphi,\psi)\land \varphi$ is unsatisfiable, and $\operatorname{Interpolate}(\varphi,\psi)$ only contains variables shared by $\varphi$ and $\psi$.

These functions are provided by many modern \emph{Satisfiability Modulo Theories} (SMT) solvers, in particular for the theories of linear integer arithmetic and linear real arithmetic, which we will use for all our examples. Note that interpolation is usually only supported for the quantifier-free fragments of these logics, while our algorithm will introduce existential quantifiers.
Therefore, we resort to quantifier elimination wherever necessary, for which there are known procedures for both linear integer arithmetic and linear real arithmetic formulas~\cite{presburger1929uber,Monniaux2008}.

In order to distinguish the two players, we will assume that a Boolean variable called $\mathbf{r} \in \mathcal{V}$ exists, which holds exactly in the states controlled by the reachability player.
For all other variables $v \in \mathcal{V}$, we let $\mathcal{D}(v)$ be the domain of $v$, and we define $\mathcal{D} = \bigcup \{\mathcal{D}(v) \mid v \in \mathcal{V}\}$.
In the remainder of the paper, we consider the variables $\mathcal{V}$ and their domains to be fixed.

\begin{definition}[Reachability Game]
	A reachability game is defined by a tuple $\G = \langle \init, \safe, \reach, \goal \rangle${}, where $\mathit{Init} \in \cal L(\mathcal{V})$ is the \emph{initial condition}, $\mathit{Safe} \in \cal L(\mathcal{V} \cup \mathcal{V'})$ defines the transitions of player $\texttt{{SAFE}}$, $\mathit{Reach} \in \cal L(\mathcal{V} \cup \mathcal{V'})$ defines the transitions of player $\texttt{{REACH}}$ and $\mathit{Goal} \in \cal L(\mathcal{V})$ is the \emph{goal condition}.

  We require the formulas $(\mathit{Safe} \implies \neg \mathbf{r})$ and $(\mathit{Reach} \implies \mathbf{r})$ to be valid.
\end{definition}

A \emph{state} $s$ of $\mathcal{G}$ is a valuation of the variables $\mathcal{V}$, i.e., a function $s\colon\mathcal{V} \to \mathcal{D}$ that satisfies $s(v) \in \mathcal{D}(v)$ for all $v \in \mathcal{V}$.
We denote the set of states by $S$, and we let $S_\texttt{{SAFE}}$ be the states $s$ such that $s(\mathbf{r}) = \texttt{false}$, and $S_\texttt{{REACH}}$ be the states $s$ such that $s(\mathbf{r}) = \texttt{true}$. The variable $\mathbf{r}$ determines whether \texttt{{REACH}}{} or \texttt{{SAFE}}{} makes the move out of the current state, and in particular $\mathit{Safe} \land \mathit{Reach}$ is unsatisfiable. 

Given a state predicate $\varphi \in \cal L(\mathcal{V})$, we denote by $\varphi(s)$ the closed formula we get by replacing each occurrence of variable $v \in \mathcal{V}$ in $\varphi$ by $s(v)$.
Similarly, given a transition predicate $\tau \in \cal L(\mathcal{V} \cup \mathcal{V'})$ and states $s,s'$, we let $\tau(s,s')$ be the formula we obtain by replacing all occurrences of $v \in \mathcal{V}$ in $\tau$ by $s(v)$, and all occurrences of $v' \in \mathcal{V'}$ in $\tau$ by $s'(v)$. For replacing only $v \in \mathcal{V}$ by $s(v)$, we define $\tau(s)\in\cal L(\mathcal{V}')$. A \emph{trap state} of $\mathcal{G}$ is a state $s$ such that $(\mathit{Safe} \lor \mathit{Reach})(s)\in\cal L(\mathcal{V}')$ is unsatisfiable (i.e., $s$ has no outgoing transitions).

A \emph{play} of $\mathcal{G}$ starting in state $s_0$ is a finite or infinite sequence of states $\rho = s_0 s_1 s_2 \ldots \in \S^+ \cup \S^\omega$ such that for all $i < \operatorname{len}(\rho)$ either $\mathit{Safe}(s_i,s_{i+1})$ or $\mathit{Reach}(s_i,s_{i+1})$ is valid, and if $\rho$ is a finite play, then $s_{\operatorname{len}(\rho)}$ is required to be a trap state.
Here, $\operatorname{len}(s_0\ldots s_n) = n$ for finite plays, and $\operatorname{len}(\rho) = \infty$ if $\rho$ is an infinite play. The set of plays of some game $\G = \langle \init, \safe, \reach, \goal \rangle${} is defined as $\operatorname{Plays}(\mathcal{G}) = \{\rho = s_0 s_1 s_2 \ldots \mid \rho\text{ is a play in } \mathcal{G} \text{ s.t. } \mathit{Init}(s_0)\text{ holds} \}$.
$\texttt{{REACH}}$ \emph{wins} some play $\rho = s_0 s_1 \ldots$ if the play reaches a goal state, i.e., if there exists some integer $0\leq k \leq\operatorname{len}(\rho)$ such that $\mathit{Goal}(s_k)$ is valid.
Otherwise, $\texttt{{SAFE}}$ wins play $\rho$.
A \emph{reachability strategy} $\sigma_{\mathit{R}}$ is a function $\sigma_{\mathit{R}} : \S^*S_\texttt{{REACH}} \to \S$ such that if $\sigma_{\mathit{R}}(\omega s) =s'$ and $s$ is not a trap state, then $\mathit{Reach}(s,s')$ is valid. 
We say that a play $\rho = s_0 s_1 s_2 \ldots$ is \emph{consistent} with $\sigma_{\mathit{R}}$ if for all $i$ such that $s_i(\mathbf{r}) = \texttt{true}$ we have $s_{i+1} = \sigma_{\mathit{R}}(s_0 \ldots s_i)$.
A reachability strategy $\sigma_{\mathit{R}}$ is \emph{winning} from some state $s$ if $\texttt{{REACH}}$ wins every play consistent with $\sigma_{\mathit{R}}$ starting in $s$. We define \emph{safety strategies} $\sigma_{\mathit{S}}$ for $\texttt{{SAFE}}$ analogously. We say that a player \emph{wins in or from a state}~$s$ if they have a winning strategy from $s$. Lastly, $\texttt{{REACH}}$ \emph{wins the game} $\mathcal{G}$ if they win from some initial state.
Otherwise, $\texttt{{SAFE}}$ wins.

We often project a transition predicate $T$ onto the source or target states of transitions satisfying $T$, which is taken care of by the formulas $\operatorname{Pre}(\mathit{T})=\exists \mathcal{V'}.\:\mathit{T}$ and $\operatorname{Post}(\mathit{T})=\exists \mathcal{V}.\:\mathit{T}$.
The notation $\exists \mathcal{V}$ (resp. $\exists \mathcal{V'}$) represents the existential quantification over all variables in the corresponding set.
Given $\varphi \in \cal L(\mathcal{V})$, we call the set of transitions in $\mathcal{G}$ that move from states not satisfying $\varphi$, to states satisfying $\varphi$, the \emph{instantiation} of $\varphi$, formally:
\[\operatorname{Instantiate}(\varphi,\mathcal{G})=(\mathit{Safe} \lor \mathit{Reach}) \land \lnot\varphi\land\varphi'.\]

\section{Subgoals}
\label{sec:subgoals}

We formally define the notion of subgoals.
Let $\mathcal{G} = \langle \mathit{Init}, \mathit{Safe}, \mathit{Reach}, \mathit{Goal} \rangle$ be a fixed reachability game throughout this section, where we assume that $\mathit{Init} \land \mathit{Goal}$ is unsatisfiable.
Whenever this assumption is not satisfied in our algorithm, we will instead consider the game $\mathcal{G}' = \langle \mathit{Init} \land \neg \mathit{Goal}, \mathit{Safe}, \mathit{Reach}, \mathit{Goal} \rangle$ which does satisfy it.
As states in $\mathit{Init} \land \mathit{Goal}$ are immediately winning for \texttt{{REACH}}, this is not a real restriction.

\begin{definition}[Enforceable transitions]
	The set of \emph{enforceable transitions} relative to a transition predicate $T \in \cal L(\mathcal{V} \cup \mathcal{V'})$ is defined by the formula
	\[\operatorname{Enf}(\mathit{T},\mathcal{G})=\; (\mathit{Safe} \lor \mathit{Reach}) \land \mathit{T} \land \lnot \exists \mathcal{V'}.\:\big(\mathit{Safe}\land\lnot\mathit{T}\big).\]
	
\end{definition}

The enforceable transitions operator serves a purpose similar to the \emph{controlled predecessors} operator commonly known in the literature, which is often used in a backwards fixed point computation, called \emph{attractor construction} \cite{Thomas95}. For both operations, the idea is to determine controllability by \texttt{{REACH}}{}. The main difference is that we do not consider the whole transition relation, but only a predetermined set of transitions and check from which predecessor states the post-condition of the set can be enforced by \texttt{{REACH}}{}. These include all transitions in $T$ controlled by \texttt{{REACH}}{} and additionally transitions in $T$ controlled by \texttt{{SAFE}}{} such that \emph{all other transitions} in the origin state of the transition also satisfy $T$. The similarity with the controlled predecessor is exemplified by the following lemma:
\begin{lemma}
  \label{lem:enf}
  Let $T$ be a transition predicate, and suppose that all states satisfying $\operatorname{Post}(T)[\varp/\var]$ are winning for \texttt{{REACH}}{} in $\mathcal{G}$.
  Then all states in $\operatorname{Pre}(\operatorname{Enf}(T,\mathcal{G}))$ are winning for \texttt{{REACH}}{} in $\mathcal{G}$.
\end{lemma}
\begin{proof}
  Clearly, all states in $\operatorname{Pre}(\operatorname{Enf}(T,\mathcal{G}))$ that are under the control of \texttt{{REACH}}{} are winning for \texttt{{REACH}}{}, as in any such state they have a transition satisfying $T$ (observe that $\operatorname{Enf}(T,\mathcal{G}) \implies T$ is valid), which leads to a winning state by assumption.

  So let $s$ be a state satisfying $\operatorname{Pre}(\operatorname{Enf}(T,\mathcal{G}))$ that is under the control of \texttt{{SAFE}}{}.
  As $\operatorname{Pre}(\operatorname{Enf}(T,\mathcal{G}))(s)$ is valid, $s$ has a transition that satisfies $T$ (in particular, $s$ is not a trap state).
  Furthermore, we know that there is no $s' \in \S$ such that $\mathit{Safe}(s,s')\land\lnot\mathit{T}(s,s')$ holds, and hence there is no transition satisfying $\lnot\mathit{T}$ from $s$. Since $\operatorname{Post}(T)[\varp/\var]$ is winning for \texttt{{REACH}}{}, it follows that from $s$ player \texttt{{SAFE}}{} cannot avoid playing into a winning state of \texttt{{REACH}}{}.
  \qed
\end{proof}

We now turn to a formal definition of \emph{necessary subgoals}, which intuitively are sets of transitions that appear on every play that is winning for \texttt{{REACH}}{}. 
\begin{definition}[Necessary subgoal]\label{necessary_subgoal}
	A \emph{necessary subgoal} $C \in \cal L(\mathcal{V} \cup \mathcal{V'})$  for~$\mathcal{G}$ is a transition predicate such that for every play $\rho = s_0 s_1 \ldots$ of $\mathcal{G}$ and $n \in \mathbb{N}$ such that $\mathit{Goal}(s_{n})$ is valid, there exists some $k < n$ such that $C(s_k,s_{k+1})$ is valid.
\end{definition}

Necessary subgoals provide a means by which winning safety player strategies can be identified, as formalized in the following lemma.

\begin{lemma}\label{prop_safestrat}
	A safety strategy $\sigma_{\mathit{S}}$ is winning in $\mathcal{G}$ if and only if there exists a necessary subgoal $\mathit{C}$ for $\mathcal{G}$ such that for all plays $\rho = s_0 s_1 \ldots$ of $\mathcal{G}$ consistent with~$\sigma_{\mathit{S}}$ there is no $n \in \mathbb{N}$ such that $C(s_n,s_{n+1})$ holds. 
\end{lemma}
\begin{proof}
  ``$\implies$''. The transition predicate $\mathit{Goal}[\var/\varp]$ (i.e., transitions with endpoints satisfying $\mathit{Goal}$) is clearly a necessary subgoal. If $\sigma_{\mathit{S}}$ is winning for \texttt{{SAFE}}, then no play consistent with $\sigma_{\mathit{S}}$ contains a transition in this necessary subgoal. \\
  \noindent ``$\Longleftarrow$''. Let $C$ be a necessary subgoal such that no play consistent with $\sigma_{\mathit{S}}$ contains a transition of $C$. Then by  \Cref{necessary_subgoal} no play consistent with $\sigma_{\mathit{S}}$ contains a state satisfying $\mathit{Goal}$. Hence $\sigma_{\mathit{S}}$ is a winning strategy for \texttt{{SAFE}}.
	\qed
\end{proof}

Of course, the question remains how to compute non-trivial subgoals. Indeed, using $\mathit{Goal}$ as outlined in the proof above provides no further benefit over a simple backwards exploration (see~\Cref{rem:attractor} in the following section).

Ideally, a subgoal should represent an interesting key decision to focus the strategy search.
As we show next, Craig interpolation allows to extract partial causes for the mutual unsatisfiability of $\mathit{Init}$ and $\mathit{Goal}$ and can in this way provide necessary subgoals. 
Recall that a Craig interpolant $\varphi$ between $\mathit{Init}$ and $\mathit{Goal}$ is a state predicate that is implied by $\mathit{Goal}$, and unsatisfiable in conjunction with $\mathit{Init}$. 
In this sense, $\varphi$ describes an observable \emph{effect} that must occur if $\texttt{{REACH}}{}$ wins, and the concrete transition that instantiates the interpolant \emph{causes} this effect.

\begin{proposition}\label{prop_necessary}
	Let $\varphi$ be a Craig interpolant for $\mathit{Init}$ and $\mathit{Goal}$. Then the transition predicate $\operatorname{Instantiate}(\varphi,\mathcal{G})$ is a necessary subgoal.
\end{proposition}
\begin{proof}
  As $\varphi$ is an interpolant, it holds that $\mathit{Goal} \implies \varphi$ is valid and $\mathit{Init} \land \varphi$ is unsatisfiable.
  Consider any play $\rho = s_0 s_1 \ldots$ of $\mathcal{G}$ such that $\mathit{Goal}(s_n)$ is valid for some $n \in \mathbb{N}$.
  It follows that $\lnot \varphi(s_0)$ and $\varphi(s_n)$ are both valid.
  Consequently, there is some $0 \leq i < n$ such that $\lnot \varphi(s_i)$ and $\varphi(s_{i+1})$ are both valid.
  As all pairs $(s_k,s_{k+1})$ satisfy either $\mathit{Safe}$ or $\mathit{Reach}$, it follows that $\big(\operatorname{Instantiate}(\varphi,\mathcal{G})\big)(s_i,s_{i+1})$ is valid.
  Hence, $\operatorname{Instantiate}(\varphi,\mathcal{G})$ is a necessary subgoal.
	\qed
\end{proof}

While avoiding a necessary subgoal is a winning strategy for \texttt{{SAFE}}{}, reaching a necessary subgoal is in general not sufficient to guarantee a win for \texttt{{REACH}}{}.
This is because there might be some transitions in the necessary subgoal that produce the desired effect described by the Craig interpolant, but that trap \texttt{{REACH}}{} in a region of the state space where they cannot enforce some other necessary effect to reach goal. 
For the purpose of describing a set of transitions that is guaranteed to be winning for the reachability player, we introduce \emph{sufficient subgoals}.

 \begin{definition}[Sufficient subgoal]
   A transition predicate $\mathit{F}\in\cal L(\mathcal{V}\cup\mathcal{V'})$ is called a \emph{sufficient subgoal} if $\texttt{{REACH}}$ wins from every state satisfying $\operatorname{Post}(\mathit{F})[\varp/\var]$.
 \end{definition}

\begin{example}
	Consider the Mona Lisa game $\mathcal{G}$ described in Section \ref{sec:motivation}.
	\[C_1 = (\mathit{Guard} \lor \mathit{Thief}) \land p \neq 1 \land p' = 1\]
	qualifies as sufficient subgoal, because $\texttt{{REACH}}$ wins from every successor state as all those states satisfy $\mathit{Goal}$. 
	Also, every play reaching $\mathit{Goal}$ eventually passes $C_1$, and hence $C_1$ is also necessary. On the other hand, 
	\[C_2 = (\mathit{Guard} \lor \mathit{Thief}) \land a \neq 0 \land a' = 0\]
	is only a necessary subgoal in $\mathcal{G}$, because $\texttt{{SAFE}}$ wins from some (in fact all) states satisfying $\operatorname{Post}(C_2)$.
	
\end{example}
 
If the set of transitions in the necessary subgoal $C$ that lead to winning states of \texttt{{REACH}}{} is definable in $\cal L$ then we call the transition predicate $F$ that defines it the \emph{largest sufficient subgoal} included in $C$. 
It is characterized by the properties (1) $F \implies C$ is valid, and (2) if $F'$ is such that $F \implies F'$ is valid, then either $F \equiv F'$, or $F'$ is not a sufficient subgoal. Since $C$ is a necessary subgoal and $F$ is maximal with the properties above, \texttt{{REACH}}{} needs to see a transition in $F$ eventually in order to win. This balance of necessity and sufficiency allows us to partition the game along $F$ into a game that happens after the subgoal and one that happens before.

\begin{proposition}
		\label{lem:slicing}
	  Let $C$ be a necessary subgoal, and $F$ be the largest sufficient subgoal included in $C$. Then \texttt{{REACH}}{} wins from an initial state $s$ in $\mathcal{G}$ if and only if \texttt{{REACH}}{} wins from $s$ in the pre-game 
    \[\mathcal{G}_{pre} = \langle \mathit{Init}, \mathit{Safe} \land \neg F, \mathit{Reach} \land \neg F, \operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G})) \rangle.\]
\end{proposition}
\begin{proof}
  ``$\implies$''. Suppose that \texttt{{REACH}}{} wins in $\mathcal{G}$ from $s$ using strategy $\sigma_R$. Assume for a contradiction that \texttt{{SAFE}}{} wins in $\mathcal{G}_{pre}$ from $s$ using strategy $\sigma_S$. Consider strategy $\sigma'_S$ such that $\sigma_{\mathit{S}}'(\omega s') = \sigma_{\mathit{S}}(\omega s')$ if $(\mathit{Safe} \land \lnot F)(s')$ is satisfiable, and else $\sigma_{\mathit{S}}'(\omega s') = \sigma_{\mathit{S}}''(\omega s')$, where $\sigma_{\mathit{S}}''$ is an arbitrary safety player strategy in $\mathcal{G}$. Let $\rho = s_0s_1\ldots$ be the (unique) play of $\mathcal{G}$ consistent with both $\sigma_R$ and $\sigma'_S$, where $s_0 = s$. Since $\sigma_R$ is winning in $\mathcal{G}$ and $C$ is a necessary subgoal in $\mathcal{G}$, there must exist some $m\in\mathbb{N}$ such that $C(s_m, s_{m+1})$ is valid. Let $m$ be the smallest such index. Since $F \implies C$, we know for all $0 \leq k < m$ that $\lnot F (s_k,s_{k+1})$ holds. Hence, there is the play $\rho' = s_0s_1\ldots s_m \ldots$ in $\mathcal{G}_{pre}$ consistent with $\sigma_S$. The state $s_{m+1}$ is winning for \texttt{{REACH}}{} in $\mathcal{G}$, as it is reached on a play consistent with the winning strategy $\sigma_R$. Hence, we know that $F(s_m, s_{m+1})$ holds, because $F$ is the largest sufficient subgoal included in $C$.
  If $(\mathit{Reach} \land F)(s_m, s_{m+1})$ held, we would have that $\operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G})(s_m)$ holds: a contradiction with $\rho'$ being consistent with $\sigma_S$, which we assumed to be winning in $\mathcal{G}_{pre}$. It follows that $(\mathit{Safe} \land F)(s_m, s_{m+1})$ holds. We can conclude that $(\mathit{Safe} \land \lnot F)(s_m)$ is unsatisfiable (i.e., $s_m$ is a trap state in $\mathcal{G}_{pre}$), because in all other cases $\texttt{{SAFE}}$ plays according to $\sigma_{\mathit{S}}$, which cannot choose a transition satisfying $F$. However, this implies that  $\operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G})(s_m)$ holds, again a contradiction with $\rho'$ being consistent with winning strategy $\sigma_S$.

	\noindent ``$\Longleftarrow$''. If $\texttt{{REACH}}$ wins in $\mathcal{G}_{pre}$ they have a strategy $\sigma_{\mathit{R}}$ such that every play consistent with $\sigma_{\mathit{R}}$ reaches the set $\operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G}))$.
  As $F$ is a sufficient subgoal, the states $\operatorname{Post}(F)$ are winning for \texttt{{REACH}}{} by definition.
  It follows by~\Cref{lem:enf} that all states satisfying $\operatorname{Pre}(\operatorname{Enf}(F,\mathcal{G}))$ are winning in $\mathcal{G}$.
  Combining $\sigma_{R}$ with a strategy that wins in all these states yields a winning strategy for \texttt{{REACH}}{} in $\mathcal{G}$.
  \qed
\end{proof}
