# Solving Infinite-State Games via Acceleration (Full Version)

Philippe Heim<EMAIL_ADDRESS>0000-0002-5433-8133 CISPA Helmholtz
Center for Information SecurityStuhlsatzenhaus 5SaarbrückenGermany66123 and
Rayna Dimitrova<EMAIL_ADDRESS>CISPA Helmholtz Center for Information
SecurityStuhlsatzenhaus 5SaarbrückenGermany66123

###### Abstract.

Two-player graph games have found numerous applications, most notably in the
synthesis of reactive systems from temporal specifications, but also in
verification. The relevance of infinite-state systems in these areas has lead
to significant attention towards developing techniques for solving infinite-
state games.

We propose novel symbolic semi-algorithms for solving infinite-state games
with temporal winning conditions. The novelty of our approach lies in the
introduction of an acceleration technique that enhances fixpoint-based game-
solving methods and helps to avoid divergence. Classical fixpoint-based
algorithms, when applied to infinite-state games, are bound to diverge in many
cases, since they iteratively compute the set of states from which one player
has a winning strategy. Our proposed approach can lead to convergence in cases
where existing algorithms require an infinite number of iterations. This is
achieved by acceleration: computing an infinite set of states from which a
simpler sub-strategy can be iterated an unbounded number of times in order to
win the game. Ours is the first method for solving infinite-state games to
employ acceleration. Thanks to this, it is able to outperform state-of-the-art
techniques on a range of benchmarks, as evidenced by our evaluation of a
prototype implementation.

infinite-duration games, infinite-state games, reactive synthesis

††ccs: Theory of computation Logic and verification††ccs: Software and its
engineering Automatic programming

##  1\. Introduction

Reactive synthesis, introduced by Church (Church, 1962), has the goal of
automatically generating an implementation (for instance, a program or a
finite-state controller) from a formal specification that describes the
desired behavior of the system. The system requirements are typically
specified using temporal logics, such as Linear Temporal Logic (LTL), which
provide expressive high-level specification languages. Recent advancements
(Bloem et al., 2012; Finkbeiner and Schewe, 2013) have made possible the
successful application of synthesis to industrial protocols and robotics.

The problem of synthesizing strategies in two-player games over graphs is
tightly connected to reactive synthesis. Synthesis from temporal logic
specifications can be reduced to computing a winning strategy in a game. Games
can also be used to model the interaction between a system and its environment
directly. There is a large body of algorithmic techniques and tools for
solving finite-state games. Many applications of two-player games, however,
naturally require the treatment of infinite-state models, such as software
synthesis and repair (Griesmayer et al., 2006), controller synthesis in
domains like robotics (Kress-Gazit et al., 2009), and software verification
against hyperproperties (Beutner and Finkbeiner, 2022). The problem of solving
(i.e., determining the winner) infinite-state games is in general undecidable,
and many practical applications lie outside of decidable classes, making
incomplete approaches necessary. As different approaches have different
strengths, a number of techniques have been developed over the last years
(Beyene et al., 2014; Neider and Topcu, 2016; Farzan and Kincaid, 2018; Samuel
et al., 2021). However, the state of the art is still far from the level of
the algorithmic approaches and tools available for the finite-state case.

We propose a novel technique for solving infinite-state games that aims to
address one of the limitations of existing approaches, namely, that they
usually diverge on game-solving tasks that require reasoning about the
unbounded iteration of strategic decisions. We illustrate this challenge with
an example.

$l_{0}$$l_{G}$$x>42{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\land
i\neq 0}$$x:=x+i$$x:=x-i$$x\leq
42{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\lor
i=0}$$x:=x$$\top$ (a) Reactive program game structure with two locations
($l_{0}$ and $l_{G}$) and two integer variables: environment-controlled _input
variable $i$_ and system-controlled _program variable_ $x$. Edges to black
squares are labeled with _guards_ (formulas over the variables), and edges
originating in black squares are labeled with _updates_ to the program
variables.

⬇

$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{0}}$:
read $i$;

if($i=0\vee x\leq 42$){ goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{G}}$
}

if($x>42$){ goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{0}^{L}}$
}

$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{G}}$:
read $i$; goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{G}}$

$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{0}^{L}}$:
$x_{0}$ := $x$

if($i=0\vee x\leq 42$){ goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{G}}^{L}$
}

if($x+i<x_{0}$){ $x$:=$x+i$; goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{E}^{L}}$
}

if($x-i<x_{0}$){ $x$:=$x-i$; goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{E}^{L}}$
}

$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{E}^{L}}$:
goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{0}}$

$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{G}^{L}}$:
goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{G}}$

(b) Reactive program with input variable $i$, program variable $x$ and
auxiliary variable $x_{0}$.

Figure 1. Reactive program game (left) and a corresponding synthesized
reactive program (right).

###### Example 1.1.

Consider the simple game shown in Figure 1(a). It models the interaction
between a reactive program (the system) and its environment. The game has two
locations, $l_{0}$ and $l_{G}$, an integer input variable $i$, and an integer
program variable $x$. The edges depict transitions and are labeled with guard
conditions over the input and output variables, and updates which are
assignments to the program variable. When we depict transitions we separate
guards and updates. Edges originating in locations are labeled with guards and
end in a black square. Edges originating in the black squares are labeled with
possible updates for the system to choose from. Note that the black squares
are used simply for visualization. When playing the game, in each step the
environment chooses a value for $i$. Then, in $l_{0}$, if $x$ is smaller than
42 or $i$ is zero, the system must leave $x$ unchanged and the game moves to
$l_{G}$. Otherwise, the system has to decide whether to add or subtract $i$
from $x$ and the game stays in $l_{0}$. Once in $l_{G}$, the game stays there
forever and $x$ is not changed.

Let us consider the _temporal specification_ where the system is required to
_eventually reach_ location $l_{G}$ from $l_{0}$ for any initial value in $x$.
The program can indeed enforce this property by _choosing the appropriate
update at every step_ : adding $i$ to $x$ if $i<0$ and subtracting $i$ from
$x$ if $i>0$. This ensures that $x$ is decremented in every step (unless the
environment sets $i$ to $0$, in which case the game moves to $l_{G}$), and
hence $i=0\vee x\leq 42$ will eventually be reached.

The number of times $x$ has to be decremented depends on its initial value,
and therefore _the number of iterations through $l_{0}$ is a priori
unbounded_. However, not only the number of iterations in the system execution
is unbounded, which would correspond to an unbounded loop, but in every
iteration, the system has to perform _strategic decisions_ which depend on the
input from the environment and impact the execution. We call these constructs
_unbounded strategy loops_.

While necessary for many practical applications, handling unbounded strategy
loops is out of the scope of existing methods for reactive synthesis. However,
in our example, the necessary argument to establish that the system can
satisfy the requirement of the game can be stated as the following simple
property: Whenever $x>42$, if the system can ensure that it can decrement $x$,
then eventually $x\leq 42$ will be reached. To utilize this reasoning, the
synthesis process has to establish that the task postulated in the sub-
property, i.e. “$x$ is decremented”, can be realized in certain situations,
i.e. $i\neq 0$. This itself is a reactive synthesis task. In this paper we
propose a symbolic method for solving infinite-state games that utilizes such
reasoning in order to handle unbounded strategy loops as the one in Figure
1(a). ∎

##### Contributions

We present a symbolic approach for solving infinite-state games with temporal
objectives, such as reachability, safety, Büchi, and co-Büchi, lifting the
respective finite-state algorithms. The key novelty of our technique is an
_acceleration method_ which, in contrast to existing approaches, accelerates
unbounded strategy loops. It uses the newly introduced notion of _acceleration
lemmas_ , which are simple inductive statements that the symbolic algorithm
lifts to accelerate the termination of the game-solving process. To the best
of our knowledge, this is the first acceleration-based method for game
solving. We implemented our method in a prototype and demonstrate its
feasibility by its successful application to standard benchmarks from the
literature, outperforming existing tools, and several new ones that are out of
the scope of these tools.

##### Paper Outline

After discussing related work in Section 2, we present in Section 3 several
examples illustrating different challenges, how our technique approaches them,
and where existing methods fall short. After the technical preliminaries in
Section 4, we introduce our game model in Section 5. We then describe the
basis of our solving techniques in Section 6. In Section 7, we present
formally our acceleration method. We continue by discussing the synthesis of
acceleration lemmas in Section 8. Lastly, Section 9 evaluates our method and
discusses our empirical observations.

##  2\. Related Work

We now overview the landscape of existing approaches for solving infinite-
state games and explain how our work addresses some of their limitations. We
also discuss relevant techniques for verification of infinite-state systems
and why they do not directly apply in the context of synthesis.

##### Infinite-State Game Solving.

In general, games over infinite graphs are undecidable. Decidable classes,
such as pushdown games (Walukiewicz, 2001) and downward-closed safety games
(Abdulla et al., 2008), as well as termination criteria for symbolic
procedures (de Alfaro et al., 2001) have been found. As many practical
applications lie outside of these classes, incomplete methods are needed.

Different approaches have been proposed for safety games. (Neider and Topcu,
2016) presents an automata-learning method for safety games over infinite
graphs, and (Markgraf et al., 2020) develops a learning-based technique for
parameterized systems with safety specifications. In (Farzan and Kincaid,
2018), the authors study safety and reachability games defined within the
theory of linear rational arithmetic. (Katis et al., 2018) presents a method
for synthesis from Assume-Guarantee contracts describing safety properties.
The tool GenSys (Samuel et al., 2021) implements a fixpoint-based solver for
infinite-state safety games using an SMT solver. (Faella and Parlato, 2023)
presents a method for solving infinite-state reachability games by reducing
the problem to checking the satisfiability of a system of constrained Horn
clauses. It is restricted to games where the reachability player has finitely
many actions to choose from. More expressive winning conditions, such as the
Büchi condition which requires repeated visits to some states, are out of the
scope of these methods.

The constraint-based approach in (Beyene et al., 2014) handles infinite-state
games with winning conditions given by LTL specifications. It can solve
problems with unbounded strategy loops. However, it requires the user to
provide templates that structure how the final system works, including
handling the unbounded strategy loops. As can be seen in the examples in
(Beyene et al., 2014) such templates can be quite complex even for small
games. In contrast, our approach uses inductive statements that are
automatically generated from generalizable templates.

Solvers for first-order fixpoint logics (Unno et al., 2023, 2020) can be used,
as described in (Unno et al., 2020), to solve games with omega-regular winning
conditions. This approach uses the fixpoint encoding of the winning sets of
states for a player in the game. Its ability to find a solution depends on the
constraint-solving engine. In Section 9 we report on experimental comparison
with the technique described in (Unno et al., 2020), demonstrating the
strengths of our approach.

Abstraction-based techniques have been extended to games (Henzinger et al.,
2003; Grumberg et al., 2005; Ball and Kupferman, 2006; Grumberg et al., 2007;
Walker and Ryzhyk, 2014). Abstraction-based controller synthesis for dynamical
systems (Tabuada, 2009) makes use of discretization. As they reduce the
solving of an infinite-state game to the finite-state case, they can use the
techniques and tools available for finite-state games. The effectiveness of
these approaches depends on the abstractions, whose iterative refinement might
diverge when unbounded strategy loops are needed.

##### Infinite-State Synthesis from Temporal Logics.

The recent works (Choi et al., 2022; Maderbacher and Bloem, 2021) both study
the problem of synthesizing reactive systems from Temporal Stream Logic modulo
theories (TSL-MT (Finkbeiner et al., 2022)) specifications. This temporal
logic can express conditions on unbounded input data and program variables.
(Choi et al., 2022) integrates a procedure for synthesis from TSL
specifications (Finkbeiner et al., 2019) and Syntax-Guided synthesis. The role
of SyGuS is to generate assumptions that are added to a refined TSL formula.
The procedure proposed in (Maderbacher and Bloem, 2021) is based on
abstraction refinement and performs a counterexample-guided synthesis loop
that invokes LTL synthesis. The refinement uses an SMT solver to analyze
counterstrategies for inconsistency with the theory. While (Choi et al., 2022)
can handle some unbounded looping behavior by using recursive functions, both
(Maderbacher and Bloem, 2021; Choi et al., 2022) cannot handle unbounded
strategy loops where at each iteration, the environment provides new input
values. (Samuel et al., 2023) proposes a symbolic fixpoint computation for
infinite-state games with LTL winning conditions. As the authors remark, their
method has the same non-termination issues as (Maderbacher and Bloem, 2021),
which implies that it will also diverge in the presence of unbounded strategy
loops.

##### Infinite-State Verification.

There is a vast variety of approaches for verification of infinite-state
systems. Above we discussed extensions of abstraction-based techniques and
deductive verification techniques to the setting of games and synthesis of
reactive systems. In contrast, other prominent approaches used in the
verification of infinite-state systems, such as acceleration (Finkel and
Leroux, 2002; Bardin et al., 2003, 2005; Leroux and Sutre, 2006) or loop
summarization (Kroening et al., 2013), do not directly extend to the setting
of two-player games, and have thus far not been explored. The key difficulty
is caused by the alternation of environment inputs and decisions by the system
player, meaning that a loop in the game structure might not be under the full
control of the system. Thus, the existence of a loop whose transitions can be
composed, does not entail that it is enforceable by the system. We illustrate
this in the next section, and discuss this challenge further in this paper.

##  3\. Overview and Motivating Examples

In this section, we give a high-level overview of our approach, highlighting
some of its strengths and distinguishing features on several simple but
challenging examples. First, we show how our acceleration method can be
applied to enable termination in certain cases, specifically in the presence
of unbounded strategy loops ( Example 1.1), where existing techniques
typically diverge. We explain, on the high level, how acceleration works, and
also discuss what are the challenges that our technique addresses. Second, we
demonstrate the advantage of our acceleration-based game solving procedure
over purely constraint-based approaches for solving fixpoint equations.
Finally, we illustrate the applicability of our acceleration method to
expressive classes of specifications encoded as Büchi objectives in the
synthesis game.

We begin with a brief, high-level, description of our game model and problem
formulation. The underlying formal definitions are presented in the later
Section 4 and Section 5.

###  3.1. Symbolic Model and Problem Formulation

We specify synthesis tasks as _reactive program game structures_ , like the
one depicted in Figure 1(a). Such a game structure consists of a finite set
$L$ of control locations, a finite set $\mathbb{I}$ of input variables, and a
finite set $\mathbb{X}$ of output variables. While the sets $\mathbb{I}$ and
$\mathbb{X}$ are finite, the domains of the variables can be infinite. Thus,
reactive program game structures can represent infinite-state games. A
reactive program game contains transitions between the locations, labeled with
guards and updates. A transition has the form $(l,g,u,l^{\prime})$, where $l$
and $l^{\prime}$ are the source and target locations respectively, $g$ is the
guard, and $u$ is the update. As in Figure 1(a), we depict such a transition
using an edge from $l$ to a black square labeled with $g$, and an edge from a
black square to $l^{\prime}$ labelled with $u$. The intermediate black squares
are for visualization only, and not part of the formal definition. A guard $g$
has to hold for the transition to be possible, and an update $u$ assigns to
each program variable a term with whose value it should be updated. A
_reactive program game_ is pair of a reactive program game structure and a
_winning condition_ expressed over the locations $L$. For example, in Figure
1(a), we consider the reachability condition that requires that location
$l_{G}$ is eventually visited. In Example 3.3 we show a reactive program game
with a Büchi winning condition that states that the system has to enforce
visiting a set of accepting locations $B\subseteq L$ infinitely often.

The reactive program game is played over the possibly infinite set of states,
where each state $(l,\nu)$ consists of the current location $l$ and an
assignment $\nu$ of values for all the program variables $\mathbb{X}$. A step
in the game is played as follows. In the current state $(l,\nu)$, the
environment chooses some values $\mathbf{i}$ for the inputs $\mathbb{I}$.
Then, the system chooses a transition $(l,g,u,l^{\prime})$ whose guard $g$ is
satisfied by the current values $\mathbf{i}$ and $\nu$, of the inputs and the
program variables respectively. The next location is $l^{\prime}$, and the
next values of the program variables are determined according to the update
$u$. Starting in some state $(l,\nu)$, this repeated interaction produces a
play, an infinite sequence of states, which is winning for the system player
if it satisfies the given winning condition.

The _realizability problem_ is to determine whether there exists a strategy
for the system to resolve the transition (i.e., update) choices that
guarantees that any play starting in any possible state
$(l_{\mathit{init}},\nu)$ for a given initial location $l_{\mathit{init}}$, is
winning for the system, regardless of the input values chosen by the
environment. The _synthesis problem_ asks to compute such a strategy if one
exists. One such a strategy for Example 1.1 with initial location $l_{0}$ is
depicted in Figure 1(b), in the form of a reactive program. The program
contains an auxiliary variable $x_{0}$, whose role will be explained later.

###  3.2. Acceleration for Unbounded Strategy Loops

Finite-state games can be solved by fixpoint algorithms that compute sets of
states from which a given player can enforce winning the game. To solve
reactive program games, we lift those algorithms to compute symbolically
infinite sets of states. We represent them as elements of a symbolic domain
$\mathcal{D}:=L\to\mathit{FOL}(\mathbb{X})$, where $\mathit{FOL}(\mathbb{X})$
is the set of first-order logic formulas with free variables among the program
variables $\mathbb{X}$. A symbolic set $d\in\mathcal{D}$ represents the set of
those $(l,\nu)$ where the assignment $\nu$ to $\mathbb{X}$ satisfies $d(l)$. A
basic notion in the fixpoint-based game-solving algorithms is the _attractor_.
For a given player and a given set of goal states, the attractor consists of
the states from which the player can enforce reaching a goal state in some
number of steps. Attractor sets can be computed via iterative fixpoint
computation, which is not guaranteed to terminate in the case of an infinite
state space. We illustrate this on Example 1.1.

Example 1.1 (Continued). Suppose we want to compute the attractor for the
system player for the symbolically represented set of states
$d:=\\{l_{0}\mapsto\bot,l_{G}\mapsto\top\\}$ (describing the set of states
whose location is $l_{G}$). After the first iteration, we get
$\\{l_{0}\mapsto(x\leq 42),l_{G}\mapsto\top\\}$. In the next one, we get
$\\{l_{0}\mapsto(\forall i.x\leq 42\lor i=0\lor x+i\leq 42\lor x-i\leq
42),l_{G}\mapsto\top\\}$ which simplifies to $\\{l_{0}\mapsto(x\leq
43),l_{G}\mapsto\top\\}$. Then $\\{l_{0}\mapsto(x\leq
44),l_{G}\mapsto\top\\}$, $\\{l_{0}\mapsto(x\leq 45),l_{G}\mapsto\top\\}$, ….
A fixpoint is never reached, since at every step of the computation we add one
state from the infinite attractor set. ∎

In Section 1 we argued intuitively why in Example 1.1 every state
$(l_{0},\nu)$ belongs to the attractor for the system player. The method we
propose in this paper is able to automatically establish this and compute the
attractor. More concretely, this is achieved as follows.

  * •

We introduce the notion of _acceleration lemmas_ , which allow us to express
in a formal way arguments like the one outlined in Section 1. An acceleration
lemma, precisely defined in Section 7.1, is a triple
$(\mathit{base},\mathit{step},\mathit{conc})$ of $\mathit{FOL}$ formulas. The
_conclusion_ $\mathit{conc}$ characterizes a set of states with the property
that from each of them, by iterating the _step relation_ described by
$\mathit{step}$, a state in the set characterized by the base condition
$\mathit{base}$ must be reached. Intuitively, $\mathit{conc}$ characterizes
the states added to the attractor by applying this acceleration lemma. For our
Example 1.1, one possible acceleration lemma is
$(\mathit{base},\mathit{step},\mathit{conc})$ with $\mathit{base}:=(x\leq
42)$, $\mathit{step}:=(x^{\prime}<x)$ and $\mathit{conc}:=\top$. In the
formula $\mathit{step}:=(x^{\prime}<x)$, the variable $x$ refers to the value
of the respective program variable at one visit to location $l_{0}$ and
$x^{\prime}$ refers to its value the next time $l_{0}$ is visited. Clearly,
starting in any state $(l_{0},\nu_{0})$, any sequence of states
$(l_{0},\nu_{0}),(l_{0},\nu_{1}),\ldots$ that satisfies $\mathit{step}$
eventually reaches a state that satisfies $x\leq 42$.

  * •

The purpose of an acceleration lemma
$(\mathit{base},\mathit{step},\mathit{conc})$ is to accelerate the computation
of an attractor set for a given player $p$ in a reactive program game
structure $\mathcal{G}$, by adding all the states $(l,\nu)$ that satisfy
$\mathit{conc}$ to the attractor at once. In order to apply such a lemma, the
attractor computation procedure must first ensure that the set of states
described by $\mathit{base}$ is included in the subset of the attractor
computed thus far. Second, it is necessary to establish that player $p$ can
_enforce the repeated iteration of the step relation_ in the game
$\mathcal{G}$ _against all possible behaviors of the opponent player_.
Intuitively, this can be guaranteed by showing that player $p$ has a strategy
to enforce looping in location $l$ such that each iteration satisfies
$\mathit{step}$. In Example 1.1 this is indeed the case for location $l_{0}$
and the acceleration lemma given above. Thus, our method is able to add all
states $(l_{0},\nu)$ to the attractor for the system player.

In Section 7 we describe in detail how our method generates acceleration
lemmas while at the same time ensuring that their step relations can be
enforced by the respective player in the underlying reactive program game
structure. Next, we give an example that illustrates why the latter condition
is crucial for the correct application of an acceleration lemma. In fact, this
is one of the major challenges for acceleration in the context of synthesis,
and a key difference to the application of acceleration techniques in
verification.

###### Example 3.1.

Consider a modification of the reactive program game depicted in Figure 1(a)
in which we have omitted the parts of the guards referring to the input
variable $i$ and colored in blue. Clearly, now the only states $(l_{0},\nu)$
for which the system can enforce reaching location $l_{G}$ are those where
$x\leq 42$, since otherwise the environment can prevent the system from
decreasing $x$ by always setting $i$ to $0$. Thus, although the reactive
program game contains loops that decrement $x$, _these loops cannot be
enforced by the system_. This is a major difference to the acceleration
techniques employed in verification, as the existence of a loop with certain
properties is a realizability problem in itself. In Section 7.1 we show how we
address this problem by the utilization of a so-called _loop game_.∎

###  3.3. Embedding Acceleration in Iterative Symbolic Fixpoint Computation

Our acceleration technique is embedded in symbolic game-solving algorithms
based on iterative fixpoint computation. This enables our method to combine
the strengths of both techniques by utilizing acceleration for unbounded
strategy loops in concert with performing a finite number of concrete
iterations of the fixpoint computation. The latter can be helpful when the set
of winning states that the game solving procedure has to compute does not have
a “simple” and “easy to discover” symbolic characterization, as the next
example illustrates.

$l_{0}$$l_{1}$$l_{G}$$l_{B}$$\top$$x:=1$$x=64$$x\neq 64\wedge$$y\leq
0$$\mathsf{skip}$$\mathsf{skip}$$y:=y+1$$\top$$\top$$x\neq
64\wedge$$y>0$$x:=2\cdot x;$$y:=y-1$

Figure 2. Reactive program game structure with two system-controlled variables
$x$ and $y$ and no input variables. We use $\mathsf{skip}$ to denote the
update $x:=x;y:=y$. If the update to some program variable is missing from the
label of an update edge, this means that the value of this variable remains
unchanged.

###### Example 3.2.

Consider the reactive program game structure depicted in Figure 2. The
specification again requires the system to reach location $l_{G}$ from $l_{0}$
for any initial values of the program variables $x$ and $y$. Note that if the
value of $y$ is at least $6$ when transitioning from location $l_{0}$ to
$l_{1}$, the system can reach $l_{G}$ after doubling $6$ times the value of
$x$. Regardless of the initial values of the variables in $l_{0}$, it is
possible to reach $l_{1}$ with $y$ having value $6$ or larger. Thus, the
specification is realizable.

If linear arithmetic formulas are used to represent sets of states, then the
set of values at location $l_{1}$ from which $l_{G}$ can be reached is
characterized by the formula $(x=64)\vee(x=32\land y\geq 1)\vee(x=16\land
y\geq 2)\vee(x=8\land y\geq 3)\vee(x=4\land y\geq 4)\vee(x=2\land y\geq
5)\vee(x=1\land y\geq 6)$. Constraint-solving techniques for fixpoint equation
systems can have difficulty generating such formulas, as we will see in our
experimental evaluation in Section 9. On the other hand, methods for iterative
symbolic attractor computation that do not apply acceleration diverge due to
the presence of the loop in $l_{0}$.

Our acceleration-based procedure successfully determines the realizability in
this case, as it integrates acceleration in the iterative fixpoint
computation. Note that, for simplicity, this example does not contain
environment inputs, but the same challenges are present even if it does. ∎

###  3.4. Acceleration Beyond Reachability and Safety Games

The synthesis approach that we propose is applicable beyond reachability
specifications. For instance, we consider Büchi specifications that require
that some set of locations is visited infinitely often, or co-Büchi
specifications that require that some set of locations is visited only
finitely many times. Accelerated attractor computation can be readily
integrated in symbolic fixpoint-based procedures for infinte-state games with
these types of objectives. The next example shows a reactive program game with
a Büchi specification, for which our attractor acceleration method allows us
to establish realizability.

$l_{0}$$l_{1}$$l_{2}$$l_{3}$$l_{4}$$\top$$x:=i$$y:=y-1$$x\leq 42\lor
i=0$$\mathsf{skip}$$\top$$y:=64$$y\geq
16$$\mathsf{skip}$$y<16$$\mathsf{skip}$$\top$$x>42\land i\neq 0\land y\leq
32$$x:=x+i$$x:=x-i$$x>42\land$ $i\neq 0\land$ $y>32$$x:=x+i$

Figure 3. Reactive program game structure with two system-controlled variables
$x$ and $y$ and input variable $i$. We use $\mathsf{skip}$ to denote the
update $x:=x;y:=y$. If the update to a variable is missing from the label of
an update edge, its value remains unchanged. Double-circles denote the Büchi
accepting locations $\\{l_{2},l_{3}\\}$.

###### Example 3.3.

In the reactive program game depicted in Figure 3, the Büchi specification
defined by the set of locations $\\{l_{2},l_{3}\\}$ requires the system to
visit some of these two locations infinitely often. Looping between $l_{0}$
and $l_{3}$ is possible as long as $y>16$ at location $l_{0}$. Otherwise, upon
reaching $l_{3}$ with $y<16$, the program will have to transition to $l_{4}$
and revisiting either of $l_{3}$ or $l_{2}$ is not possible from this point
on. From location $l_{0}$ the system can transition to $l_{1}$, from where,
similarly as in the game from Example 1.1, the system can ensure reaching
$l_{2}$ as long as $x\leq 42$ or $y\leq 32$. If $y>32$ and $x>42$ in location
$l_{1}$, the environment can prevent the system from decreasing $x$ by always
setting $i$ to a positive value. Thus, if every time in location $l_{0}$ the
system transitions to $l_{1}$ when $y\leq 32$ and to $l_{3}$ when $y>32$ it
can ensure that the set of locations $\\{l_{2},l_{3}\\}$ is visited infinitely
often and thus satisfy the given Büchi specification. Our procedure
successfully computes that every state of the form $(l_{0},\nu)$ is winning
for the system. As part of the computation, attractor acceleration is applied
to establish that from every state of the form $(l_{0},\nu)$ where $\nu(y)\leq
32$ the system has a strategy to enforce reaching $l_{2}$. Note the presence
of an unbounded strategy loop, due to which the standard symbolic method for
solving Büchi games is bound to diverge. ∎

In the above example, applying acceleration to the attractor computation
performed as part of the procedure for solving Büchi games, suffices to ensure
convergence. In Section 7.3 we give an example where this is not enough, and
describe an acceleration method for Büchi conditions.

##  4\. Technical Preliminaries

##### Functions, Terms, and First-Order Logic.

Let $\mathcal{V}$ be the set of all values of arbitrary types,
$\mathcal{F}:=\\{f:\mathcal{V}^{n}\to\mathcal{V}\leavevmode\nobreak\
|\leavevmode\nobreak\ n\in\mathbb{N}\\}$ be the set of all functions, and
$\mathcal{P}:=\\{p\in\mathcal{F}\mid\mathit{Range}(p)\subseteq\mathbb{B}\\}$
be the set of all predicates. Let $\mathit{Vars}$ be the countably infinite
set of all variables. For $V\subseteq\mathit{Vars}$, we denote with
$V^{\prime}:=\\{x^{\prime}\mid x\in V\\}$ the set of primed variables such
that $V\cap V^{\prime}=\emptyset$. Terms are used to describe functions and
predicates. Let $\Sigma_{F}$ be the set of all function symbols and
$\Sigma_{P}\subset\Sigma_{F}$ the set of all predicate symbols. Function terms
$\mathcal{T}_{F}$ are defined by the grammar
$\mathcal{T}_{F}\ni\tau_{f}::=f(\tau_{f}^{1},\dots\tau_{f}^{n})\>|\>x$ for
$f\in\Sigma_{F}$ and $x\in\mathit{Vars}$, and we denote with $\mathcal{T}_{P}$
the function terms of Boolean type.

A function $\nu:\mathit{Vars}\to\mathcal{V}$ is called a _variable assignment_
(or simply _assignment_). The set of all assignments over a set of variables
$V\subseteq\mathit{Vars}$ is denoted as $\mathit{Assignments}(V)$. We denote
the combination of two assignments $\nu^{\prime},\nu^{\prime\prime}$ over
disjoint sets of variables by $\nu^{\prime}\uplus\nu^{\prime\prime}$. Given an
assignment function $\nu$, a variable $x\in\mathit{Vars}$ and a value
$v\in\mathcal{V}$, we define the assignment function $\nu[x:=v]$ such that
$\nu[x:=v](x)=v$ and $\nu[x:=v](y)=\nu(y)$ for all $y\in\mathit{Vars}$ with
$y\neq x$.

A function $\mathcal{I}:\Sigma_{F}\to\mathcal{F}$ is called an _interpretation
of the function symbols_ (or simply _interpretation_). We require
$\mathcal{I}(p)\in\mathcal{P}$ for $p\in\Sigma_{P}$. The set of all
interpretations of a set of function symbols $\Sigma\subseteq\Sigma_{F}$ is
denoted as $\mathit{Interpretations}(\Sigma)$. We denote the combination of
two interpretations $\mathcal{I}^{\prime},\mathcal{I}^{\prime\prime}$ over
disjoint symbol sets by
$\mathcal{I}^{\prime}\uplus\mathcal{I}^{\prime\prime}$. The evaluation of
function terms $\chi_{\nu,\mathcal{I}}:\mathcal{T}_{F}\to\mathcal{V}$ is
defined by $\chi_{\nu,\mathcal{I}}(x):=\nu(x)$ for $x\in\mathit{Vars}$,
$\chi_{\nu,\mathcal{I}}(f(\tau_{0},\dots\tau_{n})):=\mathcal{I}(f)(\chi_{\nu,\mathcal{I}}(\tau_{0}),\dots\chi_{\nu,\mathcal{I}}(\tau_{n}))$
for $f\in\Sigma_{F}$.

We denote the set of all first-order formulas as $\mathit{FOL}$. Let $\varphi$
be a formula and $X=\\{x_{1},\ldots,x_{n}\\}\subseteq\mathit{Vars}$ be a set
of variables. For a quantifer $Q\in\\{\exists,\forall\\}$, we write
$QX.\varphi$ as a short-cut for $Qx_{1}.\ldots Qx_{n}.\varphi$. We denote by
$\mathit{QF}$ the set of all quantifier-free formulas in $\mathit{FOL}$. We
write $\varphi(X)$ to denote that the free variables of $\varphi$ are a subset
of $X$. We also denote with $\mathit{FOL}(X)$ and $\mathit{QF}(X)$ the set of
formulas (respectively quantifier-free formulas) whose free variables belong
to $X$. Given variables $x_{1},\ldots,x_{n}\in\mathit{Vars}$, constant
function terms with arity zero $c_{1},\ldots,c_{m}\in\mathcal{T}_{F}$ and
function terms $\tau_{f}^{1},\ldots,\tau_{f}^{n+m},\in\mathcal{T}_{F}$, we
denote with
$\varphi[x_{1}\mapsto\tau_{f}^{1},\ldots,x_{n}\mapsto\tau_{f}^{n},c_{1}\mapsto\tau_{f}^{n+1},c_{m}\mapsto\tau_{f}^{n+m}]$
the formula obtained from $\varphi$ by the simultaneous replacement of all
free occurrences of each $x_{i}$ with the respective term $\tau_{f}^{i}$ and
of each occurrence $c_{i}$ by $\tau_{f}^{n+i}$. We denote with
$\models:\mathit{Assignments}(\mathit{Vars})\times\mathit{Interpretations}(\Sigma_{F})\times\mathit{FOL}$
the entailment of first-order logic formulas. A _first-order theory_
$T\subseteq\mathit{Interpretations}(\Sigma_{F})$ restricts the possible
interpretations of function and predicate symbols. Given a theory $T$, for a
formula $\varphi(X)$ and assignment $\nu\in\mathit{Assignments}(X)$ we define
that $\nu\models_{T}\varphi$ if and only if $\nu,\mathcal{I}\models\varphi$
for all $\mathcal{I}\in T$.

##### Two-Player Games of Infinite Duration.

We consider two-player games between a _system player_ and an _environment
player_. A _game structure_ is a tuple
$G=(\mathcal{S},M_{\mathsf{e}},M_{\mathsf{s}},\rho)$, where $\mathcal{S}$ is a
set of states, $M_{\mathsf{e}}$ and $M_{\mathsf{s}}$ are the sets of possible
moves for Player $\mathit{Env}$ and Player $\mathit{Sys}$ respectively, and
$\rho\subseteq\mathcal{S}\times M_{\mathsf{e}}\times
M_{\mathsf{s}}\times\mathcal{S}$ is a _transition relation_ where: (1) for all
$s\in\mathcal{S}$, there exist $m_{\mathsf{e}}\in M_{\mathsf{e}}$,
$m_{\mathsf{s}}\in M_{\mathsf{s}}$ and $s^{\prime}\in\mathcal{S}$ such that
$(s,m_{\mathsf{e}},m_{\mathsf{s}},s^{\prime})\in\rho$, and (2) for all
$s\in\mathcal{S}$, $m_{\mathsf{e}}\in M_{\mathsf{e}}$ and $m_{\mathsf{s}}\in
M_{\mathsf{s}}$, if $(s,m_{\mathsf{e}},m_{\mathsf{s}},s_{1})\in\rho$ and
$(s,m_{\mathsf{e}},m_{\mathsf{s}},s_{2})\in\rho$ then $s_{1}=s_{2}$. Condition
(1) states that every state has a successor, and (2) states that the moves
chosen by the two players uniquely determine a successor. We define the
functions $\mathit{Act}_{\mathsf{e}}:\mathcal{S}\to 2^{M_{\mathsf{e}}}$ and
$\mathit{Act}_{\mathsf{s}}:\mathcal{S}\times M_{\mathsf{e}}\to
2^{M_{\mathsf{s}}}$ that indicate the enabled moves of a player:
$\begin{array}[]{lll}\mathit{Act}_{\mathsf{e}}(s)&:=&\\{m_{\mathsf{e}}\in
M_{\mathsf{e}}\mid\exists m_{\mathsf{s}}\in M_{\mathsf{s}}.\exists
s^{\prime}\in\mathcal{S}.\;(s,m_{\mathsf{e}},m_{\mathsf{s}},s^{\prime})\in\rho\\},\\\
\mathit{Act}_{\mathsf{s}}(s,m_{\mathsf{e}})&:=&\\{m_{\mathsf{s}}\in
M_{\mathsf{s}}\mid\exists
s^{\prime}\in\mathcal{S}.\;(s,m_{\mathsf{e}},m_{\mathsf{s}},s^{\prime})\in\rho\\}.\end{array}$

A game on $G$ is played by Player $\mathit{Env}$ and Player $\mathit{Sys}$ as
follows. In a state $s\in\mathcal{S}$, Player $\mathit{Env}$ chooses a move
$m_{\mathsf{e}}\in\mathit{Act}_{\mathsf{e}}(s)$, Player $\mathit{Sys}$ chooses
a move $m_{\mathsf{s}}\in\mathit{Act}_{\mathsf{s}}(s,m_{\mathsf{e}})$. These
choices define the next state $s^{\prime}$ such that
$(s,m_{\mathsf{e}},m_{\mathsf{s}},s^{\prime})\in\rho$, The game then continues
from $s^{\prime}$. The resulting infinite sequence
$\pi=s_{0},s_{1},s_{2},\ldots\in\mathcal{S}^{\omega}$ of states is called a
_play_. For $p\in\\{\mathit{Env},\mathit{Sys}\\}$ we define
$1-p:=\mathit{Sys}$ when $p=\mathit{Env}$, and $1-p:=\mathit{Env}$ when
$p=\mathit{Sys}$. A _strategy for Player $\mathit{Env}$_ is a function
$\sigma_{\mathsf{e}}:\mathcal{S}^{+}\to M_{\mathsf{e}}$ where
$\sigma_{\mathsf{e}}(s_{0},\ldots,s_{n})=m_{\mathsf{e}}$ implies
$m_{\mathsf{e}}\in\mathit{Act}_{\mathsf{e}}(s_{n})$. A _strategy for Player
$\mathit{Sys}$_ is a function $\sigma_{\mathsf{s}}:\mathcal{S}^{+}\times
M_{\mathsf{e}}\to M_{\mathsf{s}}$ such that
$\sigma_{\mathsf{s}}((s_{0},s_{1},\ldots,s_{n}),m_{\mathsf{e}})=m_{\mathsf{s}}$
implies $m_{\mathsf{s}}\in\mathit{Act}_{\mathsf{s}}(s_{n},m_{\mathsf{e}})$. We
denote with $\mathit{Strat}_{p}(G)$ the set of all strategies for Player
$p\in\\{\mathit{Env},\mathit{Sys}\\}$.

Given $s\in\mathcal{S}$ and strategies $\sigma_{\mathsf{e}}$ and
$\sigma_{\mathsf{s}}$ for the two players, we denote with
$\mathit{Outcome}(s,\sigma_{\mathsf{e}},\sigma_{\mathsf{s}})$ the unique play
$s_{0},s_{1},s_{2},\ldots$ such that $s_{0}=s$, and for all $i\in\mathbb{N}$
there exist $m_{\mathsf{e}}\in M_{\mathsf{e}}$ and $m_{\mathsf{s}}\in
M_{\mathsf{s}}$ such that
$\sigma_{\mathsf{e}}(s_{0},s_{1}\ldots,s_{i})=m_{\mathsf{e}}$,
$\sigma_{\mathsf{s}}((s_{0},s_{1}\ldots,s_{i}),m_{\mathsf{e}})=m_{\mathsf{s}}$
and $(s_{i},m_{\mathsf{e}},m_{\mathsf{s}},s_{i+1})\in\rho$. Given a
$\sigma_{p}\in\mathit{Strat}_{p}(G)$ and $s\in\mathcal{S}$, we define
$\mathit{Plays}(s,\sigma_{p}):=\\{\pi\in\mathcal{S}^{\omega}\mid\exists\sigma_{1-p}\in\mathit{Strat}_{1-p}(G).\mathit{Outcome}(s,\sigma_{\mathit{Env}},\sigma_{\mathit{Sys}})=\pi\\}$.
An _objective_ is a set $\Omega\subseteq\mathcal{S}^{\omega}$. The set of
_states winning for Player $p$_ with respect to objective $\Omega$ is
$W_{p}(G,\Omega):=\\{s\in\mathcal{S}\mid\exists\sigma\in\mathit{Strat}_{p}(G).\mathit{Plays}(s,\sigma)\subseteq\Omega\\}.$

##  5\. Reactive Program Games

In this section, we define _reactive program games_ , a symbolic model that we
use to specify and synthesize reactive programs that operate over infinite
domains. Figure 1(a), Figure 2, Figure 3, and Figure 4(a) depict examples of
reactive program games. The interpretation of the function symbols appearing
in a reactive program game is required to conform to a given first-order
theory $T$. Unless stated otherwise, we consider the theories of linear
(integer or real) arithmetic. The reactive program game in Figure 1(a), is
defined in the theory of linear integer arithmetic.

###### Definition 5.1 (Reactive Program Game Structure).

A _reactive program game structure_ is a tuple
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$ with the
following components. $T$ is a first-order theory.
$\mathbb{I}\subseteq\mathit{Vars}$ is a finite set of _input variables_.
$\mathbb{X}\subseteq\mathit{Vars}$ is a finite set of _program variables_
where $\mathbb{I}\cap\mathbb{X}=\emptyset$. $L$ is a finite set of _game
locations_. $\mathit{Inv}:L\to\mathit{FOL}(\mathbb{X})$ maps each location to
a _location invariant_. $\delta\subseteq
L\times\mathit{QF}(\mathbb{X}\cup\mathbb{I})\times(\mathbb{X}\to\mathcal{T}_{F})\times
L$ is a finite _symbolic transition relation_ , where for every $l\in L$ the
set of _outgoing transition guards_ $\mathit{Guards}(l):=\\{g\mid\exists
u,l^{\prime}.\leavevmode\nobreak\ (l,g,u,l^{\prime})\in\delta\\}$ satisfies
the conditions:

  * (1)

$\bigvee_{g\in\mathit{Guards}(l)}g\equiv_{T}\top$, and for all
$g_{1},g_{2}\in\mathit{Guards}(l)$ with $g_{1}\neq g_{2}$ it holds that
$g_{1}\land g_{2}\equiv_{T}\bot$,

  * (2)

for all $g,u,l_{1},l_{2}$, if $(l,g,u,l_{1})\in\delta$ and
$(l,g,u,l_{2})\in\delta$, then $l_{1}=l_{2}$, and

  * (3)

for every $l\in L$ and $\mathbf{x}\in\mathit{Assignments}(\mathbb{X})$ such
that $\mathbf{x}\models_{T}\mathit{Inv}(l)$ there exist a transition
$(l,g,u,l^{\prime})\in\delta$ and
$\mathbf{i}\in\mathit{Assignments}(\mathbb{I})$ such that
$\mathbf{x}\uplus\mathbf{i}\models_{T}g$ and
$\mathbf{x^{\prime}}\models_{T}\mathit{Inv}(l^{\prime})$ where
$\mathbf{x}^{\prime}(x)=\chi_{\mathbf{x}\uplus\mathbf{i}}(u(x))$ for every
$x\in\mathbb{X}$.

The requirements on $\delta$ imply for each $l\in L$ that: (1) the guards in
$\mathit{Guards}(l)$ partition the set
$\mathit{Assignments}(\mathbb{X}\cup\mathbb{I})$. (2) each pair of
$g\in\mathit{Guards}(l)$ and update $u$ can label at most one outgoing
transition from $l$, and (3) if there is an assignment satisfying the location
invariant at $l$, then there is an input assignment for which there is a
possible transition, i.e., there are no dead-end states. We define

  * •

the set of _input assignments_ in $\mathcal{G}$ as
$\mathit{Inputs}_{\mathcal{G}}:=\mathit{Assignments}(\mathbb{I})$, and

  * •

the set of _updates_ in $\mathcal{G}$ as
$\mathit{Updates}_{\mathcal{G}}:=\\{u\in\mathbb{X}\to\mathcal{T}_{F}\mid\exists
l,g,l^{\prime}.(l,g,u,l^{\prime})\in\delta\\}$.

The semantics of the reactive program game structure $\mathcal{G}$ is a
possibly infinite-state game structure. The set of _states of the reactive
program game structure_ $\mathcal{G}$ consists of pairs $(l,\mathbf{x})$ of
game location $l$ and assignment $\mathbf{x}$ to the program variables
$\mathbb{X}$. The moves of Player $\mathit{Env}$ (modeling the environment)
are the input assignments $\mathit{Inputs}_{\mathcal{G}}$ and are potentially
infinitely many. Player $\mathit{Sys}$ (corresponding to the program being
synthesized) chooses the updates to the program variables (from the set
$\mathit{Updates}_{\mathcal{G}}$) and has, therefore, by definition only
finitely many possible moves.

Remark: Location invariants are used to define the state-space of a reactive
program game, and thus they provide modeling flexibility. They also enable the
symbolic construction of sub-games, which are useful in game-solving
procedures. When all the location invariants in a game structure are $\top$,
as, for instance, in our examples, we omit them for the sake of brevity.

###### Definition 5.2 (Semantics of Reactive Program Game Structures).

Let $\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$ be a
reactive program game structure. The semantics of $\mathcal{G}$ is the game
structure
$\llbracket\mathcal{G}\rrbracket=(\mathcal{S},M_{\mathsf{e}},M_{\mathsf{s}},\rho)$
where

  * •

$\mathcal{S}:=\\{(l,\mathbf{x})\in
L\times\mathit{Assignments}(\mathbb{X})\mid\mathbf{x}\models_{T}\mathit{Inv}(l)\\}$;

  * •

$M_{\mathsf{e}}:=\mathit{Inputs}_{\mathcal{G}}$,
$M_{\mathsf{s}}:=\mathit{Updates}_{\mathcal{G}}$;

  * •

the transition relation $\rho$ contains
$((l,\mathbf{x}),\mathbf{i},u,(l^{\prime},\mathbf{x}^{\prime}))$ if and only
if

    * –

there exists $g\in\mathit{Guards}(l)$ such that $(l,g,u,l^{\prime})\in\delta$
and $\mathbf{x}\uplus\mathbf{i}\models_{T}g$, and

    * –

$\mathbf{x}^{\prime}(x)=\chi_{\mathbf{x}\uplus\mathbf{i}}(u(x))$ for every
$x\in\mathbb{X}$, and
$\mathbf{x}^{\prime}\models_{T}\mathit{Inv}(l^{\prime})$.

The transition relation $\rho$ is well-defined as the conditions on $\delta$
in Definition 5.1 ensure that given $(l,\mathbf{x})\in S$,
$\mathbf{i}\in\mathit{Inputs}_{\mathcal{G}}$, and
$u\in\mathit{Updates}_{\mathcal{G}}$, the successor location $l^{\prime}$ and
program variable assignment $\mathbf{x}^{\prime}$ are uniquely determined. The
successor assignment $\mathbf{x}^{\prime}$ is obtained by updating the value
of each program variable $x\in\mathbb{X}$ according to the corresponding
update term $u(x)$ and assignment $\mathbf{i}$ to the input variables. For a
state $s=(l,\mathbf{x})\in\mathcal{S}$, we denote with $\mathit{loc}(s):=l$
the location of $s$.

We consider the realizability problem for reactive program games, formally
defined below.

Realizability and Program Synthesis for Reactive Program Games Given a
reactive program game structure
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$, objective
$\Omega$ for Player $\mathit{Sys}$, and $l\in L$, the _realizability problem_
is to determine if $(l,\mathbf{x})\in
W_{\mathit{Sys}}(\llbracket\mathcal{G}\rrbracket,\Omega)$ for every
$\mathbf{x}\in\mathit{Assignments}(\mathbb{X})$ with
$\mathbf{x}\models_{T}\mathit{Inv}(l)$. The _program synthesis problem_ is to
compute a strategy for Player $\mathit{Sys}$ that is winning from every
$(l,\mathbf{x})\in W_{\mathit{Sys}}(\llbracket\mathcal{G}\rrbracket,\Omega)$.

##  6\. Symbolic Procedures for Reactive Program Games

Given a reactive program game structure
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$ and an objective
$\Omega$ for Player $p$, the _game solving problem_ is to compute the set of
states $W_{p}(\llbracket\mathcal{G}\rrbracket,\Omega)$. The realizability
question for given location $l$ can be answered by checking if this set
contains all states $s\in\mathcal{S}$ with $\mathit{loc}(s)=l$.

We present procedures for solving reactive program games with important types
of objectives considered in reactive synthesis. Similarly to the respective
algorithms for finite-state games, a building block of these procedures is the
computation of the so-called attractor sets. We lift the classical algorithms
to infinite-state games by employing a symbolic attractor computation
procedure. Since the corresponding game-solving problems are generally
undecidable, the game-solving procedures are not guaranteed to terminate. In
the next section, we propose an acceleration technique, which, when it
succeeds, enforces convergence.

###  6.1. Symbolic Representation and Operations

We now present the basic building blocks of our procedures for solving
reactive program games: the symbolic representation of sets of states and the
necessary operations on this representation.

We represent and manipulate possibly infinite sets of states symbolically,
using formulas in $\mathit{FOL}$($\mathbb{X}$) to represent sets of
assignments to the variables in $\mathbb{X}$. We define our _symbolic domain_
$\mathcal{D}:=L\to\mathit{FOL}(\mathbb{X})$ to be the set of functions mapping
locations to first-order formulas in $\mathit{FOL}$($\mathbb{X}$). The
semantics $\llbracket\cdot\rrbracket:\mathcal{D}\to 2^{\mathcal{S}}$ of an
element $d$ of $\mathcal{D}$ is defined by $\llbracket
d\rrbracket:=\\{(l,\mathbf{x})\in\mathcal{S}\mid\mathbf{x}\models_{T}d(l)\land\mathbf{x}\models_{T}\mathit{Inv}(l)\\}.$
Note that locations are treated explicitly.

We perform set operations on $\mathcal{D}$ symbolically, per location.
Formally, for $d_{1},d_{2}\in\mathcal{D}$ we define $\neg d_{1}:=\lambda
l.\;\neg d_{1}(l)$, $d_{1}\wedge d_{2}:=\lambda l.\;d_{1}(l)\wedge d_{2}(l)$,
$d_{1}\vee d_{2}:=\lambda l.\;d_{1}(l)\vee d_{2}(l)$, and write
$d_{1}\equiv_{T}d_{2}$ iff $\llbracket d_{1}\rrbracket=\llbracket
d_{2}\rrbracket$. We define $d[l\mapsto\varphi]:=(\lambda
l^{\prime}.\leavevmode\nobreak\ \text{if}\leavevmode\nobreak\
l=l^{\prime}\leavevmode\nobreak\ \text{then}\leavevmode\nobreak\
\varphi\leavevmode\nobreak\ \text{else}\leavevmode\nobreak\ d(l^{\prime}))$
for $d\in\mathcal{D}$, which is obtained from $d$ by changing the symbolic
value at a given location. We write
$\\{l_{1}\mapsto\varphi_{1},\dots,l_{n}\mapsto\varphi_{n}\\}$ for the element
$d\in\mathcal{D}$ where $d(l_{i})=\varphi_{i}$, for $i\in\\{1,\dots,n\\}$ and
$d(l)=\bot$ for $l\not\in\\{l_{1},\dots,l_{n}\\}$.

##### Attractor.

Let $R\subseteq\mathcal{S}$ be a set of states. The set of states from which
Player $p$ can enforce reaching a state in $R$ is called the _Player
$p$-attractor for $R$ in $\llbracket\mathcal{G}\rrbracket$_ and is denoted by
$\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(R)$. Formally,

$\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(R):=\\{s\in\mathcal{S}\mid\exists\sigma\in\mathit{Strat}_{p}(\llbracket\mathcal{G}\rrbracket).\forall\pi\in\mathit{Plays}(s,\sigma).\exists
n\in\mathbb{N}.\;\pi[n]\in R\\}.$

In the finite-state case, attractors are computed by a fixpoint iteration
using the so-called _controllable predecessor operators_. We define their
symbolic counterparts

$\mathit{CPre}_{\mathcal{G},\mathit{Env}}(d):=\lambda l.\leavevmode\nobreak\
\mathit{Inv}(l)\land\exists\mathbb{I}.\leavevmode\nobreak\
\bigwedge_{(l,g,u,l^{\prime})\in\delta}\left(g\land\mathit{Inv}(l^{\prime})[u]\to
d(l^{\prime})[u]\right)$ $\mathit{CPre}_{\mathcal{G},\mathit{Sys}}(d):=\lambda
l.\leavevmode\nobreak\
\mathit{Inv}(l)\land\forall\mathbb{I}.\leavevmode\nobreak\
\bigvee_{(l,g,u,l^{\prime})\in\delta}\left(g\land\mathit{Inv}(l^{\prime})[u]\land
d(l^{\prime})[u]\right)$

for $d\in\mathcal{D}$ where $\varphi[u]:=\varphi[c\mapsto u(c)\mid
c\in\mathbb{X}]$ for $u\in\mathit{Updates}_{\mathcal{G}}$ applies the
substitution defined by $u\in\mathbb{X}\to\mathcal{T}_{F}$ to
$\varphi\in\mathit{FOL}(\mathbb{X})$ resulting in the formula obtained by the
simultaneous replacement of all $x\in\mathbb{X}$ with the respective term
$u(x)$. By definition, we have that
$\mathit{CPre}_{\mathcal{G},\mathit{Env}},\mathit{CPre}_{\mathcal{G},\mathit{Sys}}:\mathcal{D}\to\mathcal{D}$.

function  _Attractor(
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$,
$\mathit{p}\in\\{\mathit{Sys},\mathit{Env}\\}$, $d\in\mathcal{D}$)_

1 $a^{0}$ := $\lambda l.\leavevmode\nobreak\ \bot$; $a^{1}$ := $d$

2 for  _$n=1,2,\ldots$_ do

3 if  _$a^{n}\equiv_{T}a^{n-1}$_ then return $a^{n}$

4 $a^{n+1}:=a^{n}\lor\mathit{CPre}_{\mathcal{G},p}(a^{n})$

Algorithm 1 Symbolic semi-algorithm for computing
$\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket d\rrbracket)$.

$l_{0}$$l_{1}$$i\geq
5$$\mathit{skip}$$i<5$$x:=i$$x\not\in[3,5]$$\mathit{skip}$$x\in[3,5]$$x:=0.5\cdot
x$$\mathit{skip}$

(a) The game structure.

$a_{0}(l_{1})=a_{1}(l_{1})=\bot$
---
$a_{2}(l_{1})=x\not\in[3,5]$
$a_{3}(l_{1})=x\not\in[3,5]\lor x\in[3,5]\land 0.5\cdot x\not\in[3,5]$
$\quad\equiv x\not\in[3,5]\lor x\in[3,5]\land x\not\in[6,10]\equiv\top$
$a_{4}(l_{1})=\top$ (fixpoint as $\equiv a_{3}(l_{1})$)

(b) Iterations of Attractor for location $l_{1}$.

Figure 4.  (right) A reactive program game with locations $\\{l_{0},l_{1}\\}$,
input $i$ and program variable $x$, both of type Real. (left) The iterative
computation of
$\textsc{Attractor}(\mathcal{G},\mathit{Sys},\\{l_{0}\mapsto\top\\})$ for
location $l_{1}$.

Algorithm 1 can be used to compute
$\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(R)$ symbolically, given a
symbolic representation of $R$. Figure 4(b) shows an example of such a
computation, and the next proposition states its soundness.

###### Proposition 6.1.

Let $\mathcal{G}$ be a reactive program game structure,
$\mathit{p}\in\\{\mathit{Sys},\mathit{Env}\\}$ and $d\in\mathcal{D}$. If
Attractor($\mathcal{G}$,$p$,$d$) terminates and returns $\mathit{attr}$, then
$\llbracket
attr\rrbracket=\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket
d\rrbracket)$.

###  6.2. Symbolic Game Solving

In reactive program games we consider _objectives defined in terms of the
locations appearing in a play_. Below we recall the definitions of common
types of objectives and the classical algorithms for solving such games,
formulated symbolically in the context of reactive program games.

##### Reachability and Safety Games.

The _reachability objective_ $\mathit{Reach}(R)$ for $R\subseteq L$, requires
that some state with location in $R$ is visited eventually. Formally,
$\mathit{Reach}(R):=\\{\pi\in\mathcal{S}^{\omega}\mid\exists
n\in\mathbb{N}.\;\mathit{loc}(\pi[n])\in R\\}$. The dual, _safety objective_
$\mathit{Safety}(S)$ for $S\subseteq L$, requires that only locations in $S$
are visited by the play. Formally,
$\mathit{Safety}(S):=\\{\pi\in\mathcal{S}^{\omega}\mid\forall
n\in\mathbb{N}.\;\mathit{loc}(\pi[n])\in S\\}$.

Reactive program games with reachability objectives for a Player $p$ can be
solved by applying Algorithm 1 to compute the Player $p$-attractor for the set
of states with locations in $R$. More concretely, Proposition 6.1 directly
implies that
$W_{p}(\llbracket\mathcal{G}\rrbracket,\mathit{Reach}(R))=\llbracket\textsc{Attractor}(\mathcal{G},p,\\{l\mapsto\mathit{Inv}(l)\mid
l\in R\\})\rrbracket$ holds if the iteration in
Attractor($\mathcal{G}$,$p$,$\\{l\mapsto\mathit{Inv}(l)\mid l\in R\\}$)
terminates.

Since safety is dual to reachability, we can solve a reactive program game
with safety objective $\mathit{Safety}(S)$ for Player $p$ by solving the game
with a reachability objective for Player $1-p$ where the set of goal locations
is $L\setminus S$. More precisely, we call Algorithm 1 as
Attractor($\mathcal{G}$,$1-p$,($\\{l\mapsto\mathit{Inv}(l)\mid l\not\in
S\\}$). If it terminates and returns $\mathit{attr}$, then we have that
$W_{p}(\llbracket\mathcal{G}\rrbracket,\mathit{Safety}(S))=\llbracket\neg\mathit{attr}\wedge\mathit{Inv}\rrbracket.$

##### Büchi and Co-Büchi Games.

The _Büchi objective_ $\mathit{Buchi}(B)$ for a set of accepting locations
$B\subseteq L$, requires that $B$ is visited infinitely often:
$\mathit{Buchi}(B):=\\{\pi\in\mathcal{S}^{\omega}\mid\forall
m\in\mathbb{N}.\exists n>m.\;\mathit{loc}(\pi[n])\in B\\}$. The dual, _co-
Büchi objective_ $\mathit{coBuchi}(C)$ for rejecting locations $C\subseteq L$
requires that $C$ is visited only finitely many times:
$\mathit{coBuchi}(C):=\\{\pi\in\mathcal{S}^{\omega}\mid\exists
m\in\mathbb{N}.\forall n\geq m.\;\mathit{loc}(\pi[n])\not\in C\\}$.

Employing the symbolic attractor computation procedure in Algorithm 1, we lift
the classical algorithm for solving finite-state games with Büchi and co-Büchi
objectives to a procedure for solving reactive program games with these
objectives. The procedure, given in Algorithm 2, is based on a nested fixpoint
computation, as the classical algorithm. The inner fixpoint iteration computes
attractor sets for the Player $p$ with Büchi objective $\mathit{Buchi}(B)$,
and the outer fixpoint iteration computes increasing underapproximations of
the set of winning states for the Player $1-p$ with co-Büchi objective
$\mathit{coBuchi}(B)$. At each iteration, we first compute $a^{n}$, which
represents the states from which Player $p$ can enforce a visit to $f^{n}$, by
calling Algorithm 1. Then, we compute $w^{n}_{1-p}$, which represents the
states from which Player $1-p$ can prevent Player $p$ from _revisiting_
$f^{n}$. This is done by calling Algorithm 1 to compute an attractor for
Player $1-p$.

function  _SolveBüchiGame(
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$,
$\mathit{p}\in\\{\mathit{Sys},\mathit{Env}\\}$, $f\in\mathcal{D}$)_

1 $f^{0}$ := $\lambda l.\leavevmode\nobreak\ \top$; $f^{1}$ := $f$;
$w_{1-p}^{0}:=\lambda l.\bot$

2 for  _$n=1,2,\ldots$_ do

3 if  _$f^{n}\equiv_{T}f^{n-1}$_ then return $w_{1-p}^{n-1}$

4 $a^{n}:=\textsc{Attractor}(\mathcal{G},p,f^{n})$

5
$w^{n}_{1-p}:=\textsc{Attractor}(\mathcal{G},1-p,\neg\mathit{CPre}_{\mathcal{G},p}(a^{n}))$

6 $f^{n+1}:=f^{n}\wedge(\mathit{Inv}\land\neg w^{n}_{1-p})$

Algorithm 2 Symbolic semi-algorithm for computing the set of states winning
for Player $1-p$ in a game with a Büchi objective for Player $p$ with set of
accepting states represented by $f$.

To solve a reactive program Büchi game defined by a set of locations $B$ in
$\mathcal{G}$, we execute Algorithm 2 with $f:=\\{l\mapsto\mathit{Inv}(l)\mid
l\in B\\}$. If the computation reaches a fixpoint, that is, for some iteration
$m$ we have that $f^{m}\equiv_{T}f^{m-1}$ (and hence,
$w_{1-p}^{m}=w^{m-1}_{1-p}$), then we have that $\llbracket
w^{m}_{1-p}\rrbracket=W_{1-p}(\llbracket\mathcal{G}\rrbracket,\mathit{coBuchi}(B))$
and $\llbracket\neg
w^{m}_{1-p}\wedge\mathit{Inv}\rrbracket=W_{p}(\llbracket\mathcal{G}\rrbracket,\mathit{Buchi}(B))$.
This follows from the correctness of the classical algorithm for solving Büchi
games (Grädel et al., 2002; Bloem et al., 2018).

###  6.3. Strategy Extraction

When the answer to the realizability question for a reactive program game is
positive, that is, for the given location $l_{\mathit{init}}$ all states
$s\in\mathcal{S}$ with $\mathit{loc}(s)=l_{\mathit{init}}$ are winning for
Player $\mathit{Sys}$, we want to extract a winning strategy for Player
$\mathit{Sys}$ in the form of a program. To this end, we lift the strategy-
generation extensions of the classical algorithms on which the symbolic
procedures are based.

We represent winning strategies for Player $\mathit{Sys}$ as simple GOTO
programs, with labels corresponding to locations, and which contain goto
statements, read statements for the input variables, conditionals, and the
selected updates from the game in form of (parallel) assignments to the
program variables. Later on, we will extend these programs with additional
labels, auxiliary variables, and simple assignments to the auxiliary
variables. We now describe how the symbolic game-solving procedures described
earlier in this section are extended to produce such programs.

The basic building block for strategy generation is the extraction of a
program statement in a location $l\in L$ from a strategic decision based on
the controllable predecessor $\mathit{CPre}_{\mathcal{G},\mathit{Sys}}(d)(l)$
for some $d\in\mathcal{D}$. This requires a strategy that enforces reaching
$d$ in one step from $l$. Such a strategy selects a transition
$(l,g,u,l^{\prime})$ where the guard $g$ holds, and after the update $u$,
$d(l^{\prime})$ and $\mathit{Inv}(l^{\prime})$ hold. For example, for
$d=\\{l^{\prime}\mapsto x>0\\}$, guard $x<5$, update $x:=x+1$, and
$\mathit{Inv}(l^{\prime})=\top$, we extract the program statement
$\texttt{if}\leavevmode\nobreak\ (x<5\land x+1>0)\leavevmode\nobreak\
\texttt{then}\leavevmode\nobreak\ x:=x+1;\leavevmode\nobreak\
\texttt{{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}goto}}\leavevmode\nobreak\
l^{\prime}\leavevmode\nobreak\ \texttt{else}\dots$ which could then be
followed by other such transition statements. Note that before branching
according to the choice of the strategy at a given location, we have to add
read statements for the input variables.

For games with reachability objectives, a winning strategy can be generated
based on the attractor computation augmented with keeping a record of the
“layers” of the attractor, that is the individual $a^{1},a^{2},\ldots$ until
termination. For each location $l\in L$ and states in $a^{n+1}(l)\land\lnot
a^{n}(l)$, that is, states added to the attractor in step $n+1$, the winning
strategy will select a transition based on the controllable predecessor
$\mathit{CPre}_{\mathcal{G},\mathit{Sys}}(a^{n})(l)$, resulting in a program
statement as described above.

For safety games, we first compute the set of states
$W_{\mathit{Sys}}(\llbracket\mathcal{G}\rrbracket,\mathit{Safety}(S))$ winning
for Player $\mathit{Sys}$, symbolically represented by some $w\in\mathcal{D}$.
Then, for each location $l\in L$, we generate a program statement representing
a strategy to remain in $w$, that is, based on
$\mathit{CPre}_{\mathcal{G},\mathit{Sys}}(w)(l)$.

The procedure for solving games with Büchi and co-Büchi objectives can also be
extended with the necessary bookkeeping to generate winning strategies by
using strategies (programs) generated from the controllable predecessor
operator and attractor computation as building blocks.

##### What about the environment?

Winning strategies for Player $\mathit{Env}$ are less useful as we are usually
interested in strategies that give us an implementation of the desired system.
They can be helpful as counterexamples, but for reactive program games,
extracting a strategy for Player $\mathit{Env}$ is more difficult, as the set
of moves $M_{\mathsf{e}}:=\mathit{Inputs}_{\mathcal{G}}$ is potentially
infinite.

##  7\. Enforcement Acceleration

The symbolic procedure for attractor computation, and hence the procedures for
solving games, presented in the previous section do not always terminate when
the set of states $\mathcal{S}$ is infinite.

As we explained in Section 3, the attractor computation for the reactive
program game structure in Figure 1(a) and the reachability winning condition
for Player $\mathit{Sys}$ to reach $l_{G}$, does not terminate. Applying the
method from the previous section as
$\textsc{Attractor}(\mathcal{G},\mathit{Sys},\\{l_{G}\mapsto\top\\})$, we get:
$a^{2}=\\{l_{0}\mapsto(x\leq 42),l_{G}\mapsto\top\\}$,
$a^{3}=\\{l_{0}\mapsto(\forall i.x\leq 42\lor i=0\lor x+i\leq 42\lor x-i\leq
42),l_{G}\mapsto\top\\}$, which simplifies to $\\{l_{0}\mapsto(x\leq
43),l_{G}\mapsto\top\\}$, $a^{4}=\\{l_{0}\mapsto(x\leq
44),l_{G}\mapsto\top\\}$, $a^{5}=\\{l_{0}\mapsto(x\leq
45),l_{G}\mapsto\top\\}$,…. A fixpoint is never reached as $\llbracket
a^{n}\rrbracket$ keeps growing in every iteration.

However, arguing for termination on an intuitive level is done quite simply as
already shown in Section 1. If $x\leq 42$ or $i=0$ in location $l_{0}$, then
$\\{l_{G}\mapsto\top\\}$ is reached in one step. Otherwise, by choosing the
correct transition in location $l_{0}$, Player $\mathit{Sys}$ can force $x$ to
decrease and go back to location $l_{0}$. Since the game is back in $l_{0}$,
decreasing $x$ can be iterated, eventually leading to $x\leq 42$.

While we cannot ensure termination in general, we will augment the attractor
computation with an acceleration operation. This operation should extend the
computed attractor set with states from infinitely many levels in finitely
many steps. Since the attractor captures strategic decisions, this
acceleration operation allows us to handle unbounded strategy loops as the one
in Figure 1(a).

For the rest of this section, we fix a first-order logical theory $T$.

###  7.1. Accelerating Symbolic Attractor Computation

From a more general perspective, the termination argument used in our running
example above states the following: _If in some location $l$, starting at some
state not part of the goal states, Player $p$ can enforce coming back to $l$
and make progress towards the goal, then Player $p$ can enforce reaching the
goal eventually._ Our aim is to employ such reasoning to accelerate the
computation performed by Algorithm 1. Suppose that $a^{n}$ is the symbolic
representation of the current subset of
$\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket d\rrbracket)$ at
the $n$-th iteration of the loop in Algorithm 1. Let $l\in L$ be a location in
the reactive program game. The goal of the acceleration operation applied to
location $l$ is to expand the set $\llbracket a^{n}\rrbracket$ by adding a set
of states at location $l$ from which Player $p$ can enforce reaching
$\llbracket a^{n}\rrbracket$ by enforcing a loop at location $l$ to be
executed some number of times. To perform such reasoning automatically, we
first introduce the new notion of _acceleration lemmas_ that allows us to
formalize inductive arguments such as the one from our running example. Next,
to perform the acceleration computation at a given location $l$, we construct
from $\mathcal{G}$ a new game structure, called a _loop game_ which we use to
reason about the loops from location $l$ back to itself. In the following, we
first give the formal definitions of these concepts and then proceed with the
description of the procedure for attractor acceleration.

#### Acceleration Lemmas

An acceleration lemma, formally introduced below, is a triple
$(\mathit{base},\mathit{step},\mathit{conc})$ of $\mathit{FOL}$ formulas. It
formalizes an inductive statement as follows. The _base condition_
$\mathit{base}$ characterizes a set of target states. The _step relation_
$\mathit{step}$ is a relation between states. The _conclusion_ $\mathit{conc}$
characterizes states from which every sequence of states in which each pair of
consecutive states conform to the relation $\mathit{step}$ will necessarily
reach the target set $\mathit{base}$. Thus, intuitively, the relation
$\mathit{step}$ captures a ranking argument for establishing the reachability
of $\mathit{base}$ starting from $\mathit{conc}$.

###### Definition 7.1 (Acceleration Lemma).

An _acceleration lemma_ is a triple
$(\mathit{base},\mathit{step},\mathit{conc})$ of formulas
$\mathit{base}\in\mathit{FOL}(V)$, $\mathit{step}\in\mathit{FOL}(V\cup
V^{\prime})$, and $\mathit{conc}\in\mathit{FOL}(V)$ for some
$V\subseteq\mathit{Vars}$, such that:

  * •

For every infinite sequence $\alpha\in\mathit{Assignments}(V)^{\omega}$, if it
holds that $\alpha[0]\models_{T}\mathit{conc}$ and
$\langle\alpha[i],\alpha[i+1]\rangle\models_{T}\mathit{step}$ for all
$i\in\mathbb{N}$, then there exists some $k\in\mathbb{N}$ such that
$\alpha[k]\models_{T}\mathit{base}$,

  * •

and, for every $\nu\in\mathit{Assignments}(V)$ with
$\nu\models_{T}\mathit{conc}$ and $\nu\not\models_{T}\mathit{base}$, and for
every $\nu^{\prime}\in\mathit{Assignments}(V)$ with
$\langle\nu,\nu^{\prime}\rangle\models_{T}\mathit{step}$, it holds that
$\nu^{\prime}\models_{T}\mathit{conc}$,

where $\langle\nu,\nu^{\prime}\rangle(x):=\nu(x)$ for $x\in V$ and
$\langle\nu,\nu^{\prime}\rangle(x^{\prime}):=\nu^{\prime}(x)$ for
$x^{\prime}\in V^{\prime}$.

We denote with $\mathsf{Lemmas}(V)$ the set of acceleration lemmas over the
set of variables $V$.

The first condition in the definition formalizes the intuition above. The
second condition is necessary for ensuring that the step relation can be
iterated. It requires that starting from any state that satisfies
$\mathit{conc}$ but not $\mathit{base}$, any successor with respect to the
relation $\mathit{step}$ is also in $\mathit{conc}$.

###### Example 7.2.

Consider $V=\\{x\\}$ where $x$ is of integer type, and let
$\mathit{base}:=(x\leq 42)$, $\mathit{step}:=(x^{\prime}<x)$ and
$\mathit{conc}:=\top$. It is easy to see that
$(\mathit{base},\mathit{step},\mathit{conc})$ is an acceleration lemma, since
the relation $<$ is well-founded on $\\{z\in\mathbb{Z}\mid z\geq 42\\}$.∎

Acceleration lemmas express generic inductive statements in a logical form.
Employing an acceleration lemma $(\mathit{base},\mathit{step},\mathit{conc})$
to accelerate the $n$-th iteration of the attractor computation at location
$l$ will result in adding the states $\\{(l,\mathbf{x})\in
S\mid\mathbf{x}\models_{T}\mathit{conc}\\}$ to the computed attractor. This
operation is correct if the following conditions are satisfied. The first
condition is that _$\mathit{base}$ is already included in $a^{n}(l)$_. For a
given acceleration lemma this condition can be established by checking the
validity of a logical implication. The second condition requires that Player
$p$ can actually _enforce the repeated iteration of the step relation_ in the
game structure $\mathcal{G}$, against all possible behaviors of the opponent
Player $1-p$. More precisely, this means that starting from any state
$(l,\mathbf{x})$ satisfying the formula $\mathit{conc}$, Player $p$ should
have a strategy to reach a state $(l,\mathbf{x}^{\prime})$ such that
$(\mathbf{x},\mathbf{x}^{\prime})$ satisfies the relation $\mathit{step}$, or
reach the current subset $a^{n}$ of the attractor. Establishing satisfaction
of this condition is more difficult because it amounts to establishing the
existence of a local strategy for Player $p$ to enforce the step relation. We
show how we can reduce this question to attractor computation in a modified
game structure, the so-called loop game at location $l$, defined next.

#### Loop Games

The _loop game_ at location $l$ is a reactive program game structure obtained
from the reactive program game structure $\mathcal{G}$ and a given location
$l$. The game structure $\mathsf{LoopGame}(\mathcal{G},l,l_{\mathit{End}})$ is
constructed by adding a new location $l_{\mathit{End}}\not\in L$ to
$\mathcal{G}$ and redirecting all edges in $\mathcal{G}$ with target location
$l$ to the new location $l_{\mathit{End}}$. Intuitively, the loop game
“splits” the loops from location $l$ to itself and captures all possible
interactions between Player $\mathit{Sys}$ and Player $\mathit{Env}$ in
$\mathcal{G}$ that start from location $l$. The splitting of the loops allows
us to reason about iterated behavior from location $l$ back to itself. More
precisely, establishing that Player $p$ can enforce iterating the step
relation in location $l$ in $\mathcal{G}$ reduces to establishing that in the
loop game Player $p$ can enforce reaching $l_{\mathit{End}}$ from $l$ while
satisfying the step relation. We do the latter by computing an attractor for
Player $p$ in the loop game on $\mathit{step}$ from $l_{\mathit{End}}$ back to
$l$. We define loop games formally as follows.

###### Definition 7.3 (Loop Game).

Given a reactive program game structure
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$, a location
$l_{\mathit{Split}}\in L$, and a fresh location $l_{\mathit{End}}\not\in L$,
the _loop game_ is the reactive program game structure
$\mathsf{LoopGame}(\mathcal{G},l_{\mathit{Split}},l_{\mathit{End}}):=(T,\mathbb{I},\mathbb{X},L\cup\\{l_{\mathit{End}}\\},\mathit{Inv}^{\prime},\delta^{\prime})$,
where
$\mathit{Inv}^{\prime}:=\mathit{Inv}\cup\\{l_{\mathit{End}}\mapsto\mathit{Inv}(l_{\mathit{Split}})\\}$,
and $\delta^{\prime}:=\\{(l_{1},g,u,l_{2})\in\delta\leavevmode\nobreak\
\mid\leavevmode\nobreak\ l_{2}\neq
l_{\mathit{Split}}\\}\cup\\{(l,g,u,l_{\mathit{End}})\leavevmode\nobreak\
\mid\leavevmode\nobreak\
(l,g,u,l_{\mathit{Split}})\in\delta\\}\cup\\{(l_{\mathit{End}},\top,\lambda
x.x,l_{\mathit{End}})\\}$.

###### Example 7.4.

Figure 5 depicts the loop game
$\mathsf{LoopGame}(\mathcal{G},l_{0},l_{\mathit{End}})$ of our running example
in Figure 1(a).

#### Attractor Acceleration with Given Acceleration Lemmas.

We now give a high-level description of how the attractor computation for
Player $p$ is accelerated for a given location $l$ using a given acceleration
lemma $(\mathit{base},\mathit{step},\mathit{conc})$. We are applying
acceleration at some step $n$ of the algorithm, and $a^{n}$ is the current
subset of the attractor computed thus far. To apply the acceleration lemma, we
fist check that $\mathit{base}$ is included in $a^{n}(l)$. We then construct
the loop game $\mathsf{LoopGame}(\mathcal{G},l,l_{\mathit{End}})$. In this
loop game, we compute the attractor for Player $p$ on the step relation
$\mathit{step}$ in $l_{\mathit{End}}$ (we will see later how $\mathit{step}$
is encoded as a state formula with the help of auxiliary variables). We then
check that the attractor computed in the loop game includes the states with
location $l$ that satisfy $\mathit{conc}$. If both conditions hold, we know
that starting at location $l$ in a state that satisfies $\mathit{conc}$,
Player $p$ can enforce reaching $a^{n}(l)$ by iterating the strategy (from the
loop game) to enforce $\mathit{step}$ from $l$ back to $l$. To see this, note
that by Definition 7.1 we know that this will eventually lead to reaching
$\mathit{base}$, and hence also $a^{n}$. This justifies extending $a^{n}(l)$
with $\mathit{conc}$, that is, setting $a^{n}(l):=a^{n}(l)\vee\mathit{conc}$.
After that, we continue with the attractor computation, possibly applying
acceleration again. We now illustrate the use of acceleration lemmas on a
concrete example.

###### Example 7.5.

We use the method outlined above to accelerate the diverging attractor
computation shown at the beginning of this section, at the point where
$a^{3}=\\{l_{0}\mapsto(x\leq 43),l_{G}\mapsto\top\\}$.

We want to apply the acceleration lemma from Example 7.2 at location $l_{0}$.
First, we check that the base condition $\mathit{base}=(x\leq 42)$ of our
acceleration lemma is a subset of $a^{3}(l_{0})=(x\leq 43)$, which is indeed
the case. Then, we have to check that starting in $l_{0}$, Player
$\mathit{Sys}$ can either enforce the step relation and come back to $l_{0}$
or reach $a^{3}$. To do this, we consider the loop game
$\mathsf{LoopGame}(\mathcal{G},l_{0},l_{\mathit{End}})$. The condition above
is satisfied if Player $\mathit{Sys}$ can enforce reaching $l_{\mathit{End}}$
from $l_{0}$ in the loop game such that the relation $\mathit{step}$ is
satisfied by the initial (at $l_{0}$) and final (at $l_{\mathit{End}}$) values
of the program variables (or reach $a^{3}$). Therefore, we compute the
attractor for Player $\mathit{Sys}$ of $\\{l_{0}\mapsto(x\leq
43),l_{G}\mapsto\top,l_{\mathit{End}}\mapsto x<e_{x}\\}$ in the loop game.
Here $x<e_{x}$ corresponds to the step relation $\mathit{step}=x^{\prime}<x$,
where $e_{x}$ represents the initial value of $x$ before the iteration. This
“shift” is necessary as we are doing a backward computation. This attractor
computation in the loop game yields $\\{l_{0}\mapsto\forall
i.\leavevmode\nobreak\ i\neq 0\land x>42\to x+i<e_{x}\lor x-i<e_{x},\dots\\}$.
Since at $l_{0}$ we have completed the iteration, we can set $e_{x}:=x$ and
the formula simplifies to $\\{l_{0}\mapsto\top,\dots\\}$. This means that
Player $\mathit{Sys}$ can indeed iterate enforcing the step relation or reach
$a^{3}$.

The property of acceleration lemmas allows us to conclude that Player
$\mathit{Sys}$ can reach $a^{3}$ starting from $\mathit{conc}$ by iterating
$\mathit{step}$. Hence, we can add $\mathit{conc}=\top$ to the attractor set
at location $l_{0}$, which results in reaching a fixpoint and the computation
terminates. ∎

$l_{0}$$l_{\mathit{End}}$$l_{G}$$x>42\land i\neq 0$$x:=x+i$$x:=x-i$$x\leq
42\lor i=0$$x:=x$$\top$$x:=x$$\top$$x:=x$ Figure 5. Loop game
$\mathsf{LoopGame}(\mathcal{G},l_{0},l_{\mathit{End}})$ for the game structure
in Figure 1(a).

Thus far, we illustrated the usefulness of acceleration lemmas in attractor
computation. To transform this idea into a general procedure for attractor
acceleration, we have to account for the following aspects. In general, the
loop game can be complex itself, and the attractor computation in the loop
game may also benefit from acceleration. Hence, our acceleration technique
should support the _nested applications of lemmas_. Another crucial aspect of
the procedure is the actual _computation of acceleration lemmas_. A simple way
to realize this would be first to generate acceleration lemmas and then check
their applicability with the described technique, backtracking if the check is
not successful. However, this quickly becomes infeasible for large spaces of
possible lemmas and game structures requiring the application of nested
acceleration. To address this, our acceleration approach performs symbolic
attractor computation with “unknown” lemmas represented by uninterpreted
symbols. More precisely, our attractor acceleration technique has two main
components.

  * •

In the remainder of this section, we show how symbolic attractor computation
is enhanced with the application of acceleration lemmas as _uninterpreted
lemmas_. An essential part of this computation is the collection of
constraints on the unknown lemmas that capture conditions which guarantee that
the lemmas are applicable.

  * •

In Section 8, we describe how we generate instances of the unknown lemmas that
meet the accumulated constraints and, therefore, constitute applicable
acceleration lemmas.

#### Attractor Acceleration with Uninterpreted Lemmas.

To represent the unknown lemmas in the symbolic attractor computation, let us
fix a countably infinite set $\mathsf{LemmaSymb}$ of triples $(b,st,c)$ of
uninterpreted predicate symbols. The symbols in such a triple represent the
corresponding elements of an acceleration lemma. In the course of the symbolic
computation of attractors, we generate and accumulate constraints, elements of
$\mathit{Constraints}:=\mathit{FOL}(\emptyset)$, featuring these symbols. For
$\Phi\subseteq\mathit{FOL}$, we denote with $\mathsf{UsedLemmaSymbols}(\Phi)$
the set of triples whose symbols appear in $\Phi$.

function  _AttractorAcc(
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$,
$\mathit{p}\in\\{\mathit{Sys},\mathit{Env}\\}$, $d\in\mathcal{D}$)_

1 $a^{0}$ := $\lambda l.\leavevmode\nobreak\ \bot$; $a^{1}$ := $d$

2 for  _$n=1,2,\ldots$_ do

3 if  _$a^{n}\equiv_{T}a^{n-1}$_ then return $a^{n}$

if  _Accelerate? $(G,p,a^{n})=\\{l\\}$_ then

$(\Psi,\varphi):=\mathsf{AccA}(\mathcal{G},p,l,a^{n})$

$a^{n}(l):=a^{n}(l)\;\lor\;\mathsf{InstantiateLemmas}(\Psi,\varphi)$

4 $a^{n+1}:=a^{n}\lor\mathit{CPre}_{\mathcal{G},p}(a^{n})$

Algorithm 3 Accelerated semi-algorithm for computing
$\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket d\rrbracket)$.

Algorithm 3 shows the procedure AttractorAcc for attractor computation with
acceleration. At each iteration, a _heuristic function Accelerate?_ is used to
decide whether an acceleration should be attempted at location $l$ at the
current step of the computation. This function returns either $\emptyset$ or a
singleton set $\\{l\\}$ of locations. We discuss possible heuristics in
Section 9.

The acceleration consists in computing a formula
$\alpha\in\mathit{FOL}(\mathbb{X})$ such that the set
$\\{(l,\mathbf{x})\mid\mathbf{x}\models_{T}\alpha\\}$ is a subset of the
attractor we aim to compute. This set is computed in two steps.

  1. (i)

First, the procedure invokes the function
$\mathsf{AccA}:\mathit{GameStructure}\times\\{\mathit{Sys},\mathit{Env}\\}\times
L\times\mathcal{D}\to\mathit{Constraints}\times\mathit{FOL}(\mathbb{X})$.
$\mathsf{AccA}$ returns a pair of formulas $(\Psi,\varphi)$, where $\Psi$ is a
constraint that captures conditions under which the formula $\varphi$ can be
used for acceleration at location $l$. This is done by constructing the loop
game at location $l$ and establishing the conditions for applying an
acceleration lemma. $\varphi$ represents the conclusion of the acceleration
lemma, which we want to add to $a^{n}(l)$. However, at this point the
acceleration lemma is not a concrete one but is represented by uninterpreted
predicate symbols which occur in $\varphi$. Furthermore, the constraint $\Psi$
over those uninterpreted symbols captures the conditions for lemma
application. The procedure AttractorAcc adds $\varphi$ to the attractor only
in case there exists an instantiation of the uninterpreted predicate symbols
that satisfies $\Psi$. This is done in the next step.

  2. (ii)

Function
$\mathsf{InstantiateLemmas}:\mathit{Constraints}\times\mathit{FOL}\to\mathit{FOL}(\mathbb{X})$
takes the result from $\mathsf{AccA}$ and searches for an instantiation to the
uninterpreted symbols used to represent the unknown acceleration lemmas. If
such exists, it returns the respective instantiation of $\varphi$ that is then
added to $a^{n}(l)$. Otherwise it simply returns $\bot$, meaning that this
acceleration attempt has failed and has no effect. We defer to Section 8 the
description of the search for instantiations.

Procedure $\mathsf{AccA}$ is described in Figure 6. It employs a helper
function
$\mathsf{IterA}:\mathit{GameStructure}\times\\{\mathit{Sys},\mathit{Env}\\}\times\mathit{Constraints}\times\mathcal{D}\to\mathit{Constraints}\times\mathcal{D}$,
which performs symbolic computation of attractor subsets. $\mathsf{AccA}$
invokes $\mathsf{IterA}$ for attractor computation in the loop game (using the
$\mathit{CPre}(\cdot)$ operator for the respective game). Intuitively, the two
procedures apply the method outlined earlier but additionally collect the
constraints for the (nested) lemma applications as those cannot be discharged
immediately since the lemmas are uninterpreted. Note that we cannot use
AttractorAcc instead of $\mathsf{IterA}$ since the uninterpreted predicates
prevent us from identifying if we have reached a fixpoint. As $\mathsf{IterA}$
underapproximates an attractor, it uses the heuristic function Iterate? to
determine when to stop the computation and return the current
underapproximation. Furthermore, $\mathsf{IterA}$ calls $\mathsf{AccA}$ to
perform nested acceleration, as determined by the heuristic function
Accelerate?.

function $\mathsf{AccA}(\mathcal{G},p,l,d)$

pick fresh $(b,st,c)\in\mathsf{LemmaSymb}$

$\mathcal{G}_{\mathit{loop}}:=\mathsf{LoopGame}(\mathcal{G},l,l_{\mathit{End}})$
with fresh location $l_{\mathit{End}}\not\in L$

$d_{\mathit{loop}}:=d\cup\\{l_{\mathit{End}}\mapsto st(E,\mathbb{X})\\}$ where
$E=\\{e_{x}\text{: fresh unint. constant}\mid x\in\mathbb{X}\\}$

$(\Psi_{\mathit{Rec}},a):=\mathsf{IterA}(\mathcal{G}_{\mathit{loop}},p,\top,d_{\mathit{loop}})[E\mapsto\mathbb{X}]$

$\Psi:=(\forall\mathbb{X}.\leavevmode\nobreak\ \mathit{Inv}(l)\land
b(\mathbb{X})\to d(l))\land(\forall\mathbb{X}.\leavevmode\nobreak\
\mathit{Inv}(l)\land\lnot d(l)\land c(\mathbb{X})\to\Psi_{\mathit{Rec}}\land
a(l))$

return $(\Psi,c(\mathbb{X})\land\mathit{Inv}(l))$

function $\mathsf{IterA}(\mathcal{G},p,\Psi,d$)

if  _$\neg\textsc{Iterate?}(\mathcal{G},p,\Psi,d)$_ then return $(\Psi,d)$

if  _$\textsc{Accelerate?}(\mathcal{G},p,\Psi,d)=\\{l\\}$_ then

$(\Psi_{\mathit{Rec}},\varphi):=\mathsf{AccA}(\mathcal{G},p,l,d)$

return $\mathsf{IterA}(\mathcal{G},p,\Psi\land\Psi_{\mathit{Rec}},d[l\mapsto
d(l)\lor\varphi])$

return
$\mathsf{IterA}(\mathcal{G},p,\Psi,d\lor\mathit{CPre}_{\mathcal{G},p}(d))$

function $\mathsf{InstantiateLemmas}(\Psi,\varphi)$

$\mathit{Symb}:=\mathsf{UsedLemmaSymbols}(\\{\Psi,\varphi\\})$

if find $\lambda:\mathit{Symb}\to\mathsf{Lemmas}(\mathbb{X})$ such that
$\textsc{Valid}(\Psi[\lambda])$ then return $\varphi[\lambda]$ else return
$\bot$

Figure 6. Procedures for attractor acceleration using uninterpreted lemmas.

Next, we describe in detail the function $\mathsf{AccA}$. Given a location
$l\in L$ and symbolic goal $d$, $\mathsf{AccA}$ computes a symbolic state for
$l$ from which Player $p$ can enforce going to $d$, if the uninterpreted
lemmas satisfy the computed constraint. $\mathsf{AccA}$ does so by introducing
and symbolically applying an acceleration lemma at location $l$ as follows.

  * •

We first pick a fresh triple $(b,st,c)$ of lemma symbols from
$\mathsf{LemmaSymb}$ for the uninterpreted lemma that we are applying.

  * •

As in Example 7.4, we construct $\mathcal{G}_{\mathit{loop}}$ for $l$, since
we want to accelerate at location $l$.

  * •

We construct $d_{\mathit{loop}}$ obtained from $d$ by mapping the new location
$l_{\mathit{End}}$ to the formula $st(E,\mathbb{X})$. $st(E,\mathbb{X})$
expresses the relation between $E$, a set of fresh uninterpreted constants
with one such constant for each variable in $\mathbb{X}$, representing the
initial assignment, and $\mathbb{X}$ representing the values of the program
variables at $l_{\mathit{End}}$.

  * •

We invoke $\mathsf{IterA}$ which recursively performs iterations of the
attractor computation. Intuitively, if Player $p$ can enforce to reach
$d_{\mathit{loop}}(l_{\mathit{End}})$, it can either get to the goal
$\llbracket d\rrbracket$ or enforce the step relation $st(E,\mathbb{X})$. As
$\mathsf{IterA}$ might call $\mathsf{AccA}$, it also returns a constraint
$\Psi_{\mathit{Rec}}$. The substitution $[E\mapsto\mathbb{X}]$ denotes the
syntactic transformation that replaces each $e_{x}$ by the respective
$x\in\mathbb{X}$. This transformation is necessary as, intuitively, for
$\Psi_{\mathit{Rec}}$ and $a(l)$ we have to consider for the constraint the
initial assignment to $\mathbb{X}$ in $l$ before performing the step.

  * •

Finally, $\mathsf{AccA}$ constructs the new constraint $\Psi$. Intuitively,
the first conjunct states that the base of the lemma $b(\mathbb{X})$ is
included in the goal $d(l)$. The second conjunct states that every state in
the conclusion $c(\mathbb{X})$ that is not an element of the goal must be in
$\llbracket a\rrbracket$, i.e. either the goal or the step relation is
enforceable from $c(\mathbb{X})$ if not already at the goal. We assume that
each quantifier uses a fresh copy (or De Bruijn indexing) of the variables in
$\mathbb{X}$ and applies the appropriate renaming. This ensures the correct
replacement of constants in $E$ with variables as described in the previous
step.

  * •

We return the new constraint $\Psi$ and the conclusion $c(\mathbb{X})$ of the
applied lemma. The constraint $\Psi$ ensures, together with the property of an
acceleration lemma, that from $c(\mathbb{X})$, Player $p$ can enforce reaching
$d$.

  * •

The incompleteness of $\mathsf{IterA}$ is not a problem, as terminating early
with an underapproximation will only result in a stronger constraint.

What remains is to define the function
$\mathsf{InstantiateLemmas}(\Psi,\varphi)$ that searches for an instantiation
of the uninterpreted symbols, representing the used acceleration lemmas, that
satisfies $\Psi$ and defines valid lemmas. If such an instantiation is found,
it returns a formula $\varphi$ in which the terms applying these symbols have
been replaced with formulas in $\mathit{FOL}$($\mathbb{X}$). In Section 8 we
discuss the practicalities of the check for the existence of lemmas. Function
$\mathsf{InstantiateLemmas}$, shown in Figure 6, requires finding a mapping
$\lambda:\mathsf{UsedLemmaSymbols}(\\{\Psi,\varphi\\})\to\mathsf{Lemmas}(\mathbb{X})$
of the lemma symbol triples used in $\Psi$ and $\varphi$ to the set of lemmas
$\mathsf{Lemmas}(\mathbb{X})$. For $\psi\in\\{\Psi,\varphi\\}$ we denote with
$\psi[\lambda]$ the formula obtained from $\psi$ by the following
transformation. For each $(b,st,c)$ such that
$\lambda((b,st,c))=(\mathit{base},\mathit{step},\mathit{conc})$, replace each
predicate term of the form

  * •

$b(\\{t_{x}\\}_{x\in\mathbb{X}})$ by $\mathit{base}[x\mapsto t_{x}\mid
x\in\mathbb{X}]$; $c(\\{t_{x}\\}_{x\in\mathbb{X}})$ by $\mathit{conc}[x\mapsto
t_{x}\mid x\in\mathbb{X}]$;

  * •

$st(\\{t_{x}\\}_{x\in\mathbb{X}},\\{t^{\prime}_{x}\\}_{x\in\mathbb{X}})$ by
$\mathit{step}[x\mapsto t_{x},x^{\prime}\mapsto t^{\prime}_{x}\mid
x\in\mathbb{X}]$.

By the construction of $\Psi$ and $\varphi$ in $\mathsf{AccA}$, all the terms
containing the lemma predicate symbols as top symbols are of the above form,
and hence, no uninterpreted acceleration lemma symbols appear in
$\psi[\lambda]$. Furthermore, all uninterpreted constants introduced during
the construction have been mapped back to variables and do not appear in the
result returned to AttractorAcc.

Note that since $\mathsf{AccA}$ only performs symbolic computation and
collects constraints, it always returns a result. If there exists no
instantiation of the uninterpreted predicate symbols that satisfies the
constraints, function $\mathsf{InstantiateLemmas}$ will fail to find one, in
which case it will return $\bot$.

###### Example 7.6.

Consider our running example from Figure 1(a) where Player $\mathit{Sys}$ has
to enforce reaching $l_{G}$. Suppose we accelerate in Algorithm 3 at location
$l_{0}$ after the first iteration, invoking procedure
$\mathsf{AccA}(\mathcal{G},\mathit{Sys},l_{0},d)$ with
$d=a^{2}=\\{l_{0}\mapsto(x\leq 42),l_{G}\mapsto\top\\}$. $\mathsf{AccA}$ picks
$(b,st,c)\in\mathsf{LemmaSymb}$ and constructs $\mathcal{G}_{\mathit{loop}}$
as shown in Figure 5. It then calls
$\mathsf{IterA}(\mathcal{G}_{\mathit{loop}},\mathit{Sys},\top,d_{\mathit{loop}})$
with $d_{\mathit{loop}}:=\\{l_{0}\mapsto(x\leq
42),l_{G}\mapsto\top,l_{\mathit{End}}\mapsto st(e_{x},x)\\}$, where $e_{x}$ is
a fresh constant for $x\in\mathbb{X}$. Suppose $\mathsf{IterA}$ performs one
iteration before Iterate? tells it to terminate with
$(\top,\\{l_{0}\mapsto\varphi,l_{G}\mapsto\top,l_{\mathit{End}}\mapsto
st(e_{x},x)\\})$ where $\varphi\equiv_{T}\forall i.\leavevmode\nobreak\ x\leq
42\lor i=0\lor st(e_{x},x-i)\lor st(e_{x},x+i)$. Back in procedure
$\mathsf{AccA}$, we have $a(l_{0})\equiv_{T}\varphi[e_{x}\mapsto
x]\equiv_{T}\forall i.\leavevmode\nobreak\ x\leq 42\lor i=0\lor st(x,x-i)\lor
st(x,x+i)$ and $\Psi:=(\forall x.\leavevmode\nobreak\ b(x)\to x\leq
42)\land(\forall x.\leavevmode\nobreak\ x>42\wedge c(x)\to a(l_{0}))\\}$.
Hence, $\mathsf{AccA}$ returns $(\Psi,c(\mathbb{X}))$. Then in
$\mathsf{InstantiateLemmas}$, it is easy to see that for
$\lambda((b,st,c)):=(x\leq 42,x^{\prime}<x,\top)$ the constraint $\Psi$ is
valid. Applying $\lambda$ to $c(\mathbb{X})$ yields $\top$ as result. Back in
AttractorAcc we get $a^{1}(l_{0}):=a^{1}(l_{0})\lor\top$ and terminate.

###### Theorem 7.7 (Soundness of Algorithm 3).

Let $\mathcal{G}$ be a reactive program game structure,
$p\in\\{\mathit{Sys},\mathit{Env}\\}$, and $d\in\mathcal{D}$. If
$\textsc{AttractorAcc}(\mathcal{G},p,d)$ terminates returning $a$, then it
holds that $\llbracket
a\rrbracket=\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket
d\rrbracket)$.

Theorem 7.7 states the correctness of our acceleration procedure. It follows
from the property of functions $\mathsf{AccA}$ and
$\mathsf{InstantiateLemmas}$ stated in the lemma below which, intuitively,
states that the constraints only allow applicable lemmas to be instantiated.
We prove Theorem 7.7 and Lemma 7.8 in Appendix A.

###### Lemma 7.8.

Let $\mathcal{G}$ be a reactive program game structure,
$p\in\\{\mathit{Sys},\mathit{Env}\\}$, $l\in L$ and $d\in\mathcal{D}$. Then,
if $\mathsf{AccA}(\mathcal{G},p,l,d)$ returns the pair $(\Psi,\varphi)$, then
for every mapping
$\lambda:\mathsf{UsedLemmaSymbols}(\\{\Psi,\varphi\\})\to\mathsf{Lemmas}(\mathbb{X})$
such that the formula $\Psi[\lambda]$ is valid it holds that
$\llbracket\\{l\mapsto\varphi[\lambda]\\}\rrbracket\subseteq\mathit{Attr}_{\llbracket\mathcal{G}\rrbracket,p}(\llbracket
d\rrbracket)$.

Note: Our method is inherently incomplete and it is difficult to characterize
the class of infinite-state games on which it terminates. This is not
surprising, as pointed out in (Abdulla et al., 2008) transferring decidability
results from verification to games is in general non-trivial.

###  7.2. Extracting Reactive Programs from Acceleration Lemmas

The extraction of programs in the presence of acceleration follows the same
principles as in Section 6.3. We only need to define the sub-program
constructed for the application of acceleration during the attractor
computation, that is the invocation of procedure $\mathsf{AccA}$.

When extracting a program for $\mathsf{AccA}$, we add new labels in the GOTO
program for each location in the loop game $\mathcal{G}_{\mathit{loop}}$. Note
that those new labels are different from the labels corresponding to the
locations in the original game $\mathcal{G}$. The program labels $l_{0}^{L}$,
$l_{G}^{L}$ and $l_{E}^{L}$ in Figure 1(b) result from the loop game in Figure
5, constructed by $\mathsf{AccA}$. Before starting the extraction for
$\mathsf{IterA}$, we introduce an auxiliary copy of the program variables that
stores the values of $\mathbb{X}$ at the label $l$ (this corresponds to the
set of fresh variables $E$). Storing these values is necessary in order to
check conditions on the step relation in the program for $\mathsf{IterA}$. The
program in Figure 1(b) contains such an auxiliary variable $x_{0}$ and the
copy assignment $x_{0}:=x$ at label $l_{0}^{L}$.

For $\mathsf{IterA}$ we extract the program as outlined in Section 6.3 except
that the conditions in the program might contain uninterpreted symbols for the
lemmas. If in the program $\mathsf{IterA}$ parts of the original attractor are
reached, we add a jump back to the respective location of $\mathcal{G}$. If
$l_{\mathit{End}}$ is reached, the program jumps back to the label of $l$. If
$\mathsf{IterA}$ applies acceleration (invokes $\mathsf{AccA}$) we apply this
extraction process recursively.

The result is a program skeleton from which we still have to remove the
uninterpreted lemma symbols. After $\mathsf{InstantiateLemmas}$ has found and
instantiation with concrete lemmas, we use this instantiation to replace all
occurrences of uninterpreted lemma symbols in the conditions of the extracted
program. In our running example, when generating the program in Figure 1(b),
we will first get a program including statements of the form
if($\mathit{step}(x_{0},x+i)$){ $x$:=$x+i$; goto
$\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}{l_{E}^{L}}$}.
Then, we plug in the acceleration lemma from Example 7.2 and
$\mathit{step}(x_{0},x+i)$ becomes $x+i<x_{0}$ (as $x+i$ corresponds to
$x^{\prime}$ in $\mathit{step}$ and $x_{0}$ to $x$) which is exactly the
statement that we have in Figure 1(b).

###  7.3. Acceleration Beyond Attractors

The symbolic semi-algorithm for solving Büchi games (and, by duality, co-Büchi
games) outlined in Section 6 is accelerated by using AttractorAcc instead of
Attractor. This amounts to replacing the calls in lines 4 and 5 in Algorithm 2
by calls to AttractorAcc. This accelerates the computation of attractor sets
in the solving procedure, and helps the overall computation of the set of
winning states to converge. More concretely, at line 4 AttractorAcc
accelerates the computation of the set of states from which the Büchi player
can reach an accepting location. At line 5, the acceleration is applied for
the co-Büchi player, accelerating the computation of the set of states winning
for the co-Büchi player. For the Büchi game in Example 3.3 the procedure for
solving Büchi games with accelerated attractor computation successfully
terminates. The evaluation in Section 9 further demonstrates the usefulness of
attractor acceleration for solving Büchi games.

We now show an example where the convergence of AttractorAcc is insufficient
to ensure the convergence of the procedure for Büchi games. Consider the
reactive program game structure in Figure 7(a) and the Büchi objective for
Player $\mathit{Sys}$ defined by $B:=\\{l_{0}\\}$. That is, the objective of
Player $\mathit{Sys}$ is to visit location $l_{0}$ infinitely often. The table
in Figure 7(b) shows the computation of the procedure in Algorithm 2. We
observe that the sets $w_{1-p}^{i}$ will keep growing, and the computation
never terminates. Player $\mathit{Env}$ wins the game for every possible state
since the initial value of $x$ bounds the number of visits to $l_{0}$.
However, this argument cannot be captured with attractor acceleration, as
Player $\mathit{Env}$  _cannot force_ Player $\mathit{Sys}$ to decrease $x$.

$l_{0}$$l_{1}$$l_{2}$$l_{3}$$\top$$\mathit{skip}$$\top$$\mathit{skip}$$\top$$x:=x-1$$x\leq
0$$\mathit{skip}$$x>0$$\mathit{skip}$$\top$$\mathit{skip}$

(a) Game with integer program variable $x$.

| $f^{0}$ | $a^{0}$ | $w_{1-p}^{1}$ | $f^{1}$ | $a^{1}$ | $w_{1-p}^{2}$ | …
---|---|---|---|---|---|---|---
$l_{0}$ | $\top$ | $\top$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}x\leq 1}$ | $x>1$ | $x>1$ | ${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}x\leq 2}$ | …
$l_{1}$ | $\bot$ | $x>1$ | $x\leq 1$ | $\bot$ | $x>2$ | $x\leq 2$ | …
$l_{2}$ | $\bot$ | $x>0$ | $x\leq 1$ | $\bot$ | $x>1$ | $x\leq 2$ | …
$l_{3}$ | $\bot$ | $\bot$ | $\top$ | $\bot$ | $\bot$ | $\top$ | …

(b) Sets computed during the procedure.

Figure 7. Example demonstrating the need for acceleration of the computation
of the set $w_{1-p}^{n}$ in the procedure for solving Büchi games outlined in
Section 6.

More abstractly, attractor acceleration cannot sufficiently enlarge the set
$w_{1-p}^{i}$ to enforce convergence of the outer loop of the procedure for
Büchi games. The reason is that attractor acceleration cannot account for
states in the winning region of Player $1-p$ from which

  * •

Player $1-p$ cannot enforce reaching $w_{1-p}^{i}$, and

  * •

the repeated visit of a Büchi accepting location by Player $p$ will eventually
lead to $w_{1-p}^{i}$.

Motivated by this observation, we introduce an additional acceleration method,
called _co-Büchi acceleration_ , that extends the scope of acceleration-based
symbolic game solving. Intuitively, this method allows us to establish
arguments of the form: “If Player $p$ with the Büchi objective keeps visiting
_a given Büchi accepting location_ , then the set of winning states of Player
$1-p$ must be reached eventually”. The aspect of “reaching the winning states
eventually” is captured by the usage of acceleration lemmas. However, in
contrast to attractor acceleration, we will not use that the step relation is
enforceable by a player, but rather that it is unavoidable by Player $p$ upon
revisiting the given accepting location.

Before diving into the detailed description, we must highlight that similarly
to attractor acceleration, the co-Büchi acceleration is focused on a single
accepting location. However, as the set $B$ of Büchi accepting locations might
contain more than one location, we need to make sure that we do not
incorrectly exclude states from the winning region of Player $p$ by accounting
only for repeated visits of the given location. Hence, in contrast to
attractor acceleration, which performs attractor computation in a loop game,
for co-Büchi acceleration we consider a loop game with a Büchi winning
condition for which we compute an underapproximation of the winning region of
the co-Büchi player. Thus, co-Büchi acceleration is not the dual of attractor
acceleration, but an extension.

The overall procedure is formalized in Figure 8. The game-solving procedure
SolveBüchi uses $\mathsf{AccB}$ to employ co-Büchi acceleration to accelerate
the outer fixpoint, which computes the sets $f^{1},f^{2},\ldots$, in addition
to invoking AttractorAcc. On a high level, the co-Büchi acceleration
computation focuses on one of the Büchi accepting locations $l\in B$ and tries
to establish a set of states with location $l$ from which the Büchi Player $p$
cannot revisit $l$ infinitely often, and cannot win the game by visiting some
of the locations in $B\setminus\\{l\\}$ infinitely often. Such states are
winning for Player $1-p$ and can be added to $w_{1-p}^{n}$. To establish that
Player $p$ cannot visit $l$ infinitely often, we use an acceleration lemma and
a loop game but require Player $p$ to enforce the negation of the step
relation upon revisiting $l$. From states where this is impossible, Player $p$
cannot enforce visiting $l$ infinitely often. As explained earlier, to account
for the remaining Büchi accepting locations $B\setminus\\{l\\}$, the loop game
constructed by $\mathsf{AccB}$ has a Büchi winning condition for Player $p$.

The function
$\mathsf{AccB}:\mathit{GameStructure}\times\\{\mathit{Sys},\mathit{Env}\\}\times
L\times\mathcal{D}\to\mathit{Constraints}\times\mathit{FOL}(\mathbb{X})$
generates the constraints for the acceleration lemmas. Therefore, it
constructs a loop game for a location $l\in B$, the set of Büchi accepting
locations, and equips it with a Büchi winning condition
$f_{\mathit{loop}}:=f\cup\\{l_{\mathit{End}}\mapsto\neg st(E,\mathbb{X})\\}$.
Intuitively, $f_{\mathit{loop}}$ requires that in the loop game, the Büchi
player enforces visiting infinitely often a location in $B\setminus\\{l\\}$,
or a visit to $l_{\mathit{End}}$ while also ensuring that the step relation of
the applied lemma is violated. Thus, the winning region of the co-Büchi player
in this game are states from which it can enforce that the play does not visit
$B\setminus\\{l\\}$ infinitely often and _if_ it visits location
$l_{\mathit{End}}$, _then_ the step relation must be satisfied at location
$l_{\mathit{End}}$. If Player $p$ loses this loop game, Player $p$ can only
win the overall game by visiting the location $l$ infinitely often while
applying $\mathit{step}$, which is not possible. This allows extending the
winning region of Player $1-p$ using an acceleration lemma. Similarly to the
function $\mathsf{AccA}$, if $\mathsf{InstantiateLemmas}$ succeeds, the
procedure adds the set of states represented by the conclusion of the lemma to
the set $w_{1-p}^{n}(l)$.

The function
$\mathsf{IterB}:\mathit{GameStructure}\times\\{\mathit{Sys},\mathit{Env}\\}\times\mathit{Constraints}\times\mathcal{D}\times\mathcal{D}\to\mathit{Constraints}\times\mathcal{D}$
performs the steps of the procedure for Büchi games and invokes
$\mathsf{IterA}$ for the (accelerated) attractor computation. A key detail
here is that the attractor sets computed for the Büchi player must not be
underapproximated. This is required as the complement set is added to the
winning region of the opponent, which would be incorrect in case of an
underapproximation. To this end, we add an additional constraint defined as
$\mathsf{Precise}(\mathcal{G},p,a):=\forall l\in L.\leavevmode\nobreak\
\mathit{CPre}_{\mathcal{G},p}(a)(l)\to a(l)$, which states that the
corresponding symbolic set overapproximates the attractor.

Similarly to Theorem 7.7 we obtain the following correctness property.

###### Proposition 7.9 (Soundness of SolveBüchiAcc).

Let $\mathcal{G}$ be a reactive program game structure,
$p\in\\{\mathit{Sys},\mathit{Env}\\}$, and $B\subseteq L$. If
$\textsc{SolveB\"{u}chiAcc}(\mathcal{G},p,\\{l\mapsto\mathit{Inv}(l)\leavevmode\nobreak\
|\leavevmode\nobreak\ l\in B\\})$ terminates returning $w$, then it holds that
$\llbracket
w\rrbracket=W_{1-p}(\llbracket\mathcal{G}\rrbracket,\mathit{coBuchi}(B))$.

function  _SolveBüchiAcc(
$\mathcal{G}=(T,\mathbb{I},\mathbb{X},L,\mathit{Inv},\delta)$,
$\mathit{p}\in\\{\mathit{Sys},\mathit{Env}\\}$, $f\in\mathcal{D}$)_

…

4 $a^{n}:=\textsc{AttractorAcc}(\mathcal{G},p,f^{n})$

5
$w^{n}_{1-p}:=\textsc{AttractorAcc}(\mathcal{G},1-p,\neg\mathit{CPre}_{\mathcal{G},p}(a^{n}))$

if  _AccelBuchi? $(G,p,w^{n}_{1-p})=\\{l\\}$_ then

$(\Psi,\varphi):=\mathsf{AccB}(\mathcal{G},p,l,f^{n}\wedge(\mathit{Inv}\land\neg
w^{n}_{1-p}))$

$w_{1-p}^{n}(l):=w_{1-p}^{n}(l)\lor\mathsf{InstantiateLemmas}(\Psi,\varphi)$

6 $f^{n+1}:=f^{n+1}\wedge(\mathit{Inv}\land\neg w^{n}_{1-p})$

function $\mathsf{AccB}(\mathcal{G},p,l,f)$

pick fresh $(b,st,c)\in\mathsf{LemmaSymb}$

$\mathcal{G}_{\mathit{loop}}:=\mathsf{LoopGame}(\mathcal{G},l,l_{\mathit{End}})$
with fresh location $l_{\mathit{End}}$

$f_{\mathit{loop}}:=f\cup\\{l_{\mathit{End}}\mapsto\neg st(E,\mathbb{X})\\}$
where $E=\\{e_{x}\text{: fresh unint. constant}\mid x\in\mathbb{X}\\}$

$(\Psi_{\mathit{Rec}},a):=\mathsf{IterB}(\mathcal{G}_{\mathit{loop}},p,\emptyset,f_{\mathit{loop}})[E\mapsto\mathbb{X}]$

$\Psi:=(\forall\mathbb{X}.\leavevmode\nobreak\ \mathit{Inv}(l)\land
b(\mathbb{X})\to\lnot f(l))$, $\land(\forall\mathbb{X}.\leavevmode\nobreak\
\mathit{Inv}(l)\land f(l)\land c(\mathbb{X})$ $\to\Psi_{\mathit{Rec}}\land
a(l))$

return $(\Psi,c(\mathbb{X})\land\mathit{Inv}(l))$

function IterB( $\mathcal{G},\mathit{p},\Psi,f,w_{1-p}$)

if  _$\neg\textsc{Iterate?}(\mathcal{G},p,\Psi,f,w_{1-p})$_ then return
$(\Psi,w_{1-p})$

$(\Psi_{1},a):=\mathsf{IterA}(\mathcal{G},p,\Psi,f)$

$\Psi_{1}:=\Psi_{1}\land\mathsf{Precise}(\mathcal{G},p,a)$

$(\Psi_{2},w^{\prime}_{1-p}):=\mathsf{IterA}(\mathcal{G},1-p,\mathit{Inv}\land\neg\mathit{CPre}_{\mathcal{G},p}(a))$

$f^{\prime}:=f\wedge(\mathit{Inv}\land\neg w^{\prime}_{1-p})$

if
_$\textsc{AccelBuchi?}(\mathcal{G},p,\Psi,f^{\prime},w_{1-p}^{\prime})=\\{l\\}$_
then

$(\Psi_{3},\varphi):=\mathsf{AccB}(\mathcal{G},p,l,f^{\prime})$

$f^{\prime}:=f^{\prime}[l\mapsto f^{\prime}(l)\land\neg\varphi]$

$w^{\prime}_{1-p}:=w^{\prime}_{1-p}[l\mapsto w^{\prime}_{1-p}(l)\lor\varphi]$

return
$\mathsf{IterB}(\mathcal{G},p,\Psi\land\Psi_{1}\land\Psi_{2}\land\Psi_{3},f^{\prime},w^{\prime}_{1-p})$

return
$\mathsf{IterB}(\mathcal{G},p,\Psi\land\Psi_{1}\land\Psi_{2},f^{\prime},w^{\prime}_{1-p})$

Figure 8. Accelerated semi-algorithm for solving Büchi games.

##  8\. Synthesis of Acceleration Lemmas and Programs

In this section we describe how our acceleration method instantiates the
uninterpreted predicate symbols representing acceleration lemmas by actual
acceleration lemmas. In order to ensure that the instantiations constitute
valid acceleration lemmas, and also in order to constrain the search space,
the lemmas are derived from templates. The templates associate with the
individual lemma components parameterized formulas conforming to certain
syntactic restrictions. By replacing the uninterpreted predicates representing
the lemmas by the respective templates, we restrict the shape of the sought
lemmas. The lemma instantiation task is then to find values for the template
parameters, called meta-variables, that satisfy the constraints generated
during the symbolic attractor computation. However, single instantiations of
the meta-variables may be overly specific and thus result in acceleration
steps with negligible effect. We address this issue by proposing a method
based on quantifier elimination that computes the combined acceleration effect
of all instantitations to the meta-variables that satisfy the constraints. We
present this method in Section 8.2 below, but first we provide in Section 8.1
the definition of the templates to which our lemmas must conform.

###  8.1. Acceleration Lemma Templates

The derived lemmas must fulfill two requirements: they must satisfy the
constraint generated during symbolic acceleration, and they must fulfill the
conditions of Definition 7.1. Since the constraint is a $\mathit{FOL}$ formula
in some theory $T$, our goal is to formulate the lemma generation task as an
SMT problem. We use templates representing acceleration lemmas in a fragment
of linear mixed integer-real arithmetic. In principle, the class of templates
can be extended to other theories. Furthermore, our method also allows for
using custom lemmas. We need to define the templates used for lemma generation
in a way that ensures that the results are valid w.r.t. the second-order
condition in Definition 7.1. In order to do this, we make use of the following
proposition.

###### Proposition 8.1.

Let $\epsilon>0$ be a constant, and let $r\in\mathcal{T}_{F}$ be a function
term of real or integer type over variables $V\subseteq\mathit{Vars}$. Then,
$(r(V)\leq 0,r(V^{\prime})+\epsilon\leq r(V),\top)$ is an acceleration lemma
over $V$.

We call $r$ the _ranking function_.

The above property provides us with a way to generate acceleration lemmas that
satisfy the first condition in Definition 7.1. To ensure that we can
effectively check satisfiability of the generated constraints, a meaningful
class of ranking functions are affine functions with bounded coefficients. For
instance, when $\mathbb{X}_{\mathit{Num}}$ are the program variables with a
numerical type, we consider

$r=\sum_{x\in\mathbb{X}_{\mathit{Num}}}p_{x}x+d\text{ with
}d\in\mathbb{R}\text{ and }p_{x}\in\\{-1,0,1\\}.$

Such a lemma is typically applicable only in some part of the state space.
This necessitates the application of multiple lemmas and specifying some
properties to be invariant under the step relation. Hence, our templates
should allow adding invariants to lemmas as stated in the following.

###### Proposition 8.2.

Let $(\mathit{base},\mathit{step},\mathit{conc})$ be an acceleration lemma
over $V$ and let $\mathit{inv}\in\mathit{FOL}(V)$ be a formula. Then,
$(\mathit{base}\land\mathit{inv},\mathit{step}\land\mathit{inv}[V\mapsto
V^{\prime}],\mathit{conc}\land\mathit{inv})$ is also an acceleration lemma.

We call $\mathit{inv}$ a _lemma invariant_. 111 _Lemma invariants_ are
generated by our acceleration procedure and are not related to the _location
invariants_ that are part of reactive program game model.

We define templates for lemma invariants as linear inequalities with bounded
coefficients. More concretely, we consider linear inequalities with $B$
variables for some selected bound $B\in\mathbb{N}$, i.e.,

$\mathit{inv}_{B}=\sum_{x\in\mathbb{X}_{\mathit{Num}}}p_{x}x\leq d\text{ with
}d\in\mathbb{R},p_{x}\in\\{-1,0,1\\}\text{ and
}\sum_{x\in\mathbb{X}}|p_{x}|\leq B.$

We distinguish the special case where $B=1$, which results in the simpler set
of lemma invariant templates $\mathit{inv}_{T}:=\\{x\leq d,x\geq d,x=d\mid
x\in\mathbb{X}_{\mathit{Num}},d\in\mathbb{R}\\}$. As lemma invariants need not
satisfy any additional restrictions, we can allow conjunctions of
inequalities, or even other given predicates.

Putting everything together, the lemma template that we use is the one from
Proposition 8.1 combined according to Proposition 8.2 with a lemma invariant
$\mathit{inv}$ that is a conjunction of several instances of
$\mathit{inv}_{B}$ and $\mathit{inv}_{T}$ where each part of the template has
its unique set of meta-variables.

###  8.2. Lemma Instantiation via Quantifier Elimination

It remains to discuss how to transform the templates into a mapping
$\lambda:\mathit{Symb}\to\mathsf{Lemmas}(\mathbb{X})$ of the used lemma
symbols $\mathit{Symb}:=\mathsf{UsedLemmaSymbols}(\\{\Psi,\varphi\\})$ to
actual lemmas. Recall that $\lambda$ is required by function
$\mathsf{InstantiateLemmas}$ in Figure 6 in order to compute the acceleration
result.

We define a _template mapping_ to be a function
$\tau:\mathit{Symb}\to\mathit{FOL}(\mathbb{X}\cup\mathit{Meta})\times\mathit{FOL}(\mathbb{X}\cup\mathit{Meta})\times\mathit{FOL}(\mathbb{X}\cup\mathit{Meta})$
that maps the uninterpreted lemma symbols to lemma templates containing meta-
variables $\mathit{Meta}$ (like $p_{x}$ or $d$ from above). For an
instantiation of the meta-variables $M:\mathit{Meta}\to\mathcal{T}_{F}$, that
maps the meta-variables to terms without meta-variables, we define
$\lambda_{\tau,M}:\mathit{Symb}\to\mathsf{Lemmas}(\mathbb{X})$ as
$\lambda_{\tau,M}(s)=\tau(s)[M]$ where in the image of $\tau$ all meta-
variables $m\in\mathit{Meta}$ are simultaneously replaced by their respective
terms $M(m)$ (slightly abusing the notation $\cdot[\cdot]$).

Thus, given a constraint $\Psi$ and a formula
$\varphi\in\mathit{FOL}(\mathbb{X})$ with uninterpreted lemma symbols, the
task of finding a mapping $\lambda$ reduces to finding a model
$M:\mathit{Meta}\to\mathcal{T}_{F}$ of the formula
$\Psi[\tau(\mathit{Meta})]$, where $\Psi[\tau(\mathit{Meta})]$ is obtained
from $\Psi$ by applying $\tau$ as substitution. If a model $M$ is found (by
the SMT solver) we have that $\Psi[\lambda_{\tau,M}]$ evaluates to true, and
the function $\mathsf{InstantiateLemmas}$ then returns
$\varphi[\lambda_{\tau,M}]$. For program extraction, $M$ provides a concrete
instantiation of the meta-variables, and hence, a concrete acceleration lemma
that we use as described in Section 7.2.

However, the generated model might yield an acceleration lemma that is not
general enough. For example, recall the acceleration lemma used for our
running example in Example 7.6, but suppose that now we want to use the method
outlined above to generate an acceleration lemma using our template format. As
our template allows for the use of lemma invariants, a model generated by the
SMT solver might result in an acceleration lemma of the form $(x\leq
42,x^{\prime}<x\land x^{\prime}\leq 100,x\leq 100)$ which is the original
lemma with the additional lemma invariant $x\leq 100$. Unlike the lemma in
Example 7.6, this lemma does not result in immediately reaching a fixpoint in
the attractor computation. One possible way to mitigate this, is to enumerate
models and thus generate multiple acceleration lemmas that can be all applied
in $\mathsf{AccA}$ to further extend the computed attractor.

Instead of computing instantiations of the meta-variables one by one from the
satisfying assignments of $\Psi[\tau(\mathit{Meta})]$, we can take a different
approach. We can consider a formula in which the meta-variables are explicitly
existentially quantified:

$\Phi(\mathbb{X}):=\exists\mathit{Meta}.\leavevmode\nobreak\
\Psi[\tau(\mathit{Meta})]\land\varphi[\tau(\mathit{Meta})].$

The set of assignments that satisfy $\Phi(\mathbb{X})$ consists of those
assignments to $\mathbb{X}$ for which there exists an instantiaton of the
meta-variables (that is, a valid acceleration lemma). Thus, it implicitly
captures all the acceleration lemmas that are possible results of
$\mathsf{InstantiateLemmas}$. Applying _quantifier elimination_ to
$\Phi(\mathbb{X})$, we obtain a formula $\mathsf{QElim}(\Phi)$ that
characterizes the final conclusion, which can be seen as the union of the
conclusions of all acceleration lemmas satisfying the templates and the
constraints. In our running example, we obtain
$\mathsf{QElim}(\Phi)\equiv\top$, as there exist an instantiation of the meta-
variables that results in a lemma with conclusion $\top$ (for example the one
from our example). With this approach, $\mathsf{InstantiateLemmas}$ returns
$\mathsf{QElim}(\Phi)$ as the result of the acceleration.

###  8.3. Program Extraction via Skolem Function Synthesis

The formula $\mathsf{QElim}(\Phi)$ characterizes all possible results of
$\mathsf{InstantiateLemmas}$ and is sufficient for computing a symbolically
represented set of states to add to the attractor. However, for extracting a
program as in Section 7.2, we need concrete acceleration lemmas, i.e. concrete
values for $\mathit{Meta}$. Since for different assignments satisfying
$\mathsf{QElim}(\Phi)$, the concrete values of $\mathit{Meta}$ can be
different, our goal is to generate functions for the meta-variables with
arguments in $\mathit{Assignments}(\mathbb{X})$. For each $\mathbf{x}$
satisfying $\mathsf{QElim}(\Phi)$ these functions should yield a valid lemma.
We consider the formula

$\forall\mathbb{X}.\exists\mathit{Meta}.\leavevmode\nobreak\
\mathsf{QElim}(\Phi)\to(\Psi[\tau(\mathit{Meta})]\land\varphi[\tau(\mathit{Meta})]).$

and the task becomes to compute _Skolem functions_
$\mathit{SK}_{m}:\mathit{Assignments}(\mathbb{X})\to\mathit{Domain}(m)$ for
the meta-variables $m\in\mathit{Meta}$. This is essentially a functional
synthesis problem. One way to do that is to skolemize the above formula by
substituting $\mathit{Meta}$ using uninterpreted function symbols and then
solve the resulting second-order satisfiability problem.

A tuple of Skolem functions $\mathit{SK}_{m}$, one for each
$m\in\mathit{Meta}$, characterizes a lemma as a function of the values of
$\mathbb{X}$ at the point _when we start applying acceleration_. Our concrete
lemmas are therefore given by the instantiation
$\lambda_{\tau,m\mapsto\mathit{SK_{m}}(\mathbb{X}_{SK})}$ where
$\mathbb{X}_{SK}$ is a copy of $\mathbb{X}$ storing the values of the program
variables before entering the sub-program generated for acceleration. Aside
from these additional auxiliary variables, the program generation proceeds as
described in Section 7.2.

##  9\. Evaluation

Name | $\Omega$ | ST | $|L|$ | $|\mathbb{X}|$ | $|\mathbb{I}|$ | Win | A | rp | R | T | G | M | extr
---|---|---|---|---|---|---|---|---|---|---|---|---|---
Cinderella 1.4 (Woeginger, 2009; Bodlaender et al., 2012) | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Env}$ | 0 | 0.3 | MO | NI | 0.2 | TO | -
Cinderella 1.5 | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Env}$ | 0 | 0.4 | MO | NI | 0.2 | TO | -
Cinderella 1.6 | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Env}$ | 0 | 0.4 | MO | NI | 0.2 | TO | -
Cinderella 1.8 | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Env}$ | 0 | 0.5 | MO | NI | 0.3 | TO | -
Cinderella 1.9 | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Env}$ | 0 | 0.9 | MO | NI | 0.6 | TO | -
Cinderella 2.0 | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Sys}$ | 0 | 0.5 | MO | NI | 0.6 | TO | 0.7
Cinderella 2.5 | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Sys}$ | 0 | 0.5 | MO | NI | 0.5 | TO | 0.7
Cinderella 3.0 | S | $\mathbb{R}$ | 4 | 5 | 5 | $\mathit{Sys}$ | 0 | 0.5 | MO | NI | 0.4 | TO | 0.7
Box (Neider and Topcu, 2016) | S | $\mathbb{Z}$ | 4 | 2 | 4 | $\mathit{Sys}$ | 0 | 0.2 |  |  | 0.2 | 3.9 | 0.4
Box Limited | S | $\mathbb{Z}$ | 4 | 2 | 2 | $\mathit{Env}$ | 0 | 0.3 | 0.9 | TO | 0.1 | 2.3 | -
Diagonal | S | $\mathbb{Z}$ | 4 | 2 | 2 | $\mathit{Sys}$ | 0 | 0.2 | 4.9 | MO | 0.1 | 3.4 | 0.3
Evasion | S | $\mathbb{Z}$ | 4 | 4 | 4 | $\mathit{Sys}$ | 0 | 0.2 | 2.3 | TO | 0.3 | 57 | 0.5
Follow | S | $\mathbb{Z}$ | 4 | 4 | 4 | $\mathit{Sys}$ | 0 | 0.3 | TO | TO | 0.5 | 112 | 0.6
Solitrary | S | $\mathbb{Z}$ | 3 | 2 | 0 | $\mathit{Sys}$ | 0 | 0.2 | 0.2 | IR | 0.2 | 0.9 | 0.3
Square-5x5 | S | $\mathbb{Z}$ | 4 | 2 | 4 | $\mathit{Sys}$ | 0 | 0.2 | 56 | TO | 0.1 | 6.8 | 0.5
Watertank Double (Maderbacher and Bloem, 2021) | S | $\mathbb{R}$ | 4 | 2 | 0 | $\mathit{Sys}$ | 0 | 0.2 | 11 | NI | NI | TO | 0.3
Watertank Single | B | $\mathbb{R}$ | 5 | 1 | 0 | $\mathit{Sys}$ | 1 | 0.6 | 25 | NI | - | 1.7 | 1.8
Elevator Simple 3 | B | $\mathbb{Z}$ | 4 | 4 | 0 | $\mathit{Sys}$ | 0 | 1.2 | 1.5 | TO | - | 19 | 2.2
Elevator Simple 4 | B | $\mathbb{Z}$ | 4 | 5 | 0 | $\mathit{Sys}$ | 0 | 1.3 | 2.4 | MO | - | TO | 2.7
Elevator Simple 5 | B | $\mathbb{Z}$ | 4 | 6 | 0 | $\mathit{Sys}$ | 0 | 1.6 | 6.3 | MO | - | TO | 3.8
Elevator Simple 8 | B | $\mathbb{Z}$ | 4 | 9 | 0 | $\mathit{Sys}$ | 0 | 3.3 | 23 | TO | - | MO | 8.6
Elevator Simple 10 | B | $\mathbb{Z}$ | 4 | 11 | 0 | $\mathit{Sys}$ | 0 | 6.3 | 93 | TO | - | MO | 16
Elevator Signal 3 | B | $\mathbb{Z}$ | 3 | 2 | 1 | $\mathit{Sys}$ | 0 | 1.4 | 17 | MO | - | 11 | 2.2
Elevator Signal 4 | B | $\mathbb{Z}$ | 3 | 2 | 1 | $\mathit{Sys}$ | 0 | 1.7 | 109 | MO | - | 12 | 2.6
Elevator Signal 5 | B | $\mathbb{Z}$ | 3 | 2 | 1 | $\mathit{Sys}$ | 0 | 1.9 | TO | MO | - | 11 | 2.9
Example-Figure 1(a) | R | $\mathbb{Z}$ | 2 | 1 | 1 | $\mathit{Sys}$ | 1 | 2.1 | (IR) | (IR) | (NI) | 73 | 32
Example-Figure 2 | R | $\mathbb{Z}$ | 4 | 2 | 0 | $\mathit{Sys}$ | 1 | 0.7 | (TO) | IR | (NI) | TO | 1.2
Rob-Grid-1d-Reach | R | $\mathbb{Z}$ | 2 | 1 | 0 | $\mathit{Sys}$ | 1 | 0.2 | (TO) | IR | (NI) | 2.8 | 0.7
Rob-Grid-2d-Reach | R | $\mathbb{Z}$ | 2 | 2 | 0 | $\mathit{Sys}$ | 1 | 0.3 | (MO) | IR | (NI) | TO | 495
Rob-Cont-1d-Reach-Real | R | $\mathbb{R}$ | 2 | 1 | 1 | $\mathit{Sys}$ | 1 | 0.3 | (TO) | (NI) | (NI) | TO | TO
Rob-Cont-2d-Reach-Real | R | $\mathbb{R}$ | 2 | 2 | 2 | $\mathit{Sys}$ | 1 | 0.4 | (TO) | (NI) | (NI) | TO | TO
Rob-Cont-1d-Reach-Unreal | R | $\mathbb{R}$ | 2 | 1 | 1 | $\mathit{Env}$ | 0 | 0.1 | (TO) | NI | (NI) | 7.5 | -
Rob-Cont-2d-Reach-Unreal | R | $\mathbb{R}$ | 2 | 2 | 2 | $\mathit{Env}$ | 2 | 30 | (TO) | NI | (NI) | TO | -
Rob-Cat-1d-Real | R | $\mathbb{Z}$ | 3 | 2 | 2 | $\mathit{Sys}$ | 1 | 30 | (TO) | (MO) | (NI) | 9.8 | TO
Rob-Cat-2d-Real | R | $\mathbb{Z}$ | 5 | 4 | 3 | $\mathit{Sys}$ | 0 | TO | (MO) | (MO) | (NI) | TO | TO
Rob-Cat-1d-Unreal | R | $\mathbb{Z}$ | 3 | 2 | 2 | $\mathit{Env}$ | 1 | 31 | (TO) | (MO) | (NI) | 1.5 | -
Rob-Cat-2d-Unreal | R | $\mathbb{Z}$ | 5 | 4 | 3 | $\mathit{Env}$ | 0 | TO | (TO) | (MO) | (NI) | 3.7 | -
Example-Figure 3 | B | $\mathbb{Z}$ | 5 | 2 | 1 | $\mathit{Sys}$ | 4 | 1.9 | (MO) | (IR) | - | 5.3 | TO
Rob-Grid-1d-Commute | B | $\mathbb{Z}$ | 4 | 2 | 1 | $\mathit{Sys}$ | 3 | 0.9 | (TO) | MO | - | 44 | TO
Rob-Grid-2d-Commute | B | $\mathbb{Z}$ | 4 | 4 | 2 | $\mathit{Sys}$ | 2 | 4.3 | (TO) | TO | - | TO | MO
Rob-Cont-1d-Commute | B | $\mathbb{R}$ | 4 | 2 | 2 | $\mathit{Sys}$ | 3 | 1.4 | (TO) | (NI) | - | TO | TO
Rob-Cont-2d-Commute | B | $\mathbb{R}$ | 4 | 4 | 4 | $\mathit{Sys}$ | 2 | 8.4 | (MO) | (NI) | - | TO | TO
Rob-Resource-1d | B | $\mathbb{Z}$ | 4 | 2 | 1 | $\mathit{Env}$ | 1 | 1.4 | (TO) | IR | - | 4.0 | -
Rob-Resource-2d | B | $\mathbb{Z}$ | 4 | 3 | 2 | $\mathit{Env}$ | 1 | 3.1 | (TO) | MO | - | 9.0 | -
Warehouse-Empty | B |  $\mathbb{R}$, $\mathbb{Z}$ | 9 | 2 | 1 | $\mathit{Sys}$ | 2 | 2.3 | (TO) | (NI) | - | TO | 7.9
Warehouse-Stock | B |  $\mathbb{R}$, $\mathbb{Z}$ | 10 | 3 | 2 | $\mathit{Sys}$ | 4 | 6.1 | (MO) | (NI) | - | TO | TO
Warehouse-Clean | B |  $\mathbb{R}$, $\mathbb{Z}$ | 13 | 6 | 5 | $\mathit{Sys}$ | 10 | 21 | (TO) | (NI) | - | TO | TO

Table 1. Evaluation Results. $\Omega$ is the objective (Safety, Reachability,
or Büchi). ST is the variable domain type (additional to $\mathbb{B}$). $|L|$,
$|\mathbb{X}|$, $|\mathbb{I}|$ are the number of respective game elements and
Win the player expected to win. For our tool we give the number of applied
accelerations A. We show the wall-clock running time in seconds for our
prototype rpgsolve, Raboniel, TeMoS, GenSys, and MuVal (with clause exchange).
We also provide the running times for our prototype with additional program
extraction. TO means timeout after 10 minutes, MO means out of memory (8GB), -
means the approach is conceptually not applicable or extraction is not
available as Player $\mathit{Env}$ wins, NI means not-implemented (but
conceptually applicable), and IR mean invalid result (by errors or incomplete
refinement loops). Parentheses $(\cdot)$ mean we expect divergence, e.g. due
to unbounded strategy loops. Two results are missing due to inconsitent
benchmarks for reasonable comparison. We highlight in bold the fastest solving
runtime result und underline it if it is the only sucessful one. The
evaluation was performed on a single core of a Intel i7 (11thGen) processor.

We implemented our game-solving method in a prototype 222Available at:
https://zenodo.org/doi/10.5281/zenodo.8409938 using Z3 (de Moura and Bjørner,
2008) as the SMT solver. The implementation realizes the heuristics from
Section 7 based on the current number of symbolic state changes $k_{l}$ per
location $l\in L$, i.e. how many times $a^{i+1}(l)\not\equiv_{T}a^{i}(l)$ so
far in the computation. Acceleration attempts incur computational costs,
increasing with the templates’ complexity. Therefore, the main goal of the
heuristics is to keep the number of these attempts low and keep the used
templates simple. In Algorithm 3, the frequency with which Accelerate?
attempts acceleration for location $l$ grows linearly in $k_{l}$, as sometimes
many exact steps are needed before we can successfully accelerate. The lemma
template is as described in Section 8 and uses an invariant that has a number
of conjuncts $\mathit{inv}_{T}$ and $\mathit{inv}_{2}$ linear in $k_{l}$.
Hence, we start with simple templates, and if those are not sufficient, we use
more complicated ones over time. For $\mathsf{IterA}$, the heuristics impose a
bound on the depth of nested acceleration that is linear in $k_{l}$ and ensure
two updates of the symbolic state per location, first an application of the
enforceable predecessor and then a potential nested acceleration. Again, the
depth bound ensures that the acceleration attempts are initially simple. As,
over time, we increase the complexity of our templates and acceleration
attempts, in $\mathsf{InstantiateLemmas}$, we query the SMT solver with a
timeout, which is quadratic in $k_{l}$.

We have not implemented the procedure in Figure 8 for Büchi acceleration in
our prototype yet. Instead, we have implemented Algorithm 2, in which we use
AttractorAcc instead of Attractor.

We compare our prototype to the fixpoint engine GenSys (Samuel et al., 2021),
the $\mu\text{CLP}$ solver MuVal (Unno et al., 2020), and the TSL modulo
theories(Finkbeiner et al., 2019, 2022) solvers Raboniel (Maderbacher and
Bloem, 2021) and TeMoS (Choi et al., 2022) (run with Strix (Meyer et al.,
2018) and cvc5 (Barbosa et al., 2022)). Note that the last two perform
synthesis from temporal logic specifications, and our tool solves directly
specified games. For benchmarks where a TSL encoding was available, we use the
existing benchmark, otherwise we encoded the game into TSL with an automatic
translation, where the game locations are encoded with an additional data cell
in the TSL formula. For MuVal, we encoded the games into $\mu\text{CLP}$ as
described in (Unno et al., 2020), where the set of winning states is described
by (nested) fixpoint equations. We did not compare to (Neider and Topcu, 2016;
Farzan and Kincaid, 2018) as those tools are outperformed by GenSys (Samuel et
al., 2021), and did not compare to (Markgraf et al., 2020) as they use a
fairly different model and perform similarly to GenSys on the shared
benchmarks. The implementation from (Beyene et al., 2014) is not available.
For (Faella and Parlato, 2023) no tool is available (instead, a small set of
SMTLib benchmark files that also contain the respective CHC encoding are
available). However, while (Faella and Parlato, 2023) did not compare to
GenSys, their performance seems similar.

##### Benchmarks.

(Neider and Topcu, 2016) introduced a set of benchmarks that are safety games
modeling one or two robots moving on an infinite two-dimensional grid while
influenced by the system and the environment. The reasoning that these games
require can be localized, and no unbounded strategy loops occur. The
Cinderella game (Woeginger, 2009; Bodlaender et al., 2012) is a standard
safety-game benchmark for infinite-state synthesis that is parametrized in
bucket size. The number of iterations needed in a strategy is bounded. Bloem
and Maderbacher introduced a set of (TSL) benchmarks in (Maderbacher and
Bloem, 2021), which model simple elevator and water tank controllers, and
whose variables have infinite domain but take values in a bounded set. We
introduce a new set of benchmarks, described in Appendix B, where a robot
moves on a grid, in a continuous space, or through a finite set of abstract
locations. It has to perform different tasks like reaching a location,
commuting between locations, executing tasks at specific locations, while
handling environment disturbances, or decreasing energy levels, or avoiding an
environment-controlled cat. Our benchmarks have unbounded variable ranges and
many contain unbounded strategy loops. We did not use the TSL benchmarks from
(Choi et al., 2022) as most are almost deterministic (and require a manual
translation from a formula into a program-like game).

###  9.1. Analysis

Table 1 shows the results of our evaluation. The benchmark sets from the
literature (Woeginger, 2009; Bodlaender et al., 2012; Neider and Topcu, 2016;