11institutetext: Graz University of Technology, Austria

# Reactive Synthesis Modulo Theories

Using Abstraction Refinement

Benedikt Maderbacher  Roderick Bloem

###### Abstract

Reactive synthesis builds a system from a specification given as a temporal
logic formula. Traditionally, reactive synthesis is defined for systems with
Boolean input and output variables. Recently, new theories and techniques have
been proposed to extend reactive synthesis to data domains, which are required
for more sophisticated programs. In particular, Temporal stream logic (TSL)
[9] extends LTL with state variables, updates, and uninterpreted functions and
was created for use in synthesis. We present a synthesis procedure for TSL(T),
an extension of TSL with theories. Synthesis is performed using a counter-
example guided synthesis loop and an LTL synthesis procedure. Our method
translates TSL(T) specifications to LTL and extracts a system if synthesis is
successful. Otherwise, it analyzes the counterstrategy for inconsistencies
with the theory. If the counterstrategy is theory-consistent, it proves that
the specification in unrealizable. Otherwise, we add temporal assumptions and
Boolean predicates to the TSL(T) specification and start the next iteration of
the the loop. We show that the synthesis problem for TSL(T) is undecidable.
Nevertheless our method can successfully synthesize or show unrealizability of
several non-Boolean examples.

##  1 Introduction

Reactive synthesis [2] is the problem of automatically constructing a system
from a specification. The user provides a specification in temporal logic and
the synthesis procedure constructs a system that satisfies it. Traditionally
this only works for systems with Boolean input and output variables. However,
real world system often use more sophisticated data like integers, reals, or
structured data. For finite domains it is possible to use bit-blasting to
obtain an equivalent Boolean specification. These will be hard for a human to
read and the large number of variables make them very challenging for a
synthesis tool to solve.

In recent years multiple theories have been proposed to perform reactive
synthesis with non Boolean inputs and outputs. There have been decidability
results for synthesis using register automata [5, 10, 6] and variable automata
[7].

Our work builds on temporal stream logic (TSL). TSL, proposed by Finkbeiner et
al. [9], uses a logic based on linear temporal logic (LTL) with state
variables, uninterpreted functions and predicates, and update expressions. TSL
allows for an elegant and efficient synthesis method that separates control
from data. However, the ability to specify how data is handled is limited
because functions and predicates remain uninterpreted. Finkbeiner et al. [8]
describe an extension to TSL modulo theories, but consider only satisfiability
and not synthesis.

In this paper we propose a synthesis algorithm for temporal stream logic
modulo theories that can be applied to arbitrary decidable theories in which
quantifier elimination is possible. Let us consider a concrete example using
the theory of linear integer arithmetic (LIA).

###### Example 1

We want to build a system with one integer state variable $x$ and one integer
input $i$. The objective is to keep the value of the state variable between
$0$ and $100$. At any time step the system can select one of two updates:
increase or decrease $x$ by $i$, where $i$ is chosen by the environment in the
interval $0\leq i<5$. We assume that the initial state is any value inside the
boundaries. These requirements can be written as the TSL formula

$\phi\triangleq(0\leq x\land x<100\land\operatorname{\mathbf{G}}(0\leq i\land
i<5))\boldsymbol{\rightarrow}\\\ \operatorname{\mathbf{G}}(0\leq x\land
x<100\land([x\leftarrow x-i]\lor[x\leftarrow x+i])),$

where the propositions $[x\leftarrow x-i]$ and $[x\leftarrow x+i]$ describe
updates to $x$.

A human programmer might write the following program satisfying the
specification:

⬇

while(true)

i := receive()

if (x-i>=0)

x := x - i

else

x := x + i

Note how this program uses a condition that doesn’t appear in the original
specification. In fact, it is impossible to write a correct system using only
the predicates from the specification.

Inspired by this example we want our synthesis algorithm to function with
expressions from theories and to find new predicates when necessary. Our
algorithm is similar to the one in the original TSL synthesis paper [9]. The
TSL specification is encoded into an LTL formula that contains a Boolean
variable for each theory predicate in the TSL formula. These variables are
seen as inputs, which means that the environment determines their truth
values. As a result, realizability of the LTL formula implies realizability of
the TSL formula, but not vice versa, because the environment can choose values
for the variables that are not consistent with the theory. The LTL formula is
then given to a propositional LTL synthesis tool [11, 13]. If Boolean
synthesis is successful we obtain a Boolean system that can be concretized
into a system that operates on the original value domain. If synthesis of the
LTL formula is not successful, we get a Boolean counter strategy that we
analyze for inconsistencies with respect to the theory. An theory-consistent
counter strategy means that the TSL specification is unrealizible. If an
inconsistency is found the counter strategy is spurious and new assumptions
and possibly new predicates are generated and integrated into the TSL
specification.

The procedure can be likened to a CEGAR loop [3], or to the DPLL(T) in which
LTL synthesis plays the role of the propositional SAT solver and the
consistency check is performed by the theory solver. The main difference is
that in our case inconsistencies can span multiple time steps.

Figure 1 shows an overview of our approach. We will show that the synthesis
problem for TSL modulo theories is undecidable and the process is thus not
guaranteed to terminate.

Figure 1: Overview of the synthesis procedure.

The central part of our algorithm and main contribution of this paper is the
theory consistency analysis of a counter strategy. It uses an theory solver —
e.g., an SMT solver — to locally analyze the states of transitions of the
counter strategy to detect inconsistencies with respect to the theory. The
assumptions it generates will contain new predicates where necessary.

The remaining paper is structured as follows: Section 2 contains required
definitions and formalizes the synthesis problem for TSL modulo theory. We
describe the Boolean abstraction and the theory consistency analysis in detail
in section 3. The main synthesis procedure is described in section 4. An
experimental evaluation was performed for multiple examples using the theories
of linear integer arithmetic and linear real arithmetic (section 5). We
conclude our work in section 6.

##  2 Preliminaries

We use Temporal Stream Logic (TSL) [9], with the addition of decidable
theories.

###  2.1 Theories and Updates

A theory $\mathcal{T}$ consists of a signature (symbols for constants,
functions, and predicates) and a domain of values $\mathbb{T}$. All symbols
are assumed to have a fixed interpretation in the domain $\mathbb{T}$. In the
following we will use $E_{\mathcal{T}}(V)$ to denote the set of expressions in
$\mathcal{T}$ with free variables that are a subset of $V$. The set
$E_{\mathcal{T}}(V)$ is partitioned into a set
$E^{\mathbb{T}}_{\mathcal{T}}(V)$ of terms (denoting values in $\mathbb{T}$)
and a set $E^{\mathbb{B}}_{\mathcal{T}}(V)$ of formulas (denoting truth
values). We assume that the theories used have decidable procedures for
satisfiability checking and quantifier elimination. We assume that we are
given a procedure sat(t)hat returns true iff a formula $\phi$ is satisfiable
and a function quantelim(t)hat takes a formula and returns a theory-equivalent
formula that does not contain quantifiers.

###### Example 2

The signature of the theory of linear integer arithmetic (LIA) can be defined
in Backus-Naur form:

$\displaystyle\langle\text{const}\rangle$ $\displaystyle:=0\mid 1\mid
2\mid\ldots$ $\displaystyle\langle\text{var}\rangle$ $\displaystyle:=x\mid
y\mid z\mid\ldots$ $\displaystyle\langle\text{term}\rangle$
$\displaystyle:=\langle\text{const}\rangle\mid\langle\text{var}\rangle\mid-\langle\text{int}\rangle\mid\langle\text{int}\rangle+\langle\text{int}\rangle\mid\langle\text{const}\rangle*\langle\text{int}\rangle$
$\displaystyle\langle\text{formula}\rangle$
$\displaystyle:=\langle\text{int}\rangle=\langle\text{int}\rangle\mid\langle\text{int}\rangle\leq\langle\text{int}\rangle\mid\forall\langle\text{var}\rangle.\langle\text{formula}\rangle$

#### Updates

In the following, we will use sets of state variables $R$ and input $I$
variables. The new values of the state variables are determined using update
functions. An update function $\mathbf{u}$ defines an update $\mathbf{u}(r)\in
E_{\mathcal{T}}^{\mathbb{T}}(R\cup I)$ for each $r\in R$. The set of all
update functions is denoted by $\mathbf{U}$.

We introduce the notations $\mathbf{R}\triangleq R\to\mathbb{T}$ and
$\mathbf{I}\triangleq I\to\mathbb{T}$ for valuations of variables. We write
$R/\mathbf{r}$ ($I/\mathbf{i}$) to denote the replacement of all variables in
$R$ ($I$, resp.) by their corresponding values in $\mathbf{r}$ ($\mathbf{i}$,
resp.). With slight abuse of notation, we identify
$e[R/\mathbf{r},I/\mathbf{i}]$ with the corresponding value in the domain.

To apply an update function $\mathbf{u}\in\mathbf{U}$ to valuations
$\mathbf{r}\in\mathbf{R}$ and $\mathbf{i}\in\mathbf{I}$ we write
$\mathbf{u}[\mathbf{r},\mathbf{i}]$ which is defined as
$\mathbf{u}[\mathbf{r},\mathbf{i}](r)=\mathbf{u}(r)[R/\mathbf{R},I/\mathbf{I}]$
for each $r$.

###  2.2 Temporal Stream Logic Modulo Theories

TSL(T) is based on linear temporal logic, but instead of Boolean variables it
uses updates and Boolean theory expressions. The grammar for TSL(T) formulas
is

$\displaystyle\langle\text{ap}\rangle$
$\displaystyle:=E_{\mathcal{T}}^{\mathbb{T}}(R\cup I)$
$\displaystyle\langle\text{theory}\rangle$
$\displaystyle:=E_{\mathcal{T}}^{\mathbb{B}}(R\cup I)$
$\displaystyle\langle\text{bconst}\rangle$
$\displaystyle:=\mathrm{true}\mid\mathrm{false}$
$\displaystyle\langle\text{upd}\rangle$
$\displaystyle:=[\langle\text{var}\rangle\leftarrow\langle\text{theory}\rangle]$
$\displaystyle\langle\text{tsl}\rangle$
$\displaystyle:=\langle\text{ap}\rangle\mid\langle\text{upd}\rangle\mid\langle\text{bconst}\rangle\mid\neg\langle\text{tsl}\rangle\mid\langle\text{tsl}\rangle\land\langle\text{tsl}\rangle\mid\langle\text{tsl}\rangle\mathrel{\mathbf{U}}\langle\text{tsl}\rangle\mid\operatorname{\mathbf{X}}\langle\text{tsl}\rangle.$

The semantics of TSL(T) are defined with respect to a trace of inputs and
state variable configurations $\rho\in(\mathbf{I}\times\mathbf{R})^{\omega}$
as follows. We assume that $\rho=\rho_{0},\rho_{1},\dots$ and that
$\rho_{j}=(\mathbf{r}_{j},\mathbf{i}_{j})$ and we define

$\displaystyle\rho\models p$ $\displaystyle\text{ iff }\rho_{0}\models p\text{
for $p\in\langle\text{ap}\rangle$}$ $\displaystyle\rho\models[r\leftarrow e]$
$\displaystyle\text{ iff }\mathbf{r}_{1}=e(R/\mathbf{r}_{0},I/\mathbf{i}_{0})$
$\displaystyle\rho\models\mathrm{true}$
$\displaystyle\rho\not\models\mathrm{false}$
$\displaystyle\rho\models\neg\phi$ $\displaystyle\text{ iff
}\rho\not\models\phi$ $\displaystyle\rho\models\phi\wedge\psi$
$\displaystyle\text{ iff }\rho\models\phi\text{ and }\rho\models\psi$
$\displaystyle\rho\models\phi\mathrel{\mathbf{U}}\psi$ $\displaystyle\text{
iff }\exists j.\rho_{j},\rho_{j+1},\dots\models\psi\text{ and }\forall
i<j.\rho_{i},\rho_{i+1},\dots\models\phi$
$\displaystyle\rho\models\operatorname{\mathbf{X}}\phi$ $\displaystyle\text{
iff }\rho_{1},\rho_{2},\dots\models\phi$

The unary temporal operators eventually ($\operatorname{\mathbf{F}}$) and
globally ($\operatorname{\mathbf{G}}$) can be added using their usual
definitions:
$\operatorname{\mathbf{F}}\varphi\equiv\mathrm{true}\mathrel{\mathbf{U}}\varphi$
and
$\operatorname{\mathbf{G}}\varphi\equiv\neg\operatorname{\mathbf{F}}\neg\varphi$.

###  2.3 Theory Mealy and Moore Machines

Theory Mealy machines are state machines with inputs and register variables
that range over the theory domain. The updates to the state variables and the
registers are restricted by a set of predicates and the selected update
functions.

A _Theory Mealy Machine_
$M_{\mathcal{T}}=(Q,q_{0},P,\mathbf{r}_{0},\delta,\mu)$ consists of a finite
set of states $Q$, an initial state $q_{0}\in Q$, a finite set of predicates
$P\subseteq E_{\mathcal{T}}^{\mathbb{B}}(R\cup I)$, an initial valuation
$\mathbf{r}_{0}\in\mathbf{R}$, a transition function $\delta\in(Q\times
2^{P})\to Q$ and a update selection function $\mu\in(Q\times
2^{P})\to\mathbf{U}$.

For a given valuation $\mathbf{v}=(\mathbf{r},\mathbf{i})$, let
$P_{\mathbf{v}}\subseteq P$ be the subset of predicates that is true in
$\mathbf{v}$: $P_{\mathbf{v}}=\\{p\in P\mid\mathbf{v}\models p\\}$.

A run $\sigma$ of a theory Mealy machine induced by a sequence of input
valuation
$\bar{\mathbf{i}}=\mathbf{i}_{0},\mathbf{i}_{1},\dots\in\mathbf{I}^{\omega}$
is an infinite sequence of states $Q$ and valuations $\mathbf{R}$
$(q_{0},\mathbf{r}_{0}),(q_{1},\mathbf{r}_{1}),\ldots$. Any two consecutive
configurations $(q_{i},\mathbf{r}_{i})$ and $(q_{i+1},\mathbf{r}_{i+1})$ must
be related by $q_{i+1}=\delta(q_{i},P_{(\mathbf{r}_{i},\mathbf{i}_{i})})$ and
$\mathbf{r}_{i+1}=\mathbf{u}_{i}[\mathbf{r}_{i},\mathbf{i}_{i}]$ where
$\mathbf{u}_{i}=\mu(q_{i},P_{(\mathbf{r}_{i},\mathbf{i}_{i})})$.

A Theory Mealy machine $M_{\mathcal{T}}$ realizes a TSL(T) formula $\phi$ if
for all inputs sequences $\bar{\mathbf{i}}\in\mathbf{I}^{\omega}$ the
resulting trace $\rho\equiv(\bar{\mathbf{i}},\bar{\mathbf{r}})$ satisfies
$\phi$.

We also define Theory Moore machines, which read the updates produced by a
Mealy machine and produce the inputs read by a Mealy machine. Intuitively,
Mealy machines are used to show realizability of a TSL(T) specification, while
Moore machines are used to show their unrealizability. A _Theory Moore
Machine_ $M_{\mathcal{T}}=(Q,q_{0},P,\mathbf{r}_{0},\delta,\iota)$ consists of
a finite set of states $Q$, an initial state $q_{0}\in Q$, a finite set of
predicates $P\subseteq E_{\mathcal{T}}^{\mathbb{B}}(R\cup I)$, an initial
valuation $\mathbf{r}_{0}\in\mathbf{R}$, and a transition function
$\delta\in(Q\times\mathbf{U})\to Q$, and
$\iota:Q\times\mathbf{R}\rightarrow\mathbf{I}$ is the output function.

A run $\sigma$ of a theory Moore machine induced by an infinite sequence of
update functions $\bar{\mathbf{u}}\in\mathbf{U}^{\omega}$ is a sequence of
states and valuations $(q_{0},\mathbf{r}_{0}),(q_{1},\mathbf{r}_{1}),\ldots$.
Any two consecutive entries $(q_{i},\mathbf{r}_{i})$ and
$(q_{i+1},\mathbf{r}_{i+1})$ must be related by
$q_{i+1}=\delta(q_{i},\mathbf{u}_{i})$ and
$\mathbf{r}_{i+1}=\mathbf{u}_{i}[\mathbf{r}_{i},\iota(q_{i})]$.

##  3 Boolean Abstraction

###  3.1 Propositional Encoding of TSL(T)

In this section, we describe the propositional encoding of TSL(T), which
closely follows that of Finkbeiner et al. [9].

A TSL(T) formula $\phi$ is encoded to an LTL formula $\phi_{\mathcal{B}}$.
Formula $\phi_{\mathcal{B}}$ is obtained by replacing each update $u$ in
$\phi$ by a Boolean output variables $p_{u}$ and each atomic proposition
$\mathrm{ap}$ by a Boolean input variable $p_{\mathrm{ap}}$. Additionally, the
formula ensures that for each variable exactly one update is active at any
point in time. This results in:

$\phi_{\mathcal{B}}\triangleq\operatorname{\mathbf{G}}(\bigwedge_{r}\bigvee_{i}(p_{[r\leftarrow
e_{i}]}\land\bigwedge_{j\neq i}\neg p_{[r\leftarrow
e_{j}]}))\land\phi[ap/p_{ap},\ldots,u/p_{u},\ldots].$

###### Example 3

The TSL(T) formula $\phi\triangleq 0\leq x\land
x<5\rightarrow\operatorname{\mathbf{G}}(0\leq x\land x<5\land([x\leftarrow
x-1]\lor[x\leftarrow x+1]))$ is encoded as the LTL formula

$\phi_{\mathcal{B}}\triangleq\operatorname{\mathbf{G}}(p_{[x\leftarrow
x-1]}\wedge\neg\ p_{[x\leftarrow x+1]}\vee p_{[x\leftarrow x+1]}\wedge\neg
p_{[x\leftarrow x-1]})\land\\\ (p_{0\leq x}\land
p_{x<5}\rightarrow\operatorname{\mathbf{G}}(p_{0\leq x}\land
p_{x<5}\land(p_{[x\leftarrow x-1]}\lor p_{[x\leftarrow x+1]}))),$

where $p_{0\leq x}$ and $p_{x<5}$ are input variables and $p_{[x\leftarrow
x-1]}$ and $p_{[x\leftarrow x+1]}$ are output variables.

###  3.2 Boolean Mealy and Moore Machines

We will now define Boolean Mealy and Moore machines. These are the abstract
versions of theory machines defined above that can be checked against
propositionally encoded TSL(T) specifications. They allow us to link Boolean
systems realizing a PTSL formula to theory systems. We also study when a
Boolean system is consistent with the theory it abstracts over.

The Boolean abstraction is based on a finite set of predicates $P\subset
E_{\mathcal{T}}^{\mathbb{B}}(R\cup I)$.

A _Boolean Mealy machine_ is a tuple
$(Q,P,q_{0},\delta_{\mathcal{B}},\mu_{\mathcal{B}})$, where $Q$ is a set of
states, $P$ is a set of predicates, $q_{0}\in Q$ is the initial state,
$\delta_{\mathcal{B}}\in Q\times 2^{P}\to Q$ is the transition function, and
$\mu_{\mathcal{B}}\in Q\times 2^{P}\to\mathbf{U}$ is the update selection
function.

A trace $\sigma_{\mathcal{B}}$ of a Boolean Mealy machine induced by a
sequence $\bar{\varphi}\in(2^{P})^{\omega}$ is an infinite alternating
sequence of states and updates ${(Q\times\mathbf{U})}^{\omega}$,
$(q_{0}^{\mathcal{B}},\mathbf{u}_{1}^{\mathcal{B}},q_{1}^{\mathcal{B}},\mathbf{u}_{2}^{\mathcal{B}},\ldots)$
where $q_{i+1}=\delta_{\mathcal{B}}(q_{i},\varphi_{i})$ and
$\mathbf{u}_{i+1}=\mu_{\mathcal{B}}(q_{i},\varphi_{i})$.

A Boolean Mealy machine $M_{\mathcal{B}}$ is theory consistent with respect to
theory $\mathcal{T}$ iff there exists a theory machine $M_{\mathcal{T}}$ such
that all $v\models p_{0}$ are initial valuations and every run of
$M_{\mathcal{T}}$ is contained in $M_{\mathcal{B}}$. More precisely this means
that $Q$, $q_{0}$, and $U$ are the same for both machines. Additionally,
$\delta_{\mathcal{B}}$ must be compatible with $\delta$ and
$\mu_{\mathcal{B}}$ with $\mu$, i.e., $\forall
q,\varphi,\mathbf{r},\mathbf{i}\ldotp\mathbf{r}\|\mathbf{i}\models\varphi\Rightarrow(\delta(q,\mathbf{r},\mathbf{i})=\delta_{\mathcal{B}}(q,\varphi)\land\mu(q,\mathbf{r},\mathbf{i})=\mu_{\mathcal{B}}(q,\varphi))$.

A Boolean Moore machine $M_{\mathcal{B}}=(Q,P,q_{0},\delta,o)$ is an abstract
version of a theory Moore machine $M_{\mathcal{T}}$. $Q$ is a set of states,
$P$ is a set of predicates, $q_{0}\in Q$ is the initial state, $\delta\in
Q\times\mathbf{U}\to Q$ is the transition function, and $o\in Q\to 2^{P}$ is
the output function. The set $\mathbf{U}$ can be encoded as a set of Boolean
variables, with one variable for every update in $U$ the input then becomes a
valuation of these Boolean variables which has to conform to an update
function. A run $\sigma_{\mathcal{B}}$ of a Boolean Moore machine induced by a
sequence $\bar{\mathbf{u}}\in\mathbf{U}^{\omega}$ is an infinite sequence of
states ${Q}^{\omega}$, $(q_{0},q_{1},\ldots)$ where
$q_{i+1}=\delta(q_{i},\mathbf{u}_{i})$.

A Boolean Moore machine $M_{\mathcal{B}}$ is theory consistent with respect to
theory $\mathcal{T}$ iff there exists a theory machine $M_{\mathcal{T}}$ such
that $\mathbf{r}_{0}\models o(q_{0})$ and every run of $M_{\mathcal{T}}$ is
contained in $M_{\mathcal{B}}$. More precisely this means that $Q$, $q_{0}$,
$U$, and $\delta$ are the same for both machines and a run
$\sigma_{\mathcal{T}}\subset\sigma_{\mathcal{B}}$ iff $\forall
i\ldotp\mathbf{r}_{i}\models o(q_{i})$. In this case we write
$M_{\mathcal{T}}\sim M_{\mathcal{B}}$.

###  3.3 Theory Consistency Analysis

When an environment strategy is deemed inconsistent the specification is
extended in one of three ways: a new single state assumption, a new transition
assumption, or a new predicate. The counter strategy analysis is performed in
two stages. The first checks for consistency of outputs in a single state
while the second one checks consistency of transitions.

def  _isconsistent($m$)_:

Data: Boolean Moore machine $m=(Q,P,U,q_{0},\delta,o)$

Result: consistent or (possibly) inconsistent with additional assumptions.

_ _ foreach  _$q\in\operatorname{reachable}(Q)$ ;_

__ // Case 1

do

if  _$\neg\texttt{sat}(o(q))$_ then

yield inconsistent, $\operatorname{\mathbf{G}}\neg o(q)$);

end if

end foreach

_ _foreach  _$(q_{i},\mathbf{u},q_{j})\in\operatorname{reachable}(\delta)$ ;_

__ // Case 2

do

if  _$\neg\texttt{sat}(o(q_{i})\land\mathbf{u}\land o(q_{j})^{\prime})$_ then

yield inconsistent,
$\operatorname{\mathbf{G}}(o(q_{i})\land\mathbf{u}\rightarrow\operatorname{\mathbf{X}}\neg
o(q_{j}))$;

end if

end foreach

_ _foreach  _$(q_{i},\mathbf{u},q_{j})\in\operatorname{reachable}(\delta)$ ;_

__ // Case 3

do

if  _$\texttt{sat}(\forall i^{\prime}_{0},\ldots,i^{\prime}_{m}\ldotp
o(q_{i})\land\mathbf{u}\land\neg o(q_{j})^{\prime})$_ then

$wp$ := weakest precondition ($\mathbf{u}$, $o(q_{j})^{\prime}$);

$\rho$ := quantelim($\exists i^{\prime}_{0},\ldots,i^{\prime}_{m}\ldotp
wp\land o(q_{i})$);

yield inconsistent, $\operatorname{\mathbf{G}}(\neg\rho\land
o(q_{i})\land\mathbf{u}\rightarrow\operatorname{\mathbf{X}}\neg o(q_{j}))$;

end if

end foreach

return consistent;

Algorithm 1 Consistent with theory and using inputs.

#### State Consistency

To check state consistency we look at every (reachable) state in the counter
strategy and use an SMT solver to check if the output assignment is consistent
with the theory. For example the two variables $p_{x\geq 5}$ and $p_{x<0}$
cannot be true in the same state. If such a problem is found we generate a new
assumption that rules out this assignment in every state. In the previous
example this would generate the assumption $\operatorname{\mathbf{G}}(\neg
p_{x\geq 5}\vee\neg p_{x<0})$. This process is similar to the interaction
between a SAT solver and a theory solver in an SMT solver with lazy encoding.

#### Transition Consistency

Once all states produce consistent outputs and there still exists a counter
strategy, we turn towards transitions. As of now there are no assumptions that
link the state before an action was performed to the state afterwards. This
step creates these assumptions where necessary and also finds new predicates
if the existing ones are not sufficient.

We again use an SMT solver to perform this analysis. Let’s look at the
transition $\\{p_{x\geq 5}\\}[x\leftarrow x+1]\\{\neg p_{x\geq 5}\\}$. To
check it the following SMT problem is generated $x\geq 5\land
x^{\prime}=x+1\land\neg(x^{\prime}\geq 5)$, this is unsatisfiable and we can
generate an assumption to eliminate it $\operatorname{\mathbf{G}}(p_{x\geq
5}\land[x\leftarrow x+1]\rightarrow\operatorname{\mathbf{X}}p_{x\geq 5})$.

Another case is that a transition is possible for some, but not all of values.
For instance, the triple $\\{p_{x<0}\\}[x\leftarrow x+1]\\{p_{x\geq 0}\\}$
does not hold for all values of $x$. This shows that our current abstraction
might not be precise enough to correctly describe this transition. In that
case we calculate the weakest precondition of the post state given the updates
of the transition. This gives us the new predicate $x\geq-1$. In case there
are input variables we give the environment the benefit of doubt when checking
if a transition is inconsistent. A transition is inconsistent if for all
possible inputs at the next time step we do not satisfy the target state
predicate. After computing the weakest precondition we use existential
quantifier elimination to remove the future inputs from our predicate. In that
case we are looking for states where transition is valid, which changes the
quantifiers from forall to exists.

###### Example 4

Algorithm 1 checks consistency on a local level, the environment strategy can
still be globally consistent if case 3 reports inconsistent. The following
Boolean Moore machine has two transitions (orange) that are reported as
inconsistentby Algorithm 1 even though the machine is globally consistent.

The transition $(q1,[x\leftarrow x+1],q2)$ would be invalid for $x=1$ in $q1$,
but for every execution $x=0$ in $q1$ and the problem does not appear. A
similar situation occurs for the transition $(q2,[x\leftarrow x+1],q0)$, where
$x$ will always be $1$ and the transition is only invalid for $x<1$. The blue
annotations show the possible values of $x$ in every state, demonstrating that
all transitions are actually consistent.

The fact that we are over eager when reporting inconsistencies means that it
will be harder to show unrealizability, but it does not affect our ability to
find realizing systems.

###### Lemma 1

If algorithm 1 reports consistent for a Boolean Moore machine
$M_{\mathcal{B}}$ there exists a theory Moore machine $M_{\mathcal{T}}$ such
that $M_{\mathcal{T}}\sim M_{\mathcal{B}}$.

###### Proof

Assuming the algorithm returns consistent. Every output function is
satisfiable, this includes the initial state which contains an initial value
of the theory machine. For every transition
$(\varphi_{i},\mathbf{u},\varphi_{j})$ where there exists a model of
$\varphi_{i}$ all of the models map to a model of $\varphi_{j}$, by the
transition property checked by the algorithm. Therefore by induction all paths
starting in the initial state and only using transitions from $\delta$ contain
a path of a theory machine. A theory machine $M_{\mathcal{T}}$ is included in
$M_{\mathcal{B}}$. ∎

###### Lemma 2

All assumptions $\psi$ added by algorithm 1 are tautological with respect to
the theory.

$\forall M_{\mathcal{T}}\ldotp M_{\mathcal{T}}\models\psi$

###### Proof

The algorithm can produce three different types of assumptions
$\psi_{s},\psi_{t},\psi_{p}$ corresponding to the three cases of the
algorithm.

Let $\psi_{s}$ be $\operatorname{\mathbf{G}}\neg o(q)$ for an unsatisfiable
$o(q)$. $M_{\mathcal{T}}$ must define a output valuation for every state,
because $o(q)$ is empty no state in any $M_{\mathcal{T}}$ can produce such an
output. Therefore all $M_{\mathcal{T}}$ satisfy $\psi_{s}$.

Let $\psi_{t}$ be
$\operatorname{\mathbf{G}}(o(q_{i})\wedge\mathbf{u}\rightarrow\operatorname{\mathbf{X}}\neg
o(q_{j}))$ where $\neg\texttt{sat}(o(q_{i})\wedge u\wedge o(q_{j})^{\prime})$
and $\texttt{sat}(o(q_{i}))$. None of the values satisfying $o(q_{i})$ have a
successor in $o(q_{j})$ after performing $u$. The added constraint is
equivalent to $\neg(o(q_{i})\wedge\mathbf{u}\wedge
o(q_{j})^{\prime})\Leftrightarrow\neg o(q_{i})\lor\neg\mathbf{u}\lor\neg
o(q_{j})^{\prime})\Leftrightarrow(o(q_{i})\land u)\rightarrow\neg
o(q_{j})^{\prime}\Leftrightarrow
o(q_{i})\wedge\mathbf{u}\rightarrow\operatorname{\mathbf{X}}\neg o(q_{j})$.
All transition in all $M_{\mathcal{T}}$ satisfy this property at all points in
time.

Let $\psi_{p}$ be $\operatorname{\mathbf{G}}(\neg
p\wedge\mathbf{u}\rightarrow\operatorname{\mathbf{X}}\neg o(q_{j}))$ where $p$
is the weakest precondition of $o(q_{j})$ under $u$ and
$\texttt{sat}(o(q_{i})\land u\land\neg o(q_{j}))$. By the definition of
weakest precondition no value in $\neg p$ leads to $o(q_{j})$ when performing
$\mathbf{u}$. This also hold in the presence of inputs. The quantifier
elimination procedure leads to the weakest precondition for unknown inputs at
the next time step. All transitions in all $M_{\mathcal{T}}$ will lead from
$\neg p$ to $\neg o(q_{j})$ when performing $\mathbf{u}$.

All added constraints are satisfied by all states and transitions in all
$M_{\mathcal{T}}$. The constraints only talk about individual states and
transitions therefore also all traces in $M_{\mathcal{T}}$ satisfy these
constraints and $M_{\mathcal{T}}\models\psi$.∎

###  3.4 Generalizing Counterexamples

The counter examples generated by algorithm 1 only block the exact state or
transition present in the counter strategy. To achieve faster and better
convergence it is necessary to generalize these counter examples.

Generalization of counter examples is done using an algorithm to find an
unsatisfiable core, i.e., a small (not necessarily minimal) subset of clauses
such that their conjunction is unsatisfiable. SMT solver such as Z3 [4]
contain an implementation of such a procedure. We are using unsat cores to
find smaller counter examples that do not depend on superficial information.
Therefore, the counter examples also block situations where unrelated
predicates or updates are different.

The counter examples generated in case 1 are straightforward to generalize. A
given output predicate, a conjuction of literals, is unsatisfiable by
calculating an unsat core we obtain a small set of these literal that is still
unsatisfiable. A counter example $\operatorname{\mathbf{G}}\neg o(q)$ is
generalized to $\operatorname{\mathbf{G}}\neg unsatcore(o(q)$.

We can use a similar idea for the assumptions generated in case 2. The SMT
encoding of a transition is unsatisfiable
$\neg\texttt{sat}(o(q_{i})\land\mathbf{u}\land o(q_{j})^{\prime})$. An unsat
core contains subsets of $o(q_{i})$, $\mathbf{u}$, and $o(q_{j})^{\prime}$
that are unsatisfiable, let them be $\overline{o(q_{i})}$,
$\overline{\mathbf{u}}$, and $\overline{o(q_{j})^{\prime}}$ respectively.
Using these we get the new assumption
$\operatorname{\mathbf{G}}(\overline{o(q_{i})}\land\overline{\mathbf{u}}\rightarrow\operatorname{\mathbf{X}}\neg\overline{o(q_{j})})$

Case 3 seems to be different as it does check for satisfiability of a
quantified formula instead of unsatisfiabiliy of a quantifier free
conjunction. However, after finding the new predicates and performing
quantifier elimination we get counter examples of a similar structure as in
case 2. The main difference is that the precondition is negated and the unsat
core algorithm cannot remove clauses from it. Because $\rho$ is the weakest
precondition we know that the transition is not possible if any of its negated
clauses are part of the precondition. This allows us to split the assumptions
into
$\bigwedge_{l}\operatorname{\mathbf{G}}(\neg\rho_{l}\land\mathbf{u}\rightarrow\operatorname{\mathbf{X}}\neg
o(q_{j}))$ where $\rho_{l}$ are the clauses of $\rho$ and generalize these
using the unsat core procedure form case 2.

##  4 Synthesis

We adapt the technique used by Finkbeiner et al. [9], but use a more
sophisticated analysis of counter strategies. The procedure starts with a
specification in TSL(T) that is translated to LTL by creating variables for
every propositional expression and action. Every predicate evaluation is
treated as an input and only actions are assumed to be outputs. This is given
to a synthesis tool for propositional LTL: if it finds a solution this is also
a solution for the TSL(T) synthesis problem, otherwise a counter strategy is
produced. In case of a counter strategy it is analyzed to find an
inconsistency with the used theory and either an extension of the
specification is produced, the counter strategy is consistent, or the verifier
is unable to decide consistency. This procedure resembles a CEGAR [3] loop and
is depicted in fig. 1.

Data: TSL(T) modulo theory specification: $\phi$

Result: Satisfying Mealy machine or unrealizable or non-termination

while  _true_ do

$\phi_{\mathcal{B}}$ := prop_encode($\phi$);

(r,m) := synth($\phi_{\mathcal{B}}$);

if  _r is unrealizable_ then

c, $\psi$ := isconsistent(m);

if  _c is inconsistent_ then

$\phi$ := $\psi\rightarrow\phi$;

else

return unrealizable;

end if

else

return m;

end if

end while

Algorithm 2 Synthesis using abstraction refinement.

For a initial specification $\phi$ the extension with new assumptions $\psi$
is given as
$\phi_{n}\triangleq\operatorname{\mathbf{G}}\bigwedge_{k=1}^{n}\psi_{k}\boldsymbol{\rightarrow}\phi$
for the $n$-th refinement of $\phi$ with $\psi_{k}$ the assumptions added in
refinement $k$.

###  4.1 Illustrative Example

Let us consider the following example: a counter $x$ has to be kept between a
minimum and a maximum value. At each time step the system can choose one of
two actions: increase the counter by an input $i$, or decrement the counter.
The environment picks the value of the input variable from a given interval at
each time step as well as the initial value of the state variable. We use the
concrete values $0\geq x<10$ and $0\geq i<5$. Formally this is defined by the
TSL(LIA) specification $\phi\triangleq(0\leq x\land
x<10\land\operatorname{\mathbf{G}}(0\leq i\land
i<5))\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}(0\leq x\land
x<10\land([x\leftarrow x-1]\lor[x\leftarrow x+i]))$.

At first this is encoded as an LTL formula
$\phi_{\mathcal{B}}\triangleq(p_{0\leq x}\land
p_{x<10}\land\operatorname{\mathbf{G}}(p_{0\leq i}\land
p_{i<5}))\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}(p_{0\leq x}\land
p{x<10}\land(p_{[x\leftarrow x-1]}\lor p_{[x\leftarrow x+i]})$ which is given
to a propositional synthesis tool. It informs us that $\phi_{\mathcal{B}}$ is
unrealizible and gives us a counter strategy as an explanation.

This counter strategy is analyzed for theory inconsistencies using algorithm
1. The output of the state $s1$ is inconsistent, because $\neg(0\leq
x)\land\neg(x<10)$ is unsatisfiable. We obtain the new assumption
$\psi_{1}\triangleq\operatorname{\mathbf{G}}(0\leq x\lor x<10)$, note that
this is a more general assumption than just the negated state formula. Section
3.4 goes into more detail on how to generalize assumptions. The new assumption
is used to extend the specification. The specification after $r$ iterations is
$\phi_{r}\triangleq\bigwedge_{k=1}^{r}\psi_{k}\boldsymbol{\rightarrow}((0\leq
x\land x<10\land\operatorname{\mathbf{G}}(0\leq i\land
i<5))\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}(0\leq x\land
x<10\land([x\leftarrow x-1]\lor[x\leftarrow x+i])))$ with $\psi_{r}$ the
assumption added in iteration $r$.

Attempting to synthesis a system for $\phi_{1}$ results in the counter
strategy

This time all outputs are consistent, but the transition $(s0,[x\leftarrow
x-1],s1)$ is inconsistent. If $x<10$ and we compute the next value with
$[x\leftarrow x-1]$ it cannot be that $x\geq 10$ in the next state. We obtain
the assumption
$\psi_{2}\triangleq\operatorname{\mathbf{G}}(x<10\land[x\leftarrow
x-1]\rightarrow\operatorname{\mathbf{X}}x<10)$.

Boolean synthesis for $\phi_{2}$ again results in a counter example, this time
the transition $(s0,[x\leftarrow x+i],s1)$ is inconsistent.

The generated assumption is $\psi_{3}\triangleq\operatorname{\mathbf{G}}(0\leq
x\land[x\leftarrow x+i]\rightarrow\operatorname{\mathbf{X}}0\leq x)$.

The Boolean synthesis problem for $\phi_{3}$ is again unrealizible with the
counter strategy:

All the output functions are consistent and none of the transitions are
invalid for all valued. We now have to look at the third category of
inconsistencies, transitions that are only valid for some of the concrete
states in its abstract origin state. The new predicate $x\geq 1$ is learned
from analyzing the transition $s0$ to $s2$. It is part of the assumption
$\psi^{\prime}_{4}\triangleq\operatorname{\mathbf{G}}(x\geq 1\land[x\leftarrow
x-1]\rightarrow\operatorname{\mathbf{X}}0\leq x)$. To reduce the required
refinements in this example we immediately add a state consistency assumption
and get $\psi_{4}\triangleq\operatorname{\mathbf{G}}(x\geq 1\lor
x<10)\land\psi^{\prime}_{4}$.

Running the Boolean synthesis algorithm again results in a counter example:

Transition $(s0,[x\leftarrow x+i],s1)$ is inconsistent. The added assumption
is $\psi_{5}\triangleq\operatorname{\mathbf{G}}(0\leq x\land
x<1\land[x\leftarrow x+i]\rightarrow\operatorname{\mathbf{X}}x<10)$.

The Boolean synthesis is executed for the last time on $\phi_{5}$. This time a
Boolean system satisfying the specification is produced.

It can be translated into a concrete imperative program.

⬇

while(true):

i := receive()

if (x>=1):

x := x - 1

else:

x := x + i

send(x)

###  4.2 Correctness

###### Theorem 4.1

If algorithm 2 returns unrealizible there is no $M_{\mathcal{T}}\models\phi$.

###### Proof

If there exists a machine $M_{\mathcal{T}}^{\prime}\models\neg\phi$ there is
no machine $M_{\mathcal{T}}\models\phi$. The propositional synthesis tool
provides us with a machine $M_{\mathcal{B}}\models\neg\phi$. The consistency
check results in consistent, so by lemma 1 there exists a
$M_{\mathcal{T}}^{\prime}\models\neg\phi$. ∎

###### Lemma 3

If $M_{\mathcal{B}}$ satisfies a propositionally encoded formula
$\phi_{\mathcal{B}}$ than any of its conrcretizations $M_{\mathcal{T}}\sim
M_{\mathcal{B}}$ satisfy the TSL(T) formula $\phi$.

$M_{\mathcal{B}}\models\phi^{\mathcal{B}}\Rightarrow\forall
M_{\mathcal{T}}\sim M_{\mathcal{B}}\ldotp M_{\mathcal{T}}\models\phi$

###### Proof

$M_{\mathcal{B}}$ wins against all interpretations of the predicates. The
theories semantics impose one interpretation of the theory symbols.

So $M_{\mathcal{T}}$ wins against the one interpretation imposed by the
theories semantics.∎

###### Theorem 4.2

If algorithm 2 returns a system $M_{\mathcal{T}}$ it holds that
$M_{\mathcal{T}}\models\phi$.

###### Proof

The algorithm 2 returns a system $M_{\mathcal{B}}$ that for some refinement
$r$ satisfies the Boolean specification $\phi_{r}^{\mathcal{B}}$. By lemma 3
any concretization $M_{\mathcal{T}}\sim M_{\mathcal{B}}$ satisfies $\phi_{r}$.
From lemma 2 it follows that $M_{\mathcal{T}}$ satisfying
$\phi_{r}\equiv(\bigwedge_{k}^{r}\psi_{k})\rightarrow\phi$ satisfies $\phi$.∎

Even though our algorithm is not guaranteed to terminate it can proof
unrealizabilty in certain cases.

$x=0\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}([x\leftarrow x+1]\land
x<3)$

Here we can perform two refinement steps and learn the new predicates $x\geq
2$ and $x\geq 1$. Using these the propositional synthesis tool is able to
build a consistent environment strategy. There are no conflicts which could be
used to further refine the specification. This shows that the specification is
unrealizable.

###  4.3 Limitations

###### Theorem 4.3

The synthesis problem for TSL(T) modulo theories is undecidable.

###### Proof

A TSL(T) formula with three state variables and a theory supporting: unbounded
integers, increment, decrement, and equality, can simulate a two counter
machine. We consider a two counter machine [12] with the three instructions
increment register $inc(r)$, decrement register $dec(r)$, and jump if zero
$jz(r,z)$. A program for a two counter machine is a list of instructions, with
out loss of generality we assume every instruction is prefixed with its
position in the instruction list (the label l) the last element of the list is
empty and has the label $h$. We also assume that all jump addresses point to
an instruction in the list. The instructions are encoded as:

$\displaystyle\llbracket l:inc(R1)\rrbracket$ $\displaystyle\triangleq
ic=l\land[ic\leftarrow ic+1]\land[r1\leftarrow r1+1]\land[r2\leftarrow r2]$
$\displaystyle\llbracket l:dec(R1)\rrbracket$ $\displaystyle\triangleq
ic=l\land[ic\leftarrow ic+1]\land[r1\leftarrow r1-1]\land[r2\leftarrow r2]$
$\displaystyle\llbracket l:jz(R1,z)\rrbracket$
$\displaystyle\triangleq(ic=l\land r1=0\land[ic\leftarrow z]\land[r1\leftarrow
r1]\land[r2\leftarrow r2])$ $\displaystyle\lor(ic=l\land r1\neq
0\land[ic\leftarrow ic+1]\land[r1\leftarrow r1]\land[r2\leftarrow r2])$

the instruction for $R2$ are the same except $r1$ and $r2$ are flipped. Given
this encoding we can build the formula $(ic=0\land r1=0\land
r2=0)\rightarrow(\bigvee_{instr\in PROG}\llbracket
instr\rrbracket\land\operatorname{\mathbf{F}}ic=h)$ for a program $PROG$.

This is realizable iff the program holds. The halting problem for two counter
machines is undecidable. Therefore the synthesis problem for TSL(T) mod
theories is undecidable. This also applies to formulas with only only one
state variable. In that case one can construct a theory over the domain
$\mathbb{N}\times\mathbb{N}\times\mathbb{N}$ with operations that work on the
individual fields.∎

Our algorithm cannot handle reachability properties where the number of
required steps depends on the concrete value of a state variable and is
unbounded. The specification

$0\leq
x\boldsymbol{\rightarrow}(\operatorname{\mathbf{F}}(x<0)\land\operatorname{\mathbf{G}}([x\leftarrow
x+1]\lor[x\leftarrow x-1]))$

with the state variable $x$ is an example of this happening. The specification
is obviously realized by a system always using the update $[x\leftarrow x-1]$.
However, we would add the new predicates $x\geq 1,x\geq 2,\ldots$ with out
ever terminating.

The algorithm fails to prove unrealizability in certain cases.

$x=1\boldsymbol{\rightarrow}(\operatorname{\mathbf{F}}(x=0)\land\operatorname{\mathbf{G}}[x\leftarrow
x+1])$

Here we would learn the predicates $x=-1,x=-2,\ldots$ with out terminating.
Note that knowing the predicate $x>1$ would allow us to prove unrealizability.
It can serve as an invariant of the loop in a bad lasso.

##  5 Experimental Evaluation

We implemented our algorithm in Haskell. Our implementation relies on several
external tools: tsltools [9] is used for parsing TSL and to perform the
propositional encoding, strix [11] is used for LTL synthesis, and Z3 [4] is
used as the SMT solver. When performing counter example analysis using
algorithm 1 we add all assumptions from the same case before we start the next
iteration. Once a system has been found we rerun strix on the last refinement
with the option to minimize the number of states. This allows us to obtain a
more compact system.

###  5.1 Illustrative example extended

The first experiment is an extension of the illustrative example from section
4.1. The system is no longer allowed to change between the two updates at
every step. Instead after changing the update it has to use the new update for
the next $c$ steps. We also varied the size of the intervals for $x$ and $i$
demonstrating that our algorithm is independent of the size of the concrete
state space. The results table lists the used parameters ($c$, $x_{max}$,
$i_{max}$), the number of refinments, the number of state in the minimized
system, the number of learned predicates during the whole execution and the
total runtime in seconds.

$\displaystyle 0\leq x\land x\leq x_{max}\land\operatorname{\mathbf{G}}(i\geq
0\land i\leq i_{max})\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}($
$\displaystyle 0\leq x\land x\leq x_{max}\land([x\leftarrow
x-i]\lor[x\leftarrow x+i])\land$ $\displaystyle(([x\leftarrow
x-i]\land\operatorname{\mathbf{X}}[x\leftarrow
x+i])\rightarrow\operatorname{\mathbf{G}}_{[1,c]}[x\leftarrow x+i])\land$
$\displaystyle(([x\leftarrow x+i]\land\operatorname{\mathbf{X}}[x\leftarrow
x-i])\rightarrow\operatorname{\mathbf{G}}_{[1,c]}[x\leftarrow x-i]))$

$c$ | $x_{max}$ | $i_{max}$ | # refinements | # states | # learned predicates | time [s]
---|---|---|---|---|---|---
1 | 100 | 5 | 4 | 1 | 2 | 1.0
2 | 100 | 5 | 5 | 2 | 2 | 1.3
2 | 1 000 | 5 | 5 | 2 | 2 | 1.3
2 | 100 000 | 50 | 5 | 2 | 2 | 1.3
3 | 100 | 5 | 9 | 2 | 4 | 2.9
3 | 1 000 | 5 | 9 | 2 | 4 | 2.9
3 | 100 000 | 50 | 10 | 2 | 4 | 3.1
3 | 1 000 000 | 5 000 | 9 | 2 | 4 | 3.0

###  5.2 Elevator

A classic example for reactive synthesis is a controller for an elevator. We
include two variants: the first naive one has no inputs and needs to visit all
floors infinitely often, the second version contains an input signal where a
user can tell the elevator where it should go.

#### Naive Elevator

The single state variable $floor$ represents the current position of the
elevator. It can start anywhere between the first floor and the maximum floor
and is not allowed to leave this interval. The controller has three options:
move elevator up or down or stay at the same position. Every floor has to be
visited infinitely often. This can be expressed as the TSL(LIA) formula

$\displaystyle(floor\geq 1\land floor\leq
max)\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}($
$\displaystyle([floor\leftarrow floor]\lor[floor\leftarrow
floor-1]\lor[floor\leftarrow floor+1])\land$ $\displaystyle floor\geq 1\land
floor\leq max\land\bigwedge_{k}^{max}\operatorname{\mathbf{F}}floor=k)$

We varied the number of floors of the building to show how our algorithm
scales with more complex specifications. No new predicates are learned as a
sufficient number of predicates is already included in the specification
(equality tests for every floor are part of the liveness properties).

# floors | # refinements | # states | time [s]
---|---|---|---
3 | 13 | 2 | 3.1
4 | 11 | 3 | 3.7
5 | 15 | 4 | 8.2
8 | 21 | 4 | 45
10 | 24 | 4 | 185

#### Elevator with an input signal

The state consists of two variables: the current $floor$, and the $target$ we
want to reach. There is one input variable $signal$ used by the environment to
request the next target. We assume the floors are numbered $1$ to $max$ and
the number $0$ denotes an undefined value. As in the naive elevator example
the elevator can move up or down or stay at the same level. It must stay
between the minimum and the maximum floor. If there is currently no target the
$signal$ can be any valid floor and this will be stored as the new $target$.
Whenever a new target is selected the elevator has to eventually reach it, at
that point $target$ is reset to zero.

$\displaystyle(floor\geq 1\land floor\leq max\land target=0\land$
$\displaystyle\operatorname{\mathbf{G}}(signal\geq 0\land signal\leq
max\land(target\neq 0\rightarrow
signal=0)))\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}($
$\displaystyle([floor\leftarrow floor]\lor[floor\leftarrow
floor-1]\lor[floor\leftarrow floor+1])\land$ $\displaystyle((signal\neq 0\land
floor\neq target)\rightarrow[target\leftarrow signal])\land$
$\displaystyle((signal=0\land floor\neq target)\rightarrow[target\leftarrow
target])\land$ $\displaystyle(floor=target\rightarrow[target\leftarrow
0])\land$ $\displaystyle floor\geq 1\land floor\leq
max\land\bigwedge_{k}^{max}(target=k\rightarrow\operatorname{\mathbf{F}}floor=k))$

# floors | # refinements | # states | time [min]
---|---|---|---
3 | 5 | 1 | 0:35
4 | 5 | 1 | 3:37
5 | 6 | 1 | 23:44

The specification above explicitly enumerates all floors and contains a
liveness guarantee for each of them. Instead one could only require that
$target$ is reset infinitely often. This makes the problem significantly
harder: 59min and 14 refinements for only three floors.

###  5.3 Sorting

TSL(LIA) can be used to specify a sorting algorithm for a finite number of
elements. Every element is represented by its own variable, which are
initialized by the environment to arbitrary integers. The system is allowed to
exchange two adjacent number or leave everything unchanged. It has to
guarantee that eventually the numbers are sorted and stay that way. The TSL(T)
formula for three variables is:

$\displaystyle\operatorname{\mathbf{F}}\operatorname{\mathbf{G}}(a\geq b\land
b\geq c)\land\operatorname{\mathbf{G}}($ $\displaystyle([a\leftarrow
b]\land[b\leftarrow a]\land[c\leftarrow c])\lor$ $\displaystyle([a\leftarrow
a]\land[b\leftarrow c]\land[c\leftarrow b])\lor$ $\displaystyle([a\leftarrow
a]\land[b\leftarrow b]\land[c\leftarrow c]))$

This problem turns out to be very hard, while a system for three numbers can
be build in less than 4s, four numbers took almost 20min and five numbers
timed out after 13h.

# variables | # refinements | # states | time
---|---|---|---
3 | 6 | 2 | 3.7 s
4 | 12 | 3 | 18:46 min
5 |  $>$10 | - | timeout ($>$13 h)

###  5.4 Water Tanks

The previous examples all used linear integer arithmetic. We can also use
other SMT theories like linear real arithmetic (LRA). Using reals allows us to
model linear cyber physical systems.

Belta et al. [1] chapter 9 describes a system of two coupled water tanks with
linear dynamics; one water tank drains ($x2$) and the other one ($x1$) is
refilled by the controller. The original input domain (refill tank x1) is
$i\in[0,0.0005]$. The input choice is discretized with two values ($0$ and
$0.0003$) and represented as different updates. We created two variants of the
system.

The first one is a safety specification where the water level of both tanks
has to be kept between $0.1$ and $0.7$.

⬇

$(0.2\leq x1\land x1<0.7\land 0.1\leq x2\land x2<0.7)$

$\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}($

$0.1\leq x1\land x1<0.7\land 0.1\leq x2\land x2<0.7\land$

$((x1<0.2\land x2<0.2)\rightarrow$

$(([x1\leftarrow x1+0.0*324.6753]\lor[x1\leftarrow x1+0.0003*324.6753])\land$

$[x2\leftarrow 0.9635*x2]))\land$

$((x1\geq 0.2\lor x2\geq 0.2)\rightarrow$

$(([x1\leftarrow 0.8281*x1+0.1719*x2+0.0*324.6753]\lor$

$\\!\\![x1\leftarrow 0.8281*x1+0.1719*x2+0.0003*324.6753])\land$

$[x2\leftarrow 0.7916*x2+0.1719*x1]))$

$)$

Synthesis of this system took 31 seconds and 4 refinements. It results in a
system with a single state.

A specification with two tanks and a liveness property is currently out of
reach for our tool. Instead we created a second specification with a single
tank and a liveness property. Whenever the water level falls below $0.1$ it
has to eventually exceed $0.4$.

$\displaystyle 0.0\leq x\land
x<0.7\boldsymbol{\rightarrow}\operatorname{\mathbf{G}}($
$\displaystyle([x\leftarrow 0.9635*x]\lor[x\leftarrow 0.9635*x+0.1])\land$
$\displaystyle(x<0.1\rightarrow\operatorname{\mathbf{F}}(x>0.4)))$

A system realizing that specification can be synthesized using 18 refinements
in 95 seconds, it consists of 2 states.

##  6 Conclusion

We presented a synthesis procedure for temporal stream logic modulo theories.
Our algorithm is based on a CEGAR [3] loop and translation to propositional
LTL synthesis. The synthesis problem for TSL modulo theories in general is
undecidable. However, we can synthesize systems or prove unrealizability in
many cases. Huge state spaces can be handled by using a symbolic
representation during synthesis. Some specifications require a system with
predicates that are not part of the original specification, in many cases we
are able to automatically find these.

## References

  * [1] Belta, C., Yordanov, B., Gol, E.A.: Formal Methods for Discrete-Time Dynamical Systems. Springer (2017)
  * [2] Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 921–962. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_27, https://doi.org/10.1007/978-3-319-10575-8_27
  * [3] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1855, pp. 154–169. Springer (2000). https://doi.org/10.1007/10722167_15
  * [4] De Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3_24
  * [5] Ehlers, R., Seshia, S.A., Kress-Gazit, H.: Synthesis with identifiers. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8318, pp. 415–433. Springer (2014). https://doi.org/10.1007/978-3-642-54013-4_23
  * [6] Exibard, L., Filiot, E., Khalimov, A.: Church synthesis on register automata over linearly ordered data domains. In: 38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, March 16-19, 2021, Saarbrücken, Germany (Virtual Conference). LIPIcs, vol. 187, pp. 28:1–28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.STACS.2021.28
  * [7] Faran, R., Kupferman, O.: On synthesis of specifications with arithmetic. In: Chatzigeorgiou, A., Dondi, R., Herodotou, H., Kapoutsis, C.A., Manolopoulos, Y., Papadopoulos, G.A., Sikora, F. (eds.) SOFSEM 2020: Theory and Practice of Computer Science - 46th International Conference on Current Trends in Theory and Practice of Informatics, SOFSEM 2020, Limassol, Cyprus, January 20-24, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12011, pp. 161–173. Springer (2020). https://doi.org/10.1007/978-3-030-38919-2_14
  * [8] Finkbeiner, B., Heim, P., Passing, N.: Temporal stream logic modulo theories. arXiv (2021), https://arxiv.org/abs/2104.14988
  * [9] Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Temporal stream logic: Synthesis beyond the bools. In: Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 609–629. Springer (2019)
  * [10] Khalimov, A., Maderbacher, B., Bloem, R.: Bounded synthesis of register transducers. In: Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 494–510. Springer (2018). https://doi.org/10.1007/978-3-030-01090-4_29
  * [11] Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 578–586. Springer (2018). https://doi.org/10.1007/978-3-319-96145-3_31
  * [12] Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall Englewood Cliffs (1967)
  * [13] Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4762, pp. 474–488. Springer (2007). https://doi.org/10.1007/978-3-540-75596-8_33


$\displaystyle\gamma_{U}^{\mathrm{read}}=$
$\displaystyle(a-xb)\frac{\zeta_{C}^{2}\lambda^{2}\sin^{2}(\phi)+\lambda^{2}\cos^{2}(\phi)+1}{\left(\zeta_{A}^{2}+\lambda^{2}\sin^{2}(\phi)\right)\left(\zeta_{C}^{2}\lambda^{2}\sin^{2}(\phi)+1\right)+\lambda^{2}\cos^{2}(\phi)\left(\zeta_{A}^{2}+2\zeta_{C}^{2}\lambda^{2}\sin^{2}(\phi)+\zeta_{C}^{2}\right)+\zeta_{C}^{2}\lambda^{4}\cos^{4}(\phi)},$
(44) $\displaystyle\tilde{\gamma}_{U}^{\mathrm{read}}$
$\displaystyle=\frac{b}{\sqrt{1+\lambda^{2}(\zeta^{2}_{C}\sin^{2}(\phi)+\cos^{2}(\phi))}},$
$\displaystyle x=$
$\displaystyle\frac{\lambda^{2}\sin(\phi)\cos(\phi)(1-\zeta_{C}^{2})}{1+\lambda^{2}(\zeta^{2}_{C}\sin^{2}(\phi)+\cos^{2}(\phi))}$

The parity being projected by the measurement is thus

$p_{U}=i\gamma_{U}^{\mathrm{read}}\tilde{\gamma}_{U}^{\mathrm{read}}.$ (45)

We note that for the case of perfect PMMs, $\zeta_{A}=\zeta_{C}=0$, one gets
$\gamma_{U}^{\mathrm{read}}\propto-\lambda\sin(\phi)\cos(\phi)\gamma_{A}+\sin(\phi)\gamma_{C}$
and
$\tilde{\gamma}_{U}^{\mathrm{read}}\propto\gamma_{A}+\lambda\cos(\phi)\gamma_{C}$.
This means that
$i\gamma_{U}^{\mathrm{read}}\tilde{\gamma}_{U}^{\mathrm{read}}\propto
i\gamma_{A}\gamma_{C}$ as expected, independent of $\lambda$ and $\phi$.

When performing the calculations of the results of the braiding protocol, we
define the fermion operators, $d_{s}=(\gamma_{s}+i\tilde{\gamma}_{s})/2$ with
$s=A,B,C$. These operators then act on the Fock basis states
$|n_{A}n_{C}n_{B}\rangle$, which allows us to write the matrices for the
various projectors.


$\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon}^{r,g_{6}})\leq\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})-\frac{\sigma\mathcal{H}^{n}(A_{l})}{2(2^{n}-1)}+\@slowromancap
iii@_{\varepsilon}^{2,\rho}+\@slowromancap iii@_{\varepsilon}^{8,r}.$

For $r$ in $[0,\rho]$, we define the following function on $N$,

$\tilde{v}_{\varepsilon}^{r,g_{6}}(y)=\begin{cases}\overline{\mathbb{H}}_{\varepsilon}(\tilde{d}(y)+r),&y\not\in
B_{\delta}^{N}(z_{0}),\\\
v_{\varepsilon}^{r,g_{6}}(F_{1}^{-1}(y)),&y\in\overline{\Upsilon_{1}}\cap
B_{\delta}^{N}(z_{0}),\\\
v_{\varepsilon}^{r,g_{6}}(F_{2}^{-1}(y)),&y\in\overline{\Upsilon_{2}}\cap
B_{\delta}^{N}(z_{0}).\end{cases}$

We can show, as in Section 5.2 and 5.3 that,
$\tilde{v}_{\varepsilon}^{r,g_{6}}$ lies in $W^{1,\infty}(N)$,
$\mathcal{F}_{\varepsilon,\lambda}(\tilde{v}_{\varepsilon}^{r,g_{6}})(N)=\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon}^{r,g_{6}})(\tilde{T})$,
and the path $r\mapsto\tilde{v}_{\varepsilon}^{r,g_{6}}$ is continuous in
$W^{1,2}(N)$.

###  7.2 Completing Path to $b_{\varepsilon}$

We construct the path from (6) to ’+1’ in Figure 2. This is done in an
identical way to Section 6.4.

For $r$ in $[\rho,2\,\text{diam}(N)]$, we define the following function on
$N$,

$\tilde{v}_{\varepsilon}^{r,g_{7}}(y)\coloneqq\overline{\mathbb{H}}_{\varepsilon}(\tilde{d}(y)+r).$

Similar to arguments in Section 6.4 we have,

$\mathcal{F}_{\varepsilon,\lambda}(\tilde{v}_{\varepsilon}^{r,g_{7}})\leq\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})-\frac{\sigma\mathcal{H}^{n}(A_{l})}{2(2^{n}-1)}+\@slowromancap
iii@_{\varepsilon}^{2,\rho}+\@slowromancap
iii@_{\varepsilon}^{8,\rho}+\@slowromancap iii@_{\varepsilon}^{9,r},$

where,

$\@slowromancap
iii@_{\varepsilon}^{9,r}=\lambda\int_{\rho}^{r}\Theta_{\varepsilon,g_{6}}^{1}(s,x)-\Theta_{\varepsilon,g_{6}}^{2}(s,x)\,d\mathcal{H}^{n}(x)\,ds.$

Again as in Section 6.4, we connect
$\tilde{v}_{\varepsilon}^{2\,\text{diam}(N),g_{7}}=1$, to $b_{\varepsilon}$,
by constant functions, $u_{\varepsilon}^{r}=r$, for $r$ in
$[1,b_{\varepsilon}]$. We have that for all $r$ in $[1,b_{\varepsilon}]$,

$\mathcal{F}_{\varepsilon,\lambda}(u_{\varepsilon}^{r})\leq\mathcal{F}_{\varepsilon,\lambda}(\tilde{v}_{\varepsilon}^{2\,\text{diam}(N),g_{7}})\leq\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})-\frac{\sigma\mathcal{H}^{n}(A_{l})}{2(2^{n}-1)}+\@slowromancap
iii@_{\varepsilon}^{2,\rho}+\@slowromancap
iii@_{\varepsilon}^{8,\rho}+\@slowromancap
iii@_{\varepsilon}^{9,2\,\text{diam}(N)}.$

Both $\tilde{v}_{\varepsilon}^{r,g_{7}}$, and $u_{\varepsilon}^{r}$ give
continuous paths in $W^{1,2}(N)$ with respect to $r$.

##  8 Conclusion of the Paths

###  8.1 Error Terms

####  8.1.1 Theta Error Terms

Consider a function $g\colon\mathbb{R}\times\tilde{M}\rightarrow\mathbb{R}$,
and the term

$\displaystyle\Theta_{\varepsilon,g}^{1}(s,x)-\Theta_{\varepsilon,g}^{2}(s,x)$
$\displaystyle=$
$\displaystyle\sigma\int_{\sigma^{-}(x)}^{\sigma^{+}(x)}\partial_{s}g(s,x)(\overline{\mathbb{H}}_{\varepsilon})^{\prime}(t-g(s,x))\theta_{t}(x)\,dt$
$\displaystyle\hskip
28.45274pt-\int_{\sigma^{-}(x)}^{\sigma^{+}(x)}\partial_{s}g(s,x)Q_{\varepsilon}(t-g(s,x))\theta_{t}(x)\,dt.$

Assuming that $g$ is monotone in the first variable, we have,

$\displaystyle|\Theta_{\varepsilon,g}^{1}(s,x)-\Theta_{\varepsilon,g}^{2}(s,x)|\leq
2\sigma|\partial_{s}g(s,x)|m_{\varepsilon}(g(s,x),x)+C_{7}\varepsilon^{2}.$

where,

$m_{\varepsilon}(T,x)=\max_{t\in[T-2\varepsilon\Lambda,T+2\varepsilon\Lambda]}\theta_{t}(x)-\min_{t\in[T-2\varepsilon\Lambda,T+2\varepsilon\Lambda]}\theta_{t}(x).$

and $C_{7}=C_{7}(N,m,\lambda,W,|g|_{C^{1}})<+\infty$.

Now we assume that $\partial_{s}g\geq 0$, and
$|\partial_{s}g|_{C^{0}(\mathbb{R}\times\tilde{M})}<+\infty$. Apply Fubini’s
Theorem to swap integrals,

$\displaystyle\int_{0}^{r}\int_{\tilde{M}}\left|\Theta_{\varepsilon,g}^{1}(s,x)-\Theta_{\varepsilon,g}^{2}(s,x)\right|\,d\mathcal{H}^{n}(x)\,ds\leq
2\sigma\int_{\tilde{M}}\int_{g(0,x)}^{g(r,x)}m_{\varepsilon}(T,x)\,dT\,\mathcal{H}^{n}(x)+C_{7}r\varepsilon^{2}.$

Fixing $x$ in $\tilde{M}$, we see that for all $T$ in
$\mathbb{R}\setminus\\{\sigma^{-}(x),\sigma^{+}(x)\\}$,

$m_{\varepsilon}(T,x)\rightarrow 0,\,as\,\varepsilon\rightarrow 0,$

and furthermore, we have the following bounds, $0\leq m_{\varepsilon}(T,x)\leq
e^{\frac{\lambda^{2}}{2m}}$. Therefore, we can apply Dominated Convergence
Theorem for fixed $x$ in $\tilde{M}$ and $r$ in $[0,\infty)$,

$\int_{g(0,x)}^{g(r,x)}m_{\varepsilon}(T,x)\,dT\rightarrow
0,\,as\,\varepsilon\rightarrow 0.$

Furthermore, as $0\leq
g(r,x)-g(0,x)\leq|\partial_{s}g|_{C^{0}(\mathbb{R}\times\tilde{M})}\,r$, we
have the bounds,

$0\leq\int_{g(0,x)}^{g(r,x)}m_{\varepsilon}(T,x)\,dT\leq|\partial_{s}g|_{C^{0}(\mathbb{R}\times\tilde{M})}re^{\frac{\lambda^{2}}{2m}}.$

Therefore, again by Dominated Convergence Theorem, we have, for fixed $r$ in
$[0,\infty)$

$\int_{\tilde{M}}\int_{g(0,x)}^{g(r,x)}m_{\varepsilon}(T,x)\,dT\,\mathcal{H}^{n}(x)\rightarrow
0,\,as\,\varepsilon\rightarrow 0.$

Define the following continuous function on $[0,+\infty)$,

$M_{\varepsilon}^{g}(r)=\int_{\tilde{M}}\int_{g(0,x)}^{g(r,x)}m_{\varepsilon}(T,x)\,dT\,\mathcal{H}^{n}(x).$

We have that $M_{\varepsilon}^{g}(r)\rightarrow 0$, pointwise, as
$\varepsilon\rightarrow 0$, and furthermore, as

$0\leq m_{\varepsilon_{1}}(T,x)\leq m_{\varepsilon_{2}}(T,x),$

for all $T$ in $\mathbb{R}$, $x$ in $\tilde{M}$, and
$0<\varepsilon_{1}<\varepsilon_{2}$, this implies that,

$0\leq M_{\varepsilon_{1}}^{g}(r)\leq M_{\varepsilon_{2}}^{g}(r),$

for all $r$ in $[0,+\infty)$. Therefore, by Dini’s Theorem, we have that,

$M_{\varepsilon}^{g}\rightarrow 0,\,as\,\varepsilon\rightarrow 0,$

uniformly on compact sets of $[0,+\infty)$. Thus,

$\int_{0}^{r}\int_{\tilde{M}}\left|\Theta_{\varepsilon,g}^{1}(s,x)-\Theta_{\varepsilon,g}^{2}(s,x)\right|\,d\mathcal{H}^{n}(x)\,ds\rightarrow
0$ (14)

as $\varepsilon\rightarrow 0$, uniformly in $r$, on compact sets of
$[0,+\infty)$. The same holds assuming that $g$ satisfies $\partial_{s}g\leq
0$, on $\mathbb{R}\times\tilde{M}$, and
$|\partial_{s}g|_{C^{0}(\mathbb{R}\times\tilde{M})}<+\infty$.

For $i=1,\ldots,7$ our $g_{i}$’s are monotone in the first variable and
$|\partial_{s}g_{i}|_{C^{0}(\mathbb{R}\times\tilde{M})}<+\infty$. Therefore,
(14) holds for each $i$.

####  8.1.2 The Other Error Terms

We first consider,

$\int_{B_{2l}}q_{\varepsilon}^{1}(x)\,d\mathcal{H}^{n}(x),$

with,

$q_{\varepsilon}^{1}(x)=\max_{t\in[-4\varepsilon\Lambda,2\varepsilon\Lambda]}(H_{t}(x)-\lambda)\theta_{t}(x).$

By choice of $\varepsilon>0$, in Remark 15, $2\varepsilon\Lambda<<\rho$.
Therefore, by choice of $\rho>0$, in Remark 11, and $\delta>0$, from Remark
16, we have

$0\leq\max_{x\in
B_{2l}}q_{\varepsilon}^{1}(x)\leq\frac{\lambda}{2}e^{\frac{\lambda^{2}}{2m}}.$

Fixing $x^{\prime}$ in $B_{2l}\setminus\\{x\colon\sigma^{-}(x)=0\\}$, we see
that there exists an
$\varepsilon^{\prime}=\varepsilon^{\prime}(x^{\prime})>0$, such that for all
$0<\varepsilon\leq\varepsilon^{\prime}$,

$[-4\varepsilon\Lambda,2\varepsilon\Lambda]\subset(\sigma^{-}(x^{\prime}),\sigma^{+}(x^{\prime})).$

Therefore, $(H_{t}(x^{\prime})-\lambda)\theta_{t}(x^{\prime})$, is a smooth
function in $t$ on $[-4\varepsilon\Lambda,2\varepsilon\Lambda]$, and clearly,

$\max_{t\in[-4\varepsilon\Lambda,2\varepsilon\Lambda]}(H_{t}(x^{\prime})-\lambda)\theta_{t}(x^{\prime})\rightarrow
0,\,as\,\varepsilon\rightarrow 0.$

Thus, $q_{\varepsilon}^{1}\rightarrow 0$, $\mathcal{H}^{n}$–a.e in $B_{2l}$,
and we can apply Dominated Convergence Theorem to say that

$\int_{B_{2l}}q_{\varepsilon}^{1}(x)\,d\mathcal{H}^{n}(x)\rightarrow
0,\,as\,\varepsilon\rightarrow 0.$

Identically we also have,

$\int_{A_{L}^{k}}q_{\varepsilon}^{2}(x)\,d\mathcal{H}^{n}(x)\rightarrow
0,\,as\,\varepsilon\rightarrow 0,$

recalling
$q_{\varepsilon}^{2}(x)=\max_{t\in[-2\varepsilon\Lambda,4\varepsilon\Lambda]}(\lambda-
H_{t}(x))\theta_{t}(x)$.

Now considering

$q_{\varepsilon}^{3}(r,x)=\max_{t\in[-2\varepsilon\Lambda,2\varepsilon\Lambda]}\zeta(x,t+g_{4}(r,x))-\zeta(x,g_{4}(r,x))$

where we are recalling the function

$\zeta(x,t)=|\nabla\tilde{f}(x)|_{(x,t)}^{2}\theta_{t}(x)$

from Claim 4. For $x$ in $B_{2L}$ such that $\tilde{f}(x)=0$, we have that
$\zeta(x,t)=0$, for all $t$. Considering $x$ in
$A_{L}^{k}\cap\\{\tilde{f}\not=0\\}$, such that
$r_{0}\tilde{f}(x)>2\varepsilon\Lambda$, then

$[-2\varepsilon\Lambda+g_{4}(r,x),2\varepsilon\Lambda+g_{4}(r,x)]\subset(0,2r_{0})\subset(\sigma^{-}(x),\sigma^{+}(x)).$

Thus, for $t$ in
$[-2\varepsilon\Lambda+g_{4}(r,x),2\varepsilon\Lambda+g_{4}(r,x)]$,

$(x,t)\in\tilde{T}\cap(B_{L}\times(-2r_{0},2r_{0}))\subset\subset\tilde{V}_{1}\cup\tilde{V}_{2},$

where we are recalling sets $\tilde{V}_{1}$ and $\tilde{V}_{2}$ from Remark 6.
Therefore, $\zeta$ is differentiable at $(x,t)$ and

$|\partial_{t}\zeta(x,t)|\leq
C(|F_{i}|_{C^{2}(B_{L}\times(-2r_{0},2r_{0}))},|\tilde{f}|_{C^{1}},\lambda)\leq
C_{6}.$

Where we are potentially rechoosing
$C_{6}=C_{6}(z_{0},M,N,g,k,L,\delta,W,\lambda)$. Therefore, for $x$ in
$A_{L}^{k}$ such that $r_{0}\tilde{f}(x)>2\varepsilon\Lambda$, we have that
$0\leq q_{\varepsilon}^{3}(r,x)\leq C_{6}\varepsilon\Lambda$. Furthermore, for
all $x$ in $A_{L}^{k}$,

$|q_{\varepsilon}^{3}(r,x)|\leq\max_{(x,t)\in
B_{L}\times(-2r_{0},2r_{0})}\zeta(x,t)\leq C_{6}.$

Again we are potentially rechoosing
$C_{6}=C_{6}(z_{0},M,N,g,k,L,\delta,W,\lambda)$.

Therefore,

$\displaystyle p_{\varepsilon}^{1}(r)$ $\displaystyle=$
$\displaystyle\int_{A_{L}^{k}\cap\\{r_{0}\tilde{f}>2\varepsilon\Lambda\\}}q_{\varepsilon}^{3}(r,x)\,d\mathcal{H}^{n}(x)+\int_{A_{L}^{k}\cap\\{0<r_{0}\tilde{f}\leq
2\varepsilon\Lambda\\}}q_{\varepsilon}^{3}(r,x)\,d\mathcal{H}^{n}(x),$
$\displaystyle\leq$ $\displaystyle
C_{6}\left(\varepsilon\Lambda+\mathcal{H}^{n}(\\{x\in A_{L}^{k}\colon
0<r_{0}\tilde{f}(x)\leq 2\varepsilon\Lambda\\})\right).$

Thus,

$\max_{r\in[0,r_{0}]}p_{\varepsilon}^{1}(r)\rightarrow 0$

as $\varepsilon\rightarrow 0$. Similarly, $p_{\varepsilon}^{2}(0)\rightarrow
0$, as $\varepsilon\rightarrow 0$.

For the remaining error terms, as
$\mathcal{H}^{n}(\\{x\in\tilde{M}\colon\,\sigma^{-}(x)=0\\})=0$, by Dominated
Convergence Theorem, we have that,

$\mathcal{H}^{n}(\\{x\in\tilde{M}\colon\,\sigma^{-}(x)\geq-2\varepsilon\Lambda\\})\rightarrow
0,$

and

$\int_{\tilde{M}}m_{\varepsilon}^{i}(x)\,d\mathcal{H}^{n}(x)\rightarrow 0,$

where,

$\displaystyle m_{\varepsilon}^{1}(x)$ $\displaystyle=$
$\displaystyle\max_{t\in[-2\varepsilon\Lambda,4\varepsilon\Lambda]}\theta_{t}(x)-\min_{t\in[-2\varepsilon\Lambda,4\varepsilon\Lambda]}\theta_{t}(x),$
$\displaystyle m_{\varepsilon}^{2}(x)$ $\displaystyle=$
$\displaystyle\max_{t\in[-6\varepsilon\Lambda,2\varepsilon\Lambda]}\theta_{t}(x)-\min_{t\in[-6\varepsilon\Lambda,2\varepsilon\Lambda]}\theta_{t}(x).$

###  8.2 Path for Theorem 2

Consider the following continuous path in $W^{1,2}(N)$, for $\varepsilon>0$,

$\gamma_{\varepsilon}(t)=\begin{cases}-1-2\text{diam}\,(N)-t,&t\in[-2\,\text{diam}\,(N)-a_{\varepsilon}-1,2\,\text{diam}\,(N)],\\\
\overline{\mathbb{H}}_{\varepsilon}(\tilde{d}-t),&t\in[-2\,\text{diam}\,(N),2\,\text{diam}\,(N)],\\\
1-2\,\text{diam}\,(N)+t,&t\in[2\,\text{diam}\,(N),2\,\text{diam}\,(N)+b_{\varepsilon}-1].\end{cases}$

which satisfies
$\gamma_{\varepsilon}(-1-2\text{diam}\,(N)-a_{\varepsilon})=a_{\varepsilon}$,
and
$\gamma_{\varepsilon}(1-2\,\text{diam}\,(N)+b_{\varepsilon})=b_{\varepsilon}$.

Replacing $r_{0}=2\varepsilon\Lambda$, in Section 6.4, and
$\rho=2\varepsilon\Lambda$, in Section 7.2, we see that, for all $\varepsilon$
in $(0,\tilde{\varepsilon})$, for some
$\tilde{\varepsilon}=\tilde{\varepsilon}(N,M,g,\lambda,W)>0$, fixed,

$\begin{cases}\mathcal{F}_{\varepsilon,\lambda}(\gamma_{\varepsilon}(t))<\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})+\@slowromancap
iii@_{\varepsilon}^{6,2\,\text{diam}\,(N)},&t\in[-2\,\text{diam}\,(N)-a_{\varepsilon}-1,2\,\text{diam}\,(N)],\\\
\mathcal{F}_{\varepsilon,\lambda}(\gamma_{\varepsilon}(t))<\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})+\@slowromancap
iii@_{\varepsilon}^{6,-t},&t\in[-2\text{diam}\,(N),-2\varepsilon\Lambda],\\\
\mathcal{F}_{\varepsilon,\lambda}(\gamma_{\varepsilon}(t))<\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})+\@slowromancap
iii@_{\varepsilon}^{9,t},&t\in[2\varepsilon\Lambda,2\text{diam}\,(N)],\\\
\mathcal{F}_{\varepsilon,\lambda}(\gamma_{\varepsilon}(t))<\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})+\@slowromancap
iii@_{\varepsilon}^{9,2\,\text{diam}\,(N)},&t\in[2\,\text{diam}\,(N),2\,\text{diam}\,(N)+b_{\varepsilon}-1].\end{cases}$

Recalling from Section 3.6

$\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})\rightarrow
2\sigma\mathcal{H}^{n}(M)-\sigma\lambda\mu_{g}(E)+\sigma\lambda\mu_{g}(N\setminus
E),$

as $\varepsilon\rightarrow 0$, and Section 8.1.1,

$\max_{t\in[2\varepsilon\Lambda,2\,\text{diam}\,(N)]}\left(\@slowromancap
iii@_{\varepsilon}^{6,t}+\@slowromancap iii@^{9,t}\right)\rightarrow 0,$

as $\varepsilon\rightarrow 0$. Therefore, for $\tau>0$, there exists a
$0<\varepsilon_{\tau}=\varepsilon_{\tau}(N,M,g,\lambda,W)\leq\tilde{\varepsilon}$,
such that for all $\varepsilon$ in $(0,\varepsilon_{\tau})$ and $t$ in
$[-2\,\text{diam}\,(N)-a_{\varepsilon}-1,2\,\text{diam}\,(N)+b_{\varepsilon}-1]\setminus(-2\varepsilon\Lambda,2\varepsilon\Lambda)$,

$\mathcal{F}_{\varepsilon,\lambda}(\gamma_{\varepsilon}(t))<2\sigma\mathcal{H}^{n}(M)-\sigma\lambda\mu_{g}(E)+\sigma\lambda\mu_{g}(N\setminus
E)+\tau.$

Furthermore, by similar arguments to those in Section 3.6, and after
potentially rechoosing $\varepsilon_{\tau}>0$, we have that for all
$\varepsilon$ in $(0,\varepsilon_{\tau})$

$\max_{t\in[-2\varepsilon\Lambda,2\varepsilon\Lambda]}\mathcal{F}_{\varepsilon,\lambda}(\gamma_{\varepsilon}(t))<2\sigma\mathcal{H}^{n}(M)-\sigma\lambda\mu_{g}(E)+\sigma\lambda\mu_{g}(N\setminus
E)+\tau.$

Therefore, this is an admissible path in $W^{1,2}(N)$, that proves that for
the limiting varifold $V=V_{\lambda}+V_{0}$, we must have that $V_{0}=0$. This
completes the proof of Theorem 2.

######  Remark 25.

Note that we can build the path $\gamma_{\varepsilon}$, for any suitable
Caccioppoli set $E$. The suitable properties are the following:

  1. 1.

$\partial^{*}E\not=\emptyset$, has a quasi embedded $\lambda$-CMC structure,
with respect to unit normal pointing into $E$.

  2. 2.

$\partial^{*}E$ satisfies the Geodesic Touching Lemma (Lemma 1).

From Remark 25 we can deduce that $E$ must be a single, connected component
and minimises the value

$F_{\lambda}(E)=\mathcal{H}^{n}(\partial^{*}E)-\lambda\mu_{g}(E)>0,$

among all suitable competitors.

###  8.3 Contradiction Path for Theorem 1

Recall all the error terms from Sections 5, 6 and 7. By Section 3.6 and 8.1,
for $\tau>0$, there exists an
$\varepsilon_{\tau}=\varepsilon(z_{0},M,N,g,\delta,W,\lambda,L,k,r_{0},\rho,\tau)\in(0,\varepsilon_{3})$,
such that for all $\varepsilon$ in $(0,\varepsilon_{\tau})$, we have that

$\displaystyle\mathcal{F}_{\varepsilon,\lambda}(v_{\varepsilon})+\max_{r\in[0,4\varepsilon\Lambda)}\@slowromancap
iii@_{\varepsilon}^{1,r}+\max_{r\in[4\varepsilon\Lambda,\rho]}\@slowromancap
iii@_{\varepsilon}^{2,r}+\max_{r\in[0,2\varepsilon\Lambda]}\@slowromancap
iii@_{\varepsilon}^{3,r}$ $\displaystyle\hskip
28.45274pt+\max_{r\in(2\varepsilon\Lambda,r_{0}]}\@slowromancap
iii@_{\varepsilon}^{4,r}+\max_{r\in[0,r_{0}]}\@slowromancap
iii@_{\varepsilon}^{5,r}+\max_{r\in[r_{0},2\,\text{diam}\,(N)]}\@slowromancap
iii@_{\varepsilon}^{6,r}$ $\displaystyle\hskip
56.9055pt+\max_{r\in[0,2\varepsilon\Lambda]}\@slowromancap
iii@_{\varepsilon}^{7,r}+\max_{r\in(2\varepsilon\Lambda,\rho]}\@slowromancap
iii@_{\varepsilon}^{8,r}+\max_{r\in[\rho,2\,\text{diam}\,(N)]}\@slowromancap
iii@_{\varepsilon}^{9,r}$ $\displaystyle\hskip
85.35826pt<2\sigma\mathcal{H}^{n}(M)-\sigma\lambda\mu_{g}(E)+\sigma\lambda\mu_{g}(N\setminus
E)+\tau.$

Therefore, for any $\tau>0$, there exists an $\varepsilon_{\tau}>0$, such that
for any $\varepsilon$ in $(0,\varepsilon_{\tau})$, we can define the
continuous path,

$\gamma_{\varepsilon}\colon[-1-a_{\varepsilon},4\,\text{diam}\,(N)+r_{0}+\rho+b_{\varepsilon}-1]\rightarrow
W^{1,2}(N),$

by

$\gamma_{\varepsilon}(t)=\begin{cases}-1-t,&t\in[-1-a_{\varepsilon},0],\\\
\overline{\mathbb{H}}_{\varepsilon}(\tilde{d}+t-2\,\text{diam}\,(N)),&[0,2\,\text{diam}\,(N)-r_{0}],\\\
\tilde{v}_{\varepsilon}^{2\,\text{diam}\,(N)-t,g_{4}},&[2\,\text{diam}\,(N)-r_{0},2\,\text{diam}\,(N)],\\\
\tilde{v}_{\varepsilon}^{2\,\text{diam}\,(N)+\rho-t,g_{3}},&[2\,\text{diam}\,(N),2\,\text{diam}\,(N)+\rho],\\\
\tilde{v}_{\varepsilon}^{2\,\text{diam}\,(N)+\rho+r_{0}-t,g_{2}},&[2\,\text{diam}\,(N)+\rho,2\,\text{diam}\,(N)+\rho+r_{0}],\\\
\tilde{v}_{\varepsilon}^{t-(2\,\text{diam}\,(N)+\rho+r_{0}),g_{6}},&[2\,\text{diam}\,(N)+\rho+r_{0},2\,\text{diam}\,(N)+2\rho+r_{0}],\\\
\overline{\mathbb{H}}_{\varepsilon}(\tilde{d}+t-(2\,\text{diam}\,(N)+\rho+r_{0})),&[2\,\text{diam}\,(N)+2\rho+r_{0},4\,\text{diam}\,(N)+\rho+r_{0}],\\\
1+t-(4\,\text{diam}\,(N)+\rho+r_{0}),&[4\,\text{diam}\,(N)+\rho+r_{0},4\,\text{diam}\,(N)+\rho+r_{0}+b_{\varepsilon}-1]\end{cases}$

This path satisfies the following;
$\gamma_{\varepsilon}(-1-a_{\varepsilon})=a_{\varepsilon}$,
$\gamma_{\varepsilon}(4\,\text{diam}\,(N)+r_{0}+\rho+b_{\varepsilon}-1)=b_{\varepsilon}$,
and

$\gamma_{\varepsilon}(t)<2\sigma\mathcal{H}^{n}(M)-\sigma\lambda\mu_{g}(E)+\sigma\lambda\mu_{g}(N\setminus
E)-\frac{\sigma\mathcal{H}^{n}(A_{l})}{2(2^{n}-1)}+\tau,$

for all $t$ in
$[-1-a_{\varepsilon},4\,\text{diam}\,(N)+r_{0}+\rho+b_{\varepsilon}-1]$. This
contradicts the min-max construction of $M$, implying that $M$ must be
embedded, and therefore completing Theorem 1.

##  9 Morse Index

Recall the functional defined on Caccioppoli sets $\Omega\subset N$,

$F_{\lambda}(\Omega)=\mathcal{H}^{n}(\partial^{*}\Omega)-\lambda\mu_{g}(\Omega).$

For a $C^{2}$ vector field $X$, we may take variations in direction $X$ by
considering its flow $\\{\Phi_{t}\\}$. We define the first variation of
$F_{\lambda}$ by,

$\delta
F_{\lambda}(\Omega)(X)=\frac{d}{dt}F_{\lambda}(\Phi_{t}(\Omega))_{|t=0}.$ (15)

and the second variation by,

$\delta^{2}F_{\lambda}(\Omega)(X)=\frac{d^{2}}{dt^{2}}F_{\lambda}(\Phi_{t}(\Omega))_{|t=0}.$
(16)

We have that $\delta F_{\lambda}(E)(X)=0$, for all $C^{1}$ vector fields $X$.
Note that we require $M$ to be embedded and orientable for the following to be
well-defined. Consider the class of vector fields $X\in
C^{2}_{c}(N\setminus(\overline{M}\setminus M))$, such that
$X_{|M}=\varphi\nu$, where $\varphi\in C_{c}^{2}(M)$. By [1, Proposition 2.5],

$\delta^{2}F_{\lambda}(E)(X)=\int_{M}|\nabla^{M}\varphi|^{2}-(|A_{M}|^{2}+\text{Ric}(\nu,\nu))\varphi^{2}\,d\mathcal{H}^{n}.$
(17)

We extend the expression on the right-hand side to all functions in
$W^{1,2}_{0}(M)$, and define the following quadratic form,

$B_{M}(\varphi,\varphi)\coloneqq\int_{M}|\nabla^{M}\varphi|^{2}-(|A_{M}|^{2}+\text{Ric}(\nu,\nu))\varphi^{2}\,d\mathcal{H}^{n},\hskip
28.45274pt\varphi\in W_{0}^{1,2}(M).$

After integrating by parts we obtain the second order elliptic operator on
$M$,

$L_{M}\coloneqq\Delta_{M}+|A_{M}|^{2}+\text{Ric}(\nu,\nu).$

We restrict ourselves to a set $W\subset\subset
N\setminus(\overline{M}\setminus M)$, to avoid our curvature term $|A_{M}|$,
from potentially blowing up. A value $\kappa=\kappa(W)\in\mathbb{R}$ is said
to be an eigenvalue of $L_{M}$ in $W$, if there exists a $\varphi\in
W_{0}^{1,2}(W\cap M)$ such that

$L_{M}\varphi+\kappa\varphi=0.$

By standard elliptic theory, see [9], the spectrum of $L_{M}$ in $W\cap M$,

$\kappa_{1}(W)\leq\kappa_{2}(W)\leq\cdots\rightarrow+\infty,$

is discrete and bounded from below. We then define the index of $M$ in $W$ by,

$\text{ind}_{W}(M)=|\\{p\colon\kappa_{p}(W)<0\\}|,$

or equivalently, it is the maximum dimension of a linear subspace of
$W_{0}^{1,2}(W\cap M)$ on which $B_{M}$ is negative definite. If
$\text{ind}_{W}(\text{ind}\,M)=0$, then we say that $M$ is stable in $W$ and
$\kappa_{p}(W)\geq 0$, for all $p$ in $\mathbb{N}$, and

$B_{M}(\varphi,\varphi)\geq 0,\,for\,all\,\varphi\in W_{0}^{1,2}(W\cap M).$

We define,

$\text{ind}(M)=\sup_{W\subset\subset N\setminus(\overline{M}\setminus
M)}(\text{ind}_{W}(M)).$

As $M$ is embedded, and our sequence of critical points $\\{u_{i}\\}$ from
Section 1.1 has $\text{ind}\,u_{i}\leq 1$, by [14, Theorem 1a.], we have that
$\text{ind}M\leq 1$.

######  Remark 26.

As $M$ is two-sided and embedded, and the inhomogeneous term is a constant, we
may also apply the ideas and arguments of [11] verbatim to conclude that
$\text{ind}M\leq 1$.

######  Claim 5.

$\text{ind}\,M=1$.

###### Proof.

We only need to show a lower bound, which follows from the Ricci positivity on
$N$. We construct an appropriate function on $M$, using a similar argument to
[2, Lemma 5.1].

We wish to prove that we can find a set $W\subset\subset
N\setminus(\overline{M}\setminus M)$, and a function $\varphi$ in
$W_{0}^{1,2}(M\cap W)$ such that,

$B_{M}(\varphi,\varphi)<0.$

By the Ricci positivity of $N$, for any $W\subset\subset
N\setminus(\overline{M}\setminus M)$, and $\varphi$ in $W_{0}^{1,2}(M\cap W)$,
we have

$B_{M}(\varphi,\varphi)\leq\int_{M}|\nabla^{M}\varphi|^{2}-|A_{M}|^{2}\varphi^{2}\,d\mathcal{H}^{n}.$

If $\overline{M}\setminus M=\emptyset$, we set $W=N$, and $\varphi=1$,

$B_{M}(\varphi,\varphi)\leq-\int_{M}|A_{M}|^{2}\,d\mathcal{H}^{n}<0.$

For $\overline{M}\setminus M\not=\emptyset$, we first we note that we must
have $n\geq 7$, and $\mathcal{H}^{n-1}(\overline{M}\setminus M)=0$. Therefore,
the 2-capacity of $\overline{M}\setminus M$ is 0, [8, Section 4.7.2, Theorem
3], implying that for all $\delta>0$, there exists a function $f_{\delta}$
such that,

$\begin{cases}f_{\delta}\in C_{c}^{\infty}(N\setminus(\overline{M}\setminus
M)),\\\ f_{\delta}(y)\in[0,1],\,y\in N,\\\ \int_{N}|\nabla
f_{\delta}|^{2}d\mu_{g}<\delta,\\\
\mu_{g}(\\{f_{\delta}=1\\})>\mu_{g}(N)-\delta.\end{cases}$

Furthermore, as $|\overline{M}|$ is a multiplicity 1 integral varifold with
uniformly bounded generalised mean curvature, we have a monotonicity formula
[17, Corollary 17.8]. The existence of such a monotonicity formula implies
Euclidean volume growth about each point in $\overline{M}$. Therefore, there
exists a constant $C_{8}=C_{8}(N,M,g)$, such that, by the construction of
$f_{\delta}$ as in [8, Section 4.7.2, Theorem 3],

$\int_{M}|\nabla^{M}f_{\delta}|^{2}\,d\mathcal{H}^{n}\leq C_{8}\delta.$

Taking $W_{\delta}=\text{supp}\,f_{\delta}\subset\subset
N\setminus(\overline{M}\setminus M)$, we have that $(f_{\delta})_{|M}\in
W^{1,2}_{0}(M\cap W_{\delta})$, and,

$B_{M}(f_{\delta},f_{\delta})\leq
C\delta-n^{-2}\lambda^{2}\mathcal{H}^{n}(\\{f_{\delta}=1\\}\cap M).$

We have that as we send $\delta\rightarrow 0$,
$\mathcal{H}^{n}(\\{f_{\delta}=1\\}\cap M)\rightarrow\mathcal{H}^{n}(M)$.
Therefore, for small enough $\delta>0$, we have that
$B_{M}(f_{\delta},f_{\delta})<0$. This implies that $\text{ind}M\geq 1$. ∎

The fact that $M$ is connected immediately follows from this, as on each
connected component we could construct a function as in Claim 5. Therefore,
each connected component adds at least $1$ to the index.

## References

  * [1] J. Barbosa and M. do Carmo, _Stability of Hypersurfaces with Constant Mean Curvature_ , Mathematische Zeitschrift 185 (1983), pp. 339 – 353.
  * [2] C. Bellettini, _Multiplicity-1 Minmax Minimal Hypersurfaces in Manifolds with Positive Ricci Curvature_ , (to appear in) Communications on Pure and Applied Mathematics, arXiv:2004.10112.
  * [3] C. Bellettini, _Generic Existence of Multiplicity-1 Minmax Minimal Hypersurfaces via Allen–Cahn_ , Calculus of Variations and Partial Differential Equations 61 (2022), ar. 149.
  * [4] C. Bellettini and N. Wickramasekera, _Stable CMC Integral Varifolds of Codimension 1: Regularity and Compactness_ (2018), arXiv:1802.00377.
  * [5] C. Bellettini and N. Wickramasekera, _Stable Prescribed-Mean-Curvature Integral Varifolds of Codimension 1: Regularity and Compactness_ (2020), arXiv:1902.09669.
  * [6] C. Bellettini and N. Wickramasekera, _The Inhomogeneous Allen–Cahn Equation and the Existence of Prescribed-Mean-Curvature Hypersurfaces_ (2020), arXiv:2010.05847.
  * [7] A. Dey, _Existence of Multiple Closed CMC Hypersurfaces with Small Mean Curvature_ , (to appear in) Journal of Differential Geometry, arXiv:1910.00989.
  * [8] L.C. Evans and R.F. Gariepy, _Measure Theory and Fine Properties of Functions_ , Studies in Advanced Mathematics, Taylor and Francis (1992).
  * [9] D. Gilbarg and N. Trudinger, _Elliptic Partial Differential Equations of Second Order_ , 2nd ed., rev. 3rd printing, Classics in Mathematics, Springer (2001).
  * [10] A. Gray, _Tubes_ , 2nd ed. Progress in Mathematics 221, Birkhäuser Basel (2004).
  * [11] F. Hiesmayr, _Spectrum and Index of Two-Sided Allen-Cahn Minimal Hypersurfaces_ , Communications in Partial Differential Equations 43 (2017), pp. 1541 – 1565.
  * [12] J. Hutchinson and Y. Tonegawa, _Convergence of Phase Interfaces in the Van der Waals-Cahn-Hilliard Theory_ , Calculus of Variations and Partial Differential Equations 10 (2000), no. 1, pp. 49 – 84.
  * [13] C. Mantegazza and A. C. G. Mennucci, _Hamilton–Jacobi Equations and Distance Functions on Riemannian Manifolds_ , Applied Mathematics and Optimization 47 (2002), pp. 1 – 25.
  * [14] C. Mantoulidis, _Variational Aspects of Phase Transitions with Prescribed Mean Curvature_ , Calculus of Variations and Partial Differential Equations 61 (2022), no. 2, ar. 43.
  * [15] M. Röger and Y. Tonegawa, _Convergence of Phase-Field Approximations to the Gibbs–Thomson Law_ , Calculus of Variations and Partial Differential Equations 32 (2008), no. 1, pp. 111 – 136.
  * [16] T. Sakai, _Riemannian Geometry_ , Translations of Mathematical Monographs, Fields Institute Communications, American Mathematical Society (1996).
  * [17] L. Simon, _Lectures on Geometric Measure Theory_ , Centre for Mathematical Analysis, Australian National University (1983).
  * [18] Y. Tonegawa, _On Stable Critical Points for a Singular Perturbation Problem_ , Communications in Analysis and Geometry 13 (2005), pp. 439 – 459.
  * [19] Y. Tonegawa and N. Wickramasekera, _Stable Phase Interfaces in the Van der Waals–Cahn–Hilliard Theory_ , Journal fur die Reine und Angewandte Mathematik (2012), no. 668, pp. 191 – 210.
  * [20] B. White, _Generic Transversality of Minimal Submanifolds and Generic Regularity of Two-Dimensional Area-Minimizing Integral Currents_ , (2019), arXiv: 1901.05148.
  * [21] N. Wickramasekera, _A General Regularity Theory for Stable Codimension 1 Integral Varifolds_ , Annals of Mathematics 179 (2014), pp. 843 – 1007.
  * [22] X. Zhou and J. Zhu, _Min-Max Theory for Constant Mean Curvature Hypersurfaces_ , Inventiones mathematicae 218 (2019), pp. 441 – 490.
  * [23] X. Zhou and J. Zhu, _Existence of Hypersurfaces with Prescribed Mean Curvature I - Generic Min-Max_ , Cambridge Journal of Mathematics 8 (2020), pp. 311 – 362.