11institutetext: LIX, Ecole Polytechnique, CNRS and IP-Paris, 91128 Palaiseau
Cedex, France

# Guaranteed approximations of arbitrarily quantified reachability problems

Eric Goubault and Sylvie Putot

###### Abstract

We propose an approach to compute inner and outer-approximations of the sets
of values satisfying constraints expressed as arbitrarily quantified formulas.
Such formulas arise for instance when specifying important problems in control
such as robustness, motion planning or controllers comparison. We propose an
interval-based method which allows for tractable but tight approximations. We
demonstrate its applicability through a series of examples and benchmarks
using a prototype implementation.

###### Keywords:

Reachability, Quantified problems, Inner-approximations

##  1 Introduction

We consider the problem of computing inner and outer approximations of sets of
reachable states constrained by arbitrarily quantified formulas. Although this
can be applied to a number of computer science and verification problems, we
focus here on quantified formulas that arise in control and validation.
Controlled systems are usually subject to disturbances, and are defined by the
flow $\varphi(t;x_{0},u,w)$ at time $t$, for any initial state $x_{0}$,
control $u$ and disturbance $w$. Robust reachability in the sense of [20] is
defined as computing, for time $t\in[0,T]$, a set such as
$R_{\forall\exists}(\varphi)(t)$:

$R_{\forall\exists}(\varphi)(t)=\\{z\ \mid\ \forall w\in\mathbb{W},\ \exists
x_{0}\in\mathbb{X}_{0},\ \exists u\in\mathbb{U},\\\ z=\varphi(t;x_{0},u,w)\\}$

and solves the problem of knowing whether a controller can compensate
disturbances or change of values of parameters that are known to the
controller. This is an example of the quantified reachability problems
targeted in this work.

In classical robust control, the problem can be different and consider the
existence of a controller leading to a target robustly whatever the
disturbances in a given set. In this case, we may need to relax the problem to
find a non-empty solution, for instance by some tolerance in time or space on
reaching the target. This leads to more complex quantified problems of the
form, for example here with a relaxation in time:

$R_{\exists\forall\exists}(\varphi)=\\{z\in\mathbb{R}^{m}\mid\exists
u\in\mathbb{U},\ \exists x_{0}\in\mathbb{X}_{0},\ \forall w\in{\mathbb{W}},\
\exists s\in[0,T]\\\ z=\varphi(s;x_{0},u,w)\\}$ (1)

This generalization is one of the motivations of the work described hereafter,
that considers arbitrary alternations of quantifiers. We discuss in Section
1.2 other problems in control requiring such alternations, among which motion
planning problems and problems specified by hyperproperties such as robustness
or comparisons of controllers.

###  1.1 Problem statement

Let $f$ be a function from $\mathbb{R}^{p}$ to $\mathbb{R}^{m}$, which can be
a flow function $\varphi$ as above, a discrete-time dynamical system etc. We
suppose the $p$ arguments of $f$ are partitioned into consecutive $j_{i}$
arguments $i=1,\ldots,2n$ corresponding to the alternations of quantifiers,
with $p=\sum\limits_{i=1}^{2n}j_{i}$. This partition, identified with the
sequence $(j_{1},\ldots,j_{2n})$ is denoted by $p$. For simplicity’s sake, we
will note ${{\makebox{\boldmath$x$}}}_{i}=(x_{k_{i}+1},\ldots,x_{k_{i+1}})$
where $k_{i}$ stands for $\sum\limits_{l=1}^{i-1}j_{l}$, $i=1,\ldots,2n+1$,
and $f(x_{1},x_{2},\ldots,$
$x_{k_{2n}})=f({{\makebox{\boldmath$x$}}}_{1},\ldots,{{\makebox{\boldmath$x$}}}_{2n})$.

We consider the general quantified problems, with $n$ alternations of
quantifiers $\forall\exists$, of finding $R_{{\makebox{\boldmath$p$}}}(f)$
defined as:

$R_{{\makebox{\boldmath$p$}}}(f)=\left\\{z\in\mathbb{R}^{m}\mid\forall{\makebox{\boldmath$x$}}_{1}\in[-1,1]^{j_{1}},\
\exists{\makebox{\boldmath$x$}}_{2}\in[-1,1]^{j_{2}},\ \ldots,\right.\\\
\left.\forall{\makebox{\boldmath$x$}}_{2n-1}\in[-1,1]^{j_{2n-1}},\exists{\makebox{\boldmath$x_{2n}$}}\in[-1,1]^{j_{2n}},\
z=f({\makebox{\boldmath$x$}}_{1},{\makebox{\boldmath$x$}}_{2},\ldots,{\makebox{\boldmath$x$}}_{{2n}})\right\\}$
(2)

###### Remark 1

Note that this formulation does not prevent us from considering a formula
starting with an existential quantifier (nor one finishing with a universal
quantifier): formally this can be done by adding a universal quantifier at the
start of the sequence of quantifiers, quantifying over a dummy variable.

When only few quantifier alternations are involved, we will use the notations
$R_{\forall}(f)$, $R_{\exists}(f)$, $R_{\forall\exists}(f)$,
$R_{\exists\forall}(f)$ etc. instead of $R_{{\makebox{\boldmath$p$}}}(f)$, for
brevity.

###### Remark 2

Problem (2) naturally also includes, up to reparametrization, quantified
problems with other boxes than $[-1,1]^{j_{i}}$. It is also possible to
consider more general sets over which to quantify variables $x_{i}$. As shown
in Proposition 2, any outer-approximation (resp. inner-approximation) of the
set of values for universally quantified variables $x_{2i-1}$ and inner-
approximation of the set for existentially quantified variables $x_{2i}$, by
boxes, provides with our method an inner-approximation (resp. outer-
approximation) of $R_{{\makebox{\boldmath$p$}}}(f)$.

###### Remark 3

In control applications, control $u$ and disturbance $w$ are generally
functions of time. We are not quantifying over functions here, which would be
a much more intricate problem to solve, but, as in e.g. [21], we are
considering that control and disturbances are discretized, hence constant,
over small time intervals: they thus are identified with a finite set of
parameters, over a bounded time horizon.

Computing reachable sets $R_{{\makebox{\boldmath$p$}}}(f)$ being intractable
in general, as it includes in particular the computation of the range of a
function, we focus on computing tight inner- and outer-approximations.

#### Running example

In the sequel, we will illustrate our approach on a simple Dubbins vehicle
model described below, where function $f$ in (4) is the flow function
$\varphi$ of the system. In general, the flow function does not admit closed
forms, but our method will still be applicable in that context as it will only
require outer-approximations of its values and of its Jacobian. Still, when
comparing with quantifier elimination methods, we will need to give polynomial
approximations for $\varphi$, which will be developed in Example 3.

######  Example 1 (Dubbins vehicle [21])

We simplify the model from [21] to consider only uncertainties on the $x$
axis: $\dot{x}=vcos(\theta)+b_{1}$, $\dot{y}=vsin(\theta)$, $\dot{\theta}=a$.
We suppose that the speed $v$ is equal to 1 and we have a control period of
$t=0.5$. The initial conditions are uncertain given in
$\mathbb{X}_{0}=\\{(x,y,\theta)\ \mid\ x\in[-0.1,0.1],\ y\in[-0.1,0.1],\
\theta\in[-0.01,0.01]\\}$, the control $a$ can take values in
$\mathbb{U}=[-0.01,0.01]$ and disturbance $b_{1}$ can take values in
$\mathbb{W}=[-0.01,0.01]$. Both control and disturbance are supposed to be
constant over the control period $[0,0.5]$. This could naturally be extended
for any number of control periods, with piecewise constant control and
disturbances. We are interested in computing approximations of reachable sets
of the form (4) where $\varphi$ is the solution flow of the system.

###  1.2 Quantified reachability problems

Quantified reachability problems are central in control and hybrid systems, we
detail below a few examples.

#### General robust reachability

A classical robust reachability problem consists in computing the states
reachable at some time $T\geq 0$ for some control, independently of
disturbances which can even be adversarial with respect to the control and
initial state:

$R_{\exists\forall}(\varphi)=\left\\{z\in\mathbb{R}^{m}\mid\exists
u\in\mathbb{U},\exists x_{0}\in\mathbb{X}_{0},\ \forall
w\in{\mathbb{W}},\right.\left.z=\varphi(T;x_{0},u,w)\right\\}$ (3)

However, requiring to reach a given target point $z\in
R_{\exists\forall}(\varphi)$ at time $T$ independently of the disturbance is
most often a too constrained problem. A better quantified problem is the
relaxation to whether we can reach this point within time $[0,T]$ instead of
at fixed time:

$R_{\exists\forall\exists}(\varphi)=\\{z\in\mathbb{R}^{m}\mid\exists
u\in\mathbb{U},\ \exists x_{0}\in\mathbb{X}_{0},\ \forall w\in{\mathbb{W}},\
\exists s\in[0,T]\\\ z=\varphi(s;x_{0},u,w)\\}$ (4)

######  Example 2 (Dubbins vehicle (continued))

We want the robust reachable set within one time period, i.e. until time
$t=0.5$, with one control value $a_{0}$ applied between times $0$ and $0.5$.
This corresponds to $R_{\exists\forall\exists}(\varphi)$ of Equation (4) with
sets $\mathbb{U}$, $\mathbb{X}_{0}$, $\mathbb{W}$ defined in Example 1 and
$T=0.5$.

Another possible relaxation of Equation (3) is to consider the set of states
that can be reached up to $\delta$. This corresponds to the quantified
problems:

$R_{\exists\forall\exists}(\varphi)=\\{z\in\mathbb{R}^{m}\mid\exists
u\in\mathbb{U},\ \exists x_{0}\in\mathbb{X}_{0},\ \forall w\in{\mathbb{W}},\\\
\exists\delta\in[-\delta,\delta]^{m},\ z=\varphi(T;x_{0},u,w)+\delta\\}$ (5)

Time and space tolerances can also be combined. We will for instance do so on
the running example, by considering the quantified problem of Equation (17).

Finally, even more complicated quantified problems are of interest in robust
control, such as:

$R_{\forall\exists\forall\exists}(\varphi)=\\{z\in\mathbb{R}^{m}\mid\forall
x_{0}\in\mathbb{X}_{0},\ \exists u\in\mathbb{U},\ \forall
w\in{\mathbb{W}},\exists s\in[0,T],\\\ z=\varphi(s;x_{0},u,w)$ (6)

where the control $u$ can observe and react to the initial conditions $x_{0}$,
but not to the disturbance $w$.

#### Motion planning

Motion planning problems are typically described by quantified formulas, for
instance when prescribing waypoints or regions along with specific time
intervals through which a controller should steer a dynamical system.

As an example, suppose we want to go through regions $S_{j}$ between times
$T_{j-1}$ and $T_{j}$, for $j=1,\ldots,k$, and characterize the set of final
states or locations $z_{k}$, this implies finding the following set
$R_{\exists\forall\ldots\forall\exists}(\varphi)$:

$\\{z_{k}\in\mathbb{R}^{m}\mid\exists u_{1}\in\mathbb{U},\ \forall
x_{0}\in\mathbb{X}_{0},\ \forall w_{1}\in\mathbb{W},\ \exists
t_{1}\in[0,T_{1}],\ \exists z_{1}\in S_{1},\ \exists u_{2}\in\mathbb{U},\\\
\forall w_{2}\in\mathbb{W},\ \exists t_{2}\in[T_{1},T_{2}],\ \exists z_{2}\in
S_{2},\ \ldots,\ \exists u_{k}\in\mathbb{U},\ \forall w_{k}\in\mathbb{W},\
\exists t_{k}\in[T_{k-1},T],\\\ \left(\begin{array}[]{c}z_{1}\\\ \ldots\\\
z_{k}\end{array}\right)=\left(\begin{array}[]{c}\varphi(t_{1};u_{1},x_{0},w_{1})\\\
\ldots\\\ \varphi(t_{k}-t_{k_{1}};u_{k},z_{k-1},w_{k})\end{array}\right)$ (7)

#### Temporal logic properties

Temporal logics such as Metric Interval Temporal Logic (MITL) and Signal
Temporal Logic (STL) have been successful in specifying numerous properties of
interest for control systems, see e.g. [11]. Such formulas naturally produce
complex quantified formulas since the semantics of ”always $\Phi$ between
times $a$ and $b$” (resp. ”eventually $\Phi$ between times $a$ and $b$”) in
terms or ordinary first-order propositional formulas is $\forall t\in[a,b],\
\Phi$ (resp. $\exists t\in[a,b],\ \Phi$).

It is not the subject here to discuss the class of temporal logic formulas
that we can interpret through Equation (2), but rather to exemplify the
potential for our approach. It is important though to note that not only we
can interpret the standard boolean semantics of a class of such temporal
formulas, but also their robust semantics [12]. Moreover, formulas such as
Equation (2) allow for quantifying over any parameters of the dynamics of a
control system, hence to express quantifications over trajectories, making it
possible to compare trajectories such as in hyperproperties, see e.g. [34].
For instance, if we consider the behavioural robustness of a system, which
specifies that small differences in system inputs result in small differences
in system outputs, this can be measured by different quantified expressions
such as:

$R_{\exists\forall\exists\forall\exists}(\varphi)=\\{z\ \mid\ \exists
x_{0}\in\mathbb{X}_{0},\ \exists\delta\in[-\epsilon,\epsilon]^{i},\\\ \forall
u\in\mathbb{U},\ \exists u^{\prime}\in\mathbb{U},\ \forall w\in\mathbb{W},\
\exists t\in[T_{1},T_{2}],\
z=\lVert\varphi(t;x_{0},u,w)-\varphi(t;x_{0}+\delta,u^{\prime},w)\rVert\\}$

which measures the distance between two trajectories of the same system when
starting with close enough initial conditions, under any disturbance but taken
equal for the two trajectories.

###  1.3 Related work

#### Set-based methods for reachability analysis

Our approach is related to outer-approximations of non-linear continuous and
controlled systems: outer-approximations of the reachable set of such systems
is a particular case of our approach and we rely on such outer-approximations
to compute outer- and inner-approximations of quantified problems. Many
methods for outer-approximating reachable sets for continuous systems have
been developed. For linear systems, direct set-based methods have been
designed for estimating the exponential of a matrix, or of Peano-Baker series
for uncertain systems [3], using support functions, [23], zonotopes [15],
ellipsoids [27], for efficient representations of sets of states. For non-
linear continuous systems, similar set-based techniques have been applied
using polytopes [35] or generalized polytopes such as polynomial zonotopes
[2]. Authors have also been considering a variety of linearization,
hybridization or polynomialization techniques such as in e.g. [2, 4]. Instead
of directly propagating tractable sets through the dynamics, Taylor methods
[30] have been applied extensively by a number of authors, e.g. [7], for
computing polynomial approximations of solutions of ODEs (flowpipes), whose
image can then be approximated using any of the tractable set representation
we mentionned above. Another approach for reachability is through Hamilton-
Jacobi techniques, see e.g. [5], that express functions whose zero sub-level
set give the reachable sets as solutions to a Hamilton-Jacobi PDE.

There are far less methods for inner-approximating images of functions or sets
of reachable states. Interval-based methods, relying on space discretization,
have been used for inner-approximating the image of functions [17]. They were
also used to outer and inner approximate solutions of differential systems
with uncertain initial conditions [31]. An interesting recent work [26]
calculates the inner-approximation by scaling down an outer-approximation,
until a suitable criterion (involving the boundary of the reachable set of
states) is met. A similar criterion is used in [40], with polytopic
approximations. An important body of the inner-approximation literature uses
either Hamilton-Jacobi methods methods see [32] and [29] or set-based
approximate backwards reachability, i.e. through the inverted dynamics see
e.g. [8] and [40].

Our approach is directly linked to previous work on modal intervals and mean-
value theorems [16, 19] but extends it considerably as we are not bound to
consider only $\forall\exists$ statements. It also includes the approximations
of robust reachable sets with time-varying inputs and disturbances as defined
in [20, 21, 22].

#### Quantifier elimination

Many verification and synthesis problems in computer science and control
theory can be represented by the first order formula

$\Phi(p_{1},\ldots,p_{m})\equiv Q_{1}x_{1},\ \ldots\ Q_{n}x_{n},\
P(p_{1},\ldots,p_{m},x_{1},\ldots,x_{n})$ (8)

where $Q_{i}\in\\{\forall,\exists\\}$ are either universal or existential
quantifiers, $p_{1},\ldots,p_{m}$ are free variables and $P$ is a quantifier-
free formula constructed by conjunction, disjunction and negation of atomic
formulas of the form $f\mbox{ op }0$ where $\mbox{op}\in\\{=,\neq,<,\leq\\}$
is a relational operator and $f$ is a polynomial.

The first quantifier elimination algorithm is due to Tarski [39] for the first
order theory of real numbers. Because of its high computational complexity,
this algorithm is not used in practice. The first practical algorithm is due
to Collins [9], and is based on cylindrical algebraic decomposition. Still,
applications of this algorithm are limited because its complexity is doubly
exponential in $n+m$.

The applications of quantifier elimination to control design [1] are numerous:
output feedback stabilization, simultaneous stabilization, robust
stabilization, frequency domain multiobjective design. In [1], they are mostly
exemplified on linear systems. The work of [1] has been extended to non-linear
systems in e.g. [25], including also some trajectory tracking properties.
Reachability is not in general solvable by algebraic methods. The reason is
that the solution set of a system of differential equations is not algebraic
in general. However, [25] considers a more restricted form of reachability,
along prescribed types of trajectories, that can be investigated using semi-
algebraic tools. Further generalizations are exemplified in [38], with
controller synthesis, stability, and collision avoidance problems. Quantifier
elimination techniques have also been applied to model predictive control, see
e.g. [37]. Finally, application of quantifier elimination to robot motion
planning, similar to the one considered in Section 1.2, has been considered in
e.g. [28], for instance for the classical piano mover’s problem [36].

Our quantified problem of Equation (2) is an instance of general quantifier
elimination, although we do not impose that functions $f$ we consider are
polynomial. We compare our method with quantifier elimination techniques in
the sequel, although our method is specifically designed to give tight inner
and outer approximations in a fast manner whereas quantifier elimination aims
at finding exact solution sets along with algebraic conditions under which
they exist, at the expense of time complexity. As quantifier elimination needs
to consider polynomials, we compare our method with quantifier elimination on
approximations of the flow function $\varphi$ given by e.g. Taylor expansions
[33], see Example 3.

#### Satisfiability modulo theory (SMT)

Some SMT solvers interpret quantified formulas over theories. Still, it has
long been known that there is no sound and complete procedure already for
first-order logic formulas of linear arithmetic with uninterpreted function
symbols [14], meaning that the corresponding SMT solvers generally rely on
heuristics to deal with quantifiers. The closer SMT solver to our approach is
dReal/dReach [13] which has support for some quantified SMT modulo the theory
of real numbers and modulo ODEs. Such SMT solvers do not synthetize the set of
states that verifies some quantified formula as we do, but can be used for
checking this set is correct, up to some ”resolution”. The time complexity of
such methods is also much higher that what we are proposing, and dReal/dReach
is limited to the exists-forall fragment.

######  Example 3 (Dubbins vehicle (continued))

We want to compute the robust reachable set of Example 2 using quantifier
elimination. As we do not have the exact flow $\varphi(t;x_{0},u,w)$, we use
approximations by Taylor expansions, see e.g. [21] where a similar example was
discussed. With the initial conditions and parameters values of Example 1, we
get the following Taylor expansion in time with zonotopic coefficients (which
gives some Taylor model of the solution flow):

$P(t):x=0.1\epsilon_{1}+(1+0.01\epsilon_{2})t+1.31\ 10^{-7}\epsilon_{3}t^{2}\
\wedge y=0.1\epsilon_{4}+(0.01\epsilon_{6}+0.01\epsilon_{7}t)t\\\
+(0.005\epsilon_{5})t^{2}\ \wedge\theta(t)=0.01\epsilon_{6}+0.01\epsilon_{7}t$
(9)

with $\epsilon_{i}\in[-1,1]$ for $i=1,\ldots,7$. and $x_{0}=0.1\epsilon_{1}$,
$b_{1}=0.01\epsilon_{2}$, $y_{0}=0.1\epsilon_{4}$, $a=0.01\epsilon_{7}$ and
$\theta_{0}=0.01\epsilon_{6}$. These were obtained by a linearization of the
cosinus and sinus and simple estimates of remainders, which could be improved
but were kept simple for the sake of readability.

We interpret the $R_{\exists\forall\exists}(\varphi)$ formula of Equation (4)
by quantifying over the symbolic variables $\epsilon_{1}$ to $\epsilon_{7}$.
We have a correspondence between initial states and inputs of the problem and
the $\epsilon_{i}$, except for $\epsilon_{3}$ and $\epsilon_{5}$ that abstract
the remainder term of the Taylor approximation of the solution. Hence an over-
approximation of $R_{\exists\forall\exists}(\varphi)$ can be obtained by
quantifier elimination on the formula:

$\exists\epsilon_{7}\in[-1,1],\ \exists\epsilon_{1}\in[-1,1],\
\exists\epsilon_{4}\in[-1,1],\ \exists\epsilon_{6}\in[-1,1],\\\
\forall\epsilon_{2}\in[-1,1],\ \exists\epsilon_{3}\in[-1,1],\
\exists\epsilon_{5}\in[-1,1],\ \exists t\in[0,0.5],\;P(t)$

where $P(t)$ is defined by Equation (9) and all symbols are existentially
quantified except $\epsilon_{2}$ which corresponds to the disturbance $b_{1}$.
There are numerous software implementing some form or another of quantifier
elimination, e.g. QEPCAD [6], REDUCE RedLog package [10], and Mathematica
[24]. We use in the sequel Mathematica and its operation Reduce. We refer the
reader to the appendix, Section 0.A, where all queries in Mathematica are
provided. Using Mathematica for the problem above times out, but when we make
independent queries on $x$, $y$ and $\theta$, we get $x\in[-0.1,0.595]$,
$y\in[-0.10875,0.10875]$ and $\theta\in[-0.015,0.015]$, with a warning about
potential inexact coefficients, respectively in about 25, 12 and 0.05 seconds
on a MacBook Pro 2.3GHz Intel Core i9 8 cores with 16GB of memory. This gives
a correct outer approximation of $R_{\exists\forall\exists}(\varphi)$.

Similarly, for inner-approximation we eliminate the quantifiers in:

$\exists\epsilon_{7}\in[-1,1],\ \exists\epsilon_{1}\in[-1,1],\
\exists\epsilon_{4}\in[-1,1],\ \exists\epsilon_{6}\in[-1,1],\\\
\forall\epsilon_{2}\in[-1,1],\
\forall\epsilon_{3}\in[-1,1],\forall\epsilon_{5}\in[-1,1],\ \exists
t\in[0,0.5],\;P(t)$

where the uncertainties $\epsilon_{3}$ and $\epsilon_{5}$ are now quantified
universally, reflecting the fact that inner-approximation corresponds to
making no hypothesis on the values of these variables corresponding to
approximation errors, apart from knowing bounds. The elimination times out for
the full problem and returns the same bounds as before up to $10^{-5}$, when
solving the problem separately on each variable $x$, $y$ and $\theta$, in
respectively 2.2, 17.1 and 0.06 seconds. However, contrarily to the over-
approximation, these independent queries do not allow us to conclude about an
actual inner-approximation for $R_{\exists\forall\exists}(\varphi)$, as the
existentially quantified variables may be assigned different values in the 3
independent queries.

###  1.4 Contributions

We extend the approach of [20], which is restricted to solving problems of the
form $R_{\exists}(f)$ or $R_{\forall\exists}(f)$, to deal with arbitrary
quantified formulas of the form of $R_{{\makebox{\boldmath$p$}}}(f)$ of
Equation (2). These include the generalized robust reachability problems
discussed in Section 1.2. The problem of finding the exact set
$R_{{\makebox{\boldmath$p$}}}(f)$ admits closed formulas for a scalar-valued
affine function $f$, as described in Section 2.1, culminating in Proposition
1. By local linearization techniques, akin to the ones used in [20], we get
explicit formulas for inner and outer-approximations of general non-linear
scalar-valued functions in Section 2.2, Theorem 2.1.

We consider the general vector-valued case in Section 3 and Theorem 3.1. The
difficulty lies, as for the $\forall\exists$ case of [20], in the computation
of inner-approximations. The solution proposed is to interpret slightly
relaxed quantified problems, one dimension at a time, that, altogether, give
guaranteed inner-approximations of $R_{{\makebox{\boldmath$p$}}}(f)$,
extending the method of [20]. The combinatorics of variables, quantifiers and
components of $f$ make the intuition of the indices used in Theorem 3.1
difficult to fully apprehend: we thus begin Section 3 by an example.

The general form of quantified problems we are considering here makes
solutions that we propose difficult to assess and compare: we are not aware of
any existing tool solving similar problems, at the exception of quantifier
elimination algorithms, discussed in Section 1.3. We also develop a sampling
method, see Remark 4, for checking the tightness of our results.

Finally, we report on our implementation of this method in Julia in Section 4.
Benchmarks show that this method is tractable, with experiments up to
thousands of variables solved in a matter of tens of seconds.

##  2 Approximations of arbitrary quantified formulas in the case of scalar-
valued functions

We first focus in Section 2.1 on the computation of
$R_{{\makebox{\boldmath$p$}}}(f)$ where $f$ is an affine function from
$\mathbb{R}^{p}$ to $\mathbb{R}$. In this case, we derive exact bounds. We
then rely on this result to carry on with the general case in Section 2.2,
using a mean-value theorem.

###  2.1 Exact bounds for scalar affine functions

We consider affine functions, i.e. functions of the form
$f(x_{1},\ldots,x_{q})=\delta_{0}+\sum_{i=1}^{q}\delta_{i}x_{i}$. For these
functions, we consider the general quantified problem defined, for
$Q_{j}=\forall$ or $\exists$, as:

$S_{q}(\delta_{0};Q_{1},\delta_{1};\ldots;Q_{q},\delta_{q})=\left\\{z\in\mathbb{R}\mid
Q_{1}x_{1}\in[-1,1],\right.\\\
Q_{2}x_{2}\in[-1,1],\ldots,\left.Q_{q}x_{q}\in[-1,1],\
z=f(x_{1},x_{2},\ldots,x_{q})\right\\}$

We first see that we have:

###### Lemma 1

$S_{q}(\delta_{0};Q_{1},\delta_{1};\ldots;Q_{q},\delta_{q})=\\\
\left\\{\begin{array}[]{l}\bigcap\limits_{x_{1}\in[-1,1]}S_{q-1}(\delta_{0}+\delta_{1}x_{1};Q_{2},\delta_{2};\ldots;Q_{q},\delta_{q})\mbox{
if $Q_{1}=\forall$}\\\
\bigcup\limits_{x_{1}\in[-1,1]}S_{q-1}(\delta_{0}+\delta_{1}x_{1};Q_{2},\delta_{2};\ldots;Q_{q},\delta_{q})\mbox{
if $Q_{1}=\exists$}\end{array}\right.$ (10)

The proof is given in Section 0.B.

###### Remark 4

The first consequence of Lemma 1 is that it gives a way to probe quantified
formulas of the form of Equation (2), by sampling, as follows. For each
quantifier $i$, in the order of encounter, join samples or ranges for $\exists
x_{i}$, intersect them for $\forall x_{i}$. For example, for the alternation
$\exists x_{1},\forall x_{2},\exists x_{3}$, we compute

$[\min_{x_{i}}\max_{x_{2}}\min_{x_{3}}f(x_{1},x_{2},x_{3}),\max_{x_{i}}\min_{x_{2}}\max_{x_{3}}f(x_{1},x_{2},x_{3})]$

This gives an estimation of the robust range of the function, which is in the
general case neither an inner-approximation nor an outer-approximation, as
this sampling approach performs inner-approximation with respect to
existential quantification and outer-approximation with respect to universal
quantification. Note that in some particular cases (e.g. affine) we can design
an exact method based on these and on unions and intersections of particular
polyhedra.

Using Lemma 1, we see that
$S_{2}(\delta_{0};\forall,\delta_{1};\exists,\delta_{2})$ is empty when the
impact on $f$ of the existentially quantified variable is not of large enough
magnitude to counteract the effect of the universally quantified variable. The
formula given below expresses such conditions for
$R_{{\makebox{\boldmath$p$}}}(f)$ to be non-empty, by imposing a bound on the
${\ell}_{1}$ norm of the universally quantified variables, by a suitable
combination of the $\ell_{1}$ norms, noted $||{{\makebox{\boldmath$x$}}}||$,
of other variables, in particular the existentially quantified ones.

###### Proposition 1

Let $f$ be an affine function defined by:

$f({{\makebox{\boldmath$x$}}}_{1},{{\makebox{\boldmath$x$}}}_{2},\ldots,{{\makebox{\boldmath$x$}}}_{2n})=\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle+\langle\Delta_{2},{{\makebox{\boldmath$x$}}}_{2}\rangle+\ldots+\langle\Delta_{2n},{{\makebox{\boldmath$x$}}}_{2n}\rangle$

with
${\Delta}_{i}=(\delta_{k_{i}+1},\ldots,\delta_{k_{i+1}})\in\mathbb{R}^{j_{i}}$,
$i=1,\ldots,2n$, where $k_{i}=\sum\limits_{l=1}^{i-1}j_{l}$, and
$\langle.,.\rangle$ denotes the scalar product. Consider
$R_{{\makebox{\boldmath$p$}}}(f)$ for the partition
${{\makebox{\boldmath$p$}}}=(j_{1},\ldots,j_{2n})$ of $p$, as in Equation (2),
then we have:

$R_{{\makebox{\boldmath$p$}}}(f)=\delta_{0}+\left[\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k-1}||-||{\Delta}_{2k}||\right)\right.,\left.\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k-1}||\right)\right]$

if
$||{\Delta}_{2l-1}||\leq||{\Delta}_{2l}||+\sum\limits_{k=l+1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k-1}||\right)$
for $l=1,\ldots,n$, otherwise $R_{{\makebox{\boldmath$p$}}}(f)=\emptyset$

The proof is given in Appendix 0.C.

###### Remark 5

In the sequel, when applying Proposition 1, we will use notations $\Delta_{x}$
with $x$ such as control $a$, disturbance $b_{1}$, angle $\theta$ instead of
using for indices a potentially less understandable numbering.

###  2.2 Inner and outer-approximations for non-linear scalar-valued functions

We are now in a position to give inner and outer approximations of
$R_{{\makebox{\boldmath$p$}}}(f)$ for general scalar-valued
$f({{\makebox{\boldmath$x$}}}_{1},{{\makebox{\boldmath$x$}}}_{2},\ldots,{{\makebox{\boldmath$x$}}}_{2n})$
from $\mathbb{R}^{p}$ to $\mathbb{R}$. The principle is to carefully linearize
$f$, so that inner and outer-approximations of
$R_{{\makebox{\boldmath$p$}}}(f)$ are given by inner and outer-approximations
of a similar quantified problem on its linearization, this is Proposition 2.
Combining this with e.g. simple mean-value approximations mentioned in Remark
6, we obtain Theorem 2.1. After exemplifying these formulas on toy examples,
we apply it, twice, to the Dubbins vehicle model of Example 1. We first use
the Taylor approximation of its dynamics, Example 4. We then show that we do
not need to compute such approximations and that our approach can also compute
direct inner and outer-approximations of $R_{{\makebox{\boldmath$p$}}}(f)$
where $f$ is the solution of a differential equation, Example 5.

As before, for a given function $f:\ \mathbb{R}^{p}\rightarrow\mathbb{R}$, we
denote by ${{\makebox{\boldmath$p$}}}=(j_{1},\ldots,j_{2n})$ a partition of
the $p$ arguments of $f$ and $k_{l}=\sum\limits_{i=1}^{l-1}j_{i}$, for
$l=1,\ldots,2n+1$. We suppose we have $p$ intervals $A_{1},\ldots,A_{p}$ and
we write
${{\makebox{\boldmath$A$}}}_{i}=(A_{k_{i}+1},\ldots,A_{k_{i+1}}),\;i=1,\ldots,2n$
the corresponding boxes in $\mathbb{R}^{j_{i}}$. We will use the notation:

${\mathcal{C}}({{\makebox{\boldmath$A$}}}_{1},\ldots,{{\makebox{\boldmath$A$}}}_{2n})=\\{z\mid\forall{\alpha}_{1}\in{{\makebox{\boldmath$A$}}}_{1},\
\exists{\alpha}_{2}\in{{\makebox{\boldmath$A$}}}_{2},\ldots,\\\
\forall{\alpha}_{2n-1}\in{{\makebox{\boldmath$A$}}}_{2n-1},\
\exists{\alpha}_{2n}\in{{\makebox{\boldmath$A$}}}_{2n},\
z=\sum\limits_{j=1}^{2n}\alpha_{j}\\}.$

###### Proposition 2

Given function $f:\ \mathbb{R}^{p}\rightarrow\mathbb{R}$ and partition $p$ as
above, define the following families of functions

$h^{x_{1},\ldots,x_{j-1}}(x_{j})=f(x_{1},\ldots,x_{j-1},x_{j},0,\ldots,0)-f(x_{1},\ldots,x_{j-1},0,\ldots,0)$

for $j=1,\ldots,p$, and suppose we have the following inner and outer-
approximations of their images, independently of $x_{1},\ldots,x_{j-1}$,
denoted by $range(.)$: ${I}_{j}\subseteq
range(h^{x_{1},\ldots,x_{j-1}})\subseteq{O}_{j}$ for $j=1,\ldots,p$. Then,
writing
${{\makebox{\boldmath$I$}}}_{i}=\mathop{\Pi}\limits_{j=k_{i}+1}^{k_{i+1}}[\underline{I}_{j},\overline{I}_{j}]$,
${{\makebox{\boldmath$O$}}}_{i}=\mathop{\Pi}\limits_{j=k_{i}+1}^{k_{i+1}}[\underline{O}_{j},\overline{O}_{j}]$,
$i=1,\ldots,2n$, we have:

$f(0,\ldots,0)+{\mathcal{C}}({{\makebox{\boldmath$O$}}}_{1},{{\makebox{\boldmath$I$}}}_{2},\ldots,{{\makebox{\boldmath$O$}}}_{2n-1},{{\makebox{\boldmath$I$}}}_{2n})\subseteq
R_{{\makebox{\boldmath$p$}}}(f)\\\ \subseteq
f(0,\ldots,0)+C({{\makebox{\boldmath$I$}}}_{1},{{\makebox{\boldmath$O$}}}_{2},\ldots,{{\makebox{\boldmath$I$}}}_{2n-1},{{\makebox{\boldmath$O$}}}_{2n})$
(11)

###### Proof

The proof is based on the fact that $f$ is the sum of all the $h_{i}$,
$i=1,\ldots,2n$, and of $f(0,\ldots,0)$, and is proven by induction on the
number of quantifier alternations, see Section 0.E.

###### Remark 6

We do have such approximants of the range as necessary for Proposition 2,
thanks to a generalized mean-value theorem [16, 21]. If we have, for all
$i=1,\ldots,2n$ and all $j=k_{i}+1,\ldots,k_{i+1}$,
${\nabla}_{j}=[\underline{\nabla}_{j},\overline{\nabla}_{j}]$ such that:

$\left\\{\left|\frac{\partial
f}{\partial{x}_{j}}({{\makebox{\boldmath$x$}}}_{1},\ldots,{{\makebox{\boldmath$x$}}}_{{i}},0,\ldots,0)\right|\mid{{\makebox{\boldmath$x$}}}_{l}\in[-1,1]^{j_{l}},\
l=1,\ldots,i\right\\}\subseteq{\nabla}_{j}$

then we can use, for all $j=1,\ldots,2n$:
${I}_{i}=\underline{\nabla}_{j}[-1,1]$, and
${O}_{j}=\overline{\nabla}_{j}[-1,1]$. We can naturally also use other
approximation methods.

We now deduce inner and outer-approximations of $R_{\bf p}(f)$:

###### Theorem 2.1

With the hypotheses of Proposition 2 on sets ${I}_{j}$ and ${O}_{j}$, and
denoting $\sum{{\makebox{\boldmath$A$}}}$, for $A$ any vector of reals, the
sum of all its components, we have:

$f(0,\ldots,0)+\left[\sum\limits_{k=1}^{n}\sum\left(\overline{{\makebox{\boldmath$O$}}}_{2k-1}+\underline{{\makebox{\boldmath$I$}}}_{2k}\right),\right.\
\left.\sum\limits_{k=1}^{n}\sum\left(\overline{{\makebox{\boldmath$I$}}}_{2k}+\underline{{\makebox{\boldmath$O$}}}_{2k-1}\right)\right]\subseteq
R_{{\makebox{\boldmath$p$}}}(f)$

if
$\sum\overline{{\makebox{\boldmath$O$}}}_{2l-1}-\sum\underline{{\makebox{\boldmath$O$}}}_{2l-1}\leq\sum\limits_{k=l}^{n}\sum\left(\overline{{\makebox{\boldmath$I$}}}_{2k}-\underline{{\makebox{\boldmath$I$}}}_{2k}\right)-\sum\limits_{k=l+1}^{n}\sum\left(\overline{{\makebox{\boldmath$O$}}}_{2k-1}-\underline{{\makebox{\boldmath$O$}}}_{2k-1}\right)$
for $l=1,\ldots,n$, otherwise the inner-approximation is empty, and:

$R_{{\makebox{\boldmath$p$}}}(f)\subseteq
f(0,\ldots,0)+\left[\sum\limits_{k=1}^{n}\sum\left(\overline{{\makebox{\boldmath$I$}}}_{2k-1}+\underline{{\makebox{\boldmath$O$}}}_{2k}\right),\right.\
\left.\sum\limits_{k=1}^{n}\sum\left(\overline{{\makebox{\boldmath$O$}}}_{2k}+\underline{{\makebox{\boldmath$I$}}}_{2k-1}\right)\right]$

if
$\sum\overline{{\makebox{\boldmath$I$}}}_{2l-1}-\sum\underline{{\makebox{\boldmath$I$}}}_{2l-1}\leq\sum\limits_{k=l}^{n}\sum\left(\overline{{\makebox{\boldmath$O$}}}_{2k}-\underline{{\makebox{\boldmath$O$}}}_{2k}\right)-\sum\limits_{k=l+1}^{n}\sum\left(\overline{{\makebox{\boldmath$I$}}}_{2k-1}-\underline{{\makebox{\boldmath$I$}}}_{2k-1}\right)$
for $l=1,\ldots,n$, otherwise the outer-approximation is empty.

###### Proof

The proof uses Proposition 1 on
$C({{\makebox{\boldmath$O$}}}_{1},{{\makebox{\boldmath$I$}}}_{2},\ldots,{{\makebox{\boldmath$O$}}}_{2n-1},{{\makebox{\boldmath$I$}}}_{2n})$
and $C({{\makebox{\boldmath$I$}}}_{1},{{\makebox{\boldmath$O$}}}_{2},$
$\ldots,{{\makebox{\boldmath$I$}}}_{2n-1},{{\makebox{\boldmath$O$}}}_{2n})$,
after rescaling of the interval ${{\makebox{\boldmath$O$}}}_{i}$ and
${{\makebox{\boldmath$I$}}}_{j}$ to $[-1,1]$, and Proposition 2. It is
detailed in Section 0.F.

In Example 4, we now apply Theorem 2.1 to the $x$ component of the Dubbins
vehicle as expressed in Example 3, ignoring any constraint on $y$ and
$\theta$.

######  Example 4 (Dubbins vehicle (continued))

We recall that:

$x(t)=0.1\epsilon_{1}+(1+0.01\epsilon_{2})t+(1.31\ 10^{-7}\epsilon_{3})t^{2}$

The $\nabla_{k}$, outer-approximations of the absolute value of the partial
derivatives of Remark 6, $\frac{\partial x}{\partial\epsilon_{k}}$ and
$\frac{\partial x}{\partial t}$ evaluated between times $t=0$ and $t=0.5$,
are: $\nabla_{\epsilon_{1}}=0.1$, $\nabla_{\epsilon_{2}}=[0,0.005]$,
$\nabla_{\epsilon_{3}}=[0,3.275\ 10^{-8}]$,
$\nabla_{t}=[0.989999869,1.010000131]$. We thus have
$I_{\epsilon_{1}}=O_{\epsilon_{1}}=[-0.1,$ $0.1]$, $I_{\epsilon_{2}}=0$,
$O_{\epsilon_{2}}=[-0.005,0.005]$, and $I_{\epsilon_{3}}=0$,
$O_{\epsilon_{3}}=[-3.275\ 10^{-8},$ $3.275\ 10^{-8}]$ by a direct application
of Remark 6. Note that for computing $I_{t}$ and $O_{t}$, we use the
generalized mean-value theorem of [16] again, but in a slightly different way
than in Remark 6, since the point at which we can evaluate the corresponding
function is $t=0$, which is the lower bound of the extent of the values of $t$
($[0,5]$) and not its center as for other variables. In that case we can
compute the tighter bounds:
$I_{t}=\underline{\nabla}_{t}[0,0.5]=[0,0.4949999345]$ and
$O_{t}=\overline{\nabla}_{t}[0,0.5]=[0,0.5050000655]$.

The quantified formula of Example 2 has only one $\forall$, $\exists$
alternation, the condition of Theorem 2.1 will involve
$O_{\epsilon_{2}}+O_{\epsilon_{3}}=[-0.005,0.005]+[-3.275\ 10^{-8},3.275$
$10^{-8}]$ and $I_{t}=[0,0.4949999345]$. We see that indeed,
$(\overline{O}_{\epsilon_{2}}-\underline{O}_{\epsilon_{3}})+(\overline{O}_{\epsilon_{3}}-\underline{O}_{\epsilon_{2}})=0.010000066\leq\overline{I}_{t}-\underline{I}_{t}=0.4949999345$,
hence we can compute an inner-approximation for the $x$ component of
$\varphi$. Its lower bound is:

$\begin{array}[]{ccccccc}x_{c}&+\underline{I}_{\epsilon_{1}}&+\overline{O}_{\epsilon_{2}}&+\overline{O}_{\epsilon_{3}}&+\underline{I}_{t}&&\\\
=0&-0.1&+0.005&+3.275\ 10^{-8}&+0&=&-0.095\end{array}$

and its upper bound:

$\begin{array}[]{ccccccc}x_{c}&+\overline{I}_{\epsilon_{1}}&+\underline{O}_{\epsilon_{2}}&+\underline{O}_{\epsilon_{3}}&+\overline{I}_{t}&&\\\
=0&+0.1&-0.005&-3.275\ 10^{-8}&+0.4949999345&=&0.59.\end{array}$

Similarly, we compute an outer-approximation and find the following bounds for
$R_{\exists\forall\exists}(\varphi_{x})$: $[-0.095,0.590]\subseteq
R_{\exists\forall\exists}(\varphi)\subseteq[-0.1,0.605]$, to be compared with
the solution from Mathematica quantifier elimination $-0.1\leq x\leq 0.595$.
Sampling also yields estimate $[-0.1,0.595]$.

In the former example, and in general for continuous-time controlled systems
defined by a flow function $\varphi(t;x_{0},u,w)$ solution of an initial value
problem, we do not need as with quantifier elimination techniques to first
compute polynomial approximations. We only need to compute outer
approximations of the flow for one initial condition (”central trajectory”)
and of the Jacobian of the flow for the set of initial conditions, as
exemplified below.

######  Example 5 (Dubbins vehicle (continued))

We consider again the Dubbins vehicle, but defined as the direct solution of
the ODEs of Example 1. We first compute an outer-approximation of a ”central
trajectory” $(x_{c},y_{c},\theta_{c})$, i.e. of the trajectory starting at
$x=0$, $y=0$, $\theta=0$, $b_{1}=0$ and $a=0$. This gives $x_{c}=t$, $y_{c}=0$
and $\theta_{c}=0$.

We note that $\frac{\partial x}{\partial
t}=cos(\theta)+b_{1}\in[0.989999965,1.01]$ thus, using notations from Remark
6, we have the inner and outer-approximations of the effect of variable $t$ on
the value of $x$, $I_{x,t}=[0,0.494999982]$, $O_{x,t}=[0,0.505]$, and
similarly for the other variables: $I_{y,t}=0$,
$O_{y,t}=[-sin(0.015)/2,sin(0.015)/2]=[-1.309\ 10^{-4},1.309\ 10^{-4}]$ and
$I_{\theta,t}=0$, $O_{\theta,t}=[-0.005,0.005]$.

The Jacobian of $\varphi$ with respect to $x_{0}$, $y_{0}$, $\theta_{0}$,
$b_{1}$ and $a$, $J_{i,x_{0}}=\frac{\partial\varphi_{i}}{\partial t}$,
$J_{i,y_{0}}=\frac{\partial\varphi_{i}}{\partial t}$,
$J_{i,\theta_{0}}=\frac{\partial\varphi_{i}}{\partial t}$,
$J_{i,b_{1}}=\frac{\partial\varphi_{i}}{\partial t}$ and
$J_{i,a}=\frac{\partial\varphi_{i}}{\partial t}$, for $i=x,y,\theta$
respectively, satisfies a variational equation [20], solved in appendix,
Section 0.I. By Remark 6, this gives the following inner and outer
approximations for all parameters $x_{0}$, $y_{0}$, $\theta_{0}$, $a$ and
$b_{1}$, and all components $x$, $y$ and $\theta$ of $\varphi$:

  * •

$I_{x,a}=0$, $O_{x,a}=[-6.545\ 10^{-7},6.545\ 10^{-7}]$,
$I_{x,x_{0}}=O_{x,x_{0}}=[-0.1,0.1]$, $I_{x,\theta_{0}}=0$,
$O_{x,\theta_{0}}=[-1.309\ 10^{-6},1.309\ 10^{-6}]$, $I_{x,b_{1}}=0$,
$O_{x,b_{1}}=[-0.005,0.0$ $05]$,

  * •

$I_{y,a}=0$, $O_{y,a}=[-0,0025,$ $0.0025]$,
$I_{y,y_{0}}=O_{y,y_{0}}=[-0.1,0.1]$, $I_{y,\theta_{0}}=0$,
$O_{y,\theta_{0}}=[-0,005,0.005]$,

  * •

$I_{\theta,\theta_{0}}=O_{\theta,\theta_{0}}=[-0.01,0.01]$, $I_{\theta,a}=0$,
$O_{\theta,a}=[0,0.005]$,

We now compute the set $R_{\exists\forall\exists}$ consisting of $z$ such
that:

$\exists a\in[-0.01,0.01],\ \exists x_{0}\in[-0.1,0.1],\ \exists
y_{0}\in[-0.1,0.1],\\\ \exists\theta_{0}\in[-0.01,0.01],\ \forall
b_{1}\in[-0.01,0.01],\ \exists t\in[0,0.5],\
z=\varphi(t;x_{0},y_{0},\theta_{0},a,b_{1})$

Applying Theorem 2.1 we find first an inner-approximation for $x$ (again,
ignoring any condition on $y$ and $\theta$) of $\varphi$. Its lower bound is:

$\begin{array}[]{ccccccc}x_{c}&+\underline{I}_{x,a}&+\underline{I}_{x,x_{0}}&+\underline{I}_{x,y_{0}}&+\underline{I}_{x,\theta_{0}}&+\overline{O}_{x,b_{1}}&+\underline{I}_{x,t}\\\
=0&-0&-0.1&+0&-0&+0.005&+0\end{array}$

which is equal to -0.095, and its upper bound:

$\begin{array}[]{ccccccc}x_{c}&+\overline{I}_{x,a}&+\overline{I}_{x,x_{0}}&+\overline{I}_{x,y_{0}}&+\overline{I}_{x,\theta_{0}}&+\underline{O}_{x,b_{1}}&+\overline{I}_{x,t}\\\
0&+0&+0.1&+0&+0&-0.005&+0.494999982\end{array}$

which is equal to 0.589999982. Therefore the inner-approximation for $x$ is
equal to $[-0.095,0.589999982]$, given that the conditions for the inner-
approximation to be non-void are met. Similarly, we compute an outer-
approximation for the $x$ component of $\varphi$ and find
$[-0.1000019635,0.6050019635]$.

The approximations for the $y$ and $\theta$ components of $\varphi$ are
computed similarly, see Appendix, Section 0.J for detailed computation. We
obtain for $y$ the inner-approximation $[-0.1,0.1]$ and over-approximation
$[0.1076309,0.1076309]$, and for $\theta$ the inner-approximation $[-0.01,$
$0.01]$ and over-approximation $[-0.02,0.02]$.

All these results are very close the the ones obtained in Section 1.3 with
quantifier elimination111Note though that the linearization we used for
simplifying formulas given to a quantifier elimination tool are slightly over-
approximated (especially in the $y$ component)., but are obtained here with a
much smaller complexity.

##  3 Approximations in the case of vector-valued functions

Outer-approximations in the general case when $f$ goes from $\mathbb{R}^{p}$
to $\mathbb{R}^{m}$ for any strictly positive value of $m$ are directly
obtained by the Cartesian product of the ranges obtained separately by the
method of Section 2.2 on each component of $f$. The case of inner-
approximations is more involved, since a Cartesian product of inner-
approximations is not in general an inner-approximation.

In this section, we generalize the method of [21] to the case of arbitrary
quantified formulas. We begin by a simple example, before stating the result
for the general case in Theorem 3.1.

###### Example 6

Suppose we want to inner approximate the following set
$R_{\forall\exists\forall\exists}(f)$ for a function $f$ with two components
$f_{1}$ and $f_{2}$:

$R_{\forall\exists\forall\exists}(f)=\\{z\ |\ \forall x_{1},\ \exists x_{2},\
\exists x_{3},\ \forall x_{4},\ \exists x_{5},\ \exists x_{6},z=f(x)\\}.$

The main idea is that we can rely on the conjunction of quantified formulas
for each component if no variable is existentially quantified for several
components. We thus transform if necessary the quantified formula by
strengthening them for that objective, which is sound with respect to
computing inner-approximations. For example here, we can interpret, for all
$z_{1}$ and $z_{2}$:

$\displaystyle\forall x_{1},\ \forall x_{2},\ \exists x_{3},\ \forall x_{4},\
\forall x_{5},\ \exists x_{6},\
z_{1}=f_{1}(x_{1},x_{2},x_{3},x_{4},x_{5},x_{6})$ (12) $\displaystyle\forall
x_{1},\ \forall x_{3},\ \exists x_{2},\ \forall x_{4},\ \forall x_{6},\
\exists x_{5},\ z_{2}=f_{2}(x_{1},x_{2},x_{3},x_{4},x_{5},x_{6})$ (13)

Then we get Skolem functions: $x_{3}(z_{1},x_{1},x_{2})$ and
$x_{6}(z_{1},x_{1},x_{2},x_{3},x_{4},$ $x_{5})$ from Equation (12), such that
$z_{1}=f_{1}(x_{1},x_{2},x_{3}(z_{1},x_{1},x_{2}),x_{4},x_{5},x_{6}(z_{1},x_{1},x_{2},x_{3},$
$x_{4},x_{5}))$ and $x_{2}(z_{2},x_{1},x_{3})$ and
$x_{5}(z_{2},x_{1},x_{2},x_{3},x_{4},x_{6})$ from (13), such that
$z_{2}=f_{2}(x_{1},$
$x_{2}(z_{2},x_{1},x_{3}),x_{3},x_{4},x_{5}(z_{2},x_{1},x_{2},x_{3},x_{4},x_{6}),x_{6}).$
Supposing that $f_{1}$ and $f_{2}$ are elementary functions, these Skolem
functions can be chosen to be continuous [16, 18]. Consider now functions
$g_{z_{1},z_{2}}:\mathbb{R}^{6}\rightarrow\mathbb{R}^{6}$ defined by

$g(x_{1},x_{2},x_{3},x_{4},x_{5},x_{6})=(x_{1},x_{2}(z_{2},x_{1},x_{3}),x_{3}(z_{1},x_{1},x_{2}),x_{4},\\\
x_{5}(z_{2},x_{1},x_{2},x_{3},x_{4},x_{6}),x_{6}(z_{1},x_{1},x_{2},x_{3},x_{4},x_{5}))$

for all
$(z_{1},z_{2})\in{\makebox{\boldmath$z$}}_{1}\times{\makebox{\boldmath$z$}}_{2}$.
This is a continuous function as composition of continuous functions, from
${\makebox{\boldmath$x$}}={\makebox{\boldmath$x$}}_{1}\times{\makebox{\boldmath$x$}}_{2}\times\ldots\times{\makebox{\boldmath$x$}}_{6}$
to itself.

By Brouwer’s fixpoint theorem, we have fixpoints $x^{\infty}_{3}(z_{1},z_{2},$
$x_{1})$, $x^{\infty}_{6}(z_{1},z_{2},$ $x_{1},x_{4})$,
$x^{\infty}_{2}(z_{1},z_{2},x_{1})$ and
$x^{\infty}_{5}(z_{1},z_{2},x_{1},x_{4})$, for all values of $z_{1}$, $z_{2}$,
$x_{1}$, $x_{4}$ ($x_{1}$ and $x_{4}$ being the existentially quantified input
variables of Equation (6)), such that
$x^{\infty}_{3}(z_{1},z_{2},x_{1})=x_{3}(z_{1},x_{1},x^{\infty}_{2}(z_{1},$
$z_{2},x_{1}))$,
$x^{\infty}_{6}(z_{1},z_{2},x_{1},x_{4})=x_{6}(z_{1},x_{1},x^{\infty}_{2}(z_{1},$
$z_{2},x_{1}),x^{\infty}_{3}(z_{1},z_{2},x_{1}),$
$x_{4},x^{\infty}_{5}(z_{1},z_{2},x_{1},x_{4}))$,
$x^{\infty}_{2}(z_{1},z_{2},x_{1})=x_{2}(z_{2},x_{1},x^{\infty}_{3}(z_{1},$
$z_{2},x_{1}))$ and
$x^{\infty}_{5}(z_{1},z_{2},x_{1},x_{4})=x_{5}(z_{2},x_{1},x^{\infty}_{2}(z_{1},z_{2},x_{1},x_{4}),x^{\infty}_{3}(z_{1},z_{2},x_{1},x_{4}),$
$x_{4},$ $x^{\infty}_{6}(z_{1},z_{2},x_{1},$ $x_{4}))$. This implies that for
all $(z_{1},z_{2})\in{\makebox{\boldmath$z$}}$ and for all $x_{1}$, $x_{4}$:

$\begin{array}[]{rcl}z_{1}&=&f_{1}(x_{1},x^{\infty}_{2}(z_{1},z_{2},x_{1}),x_{3}^{\infty}(z_{1},x_{1},x_{4}),x_{4},x^{\infty}_{5}(z_{1},z_{2},x_{1},x_{4}),x_{6}^{\infty}(z_{1},z_{2},x_{1},x_{4}))\\\
z_{2}&=&f_{2}(x_{1},x^{\infty}_{2}(z_{1},z_{2},x_{1}),x^{\infty}_{3}(z_{1},z_{2},x_{1}),x_{4},x^{\infty}_{5}(z_{1},z_{2},x_{1},x_{4}),x^{\infty}_{6}(z_{1},z_{2},x_{1},x_{4}))\end{array}$

allowing to deduce an inner-approximation of
$R_{\forall\exists\forall\exists}(f)$ since:

$\forall z,\ \forall x_{1},\ \forall x_{4},\ \exists
x_{2}=x_{2}^{\infty}(z_{1},z_{2},x_{1}),\ \exists
x_{3}=x_{3}^{\infty}(z_{1},z_{2},x_{1}),\\\ \exists
x_{5}=x_{5}^{\infty}(z_{1},z_{2},x_{1},x_{4}),\ \exists
x_{6}=x_{6}^{\infty}(z_{1},z_{2},x_{1},x_{4}),\
z=f(x_{1},x_{2},x_{3},x_{4},x_{5},x_{6})$

is equivalent to: $\forall z,\ \forall x_{1},\ \exists
x_{2}=x_{2}^{\infty}(z_{1},z_{2},x_{1}),\ \exists
x_{3}=x_{3}^{\infty}(z_{1},z_{2},x_{1}),\ \forall x_{4},\\\ \exists
x_{5}=x_{5}^{\infty}(z_{1},z_{2},x_{1},x_{4}),\ \exists
x_{6}=x_{6}^{\infty}(z_{1},z_{2},x_{1},x_{4}),\
z=f(x_{1},x_{2},x_{3},x_{4},x_{5},x_{6}).$

In Theorem 3.1, we formalize this for any number of quantifier alternations
and dimension for $z$. The principle is similar to the approach used in [21]
for the joint range in the case of $\forall\exists$ formulas.

As previously, we are going to solve the quantified problem
$R_{{\makebox{\boldmath$p$}}}(f)$ where sets $J_{A}^{i}=\\{k_{2i-1}+1,\ldots
k_{2i}\\}$ and $J_{E}^{i}=\\{k_{2i}+1,\ldots,k_{2i+1}\\}$ for $i=1,\ldots,n$
define the $n$ sequences of indices of variables that are universally
quantified ($J_{A}^{i}$) and existentially quantified ($J_{E}^{i}$).

The principle is to choose for each existentially quantified variable $x_{j}$
a unique component of $f$ (among the $m$ ones) that will be used with an
existential quantifier as one of the $m$ scalar quantified problems to solve.
In the $m-1$ remaining quantified problem, $x_{j}$ will be universally
quantified. This choice is described by the functions $\pi^{i}$ in Theorem
3.1. There are $n$ such functions, one for each existential block appearing in
the quantified problem $R_{{\makebox{\boldmath$p$}}}(f)$. This is Theorem 3 of
[21] generalized to arbitrary alternation of quantifiers $\forall\exists$.

###### Theorem 3.1

Let $f:\mathbb{R}^{u}\rightarrow\mathbb{R}^{m}$ be an elementary function and
$\pi^{i}:\\{k_{2i}+1,\ldots,k_{2i+1}\\}\rightarrow\\{1,\ldots,m\\}$ for
$i=1,\ldots,n$. Let us note, for all $i\in\\{1,\ldots n\\}$,
$j\in\\{1,\ldots,m\\}$
$J_{E,z_{j}}^{i}=\\{l\in\\{k_{2i}+1,\ldots,k_{2i+1}\\},\;\pi^{i}(l)=j\\}$ and
$J_{A,z_{j}}^{i}=\\{k_{2i-1}+1,\ldots,k_{2i}\\}\setminus J_{E,z_{i}}$.
Consider the following $m$ quantified problems, $j\in\\{1,\ldots,m\\}$:

$\forall
z_{j}\in{\makebox{\boldmath$z$}}_{j},\>(\forall{\makebox{\boldmath$x$}}_{l}\in[-1,1])_{l\in
J_{A,z_{j}}^{1}},\>(\exists{\makebox{\boldmath$x$}}_{l}\in[-1,1])_{l\in
J_{E,z_{j}}^{1}},\ldots\\\
\>(\forall{\makebox{\boldmath$x$}}_{l}\in[-1,1])_{l\in
J_{A,z_{j}}^{n}},\>(\exists x_{j}\in[-1,1])_{l\in
J_{E,z_{j}}^{n}},\>z_{i}=f_{i}(x_{1},\ldots,x_{k_{2n}})$

Then
${\makebox{\boldmath$z$}}={\makebox{\boldmath$z$}}_{1}\times{\makebox{\boldmath$z$}}_{2}\times\ldots\times{\makebox{\boldmath$z$}}_{n}$,
if non-empty, is an inner-approximation of $R_{{\makebox{\boldmath$p$}}}(f)$
defined in Equation (2).

The proof is a generalization of the example given in the beginning of this
section, and is detailed in Section 0.K.

###### Remark 7

It is possible to include skewed boxes that can be much tighter than boxes as
in Theorem 3.1, using similar ideas as in [22]. There are also simple
heuristics to be used that allows us not to go through the combinatorics of
potential choices, for getting the best possible inner-approximation. The
sensitivity of the output to variables is computed as part of our algorithm
and the best choices of quantifiers are the ones which quantify universally
the variables for which there is lower sensitivity, and which quantify
existentially the variables for which there is higher sensitivity, giving
higher contributions to the inner-approximations.

###### Example 7

Consider the function
$f=(f_{1},f_{2}):\mathbb{R}^{4}\rightarrow\mathbb{R}^{2}$:

$\begin{array}[]{rcl}f_{1}(x_{1},x_{2},x_{3},x_{4})&=&2+2x_{1}+x_{2}+3x_{3}+x_{4}\\\
f_{2}(x_{1},x_{2},x_{3},x_{4})&=&-1-x_{1}-x_{2}+x_{3}+5x_{4}\end{array}$

We want to find the disturbance set

$R_{\exists\forall\exists}(f)=\\{z\in\mathbb{R}^{2}|\exists x_{1}\in[-1,1],\
\forall x_{2}\in[-1,1],\ \exists x_{3}\in[-1,1],\\\ \exists x_{4}\in[-1,1],\
z=f(x_{1},x_{2},x_{3},x_{4})\\}$ (14)

An outer-approximation for $R_{\exists\forall\exists}(f)$ is found to be
$[-3,7]\times[-7,5]$, using a the 1D computation of the previous section, one
component at a time.

Now, there are several possible quantified formulas giving a 2D inner-
approximation. One of them is,

$\displaystyle\framebox{$\exists x_{1}$},\ \forall x_{2},\ \forall x_{4},\
\framebox{$\exists x_{3}$},\ z_{1}=f_{1}(x_{1},x_{2},x_{3},x_{4})$ (15)
$\displaystyle\forall x_{1},\ \forall x_{2},\ \forall x_{3},\
\framebox{$\exists x_{4}$},\ z_{2}=f_{2}(x_{1},x_{2},x_{3},x_{4})$ (16)

The conditions of Proposition 1 for obtaining a non-empty inner-approximation
are met and we get for Equation (26):

$\begin{array}[]{ccccccccc}{[}&z_{1}^{c}&-||\Delta_{x_{1}}||&+||\Delta_{x_{2},x_{4}}||&-||\Delta_{x_{3}}||,&z_{1}^{c}&+||\Delta_{x_{1}}||&-||\Delta_{x_{2},x_{4}}||&+||\Delta_{x_{3}}||]\\\
={[}&2&-2&+1+1&-3,&2&+2&-1-1&+3]\end{array}$

which is equal to $[-1,5]$, and for Equation (27):

$z_{1}$$z_{2}$$z^{0}$$z^{1}$$z^{2}$$z^{3}$$z^{4}$$z^{5}$$z^{6}$$z^{7}$$z^{8}$$z^{9}$$z^{10}$$z^{11}$$z^{12}$$z^{13}$$z^{14}$$z^{15}$

$\begin{array}[]{ccccccc}{[}&z_{2}^{c}&+||\Delta_{x_{1},x_{2},x_{4}}||&-||\Delta_{x_{3}}||,&z_{1}^{c}&-||\Delta_{x_{1},x_{2},x_{4}}||&+||\Delta_{x_{3}}||]\\\
={[}&-1&+1+1+1&-5,&-1&-1-1-1&+5]\end{array}$

which is equal to $[-3,1]$. Hence $[-1,5]\times[-3,1]$ is in the set
$R_{\exists\forall\exists}(f)$.

These inner and outer-approximations, together with the exact robust joint
range, are depicted in the figure on the right-hand side: we represented some
particular points of the image by $z^{1}$ to $z^{13}$; the inner and outer
boxes represent the inner and outer-approximations $[-1,5]\times[-3,1]$ and
$[-3,7]\times[-7,5]$; finally the polyhedron lying in between is the exact
robust image. Other possibilities are discussed in Appendix 0.L.

######  Example 8 (Generalized robust reachability for the Dubbins vehicle)

We consider the following problem, which is a slight space relaxation of the
original problem solved in 1D in Example 5:

$R_{\exists\forall\exists}(\varphi)=\\{(x,y,\theta)\mid\exists
a\in[-0.01,0.01],\ \exists x_{0}\in[-0.1,0.1],\ \exists y_{0}\in[-0.1,0.1],\\\
\exists\theta_{0}\in[-0.01,0.01],\ \forall b_{1}\in[-0.01,0.01],\ \exists
t\in[0,0.5],\ \exists\delta_{2}\in[-1.31e^{-4},1.31e^{-4}],\\\
\exists\delta_{3}\in[-0.005,0.005],\
(x,y,\theta)=\varphi(t;x_{0},y_{0},\theta_{0},a,b_{1})+(0,\delta_{2},\delta_{3})\\}$
(17)

where $\varphi$ is the flow map for the Dubbins vehicle of Example 1. This
means we want to characterize precisely which abscissa $x$ can be reached for
some control $a$, whatever the disturbance $b_{1}$. We allow here a relaxation
in space and will determine an inner-approximation of the sets of ordinate $y$
and angle $\theta$ which can be reached with control $a$ whatever disturbance
$b_{1}$, up to a small tolerance of $1.309\ 10^{-4}$ for the ordinate and
$0.005$ for $\theta$.

The outer-approximation for $R_{\exists\forall\exists}(\varphi)$ is easy to
find from the outer-approximations of each component of $\varphi$ we already
computed in Example 5. We just need to add the extra contributions of
$\delta_{2}$ to $y$ and $\delta_{3}$ to $\theta$, giving

$R_{\exists\forall\exists}(\varphi)\subseteq[-0.10000196,0.60500196]\times[0.1077618,0.1077618]\times[-0.025,0.025]$

In order to find an inner-approximation of
$R_{\exists\forall\exists}(\varphi)$, we interpretet the following quantified
formulas (with the same interval bounds as in Equation (17) for the inputs):

$\forall a,\ \forall y_{0},\forall\theta_{0},\ \framebox{$\exists x_{0}$},\
\forall b_{1},\ \forall\delta_{2},\ \forall\delta_{3},\ \framebox{$\exists
t$},\ x=\varphi_{x}(t;x_{0},y_{0},\theta_{0},a,b_{1})$
$\forall a,\ \forall x_{0},\forall\theta_{0},\ \framebox{$\exists y_{0}$},\
\forall b_{1},\ \forall\delta_{3},\ \forall t,\
\framebox{$\exists\delta_{2}$},\
y=\varphi_{y}(t;x_{0},y_{0},\theta_{0},a,b_{1})+\delta_{2}$
$\forall x_{0},\ \forall y_{0},\framebox{$\exists\theta_{0},\ \exists a$},\
\forall b_{1},\ \forall\delta_{2},\ \forall t,\
\framebox{$\exists\delta_{3}$},\
\theta=\varphi_{\theta}(t;x_{0},y_{0},\theta_{0},a,b_{1})+\delta_{3}\mbox{ and
find}$

$[-0.0949993455,0.5899993275]\times[-0.0925,0.0925]\
\times[-0.01,0.01]\subseteq R_{\exists\forall\exists}(\varphi)$.

Note that we were not able to obtain an estimate of the solution of this joint
quantified problem (translated using the linearisation for $\varphi$ of
Example 3) with Mathematica, it resulted in a timeout.

##  4 Implementation and benchmarks

We implemented the method, including the non-linear case of Theorem 2.1 and
the vector-valued case of Theorem 3.1 in Julia, using packages LazySets for
manipulating boxes (Hyperrectangles) and Symbolics for automatic
differentiation.

Table 1: Benchmark for quantified reachability problems Benchmark | # vars | dim | # alternations | non-linear | time (s) | inner/sample | outer/sample
---|---|---|---|---|---|---|---
Ex11 | 3 | 1 | 2 | ✓ | 0.29 | 0.33 | 2.12
Ex4 | 4 | 1 | 2 | ✓ | 0.32 | 1 | 1.03
Ex7 | 4 | 2 | 2 |  | 0.21 | (0.78,0.40) | (1.30,1.21)
Linear-2 | 4 | 1 | 2 |  | 0.43 | 1 | 1
Linear-5 | 10 | 1 | 5 |  | 0.4 | 1 | 1
Linear-10 | 20 | 1 | 10 |  | 0.41 | 1 | 1
Linear-25 | 50 | 1 | 25 |  | 0.47 | 1 | 1
Linear-50 | 100 | 1 | 50 |  | 0.58 | 1 | 1
Linear-100 | 200 | 1 | 100 |  | 0.91 | 1 | 1
Linear-500 | 1000 | 1 | 500 |  | 8.1 | 1 | 1
Linear-1000 | 2000 | 1 | 1000 |  | 28.25 | 1 | 1
Motion-2 | 7 | 1 | 3 | ✓ | 0.62 | – | –
Motion-5 | 14 | 1 | 6 | ✓ | 0.76 | – | –
Motion-10 | 24 | 1 | 11 | ✓ | 1.06 | – | –
Motion-25 | 54 | 1 | 26 | ✓ | 9.4 | – | –
Motion-50 | 104 | 1 | 51 | ✓ | 148.68 | – | –

We ran benchmarks reported in Table 1 on a Macbook Pro 2.3GHz Intel core i9
with 8 cores, measuring timings using the Benchmark Julia package. The colums
# vars, dim, # alternations, non-linear, time, inner/sample, outer/sample
denote, respectively, for each benchmark, the number of quantified variables,
the dimension of the image of the function considered, the number of
alternations $\forall$/$\exists$, whether the function considered is non-
linear or not, the time the analyzer took to compute both the inner and the
outer-approximation of the quantified reachability problem, the estimated
ratio of the width of the inner-approximation, then the outer-approximation,
for each component of the function, with respect to the estimate using
sampling222Sampling is too slow and imprecise when the number of variables
grows, hence we could not use it in the case of Motion-$k$, $k>2$. For
Motion-2, it terminates but with at most 30 samples per dimension, and in
dimension 7, this is not representative. In the case of Linear-$k$, the
estimate is always one since our method is exact in 1D, for linear functions..

In this table, Ex$k$ correspond to Example $k$ of this paper, Linear-$k$ are
random linear functions on $2k$ variables, quantified as $\forall,\ \exists$
$k$ times, and Motion-2 to 50 are several instances of a motion planning
problem of the same type as the one of Equation 7. Motion-$k$ consists of the
$x$ component of the same perturbed Dubbins vehicle as modeled in Example 1,
see Appendix 0.M, with $k$ control steps, generating $3+2k$ variables and
$k+1$ quantifier alternations. These variables are the $k$ (angular) controls
$a_{i}$, the $k$ perturbations $b_{i}$ and the two initial conditions on $x$
and $\theta$. The function, from $\mathbb{R}^{4+2k}$ to $\mathbb{R}$, that
expresses the dynamics at the $k$th control step is a sum of $2k$ sine
functions evaluated on sums of 1 to $k+1$ variables, plus a sum of $k+1$
variables.

The theoretical complexity of our method, both for inner and for outer-
approximation, for a $n$ dimensional vector-valued quantified problem on $p$
quantified variables, is of the order of $n$ times the complexity of a 1D
quantified problem on $p$ quantified variables. Each of these 1D problems has
a cost of the order of $p$ times the cost of the evaluation of the function on
a (center) point plus the cost of evaluation of its Jacobian on an interval.
In the Linear-$k$ problem, the cost of evaluation of the function on a point
is of the order of $k$, and for the Jacobian, apart from the cost of the
automatic differentiation, it is of the order of $k$ again. The resolution
time can slightly decrease for higher-dimensional problems, which is due to
the fact that some of these random problems are found to have empty quantified
reachable sets already with few quantifiers. In the Motion-$k$ problem, which
has always a non-empty quantified reachable set, the cost of evaluation of the
function on a point is of the order of $k^{2}$, and for the Jacobian, it is of
the order of $k^{3}$ without the cost of the automatic differentiation.

##  5 Conclusion

In this article, we designed a method for inner and outer-approximating
general problems, which is essentially an order 0 method, generalizing mean-
value theorems. In future work, we are planning on describing higher order
methods, generalizing again the higher order methods of [22]. We will also
consider preconditioning and quadrature formulas for general quantified
formulas.

Finally, we intend to generalize this work to other kinds of quantified
problems where the objective is to find a set $R$ such that the quantified
predicate is
$f({\makebox{\boldmath$x$}}_{1},{\makebox{\boldmath$x$}}_{2},\ldots,{\makebox{\boldmath$x$}}_{{2n}})\in
R$, and not an equality predicate as in this work. This should be most useful
for finding generalized invariant sets, in addition to generalized reachable
sets.

## References

  * [1] Chaouki Abdallah, Peter Dorato, and Wei Yang.  Applications of quantifier elimination theory to control system design.  02 1970.
  * [2] M. Althoff.  Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets.  In HSCC, pages 173–182. ACM publishers, 2013.
  * [3] M. Althoff, C. Le Guernic, and B. H. Krogh.  Reachable set computation for uncertain time-varying linear systems.  In International Conference on Hybrid Systems: Computation and Control, pages 93––102, 2011.
  * [4] M. Althoff, O. Stursberg, and M. Buss.  Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization.  In Proceedings of CDC, pages 4042–4048, 2008.
  * [5] S. Bansal, M. Chen, S. L. Herbert, and C. J. Tomlin.  Hamilton-jacobi reachability: A brief overview and recent advances.  In CDC, 2017.
  * [6] Christopher W. Brown.  Qepcad b: A program for computing with semi-algebraic sets using cads.  SIGSAM Bull., 37(4):97–108, dec 2003.
  * [7] X. Chen, E. Ábrahám, and S. Sankaranarayanan.  Taylor model flowpipe construction for non-linear hybrid systems.  In RTSS, 2012.
  * [8] X. Chen, S. Sankaranarayanan, and E. Abraham.  Under-approximate flowpipes for non-linear continuous systems.  In FMCAD, 2014.
  * [9] George E. Collins.  Quantifier elimination for real closed fields by cylindrical algebraic decompostion.  In H. Brakhage, editor, Automata Theory and Formal Languages, pages 134–183, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg.
  * [10] Andreas Dolzmann and Thomas Sturm.  Redlog: Computer algebra meets computer logic.  SIGSAM Bull., 31(2):2–9, jun 1997.
  * [11] Alexandre Donzé.  On signal temporal logic.  In RV, volume 8174 of LNCS. Springer, 2013.
  * [12] Georgios E. Fainekos and George J. Pappas.  Robustness of temporal logic specifications for continuous-time signals.  Theor. Comput. Sci., 410(42), 2009.
  * [13] Sicun Gao, Soonho Kong, and Edmund Clarke.  dreal: An smt solver for nonlinear theories of the reals (tool paper).  In CADE (Conference on Automated Deduction), 2013.
  * [14] Yeting Ge and Leonardo de Moura.  Complete instantiation for quantified formulas in satisfiability modulo theories.  In Computer Aided Verification, pages 306–320, 2009.
  * [15] A. Girard, C. Le Guernic, and O. Maler.  Efficient computation of reachable sets of linear time-invariant systems with inputs.  In HSCC, 2006.
  * [16] A. Goldsztejn, D. Daney, M. Rueher, and P. Taillibert.  Modal intervals revisited: a mean-value extension to generalized intervals.  In QCP’05, 2005.
  * [17] A. Goldsztejn and L. Jaulin.  Inner approximation of the range of vector-valued functions.  Reliable Computing, 14, 2010.
  * [18] Alexandre Goldsztejn.  Modal intervals revisited, part 1: A generalized interval natural extension.  Reliable Computing, 16:130–183, 2012.
  * [19] Alexandre Goldsztejn.  Modal intervals revisited, part 2: A generalized interval mean value extension.  Reliable Computing, 16:184–209, 2012.
  * [20] Eric Goubault and Sylvie Putot.  Inner and outer reachability for the verification of control systems.  In Necmiye Ozay and Pavithra Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pages 11–22. ACM, 2019.
  * [21] Eric Goubault and Sylvie Putot.  Robust under-approximations and application to reachability of non-linear control systems with disturbances.  IEEE Control. Syst. Lett., 4(4):928–933, 2020.
  * [22] Eric Goubault and Sylvie Putot.  Tractable higher-order under-approximating AE extensions for non-linear systems.  In 7th IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2021, Brussels, Belgium, July 7-9, 2021, pages 235–240, 2021\.
  * [23] C. Le Guernic and A. Girard.  Reachability analysis of hybrid systems using support functions.  In CAV, 2009.
  * [24] Wolfram Research, Inc.  Mathematica, Version 13.1.  Champaign, IL, 2022.
  * [25] Mats Jirstrand.  Nonlinear control system design by quantifier elimination.  J. Symb. Comput., 24:137–152, 1997.
  * [26] Niklas Kochdumper and Matthias Althoff.  Computing non-convex inner-approximations of reachable sets for nonlinear continuous systems.  In 2020 59th IEEE Conference on Decision and Control (CDC), pages 2130–2137, 2020.
  * [27] A. B. Kurzhanski and P. Varaiya.  Ellipsoidal techniques for reachability analysis.  In HSCC, 2000.
  * [28] Steven M. Lavalle.  Planning Algorithms.  Cambridge University Press, 2006.
  * [29] M. Li, P.N. Mosaad, M. Fränzle, Z. She, and B. Xue.  Safe over- and under- approximation of reachable sets for autonomous dynamical systems.  In FORMATS, pages 252––270, 2018.
  * [30] K. Makino and M. Berz.  Taylor models and other validated functional inclusion methods.  Int. J. Pure Appl. Math, 2003.
  * [31] Thomas Le Mézo, Luc Jaulin, and Benoît Zerr.  Bracketing the solutions of an ordinary differential equation with uncertain initial conditions.  Applied Mathematics and Computation, 318, 2018.
  * [32] I. Mitchell, A. Bayen, and C. Tomlin.  A time-dependent hamilton–jacobi formulation of reachable sets for continuous dynamic games.  IEEE Transactions on Automatic Control, 50(7):947––957, 2005\.
  * [33] M. Neher, K. R. Jackson, and N. S. Nedialkov.  On taylor model based integration of odes.  SIAM J. Numer. Anal, 45, 2007.
  * [34] Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, and Taylor T. Johnson.  Hyperproperties of real-valued signals.  In MEMOCODE ’17, 2017.
  * [35] M. A. Ben Sassi, R. Testylier, T. Dang, and A. Girard.  Reachability analysis of polynomial systems using linear programming relaxations.  volume 7561 of LNCS, 2012.
  * [36] Jacob T Schwartz and Micha Sharir.  On the “piano movers” problem. ii. general techniques for computing topological properties of real algebraic manifolds.  Advances in Applied Mathematics, 4(3):298–351, 1983.
  * [37] K. Siaulys and J. M. Maciejowski.  Verification of model predictive control laws using weispfenning’s quantifier elimination by virtual substitution algorithm.  In 2016 IEEE 55th Conference on Decision and Control (CDC), pages 1452–1457, 2016.
  * [38] Thomas Sturm and Ashish Tiwari.  Verification and synthesis using real quantifier elimination.  In Proc. ISSAC 2011, page 329, San Jose, United States, June 2011\. ACM Press.
  * [39] A. Tarski.  A decision method for elementary algebra and geometry.  Technical report, Rand Corporation, 1948.
  * [40] B. Xue, Z. She, and A. Easwaran.  Under-approximating backward reachable sets by polytopes.  In CAV, 2016.

##  Appendix 0.A Mathematica expressions used in the Examples

The quantified problem for calculating the outer-approximation of Example 3 is
expressed in Mathematica as:

$\text{Reduce}\left[\exists\\{\epsilon_{7},\epsilon_{1},\epsilon_{4},\epsilon_{6}\\},\epsilon_{7}\geq-1\land\epsilon_{7}\leq
1\land\epsilon_{1}\geq-1\right.\\\ \land\epsilon_{1}\leq
1\land\epsilon_{4}\geq-1\land\epsilon_{4}\leq
1\land\epsilon_{6}\geq-1\land\epsilon_{6}\leq 1,\\\
\forall{\epsilon_{2},\epsilon_{2}\geq-1\land\epsilon_{2}\leq 1}\\\
\exists{\\{t,\epsilon_{3},\epsilon_{5}\\},t\geq 0\land t\leq
0.5\land\epsilon_{3}\geq-1\land\epsilon_{3}\leq
1\land\epsilon_{5}\geq-1\land\epsilon_{5}\leq 1}\\\
\left(x=0.1\epsilon_{1}+(1+0.01\epsilon_{2})t+\text{1.31
10${}^{-7}$}\epsilon_{3}t^{2}\right.\\\ \land
y=0.1\epsilon_{4}+(0.01\epsilon_{6}+0.01\epsilon_{7}t)t+0.05\epsilon_{5}t^{2}\\\
\left.\land\left.theta=0.01\epsilon_{6}+0.01\epsilon_{7}t\right),\\{y,z,u\\},\mathbb{R}\right]$

For the outer-approximations of each component of $\varphi$, we have the
following Mathematica problems, for $\varphi_{x}$ first:

$\texttt{Timing}[\texttt{Reduce}[\texttt{Exists}[\\{e7,e1,e4,e6\\},(e7>=-1)\&\&(e7<=1)\\\
\&\&(e1>=-1)\&\&(e1<=1)\&\&(e4>=-1)\&\&(e4<=1)\\\
\&\&(e6>=-1)\&\&(e6<=1),\texttt{ForAll}[e2,(e2>=-1)\&\&(e2<=1),\\\
\texttt{Exists}[\\{t,e3,e5\\},(t>=0)\&\&(t<=0.5)\\\
\&\&(e3>=-1)\&\&(e3<=1)\&\&(e5>=-1)\&\&(e5<=1),\\\
x==0.1e1+t+0.01e2t+0.000000131e3t^{2}]]],\\{x\\},Reals]]$

Then for $\varphi_{y}$:

$\texttt{Timing}[\texttt{Reduce}[\texttt{Exists}[\\{e7,e1,e4,e6\\},(e7>=-1)\&\&(e7<=1)\\\
\&\&(e1>=-1)\&\&(e1<=1)\&\&(e4>=-1)\&\&(e4<=1)\\\
\&\&(e6>=-1)\&\&(e6<=1),\texttt{ForAll}[e2,(e2>=-1)\&\&(e2<=1),\\\
\texttt{Exists}[\\{t,e3,e5\\},(t>=0)\&\&(t<=0.5)\\\
\&\&(e3>=-1)\&\&(e3<=1)\&\&(e5>=-1)\&\&(e5<=1),\\\
y==0.1e4+(0.01e6+0.01e7t)t+(0.005e5)t^{2}]]],\\{y\\},Reals]]$

And finally for $\varphi_{\theta}$:

$Timing[\texttt{Reduce}[\texttt{Exists}[\\{e7,e1,e4,e6\\},(e7>=-1)\&\&(e7<=1)\\\
\&\&(e1>=-1)\&\&(e1<=1)\&\&(e4>=-1)\&\&(e4<=1)\\\
\&\&(e6>=-1)\&\&(e6<=1),\texttt{ForAll}[e2,(e2>=-1)\&\&(e2<=1),\\\
\texttt{Exists}[\\{t,e3,e5\\},(t>=0)\&\&(t<=0.5)\\\
\&\&(e3>=-1)\&\&(e3<=1)\&\&(e5>=-1)\&\&(e5<=1),\\\
theta==0.01e6+0.01e7t]]],\\{theta\\},Reals]]$

For the inner-approximations of all components of $\varphi$, first for
$\varphi_{x}$, we have:

$Timing[\texttt{Reduce}[\texttt{Exists}[\\{e7,e1,e4,e6\\},(e7>=-1)\&\&(e7<=1)\\\
\&\&(e1>=-1)\&\&(e1<=1)\&\&(e4>=-1)\&\&(e4<=1)\\\
\&\&(e6>=-1)\&\&(e6<=1),\texttt{ForAll}[\\{e2,e3,e5\\},\\\
(e2>=-1)\&\&(e2<=1)\&\&(e3>=-1)\&\&(e3<=1)\\\
\&\&(e5>=-1)\&\&(e5<=1),\texttt{Exists}[\\{t\\},(t>=0)\&\&(t<=0.5),\\\
x==0.1e1+t+0.01e2t+0.000000131e3t^{2}]]],\\{x\\},Reals]]$

Then for $\varphi_{y}$:

$Timing[\texttt{Reduce}[\texttt{Exists}[\\{e7,e1,e4,e6\\},(e7>=-1)\\\
\&\&(e7<=1)\&\&(e1>=-1)\&\&(e1<=1)\&\&(e4>=-1)\&\&(e4<=1)\\\
\&\&(e6>=-1)\&\&(e6<=1),\texttt{ForAll}[\\{e2,e3,e5\\},\\\
(e2>=-1)\&\&(e2<=1)\&\&(e3>=-1)\&\&(e3<=1)\\\
\&\&(e5>=-1)\&\&(e5<=1),\texttt{Exists}[\\{t\\},(t>=0)\&\&(t<=0.5),\\\
y==0.1e4+(0.01e6+0.01e7t)t+(0.005e5)t^{2}]]],\\{y\\},Reals]]$

And finally for $\varphi_{\theta}$:

$Timing[\texttt{Reduce}[\texttt{Exists}[\\{e7,e1,e4,e6\\},(e7>=-1)\&\&(e7<=1)\\\
\&\&(e1>=-1)\&\&(e1<=1)\&\&(e4>=-1)\&\&(e4<=1)\\\
\&\&(e6>=-1)\&\&(e6<=1),\texttt{ForAll}[\\{e2,e3,e5\\},\\\
(e2>=-1)\&\&(e2<=1)\&\&(e3>=-1)\&\&(e3<=1)\\\
\&\&(e5>=-1)\&\&(e5<=1),\texttt{Exists}[\\{t\\},(t>=0)\&\&(t<=0.5),\\\
theta==0.01e6+0.01e7t]]],\\{theta\\},Reals]]$

##  Appendix 0.B Proof of Lemma 1

We distinguish two cases:

  * •

If $Q_{1}=\forall$, then $z\in
S_{n}(\delta_{0};Q_{1},\delta_{1};\ldots;Q_{n},\delta_{n})$ iff $\forall
x_{1}\in[-1,1],\ Q_{2}x_{2}\in[-1,1],\ldots,\ Q_{n}x_{n}\in[-1,1],\
z=f(x_{1},x_{2},$ $\ldots,x_{n})$. This is equivalent to, for all
$x_{1}\in[-1,1]$: $Q_{2}x_{2}\in[-1,1],\ldots,\ Q_{n}x_{n}\in[-1,1],\
z=(\delta_{0}+\delta_{1}x_{1})+\sum\limits_{i=2}^{k}\delta_{i}x_{i}$, hence
$z\in
S_{n-1}(\delta_{0}+\delta_{1}x_{1};Q_{2},\delta_{2};\ldots;Q_{n},\delta_{n})$.
Therefore, this is equivalent to

$z\in\bigcap\limits_{x_{1}\in[-1,1]}S_{n-1}(\delta_{0}+\delta_{1}x_{1};Q_{2},\delta_{2};\ldots;Q_{n},\delta_{n})$

  * •

If $Q_{1}=\exists$, then $z\in
S_{n}(\delta_{0};Q_{1},\delta_{1};\ldots;Q_{n},\delta_{n})$ iff $\exists
x_{1}\in[-1,1],\ Q_{2}x_{2}\in[-1,1],\ldots,\ Q_{n}x_{n}\in[-1,1],\
z=f(x_{1},x_{2},$ $\ldots,x_{n})$. This is equivalent to, for some
$x_{1}\in[-1,1]$: $Q_{2}x_{2}\in[-1,1],\ldots,\ Q_{n}x_{n}\in[-1,1],\
z=(\delta_{0}+\delta_{1}x_{1})+\sum\limits_{i=2}^{k}\delta_{i}x_{i}$, hence
$z\in
S_{n-1}(\delta_{0}+\delta_{1}x_{1};Q_{2},\delta_{2};\ldots;Q_{n},\delta_{n})$
for some $x_{1}\in[-1,1]$. Therefore, this is equivalent to

$z\in\bigcup\limits_{x_{1}\in[-1,1]}S_{n-1}(\delta_{0}+\delta_{1}x_{1};Q_{2},\delta_{2};\ldots;Q_{n},\delta_{n})$

##  Appendix 0.C Proof of Proposition 1

Note first that

$R_{{\makebox{\boldmath$p$}}}(f)=S_{p}(\delta_{0};\forall,{\delta}_{k_{1}+1};\ldots;\forall,{\delta}_{{k}_{2}};\exists,{\delta}_{{k}_{2}+1};\ldots;\\\
\exists,{\delta}_{{k}_{3}};\ldots;\forall,{\delta}_{k_{2n-1}+1};\ldots;\forall,{\delta}_{k_{2n}};\exists,{\delta}_{k_{2n}+1};\ldots;\exists,{\delta}_{k_{2n+1}})$
(18)

where $k_{i}=\sum\limits_{l=1}^{i-1}j_{l}$ for all $i=1,\ldots,2n+1$.

We use the notation $\Delta_{i}$ to improve readability of formula (18), that
we rewrite:
$R_{{\makebox{\boldmath$p$}}}(f)=S_{p}(\delta_{0};\forall,{\Delta}_{1};\exists,{\Delta}_{2};\ldots;\forall,{\Delta}_{{2n-1}};\exists,{\Delta}_{{2n}})$.

The proof uses the induction relation (10) on $S_{n}$. Let us call $P_{2n}$
the property we wish to prove on $R_{{\makebox{\boldmath$p$}}}(f)$ for any
partition ${{\makebox{\boldmath$p$}}}=(j_{1},\ldots,j_{2n})$ of
$p=\sum\limits_{i=1}^{2n}j_{i}$. For all partitions
${{\makebox{\boldmath$p$}}^{\prime}}=(j^{\prime}_{1},\ldots,j^{\prime}_{2n-1})$
of $p^{\prime}=\sum\limits_{i=1}^{2n-1}j^{\prime}_{i}$ and associated
functions $f^{\prime}:\ \mathbb{R}^{p^{\prime}}\rightarrow\mathbb{R}^{m}$ with
$f^{\prime}({{\makebox{\boldmath$x$}}}_{1},{{\makebox{\boldmath$x$}}}_{2},\ldots,{{\makebox{\boldmath$x$}}}_{2n-1})=\delta^{\prime}_{0}+\langle\Delta^{\prime}_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle+\langle\Delta^{\prime}_{2},{{\makebox{\boldmath$x$}}}_{2}\rangle+\ldots+\langle\Delta^{\prime}_{2n-1},{{\makebox{\boldmath$x$}}}_{2n-1}\rangle$,
we define:

$T_{{\makebox{\boldmath$p$}}^{\prime}}(f^{\prime})=S_{p^{\prime}}(\delta^{\prime}_{0};\exists,{\Delta^{\prime}}_{1};\forall,{\Delta^{\prime}}_{2};\exists\Delta^{\prime}_{3};\ldots;\ldots;\forall,{\Delta^{\prime}}_{{2n-2}};\exists,{\Delta^{\prime}}_{{2n-1}})$
(19)

and we will prove the following property $Q_{2n-1}$:

$T_{{\makebox{\boldmath$p$}}^{\prime}}(f^{\prime})=\left[\delta^{\prime}_{0}+\sum\limits_{k=1}^{n-1}\left(||{\Delta^{\prime}}_{2k}||-||{\Delta^{\prime}}_{2k-1}||\right)-||{\Delta^{\prime}}||_{2n-1}\right.,\\\
\left.\delta^{\prime}_{0}+\sum\limits_{k=1}^{n-1}\left(||{\Delta^{\prime}}_{2k-1}||-||{\Delta^{\prime}}_{2k}||\right)+||{\Delta^{\prime}}||_{2n-1}\right]$

if
$||{\Delta^{\prime}}_{2l}||\leq||{\Delta^{\prime}}_{2l+1}||+\sum\limits_{k=l+1}^{n-1}\left(||{\Delta^{\prime}}_{2k+1}||-||{\Delta^{\prime}}_{2k}||\right)$
for $l=1,\ldots,n-1$, otherwise
$T_{{\makebox{\boldmath$p$}}^{\prime}}(f)=\emptyset$.

We first have the base case $P_{0}$ and $Q_{-1}$, which are both equal to
$[\delta_{0},\delta_{0}]$.

We now suppose $Q_{2n-1}$ and $P_{2n}$ and prove $Q_{2n+1}$ and $P_{2n+2}$.
Consider first the case of $Q_{2n+1}$ and, for a function $f^{\prime}:\
\mathbb{R}^{p^{\prime}}\rightarrow\mathbb{R}^{m}$,
$f^{\prime}({{\makebox{\boldmath$x$}}}_{1},\ldots,{{\makebox{\boldmath$x$}}}_{2n+1})=\delta^{\prime}_{0}+\sum\limits_{i=1}^{2n+1}\langle\Delta^{\prime}_{i},{{\makebox{\boldmath$x$}}}_{i}\rangle$
with a partition
${{\makebox{\boldmath$p$}}^{\prime}}=(j^{\prime}_{1},\ldots,j^{\prime}_{2n+1})$
of the arguments of $f^{\prime}$, consider the set:

$T_{{\makebox{\boldmath$p$}}^{\prime}}(f^{\prime})=S_{{p^{\prime}}}(\delta^{\prime}_{0};\exists,{\Delta^{\prime}}_{1};\forall,{\Delta^{\prime}}_{2};\exists,{\Delta^{\prime}}_{3};\ldots;\forall,{\Delta^{\prime}}_{2n};\exists,{\Delta^{\prime}}_{{2n+1}}).$

By the universal quantifier case of Lemma 1 applied $j_{1}$ times, this is
equal to:

$\bigcup\limits_{{{\makebox{\boldmath$x$}}}_{1}\in[-1,1]^{j_{1}}}S_{p^{\prime\prime}}(\delta^{\prime}_{0}+\langle\Delta^{\prime}_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle;\forall,{\Delta^{\prime}}_{2};\exists,{\Delta^{\prime}}_{3};\ldots;\forall,{\Delta^{\prime}}_{2n};\exists,{\Delta^{\prime}}_{{2n+1}})$

where
$S_{p^{\prime\prime}}(\ldots)=R_{{\makebox{\boldmath$p$}}^{\prime\prime}}(f^{\prime\prime})$
with partition
${{\makebox{\boldmath$p$}}^{\prime\prime}}=(j^{\prime}_{2},\ldots,j^{\prime}_{2n+1})$,
$p^{\prime\prime}=\sum\limits_{i=2}^{2n+1}j^{\prime}_{i}$, and
$f^{\prime\prime}({{\makebox{\boldmath$x$}}}_{2},\ldots,{{\makebox{\boldmath$x$}}}_{2n+1})=f^{\prime}({{\makebox{\boldmath$x$}}}_{1},{{\makebox{\boldmath$x$}}}_{2},$
$\ldots,{{\makebox{\boldmath$x$}}}_{2n+1})$.

Then by the induction hypothesis $P_{2n}$ applied to partition
${\makebox{\boldmath$p$}}^{\prime\prime}$, each $S_{p^{\prime\prime}}(\ldots)$
is equal to:

$\delta^{\prime}_{0}+\langle\Delta^{\prime}_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle+\left[\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k-1}||-||{\Delta}_{2k}||\right)\right.,\left.\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k-1}||\right)\right]$

if
$||{\Delta}_{2l-1}||\leq||{\Delta}_{2l}||+\sum\limits_{k=l+1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k-1}||\right)$
for $l=1,\ldots,n$, with $\Delta_{i}=\Delta^{\prime}_{i+1}$, $i=1,\ldots,2n$,
otherwise is equal to the empty set. Substituting $\Delta_{i}$ by
$\Delta^{\prime}_{i+1}$, we obtain for each $S_{p^{\prime\prime}}(\ldots)$:

$\delta^{\prime}_{0}+\langle{\Delta^{\prime}}_{1},x_{1}\rangle+\left[\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k}||-||{\Delta^{\prime}}_{2k+1}||\right)\right.,\left.\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k+1}||-||{\Delta^{\prime}}_{2k}||\right)\right]$

if
$||{\Delta^{\prime}}_{2l}||\leq||{\Delta^{\prime}}_{2l+1}||+\sum\limits_{k=l+1}^{n}\left(||{\Delta^{\prime}}_{2k+1}||-||{\Delta^{\prime}}_{2k}||\right)$
for $l=1,\ldots,n$, otherwise it is empty. Finally,

$\delta^{\prime}_{0}-||{\Delta^{\prime}}_{1}||\leq\delta^{\prime}_{0}+\langle{\Delta^{\prime}}_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle\leq\delta^{\prime}_{0}+||{\Delta^{\prime}}_{1}||$

each bound being reached by some ${{\makebox{\boldmath$x$}}}_{1}$. Hence,

$T_{{\makebox{\boldmath$p$}}^{\prime}}(f^{\prime})=\left[\delta^{\prime}_{0}-||{\Delta^{\prime}}_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k}||-||{\Delta^{\prime}}_{2k+1}||\right)\right.,\\\
\left.\delta^{\prime}_{0}+||{\Delta^{\prime}}_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k+1}||-||{\Delta^{\prime}}_{2k}||\right)\right]$

if
$||{\Delta^{\prime}}_{2l}||\leq||{\Delta^{\prime}}_{2l+1}||+\sum\limits_{k=l+1}^{n}\left(||{\Delta^{\prime}}_{2k+1}||-||{\Delta^{\prime}}_{2k}||\right)$
for $l=1,\ldots,n$, otherwise
$T_{{\makebox{\boldmath$p$}}^{\prime}}(f^{\prime})=\emptyset$. This is
precisely $Q_{2n+1}$ since
$-||{\Delta^{\prime}}_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k}||-||{\Delta^{\prime}}_{2k+1}||\right)=\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k}||-||{\Delta^{\prime}}_{2k-1}||\right)-||{\Delta^{\prime}}||_{2n+1}$
and
$||{\Delta^{\prime}}_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k+1}||-||{\Delta^{\prime}}_{2k}||\right)=\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k-1}||-||{\Delta^{\prime}}_{2k}||\right)+||{\Delta^{\prime}}||_{2n+1}$.

The case of $P_{2n+2}$ is similar, using Lemma 1 and property $Q_{2n+1}$:
suppose again that the induction hypothesis holds, i.e. we suppose $P_{2n}$
and $Q_{2n-1}$, and we prove $Q_{2n+1}$ and $P_{2n+2}$. We proved $Q_{2n+1}$
and we now examine the case of $P_{2n+2}$ and consider the following set,
starting with a function $f:\ \mathbb{R}^{p}\rightarrow\mathbb{R}^{m}$,
$f({{\makebox{\boldmath$x$}}}_{1},\ldots,{{\makebox{\boldmath$x$}}}_{2n+2})=\delta_{0}+\sum\limits_{i=1}^{2n+2}\langle\Delta_{i},{{\makebox{\boldmath$x$}}}_{i}\rangle$
with a partition ${{\makebox{\boldmath$p$}}}=(j_{1},\ldots,j_{2n+2})$ of the
$p=\sum\limits_{i=1}^{2n+2}j_{i}$ arguments of $f$:

$R_{{\makebox{\boldmath$p$}}}(f)=S_{{p}}(\delta_{0};\forall,{\Delta}_{1};\exists,{\Delta}_{2};\ldots;\forall,{\Delta}_{2n+1};\exists,{\Delta}_{{2n+2}})$
(20)

By the existential quantifier case of Lemma 1 applied $j_{1}$ times, this is
equal to (we set $p^{\prime}=\sum\limits_{i=2}^{2n+2}j_{i}$):

$\bigcap\limits_{{{\makebox{\boldmath$x$}}}_{1}\in[-1,1]^{j_{1}}}S_{p^{\prime}}(\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle;\exists,{\Delta}_{2};\forall,{\Delta}_{3};\ldots;\forall,{\Delta}_{2n+1};\exists,{\Delta}_{{2n+2}})$
(21)

As
$S_{p^{\prime}}(\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle;\exists,{\Delta}_{2};\forall,{\Delta}_{3};\ldots;\forall,{\Delta}_{2n+1};\exists,{\Delta}_{{2n+2}})$
is equal to $T_{{\makebox{\boldmath$p$}}^{\prime}}(f^{\prime})$, by Equation
(19), with
$f^{\prime}({{\makebox{\boldmath$x$}}}_{2},\ldots,{{\makebox{\boldmath$x$}}}_{2n+2})=f({{\makebox{\boldmath$x$}}}_{1},{{\makebox{\boldmath$x$}}}_{2},$
$\ldots,{{\makebox{\boldmath$x$}}}_{2n+2})$ and
${{\makebox{\boldmath$p$}}^{\prime}}=(j_{2},\ldots,j_{2n+2})$ is a partition
of $p^{\prime}=\sum\limits_{i=2}^{2n+2}j_{i}$, by the induction hypothesis
$Q_{2n+1}$ applied to partition ${\makebox{\boldmath$p$}}^{\prime}$, each
$S_{p^{\prime}}(\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle;\exists,{\Delta}_{2};\forall,{\Delta}_{3};\ldots;\forall,{\Delta}_{2n+1};\exists,{\Delta}_{{2n+2}})$
is equal to:

$\left[\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle+\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k}||-||{\Delta^{\prime}}_{2k-1}||\right)-||{\Delta^{\prime}}||_{2n+1}\right.,\\\
\left.\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle+\sum\limits_{k=1}^{n}\left(||{\Delta^{\prime}}_{2k-1}||-||{\Delta^{\prime}}_{2k}||\right)+||{\Delta^{\prime}}||_{2n+1}\right]$

if
$||{\Delta^{\prime}}_{2l}||\leq||{\Delta^{\prime}}_{2l+1}||+\sum\limits_{k=l+1}^{n-1}\left(||{\Delta^{\prime}}_{2k+1}||-||{\Delta^{\prime}}_{2k}||\right)$
for $l=1,\ldots,n-1$ (otherwise, is equal to the empty set), with
$\Delta^{\prime}_{i}=\Delta_{i+1}$, for all $i=1,\ldots,2n+1$,
$\Delta^{\prime}_{1}=\Delta_{1}$ and $\delta^{\prime}_{0}=\delta_{0}$.

Replacing $\Delta^{\prime}_{i}$ by $\Delta_{i+1}$, $\Delta^{\prime}_{1}$ by
$\Delta_{1}$ and $\delta^{\prime}_{0}$ by $\delta_{0}$, we obtain the value:

$\left[\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle+\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k+1}||-||{\Delta}_{2k}||\right)-||{\Delta}||_{2n+2}\right.,\\\
\left.\delta_{0}+\langle\Delta_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle+\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k+1}||\right)+||{\Delta}||_{2n+2}\right]$
(22)

if
$||{\Delta}_{2l+1}||\leq||{\Delta}_{2l+2}||+\sum\limits_{k=l+1}^{n-1}\left(||{\Delta}_{2k+2}||-||{\Delta}_{2k+1}||\right)$
for $l=1,\ldots,n-1$, otherwise is empty.

Now,

$\delta_{0}-||{\Delta}_{1}||\leq\delta_{0}+\langle{\Delta}_{1},{{\makebox{\boldmath$x$}}}_{1}\rangle\leq\delta_{0}+||{\Delta}_{1}||$

each bound being reached by some ${{\makebox{\boldmath$x$}}}_{1}$, and the
intersection of the intervals of Equation (22), where
${{\makebox{\boldmath$x$}}}_{1}$ varies over $[-1,1]^{j_{1}}$ is
$R_{{\makebox{\boldmath$p$}}}(f)$ by Equation (21):

$R_{{\makebox{\boldmath$p$}}}(f)=\left[\delta_{0}+||\Delta_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k+1}||-||{\Delta}_{2k}||\right)-||{\Delta}||_{2n+2}\right.,\\\
\left.\delta_{0}-||\Delta_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k+1}||\right)+||{\Delta}||_{2n+2}\right]$

when
$||{\Delta}_{2l+1}||\leq||{\Delta}_{2l+2}||+\sum\limits_{k=l+1}^{n-1}\left(||{\Delta}_{2k+2}||-||{\Delta}_{2k+1}||\right)$
for $l=1,\ldots,n-1$, which is exactly $P_{2n+2}$ since:

$\delta_{0}+||{\Delta}_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k+1}||-||{\Delta}_{2k}||\right)-||{\Delta}||_{2n+2}=\delta_{0}+\sum\limits_{k=1}^{n+1}\left(||{\Delta}_{2k-1}||-||{\Delta}_{2k}||\right)$

and,

$\delta_{0}-||\Delta_{1}||+\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k+1}||\right)+||{\Delta}||_{2n+2}\\\
=\sum\limits_{k=1}^{n+1}\left(||{\Delta}_{2k}||-||{\Delta}_{2k-1}||\right)$

Finally, note, that $R_{{\makebox{\boldmath$p$}}}(f)$ is not empty if and only
if
$||{\Delta}_{2l+1}||\leq||{\Delta}_{2l+2}||+\sum\limits_{k=l+1}^{n-1}\left(||{\Delta}_{2k+2}||-||{\Delta}_{2k+1}||\right)$
for $l=1,\ldots,n-1$ as before, which is equivalent to:
$||{\Delta}_{2l-1}||\leq||{\Delta}_{2l}||+\sum\limits_{k=l}^{n}\left(||{\Delta}_{2k+2}||-||{\Delta}_{2k+1}||\right)$
for $l=2,\ldots,n-1$ and if the radius of $R_{{\makebox{\boldmath$p$}}}(f)$ is
positive i.e.

$||\Delta_{1}||\leq\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k}||-||{\Delta}_{2k+1}||\right)+||{\Delta}||_{2n+2}$

which is equivalent to:

$||{\Delta}_{1}||\leq||{\Delta}_{2}||+\sum\limits_{k=1}^{n}\left(||{\Delta}_{2k+2}||-||{\Delta}_{2k+1}||\right)$

which is
$||{\Delta}_{2l-1}||\leq||{\Delta}_{2l}||+\sum\limits_{k=l}^{n}\left(||{\Delta}_{2k+2}||-||{\Delta}_{2k+1}||\right)$
for $l=1$. Overall, the non-vacuity condition for
$R_{{\makebox{\boldmath$p$}}}(f)$ amounts to:

$||{\Delta}_{2l-1}||\leq||{\Delta}_{2l}||+\sum\limits_{k=l}^{n}\left(||{\Delta}_{2k+2}||-||{\Delta}_{2k+1}||\right)$

for $l=1,\ldots,n$.

##  Appendix 0.D Difference between $\forall,\ \exists$ and $\exists,\
\forall$ in the linear case

######  Example 9 (Difference between $\forall,\exists$ and $\exists,\forall$)

Consider, for a function $f$ from $\mathbb{R}^{2}$ to $\mathbb{R}$ the sets
$R_{\forall\exists}(f)=\\{z\ |\ \forall x_{2},\ \exists x_{1},\
z=f(x_{1},x_{2})\\}$ and $R_{\exists\forall}(f)=\\{z\ |\ \exists x_{1},\
\forall x_{2},\ z=f(x_{1},x_{2})\\}$. In any case,
$R_{\exists\forall}(f)\subseteq R_{\forall\exists}(f)$. We consider the affine
function $f(x_{1},x_{2})=a+bx_{1}+cx_{2}$. It is easy to see that

  * •

$R_{\exists\forall}(f)=\emptyset$ if $c\neq 0$, since $z\in
R_{\exists\forall}(f)$ implies $\exists x_{1}$ such that e.g. for $x_{2}=0$,
$f(x_{1},0)=z$, and for e.g. $x_{2}=1$, $f(x_{1},1)=z$. Hence
$a+bx_{1}=z=a+c+bx_{1}$ implying $c=0$. Conversely, if $c=0$,
$R_{\exists\forall}(f)=[a-|b|,a+|b|]$,

  * •

$R_{\forall\exists}(f)=[a+|c|-|b|,a-|c|+|b|]$ if $|c|\leq|b|$, otherwise it is
empty.

Hence in the linear case, either $c\neq 0$ and
$R_{\exists\forall}(f)=\emptyset\neq R_{\forall\exists}(f)$ or
$R_{\exists\forall}(f)=R_{\forall\exists}(f)$.

##  Appendix 0.E Proof of Proposition 2

Note first that, trivially,

$f({x}_{1},\ldots,{x}_{p})=f(0,\ldots,0)+\sum\limits_{j=1}^{p}h^{x_{1},\ldots,x_{j-1}}({x}_{j})$

Consider now
$z\in{\mathcal{C}}({{\makebox{\boldmath$O$}}}_{1},{{\makebox{\boldmath$I$}}}_{2},\ldots,0_{2n-1},{{\makebox{\boldmath$I$}}}_{2n})$.
Take any ${{\makebox{\boldmath$x$}}}_{1}$ in $[-1,1]^{j_{1}}$. As
${{\makebox{\boldmath$O$}}}_{1}$ is an outer-approximation of
$range(h)\times\ldots\times range(h^{x_{1},\ldots,x_{k_{2}}})$,
$h({{\makebox{\boldmath$x$}}}_{1})=\mathop{\Pi}\limits_{j=1}^{k_{2}}h^{x_{1},\ldots,x_{j-1}}({{\makebox{\boldmath$x$}}}_{1})\in{{\makebox{\boldmath$O$}}}_{1}$,
and there exists ${\alpha}_{2}\in{{\makebox{\boldmath$I$}}}_{2}$, such that
$\forall{\alpha}_{3}\in{{\makebox{\boldmath$O$}}}_{3},\ \ldots,$
$\exists{\alpha}_{2n}\in{{\makebox{\boldmath$I$}}}_{2n}$ with
$z=h({{\makebox{\boldmath$x$}}}_{1})+\alpha_{2}+\ldots+\alpha_{2n}$.

But each component of ${{\makebox{\boldmath$I$}}}_{2}$ is an inner-
approximation of range of $h^{x_{k_{2}+1},\ldots,x_{j-1}}$ for some
$j\in[k_{2}+1,\ldots,k_{3}-1]$, so there exists
${{\makebox{\boldmath$x$}}}_{2}\in[-1,1]^{j_{2}}$ such that $\alpha_{2}$ is
the image of ${{\makebox{\boldmath$x$}}}_{2}$ by
$h^{{{\makebox{\boldmath$x$}}}_{1}}=\mathop{\Pi}\limits_{j=k_{2}+1}^{k_{3}-1}h^{x_{k_{2}+1},\ldots,x_{j}}$.
Therefore we have so far $\forall{{\makebox{\boldmath$x$}}}_{1}$,
$\exists{{\makebox{\boldmath$x$}}}_{2}$ such that
$\forall{\alpha}_{3}\in{{\makebox{\boldmath$O$}}}_{3},\
\ldots,\exists{\alpha}_{2n}\in{{\makebox{\boldmath$I$}}}_{2n}$ with
$z=h({{\makebox{\boldmath$x$}}}_{1})+h^{{{\makebox{\boldmath$x$}}}_{1}}({{\makebox{\boldmath$x$}}}_{2})+\alpha_{3}+\ldots+\alpha_{2n}$.

We carry on inductively to find that
$z\in{\mathcal{C}}({{\makebox{\boldmath$O$}}}_{1},{{\makebox{\boldmath$I$}}}_{2},\ldots,0_{2n-1},{{\makebox{\boldmath$I$}}}_{2n})$
is such that $\forall{{\makebox{\boldmath$x$}}}_{1}$,
$\exists{{\makebox{\boldmath$x$}}}_{2}$, $\ldots$,
$\exists{{\makebox{\boldmath$x$}}}_{2n}$,
$z=h({{\makebox{\boldmath$x$}}}_{1})+\ldots+h^{{{\makebox{\boldmath$x$}}}_{1},\ldots,{{\makebox{\boldmath$x$}}}_{2n-1}}({{\makebox{\boldmath$x$}}}_{2n})$,
i.e.
$z=f({{\makebox{\boldmath$x$}}}_{1},\ldots,{{\makebox{\boldmath$x$}}}_{2n})-f(0,\ldots,0)$.
Thus $z+f(0,\ldots,0)\in R_{\bf p}(f)$.

The case of outer-approximations of $R_{\bf p}(f)$ is similar.

##  Appendix 0.F Proof of Theorem 2.1

Writing $A_{l}=[\underline{A}_{l},\overline{A}_{l}]$ for $l=1,\ldots,p$, and
${{\makebox{\boldmath$A$}}}_{i}=(A_{k_{i}+1},\ldots,A_{k_{i+1}})$, for
$i=1,\ldots,2n$, we have

${\mathcal{C}}({{\makebox{\boldmath$A$}}}_{1},\ldots,{{\makebox{\boldmath$A$}}}_{2n})=S_{p}\left(\sum\limits_{j=1}^{p}\frac{\overline{A}_{j}+\underline{A}_{j}}{2};\forall,\frac{\overline{{\makebox{\boldmath$A$}}}_{1}-\underline{{\makebox{\boldmath$A$}}}_{1}}{2};\right.\\\
\left.\exists,\frac{\overline{{\makebox{\boldmath$A$}}}_{2}-\underline{{\makebox{\boldmath$A$}}}_{2}}{2};\ldots;\exists,\frac{\overline{{\makebox{\boldmath$A$}}}_{2n}-\underline{{\makebox{\boldmath$A$}}}_{2n}}{2}\right)$

where the arithmetic operations on vectors ${{\makebox{\boldmath$A$}}}_{j}$
are taken componentwise. Thus, by Equation (18),
$C({{\makebox{\boldmath$A$}}}_{1},\ldots,{{\makebox{\boldmath$A$}}}_{2n})=R_{{\makebox{\boldmath$p$}}}(f)$
with
$f({{\makebox{\boldmath$x$}}}_{1},\ldots,{{\makebox{\boldmath$x$}}}_{2n})=\sum\limits_{j=1}^{p}\frac{\overline{A}_{j}+\underline{A}_{j}}{2}+\left\langle\frac{\overline{{\makebox{\boldmath$A$}}}_{1}-\underline{{\makebox{\boldmath$A$}}}_{1}}{2},{{\makebox{\boldmath$x$}}}_{1}\right\rangle+\ldots\left\langle\frac{\overline{{\makebox{\boldmath$A$}}}_{2n}-\underline{{\makebox{\boldmath$A$}}}_{2n}}{2},{{\makebox{\boldmath$x$}}}_{2n}\right\rangle$.

Therefore, by Proposition 1,
${\mathcal{C}}({{\makebox{\boldmath$O$}}}_{1},{{\makebox{\boldmath$I$}}}_{2},\ldots,{{\makebox{\boldmath$O$}}}_{2n-1},{{\makebox{\boldmath$I$}}}_{2n})$
is equal to:

$\sum\limits_{l=1}^{n}\left(\sum\limits_{j=k_{2l-1}+1}^{k_{2l}}\frac{\overline{O}_{j}+\underline{O}_{j}}{2}+\sum\limits_{j=k_{2l}+1}^{k_{2l+1}}\frac{\overline{I}_{j}+\underline{I}_{j}}{2}\right)+\\\
\frac{1}{2}\left[\sum\limits_{k=1}^{n}\left(||\overline{{\makebox{\boldmath$O$}}}_{2k-1}-\underline{{\makebox{\boldmath$O$}}}_{2k-1}||-||\overline{{\makebox{\boldmath$I$}}}_{2k}-\underline{{\makebox{\boldmath$I$}}}_{2k}||\right)\right.,\\\
\left.\sum\limits_{k=1}^{n}\left(||\overline{{\makebox{\boldmath$I$}}}_{2k}-\underline{{\makebox{\boldmath$I$}}}_{2k}||-||\overline{{\makebox{\boldmath$O$}}}_{2k-1}-\underline{{\makebox{\boldmath$O$}}}_{2k-1}||\right)\right]$
(23)

if
$||\overline{{\makebox{\boldmath$O$}}}_{2l-1}-\underline{{\makebox{\boldmath$O$}}}_{2l-1}||\leq||\overline{{\makebox{\boldmath$I$}}}_{2l}-\underline{{\makebox{\boldmath$I$}}}_{2l}||+\sum\limits_{k=l+1}^{n}\left(||{\overline{{\makebox{\boldmath$I$}}}}_{2k}-\underline{{\makebox{\boldmath$I$}}}_{2k}||-||{\overline{{\makebox{\boldmath$O$}}}}_{2k-1}-{\underline{{\makebox{\boldmath$O$}}}}_{2k-1}||\right)$
for $l=1,\ldots,n$, otherwise, is empty. This is equivalent to
$\sum\overline{{\makebox{\boldmath$O$}}}_{2l-1}-\sum\underline{{\makebox{\boldmath$O$}}}_{2l-1}\leq\sum\limits_{k=l}^{n}\sum\left(\overline{{\makebox{\boldmath$I$}}}_{2k}-\underline{{\makebox{\boldmath$I$}}}_{2k}\right)-\sum\limits_{k=l+1}^{n}\sum\left(\overline{{\makebox{\boldmath$O$}}}_{2k-1}-\underline{{\makebox{\boldmath$O$}}}_{2k-1}\right)$
for $l=1,\ldots,n$.

The left bound of the interval in Equation (23) above is equal to:

$\sum\limits_{l=1}^{n}\left(\sum\limits_{j=k_{2l-1}+1}^{k_{2l}}\frac{\overline{O}_{j}+\underline{O}_{j}}{2}+\sum\limits_{j=k_{2l}+1}^{k_{2l+1}}\frac{\overline{I}_{j}+\underline{I}_{j}}{2}\right)+\\\
\frac{1}{2}\sum\limits_{k=1}^{n}\left(||\overline{{\makebox{\boldmath$O$}}}_{2k-1}-\underline{{\makebox{\boldmath$O$}}}_{2k-1}||-||\overline{{\makebox{\boldmath$I$}}}_{2k}-\underline{{\makebox{\boldmath$I$}}}_{2k}||\right)$

which is equal to:

$\sum\limits_{l=1}^{n}\left(\sum\limits_{j=k_{2l-1}+1}^{k_{2l}}\frac{\overline{O}_{j}+\underline{O}_{j}}{2}+\sum\limits_{j=k_{2l}+1}^{k_{2l+1}}\frac{\overline{I}_{j}+\underline{I}_{j}}{2}\right)+\\\
\sum\limits_{l=1}^{n}\left(\sum\limits_{j=k_{2l-1}+1}^{k_{2l}}\frac{1}{2}||\overline{O}_{j}-\underline{O}_{j}||-\sum\limits_{j=k_{2l}+1}^{k_{2l+1}}\frac{1}{2}||\overline{I}_{j}-\underline{{\makebox{\boldmath$I$}}}_{j}||\right)\\\
=\sum\limits_{l=1}^{n}\left(\sum\limits_{j=k_{2l-1}+1}^{k_{2l}}\left(\frac{\overline{O}_{j}+\underline{O}_{j}}{2}+\frac{1}{2}||\overline{O}_{j}-\underline{O}_{j}||\right)\right.\\\
\left.+\sum\limits_{j=k_{2l}+1}^{k_{2l+1}}\left(\frac{\overline{I}_{j}+\underline{I}_{j}}{2}-\frac{1}{2}||\overline{I}_{j}-\underline{{\makebox{\boldmath$I$}}}_{j}||\right)\right)$

but:

$\begin{array}[]{rcl}\frac{\overline{O}_{j}+\underline{O}_{j}}{2}+\frac{1}{2}||\overline{O}_{j}-\underline{O}_{j}||&=&\overline{O}_{j}\\\
\frac{\overline{I}_{j}+\underline{I}_{j}}{2}-\frac{1}{2}||\overline{I}_{j}-\underline{{\makebox{\boldmath$I$}}}_{j}||&=&\underline{I}_{j}\end{array}$

Therefore, the left bound of the interval of Equation (23) is:

$\sum\limits_{l=1}^{n}\left(\sum\limits_{j=k_{2l-1}+1}^{k_{2l}}\overline{O}_{j}+\sum\limits_{j=k_{2l}+1}^{k_{2l+1}}\underline{I}_{j}\right)=\sum\limits_{l=1}^{n}\left(\sum\overline{{\makebox{\boldmath$O$}}}_{2l-1}+\sum\underline{{\makebox{\boldmath$I$}}}_{2l}\right)$

The right bound of the interval of Equation (23) is treated similarly, and we
find:

$\sum\limits_{l=1}^{n}\left(\sum\limits_{j=k_{2l-1}+1}^{k_{2l}}\underline{O}_{j}+\sum\limits_{j=k_{2l}+1}^{k_{2l+1}}\overline{I}_{j}\right)=\sum\limits_{l=1}^{n}\left(\sum\underline{{\makebox{\boldmath$O$}}}_{2l-1}+\sum\overline{{\makebox{\boldmath$I$}}}_{2l}\right)$

Similarly,
${\mathcal{C}}({{\makebox{\boldmath$O$}}}_{1},{{\makebox{\boldmath$I$}}}_{2},\ldots,{{\makebox{\boldmath$O$}}}_{2n-1},{{\makebox{\boldmath$I$}}}_{2n})$
is found, by echanging the roles of ${{\makebox{\boldmath$O$}}}_{k}$ with
${{\makebox{\boldmath$I$}}}_{k}$, to be equal to:

$\left[\sum\limits_{l=1}^{n}\left(\sum\overline{{\makebox{\boldmath$I$}}}_{2l-1}+\sum\underline{{\makebox{\boldmath$O$}}}_{2l}\right),\sum\limits_{l=1}^{n}\left(\sum\underline{{\makebox{\boldmath$I$}}}_{2l-1}+\sum\overline{{\makebox{\boldmath$O$}}}_{2l}\right)\right]$

This, combined with (11) of Proposition 2 yields the result.

##  Appendix 0.G Difference between $\forall,\ \exists$ and $\exists,\
\forall$ in the non-linear case

######  Example 10 (Difference between $\forall,\exists$ and
$\exists,\forall$)

Consider as in Example 9, for a function $f$ from $\mathbb{R}^{2}$ to
$\mathbb{R}$ the sets $R_{\forall\exists}(f)=\\{z\ |\ \forall x_{2},\ \exists
x_{1},\ z=f(x_{1},x_{2})\\}$ and $R_{\exists\forall}(f)=\\{z\ |\ \exists
x_{1},\ \forall x_{2},\ z=f(x_{1},x_{2})\\}$. In any case,
$R_{\exists\forall}(f)\subseteq R_{\forall\exists}(f)$.

For non-linear $f$, the only difference with the linear case is that there may
be isolated values for $x_{1}$ such that $f(x_{1},x_{2})$ does not depend on
$x_{2}$, which gives a finite set of isolated points for
$R_{\exists\forall}(f)$, while $R_{\forall\exists}(f)$ can be a strict
superset of $R_{\exists\forall}(f)$.

Take $f(x_{1},x_{2})=(x_{1}^{2}-1)x_{2}+x_{1}$ for $x_{1}\in[-1,1]$ and
$x_{2}\in[-1,1]$. For $x_{1}=1$ and $x_{1}=-1$, $f(x_{1},x_{2})=x_{1}$, hence
1 and -1 belong to $R_{\exists\forall}(f)$, and
$R_{\exists\forall}(f)=\\{-1,1\\}$. A study of $f$ reveals that
$R_{\forall\exists}(f)=[-1,1]$, which is a strict superset of
$R_{\exists\forall}(f)=\\{-1,1\\}$.

Indeed, a careful study of $f$ reveals that:

  * •

for $x_{2}\in\left[-\frac{1}{2},\frac{1}{2}\right]$, $f(x_{1},x_{2})$ is
monotonic, and has exact range $[f(-1,x_{2})=-1,f(1,x_{2})=1]$; when
$x_{2}\in\left[\frac{1}{2},\infty\right[$,

  * •

$f(x_{1},x_{2})$ has exact range
$\left[-\frac{1+4x_{2}^{2}}{4x_{2}},1\right]$, with
$-\frac{1+4x_{2}^{2}}{4x_{2}}$ having itself exact range
$\left[-\frac{5}{4},-1\right]$ ($f(.,x_{2})$ is decreasing from -1 to
$-\frac{1}{2x_{2}}$ with value $-\frac{1+4x_{2}^{2}}{4x_{2}}$ and then
increasing to 1),

  * •

$f(x_{1},x_{2})$ has exact range
$\left[-1,-\frac{1+4x^{2}_{2}}{4x_{2}}\right]$ when
$x_{2}\in\left]-\infty,-\frac{1}{2}\right]$ ($f(.,x_{2})$ is increasing from
-1 to $-\frac{1}{2x_{2}}$ with value $-\frac{1+4x_{2}^{2}}{4x_{2}}$ which can
range from 1 to $\frac{5}{4}$, and decreasing up to 1).

Thus the intersection of the ranges of $f(.,x_{2})$ for all $x_{2}$ is exactly
$[-1,1]$, and by Lemma 1, we conclude that $R_{\forall\exists}(f)=[-1,1]$.

##  Appendix 0.H Example 11

###### Example 11

Consider function $g\ :\ \mathbb{R}^{3}\rightarrow\mathbb{R}$ given by

$g(x_{1},x_{2},x_{3})=\frac{x_{1}^{2}}{4}+(x_{2}+1)(x_{3}+2)+(x_{3}+3)^{2}.$

On $[-1,1]^{3}$, $\nabla_{1}=|\frac{\partial g}{\partial
x_{1}}|=|\frac{x_{1}}{2}|\in\left[0,\frac{1}{2}\right]$,
$\nabla_{2}=|\frac{\partial g}{\partial x_{2}}|=|x_{3}+2|\in[1,3]$,
$\nabla_{3}=|\frac{\partial g}{\partial
x_{3}}|=|x_{2}+1+2(x_{3}+3)|\in[4,10]$, and $c=g(0,0,0)=11$. Therefore, we can
compute the outer and inner approximations $O_{i}$ and $I_{i}$, $i=1,2,3$, of
Remark 6: $O_{1}=\left[-\frac{1}{2},\frac{1}{2}\right]$, $I_{1}=0$,
$O_{2}=[-3,3]$, $I_{2}=[-1,1]$ and $O_{3}=[-10,10]$, $I_{3}=[-4,4]$. We can
deduce an outer-approximation of the disturbance set:

$\\{z\,|\;\exists x_{1}\in[-1,1],\ \forall x_{2}\in[-1,1],\ \exists
x_{3}\in[-1,1],z=g(x_{1},x_{2},x_{3})\\}$

Let us first note that in order to apply Theorem 1 with $n=2$, we must
introduce a dummy universally quantified first variable, which means that all
indices above should be added 1. Then, by a ”direct” (adding 1 to variables
indices) application of Theorem 2.1:

$\begin{array}[]{ccccccccccc}{[}&c&+\underline{O}_{1}&+\overline{I}_{2}&+\underline{O}_{3},&c&+\overline{O}_{1}&+\underline{I}_{2}&+\overline{O}_{3}&{]}&\\\
={[}&11&-\frac{1}{2}&+1&-10,&11&+\frac{1}{2}&-1&+10&{]}&=[1.5,20.5]\end{array}$

In comparison, the sampling based estimation is $[6.25,16.25]$.

Now, as
$\overline{I}_{3}+\underline{O}_{2}=1\geq\underline{I}_{3}+\overline{O}_{2}=-1$,
we get by Theorem 2.1 an inner approximation of the disturbance set for $g$:

$\begin{array}[]{ccccccccccc}{[}&c&+\underline{I}_{1}&+\overline{O}_{2}&+\underline{I}_{3},&c&+\overline{I}_{1}&+\underline{O}_{2}&+\overline{I}_{3}&{]}&\\\
={[}&11&0&+3&-4,&11&+0&-3&+4&{]}&=[10,12]\end{array}$

##  Appendix 0.I Calculation of the Jacobian for Example 5

The Jacobian of $\varphi$ with respect to $x_{0}$, $y_{0}$, $\theta_{0}$,
$b_{1}$ and $a$, $J_{i,x_{0}}=\frac{\partial\varphi_{i}}{\partial t}$,
$J_{i,y_{0}}=\frac{\partial\varphi_{i}}{\partial t}$,
$J_{i,\theta_{0}}=\frac{\partial\varphi_{i}}{\partial t}$,
$J_{i,b_{1}}=\frac{\partial\varphi_{i}}{\partial t}$ and
$J_{i,a}=\frac{\partial\varphi_{i}}{\partial t}$, for $i=x,y,\theta$
respectively, satisfies the following variational equation [20]:

$\displaystyle\dot{J}_{x,x_{0}}$ $\displaystyle=$ $\displaystyle-
sin(\theta)J_{\theta,x_{0}}$ $\displaystyle\dot{J}_{x,y_{0}}$ $\displaystyle=$
$\displaystyle-sin(\theta)J_{\theta,y_{0}}$
$\displaystyle\dot{J}_{x,\theta_{0}}$ $\displaystyle=$ $\displaystyle-
sin(\theta)J_{\theta,\theta_{0}}$ $\displaystyle\dot{J}_{x,b_{1}}$
$\displaystyle=$ $\displaystyle-sin(\theta)J_{\theta,b_{1}}+1$
$\displaystyle\dot{J}_{x,a}$ $\displaystyle=$ $\displaystyle-
sin(\theta)J_{\theta,a}$ $\displaystyle\dot{J}_{y,x_{0}}$ $\displaystyle=$
$\displaystyle cos(\theta)J_{\theta,x_{0}}$ $\displaystyle\dot{J}_{y,y_{0}}$
$\displaystyle=$ $\displaystyle cos(\theta)J_{\theta,y_{0}}$
$\displaystyle\dot{J}_{y,\theta_{0}}$ $\displaystyle=$ $\displaystyle
cos(\theta)J_{\theta,\theta_{0}}$

$\displaystyle\dot{J}_{y,b_{1}}$ $\displaystyle=$ $\displaystyle
cos(\theta)J_{\theta,b_{1}}$ $\displaystyle\dot{J}_{y,a}$ $\displaystyle=$
$\displaystyle cos(\theta)J_{\theta,a}$ $\displaystyle\dot{J}_{\theta,x_{0}}$
$\displaystyle=$ $\displaystyle 0$ $\displaystyle\dot{J}_{\theta,y_{0}}$
$\displaystyle=$ $\displaystyle 0$ $\displaystyle\dot{J}_{\theta,\theta_{0}}$
$\displaystyle=$ $\displaystyle 0$ $\displaystyle\dot{J}_{\theta,b_{1}}$
$\displaystyle=$ $\displaystyle 0$ $\displaystyle\dot{J}_{\theta,a}$
$\displaystyle=$ $\displaystyle 1$

with initial conditions $J_{i,x_{0}}=\delta_{i,x}$,
$J_{i,y_{0}}=\delta_{i,y}$, $J_{i,\theta_{0}}=\delta_{i,\theta}$ where
$\delta$ is the Kronecker symbol. Therefore, the only non-null entries of the
Jacobian of $\varphi$ are: $J_{x,x_{0}}=1$, $J_{x,b_{1}}=t$, $J_{y,y_{0}}=1$,
$J_{\theta,\theta_{0}}=1$, $J_{\theta,a}=t$, and also $J_{x,\theta_{0}}$,
$J_{x,a}$, $J_{y,\theta_{0}}$ and $J_{y,a}$ are given by the ODEs:

$\begin{array}[]{lcll}\dot{J}_{x,\theta_{0}}&=&-sin(\theta)&\mbox{with
$\dot{J}_{x,\theta_{0}}=0$ at time $0$}\\\
\dot{J}_{x,a}&=&-sin(\theta)t&\mbox{with $\dot{J}_{x,a}=0$ at time $0$}\\\
\dot{J}_{y,\theta_{0}}&=&cos(\theta)&\mbox{with $\dot{J}_{y,\theta_{0}}=0$ at
time $0$}\\\ \dot{J}_{y,a}&=&cos(\theta)t&\mbox{with $\dot{J}_{y,a}=0$ at time
$0$}\\\ \end{array}$

In order to find an over-approximation of these entries of the Jacobian, we
use here a simple mean-value theorem, given that $\theta(t)\in[-0.015,0.015]$
for $t\in[0,0.15]$:

$\begin{array}[]{rcl}J_{x,\theta_{0}}&=&-sin([-0.015,0.015])t\\\ &\in&[-1.309\
10^{-4},1.309\ 10^{-4}]\\\ J_{x,a}&=&-[0,0.5]sin([-0.015,0.015])t\\\
&\in&[-6.545\ 10^{-5},6.545\ 10^{-5}]\\\
J_{y,\theta_{0}}&=&cos([-0.015,0.015])t\\\ &\in&[0,0.5]\\\
J_{y,a}&=&[0,0.5]cos([-0.015,0.015])t\\\ &\in&[0,0.25]\\\ \end{array}$

By Remark 6, this gives the following inner and outer approximations for all
parameters $x_{0}$, $y_{0}$, $\theta_{0}$, $a$ and $b_{1}$, and all components
$x$, $y$ and $\theta$ of $\varphi$:

  * •

$I_{x,a}=0$, $O_{x,a}=[-6.545\ 10^{-7},6.545\ 10^{-7}]$,
$I_{x,x_{0}}=O_{x,x_{0}}=[-0.1,0.1]$, $I_{x,\theta_{0}}=0$,
$O_{x,\theta_{0}}=[-1.309\ 10^{-6},1.309\ 10^{-6}]$, $I_{x,b_{1}}=0$,
$O_{x,b_{1}}=[-0.005,0.005]$,

  * •

$I_{y,a}=0$, $O_{y,a}=[-0,0025,$ $0.0025]$,
$I_{y,y_{0}}=O_{y,y_{0}}=[-0.1,0.1]$, $I_{y,\theta_{0}}=0$,
$O_{y,\theta_{0}}=[-0,005,0.005]$,

  * •

$I_{\theta,\theta_{0}}=O_{\theta,\theta_{0}}=[-0.01,0.01]$, $I_{\theta,a}=0$,
$O_{\theta,a}=[0,0.005]$,

We note also that $\frac{\partial x}{\partial
t}=cos(\theta)+b_{1}\in[0.989999965,1.01]$ thus $I_{x,t}=[0,0.49499$ $9982]$,
$O_{x,t}=[0,0.505]$, similarly, $I_{y,t}=0$,
$O_{y,t}=[-sin(0.015)/2,sin(0.015)/2]=[-1.309\ 10^{-4},1.309\ 10^{-4}]$ and
$I_{\theta,t}=0$, $O_{\theta,t}=[-0.005,0.005]$.

##  Appendix 0.J Computation of components $y$ and $\theta$ for Example 5

Inner-approximation for the $y$ component of $\varphi$ is computed similarly
as for $x$, its lower bound is:

$\begin{array}[]{ccccccc}y_{c}&+\underline{I}_{y,a}&+\underline{I}_{y,x_{0}}&+\underline{I}_{y,y_{0}}&+\underline{I}_{y,\theta_{0}}&+\overline{O}_{y,b_{1}}&+\underline{I}_{y,t}\\\
=0&+0&+0&-0.1&+0&+0&+0\end{array}$

which is equal to -0.1, and its upper bound:

$\begin{array}[]{ccccccc}y_{c}&+\overline{I}_{y,a}&+\overline{I}_{y,x_{0}}&+\overline{I}_{y,y_{0}}&+\overline{I}_{y,\theta_{0}}&+\underline{O}_{y,b_{1}}&+\overline{I}_{y,t}\\\
=0&+0&+0&+0.1&+0&+0&+0\end{array}$

which is equal to 0.1. Therefore the inner-approximation for $y$ is equal to
$[-0.1,0.1]$.

Outer-approximation for the $y$ component of $\varphi$ has as lower bound:

$\begin{array}[]{ccccccc}y_{c}&+\underline{O}_{y,a}&+\underline{O}_{y,x_{0}}&+\underline{O}_{y,y_{0}}&+\underline{O}_{y,\theta_{0}}&+\overline{I}_{y,b_{1}}&+\underline{O}_{y,t}\\\
=0&-0,0025&-0&-0.1&-0,005&+0&-1.309\ 10^{-4}\end{array}$

which is equal to 0.1076309, and its upper bound:

$\begin{array}[]{ccccccc}y_{c}&+\overline{O}_{y,a}&+\overline{O}_{y,x_{0}}&+\overline{O}_{y,y_{0}}&+\overline{O}_{y,\theta_{0}}&+\underline{I}_{y,b_{1}}&+\overline{O}_{y,t}\\\
=0&+0.0025&+0&+0.1&+0,005&-0&+1.309\ 10^{-4}\end{array}$

which is equal to 0.1076309. Therefore the outer-approximation for $y$ is
equal to $[0.1076309,0.1076309]$.

Inner-approximation for the $\theta$ component of $\varphi$ is computed
similarly, its lower bound is:

$\begin{array}[]{ccccccc}\theta_{c}&+\underline{I}_{\theta,a}&+\underline{I}_{\theta,x_{0}}&+\underline{I}_{\theta,y_{0}}&+\underline{I}_{\theta,\theta_{0}}&+\overline{O}_{\theta,b_{1}}&+\underline{I}_{\theta,t}\\\
=0&+0&+0&+0&-0.01&+0&+0\end{array}$

which is equal to -0.01, and its upper bound:

$\begin{array}[]{ccccccc}\theta_{c}&+\overline{I}_{\theta,a}&+\overline{I}_{\theta,x_{0}}&+\overline{I}_{\theta,y_{0}}&+\overline{I}_{\theta,\theta_{0}}&+\underline{O}_{\theta,b_{1}}&+\overline{I}_{\theta,t}\\\
=0&+0&+0&+0&+0.01&+0&+0\end{array}$

which is equal to 0.01. Therefore the inner-approximation for $\theta$ is
equal to $[-0.01,0.01]$.

Outer-approximation for the $\theta$ component of $\varphi$ has as lower
bound:

$\begin{array}[]{ccccccc}\theta_{c}&+\underline{O}_{\theta,a}&+\underline{O}_{\theta,x_{0}}&+\underline{O}_{\theta,y_{0}}&+\underline{O}_{\theta,\theta_{0}}&+\overline{I}_{\theta,b_{1}}&+\underline{O}_{\theta,t}\\\
=0&+0&+0&+0&-0.01&+0&-0.005\end{array}$

which is equal to -0.02, and its upper bound:

$\begin{array}[]{ccccccc}\theta_{c}&+\overline{O}_{\theta,a}&+\overline{O}_{\theta,x_{0}}&+\overline{O}_{\theta,y_{0}}&+\overline{O}_{\theta,\theta_{0}}&+\underline{I}_{\theta,b_{1}}&+\overline{O}_{\theta,t}\\\
=0&+0.005&+0&+0&+0.01&+0&+0.005\end{array}$

which is equal to 0.02. Therefore the outer-approximation for $\theta$ is
equal to $[-0.02,0.02]$.

##  Appendix 0.K Proof of Theorem 3.1

The principle is the same as in the case of one alternation of, for all and
there exists quantifiers, treated in [21].

For each $i\in\\{1,\ldots,n\\}$, function $\pi^{i}$ associates to each $x_{j}$
for $j\in\\{k_{2i}+1,\ldots,k_{2{i+1}}\\}$ the index $l\in\\{1,\ldots,m\\}$ of
the unique output component of the function in which it will be existentially
quantified.

First suppose $\pi^{i}$ are jointly surjective (i.e. the union of their image
is $\\{1,\ldots,$ $m\\}$). For each of the $m$ quantified problems for $z_{j}$
o Theorem 3.1, for all $i=1,\ldots,n$, and for all $l^{i}_{j}\in
J_{E,z_{j}}^{i}$ we can associate the continuous selection

$g_{l^{i}_{j}}\left(z_{j},(x_{p})_{p\in\\{1,\ldots,k_{2i-1}\\}\cup
J_{A,z_{j}}^{i}}\right)$

by [19], since $f$ is elementary. For a given
$(z_{1},\ldots,z_{m})\in{\makebox{\boldmath$z$}}$, let us define the
continuous map $g$ that associates to each
$(x_{1},\ldots,x_{u})\in{\makebox{\boldmath$x$}}$,

$\left((g_{l^{1}_{j}})_{j\in\\{1,\ldots,m\\}},\ldots,(g_{l^{n}_{j}})_{j\in\\{1,\ldots,m\\}}\right)$

which can be completed adding identities on the components which are not
defined, to be in value in in
${\makebox{\boldmath$x$}}\subseteq\mathbb{R}^{m}$. By Brouwer fixed point
theorem, $\forall z\in{\makebox{\boldmath$z$}}$, there is a fixed point
$x^{z}\in{\makebox{\boldmath$x$}}$ of $g$, which thus satisfies $z=f(x^{z})$
as the $\pi^{i}$s are jointly surjective. We observe that the fixed point
obtained does depend on the quantified variables, in the same order than in
the original quantified problem $R_{{\makebox{\boldmath$p$}}}(f)$.

Finally, if the $\pi^{i}$s are not jointly surjective, there exist $z_{i}$ in
which no input variable is existentially quantified. The corresponding under-
approximation will be empty or reduced to a point and the previous proof still
holds on the other components.

##  Appendix 0.L Example 7 detailed

There are several possible quantified formulas giving a 2D inner-approximation
for Example 7.

One of them is, for all $z_{1}$ and $z_{2}$:

$\displaystyle\framebox{$\exists x_{1}$},\ \forall x_{2},\ \forall x_{3},\
\framebox{$\exists x_{4}$},\ z_{1}=f_{1}(x_{1},x_{2},x_{3},x_{4})$ (24)
$\displaystyle\forall x_{1},\ \forall x_{2},\ \forall x_{4},\
\framebox{$\exists x_{3}$},\ z_{2}=f_{2}(x_{1},x_{2},x_{3},x_{4})$ (25)

where we indicated above the existential quantifiers for each group
$\forall\exists$ within a framed box. By Theorem 2.1, we get an empty set for
$z_{1}$ as defined by Equation (24), since the constraints of Proposition 1
are not satisfied: the contribution of the existentially quantified $x_{4}$ is
$[-1,1]$ whereas the universally quantified $x_{2}$ and $x_{3}$ account for
$[-4,4]$, which thus cannot be fully compensated.

Similarly Equation (25) yields an empty inner-approximation since it does not
satisfy the constraints of Proposition 1, the contribution of $x_{3}$ being
too small to counteract the contribution of $x_{1}$, $x_{2}$ and $x_{4}$.

Another possibility is to interpret the following quantified formulas, for all
$z_{1}$ and $z_{2}$:

$\displaystyle\framebox{$\exists x_{1}$},\ \forall x_{2},\ \forall x_{4},\
\framebox{$\exists x_{3}$},\ z_{1}=f_{1}(x_{1},x_{2},x_{3},x_{4})$ (26)
$\displaystyle\forall x_{1},\ \forall x_{2},\ \forall x_{3},\
\framebox{$\exists x_{4}$},\ z_{2}=f_{2}(x_{1},x_{2},x_{3},x_{4})$ (27)

This time, the conditions of Proposition 1 for obtaining a non-empty inner-
approximation are met and we get for Equation (26):

$\begin{array}[]{ccccccccc}{[}&z_{1}^{c}&-||\Delta_{x_{1}}||&+||\Delta_{x_{2},x_{4}}||&-||\Delta_{x_{3}}||,&z_{1}^{c}&+||\Delta_{x_{1}}||&-||\Delta_{x_{2},x_{4}}||&+||\Delta_{x_{3}}||]\\\
={[}&2&-2&+1+1&-3,&2&+2&-1-1&+3]\end{array}$

which is equal to $[-1,5]$, and for Equation (27):

$\begin{array}[]{ccccccc}{[}&z_{2}^{c}&+||\Delta_{x_{1},x_{2},x_{4}}||&-||\Delta_{x_{3}}||,&z_{1}^{c}&-||\Delta_{x_{1},x_{2},x_{4}}||&+||\Delta_{x_{3}}||]\\\
={[}&-1&+1+1+1&-5,&-1&-1-1-1&+5]\end{array}$

which is equal to $[-3,1]$. Hence $[-1,5]\times[-3,1]$ is in the set
$R_{\exists\forall\exists}(f)$.

Finally, there are two other possibilities for finding joint inner-
approximations of $R_{\exists\forall\exists}(f)$ of Equation (14):

$\displaystyle\forall x_{1},\ \forall x_{2},\ \forall x_{3},\
\framebox{$\exists x_{4}$},\ z_{1}=f_{1}(x_{1},x_{2},x_{3},x_{4})$ (28)
$\displaystyle\framebox{$\exists x_{1}$},\ \forall x_{2},\ \forall x_{4},\
\framebox{$\exists x_{3}$},\ z_{2}=f_{2}(x_{1},x_{2},x_{3},x_{4})$ (29)

For the same reason as for Equations (24) and (25), Equations (28) and (29)
yield empty inner-approximations since the contribution to it of the last
existentially quantified variables is the same in both cases (e.g. [-1,1] for
$x_{4}$ in Equations (24) and (28)), and is not big enough to compensate for
the next universally quantified variables (e.g. [3,-3] for variable $x_{3}$ in
Equations (24) and (28)). Similarly for the last choice:

$\displaystyle\forall x_{1},\ \forall x_{2},\ \forall x_{4},\
\framebox{$\exists x_{3}$},\ z_{1}=f_{1}(x_{1},x_{2},x_{3},x_{4})$ (30)
$\displaystyle\framebox{$\exists x_{1}$},\ \forall x_{2},\ \forall x_{3},\
\framebox{$\exists x_{4}$},\ z_{2}=f_{2}(x_{1},x_{2},x_{3},x_{4})$ (31)

for which the Equation (30) gives an empty set, and Equation (31) gives
$[-1-1+1+1-5.-1+1-1-1+5]$ which is equal to $[-3,3]$. Overall, this choice of
alternation of quantifiers allowed by Theorem 3.1 gives an empty joint inner-
approximation for the quantified problem $R_{\exists\forall\exists}(f)$ of
Equation (14).

##  Appendix 0.M Example Motion-$n$

We consider the Dubbins vehicle of Example 4, and compute the $x$ component at
time $nT$, $x_{n}$, with $T=0.5s$, given a piecewise constant control $a_{i}$
on each of the control periods $[(i-1)T,iT]$, which is given by the following
function below, after integration of the dynamics:

$x_{n}=x_{0}+\sum\limits_{k=1}^{n}\frac{1}{a_{k}}\left(sin\left(\theta_{0}+T\sum\limits_{l=1}^{n}a_{l}\right)-sin\left(\theta_{0}+T\sum\limits_{l=1}^{n-1}a_{l}\right)\right)+T\sum\limits_{k=1}^{n}b_{k}$

and we consider the following motion planning problem (up to a small
relaxation $\delta$):

$\exists x_{0},\ \exists\theta_{0},\ \exists a_{1},\ \forall b_{1},\ \ldots,\
\exists a_{n},\ \forall b_{n},\ \exists\delta,\
x=x_{n}(x_{0},\theta_{0},a_{1},b_{1},\ldots,a_{n},b_{n})+\delta$