数理解析研究所講究録
1199 巻 2001 年 100-113

100

Reach Set Computations Using Real Quantifier
Elimination
宏和 (Hirokazu ANAI)

FUJITSU LABORATORIES LTD

穴井

Universit\"at Passau

Volker WEISPFENNING\dagger$*$

Abstract
Reach set computations are of fundamental importance in control theory. We consider thereach set problem for open-loop systems described by parametric inhomogeneous linear differenti alsystems and use real quantifier elimination methods to get exact and approximate solutions. The
method employs a reduction of the forward and backward reach set and control parameter set
problems to the transcendental implicitization problems for the components of special solutionsof simpler non-parametric systems. For simple elementary functions we give an exact calculationof the cases where exact semialgebraic transcendental implicitization is possible. For the negative
cases we provide approximate alternating using discrete point checking or safe estimations of reachsets and control parameter sets. Examples are computed using the REDLOG and QEPCAD packages.

1 Introduction
Today integrated systems which combine physical processes with information systems $(i.e$.
digital programs) are in great demand. In fact complex systems which have been designed recently incorporate both differential equations to model the continuous behavior and discrete event
systems to model instantaneous state changes in response to events. Systems that are finite statemachines with differential equations at each discrete state are called Hybrid Systems.
A lot of research effort has been devoted to develop mathematical models, specification formalisms,
methods and tools to help control engineers in building such
systems (see [18, 30, 26]). Most of the applications of hybrid systems are safety critical. Safety
is usually encoded as avoidance of an undesirable region of the state space. Consequently, themost important problems for analyzing hybrid systems are verification problems; these are essentially reachability problems, that ask whether trajectories of the hybrid systems reach certain
undesirable (unsafe) regions from an initial region.
Computing the reach set of hybrid systems is difficult because hybrid systems have an infinite
state space. Due to the difficulty of computing the reach set for systems of differential equations,formal verification methods and tools for hybrid systems have been developed $[2, 17]$ . Thesemethods and tools, however, can deal with only very simple continuous models as, $e.g.\dot{x}=1$ ,$\mathrm{a}\mathrm{n}\mathrm{a}\mathrm{l}\mathrm{y}\mathrm{s}\mathrm{i}\mathrm{s}/\mathrm{d}\mathrm{e}\mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}/\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\mathrm{r}\mathrm{o}\mathrm{l}$*anai@jp.fujitsu.com\dagger weispfen@fmi.uni-passau.de101$A\dot{x}=b$. What is actually required is to handle hybrid systems with more complicated continuous

parts.
Decidability of reachability problem for hybrid systems with linear differential equation of
the form $\dot{y}=Ay+Bu$ is discussed in $[23, 24]$ . This is a significant class of linear differential
equations that is widely used in linear control theory. The results are based on the notion of]$[11]$ .
$[16]$ from model theory and “quantifier-minimality is used
to define a class of hybrid systems -minimal hybrid systems” and it is shown that all o-minimal
hybrid systems admit finite bisimulations in [22]. To make the bisimulation algorithm computationally feasible, they utilize mathematical logic, in particular, real quantifier elimination, as
main tool to represent and manipulate sets symbolically. Since quantifier elimination, in general, is possible for the polynomial theory of reals [11], they have found subclasses of o-minimal
hybrid systems that are definable in the theory.
Remark: There are many results that apply quantifier elimination to control theory [6, 15, 19, 4]. In“”$0- \mathrm{m}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{m}\mathrm{a}$$\mathrm{e}\mathrm{l}\mathrm{i}\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$”$\mathrm{O}$$\mathrm{i}\mathrm{t}\mathrm{y}$“$0$$[28, 3]$ quantifier elimination is used for verification problems (reachability and observability problems) of
discrete-time polynomial systems.

In this paper we study in particular reach set problems for continuous open-loop systems
described by parametric systems of linear differential equations [21]. Roughly speaking reachset problems are concerned with the relations between possible values of the state variables atsome initial time and the corresponding values at later points in time. The specific problems
studied in this paper are the following:$t_{0}$

1. Fix a set $M$ of values of the state variables at ; what are the possible corresponding values
at later points in time (up to some bound or ). (Forward reach set)$t_{0}$$t$$t_{1}$$\infty$values of the state variables. Find a set $M$ as large as possible of initialthat guarantees that the values of the state variables
values of the state variables at time
will for all later time points (up to some bound or ) remain inside N. (Backward reach

2. Fix a set$N\mathrm{o}\mathrm{f}$”“$\mathrm{s}\mathrm{a}\mathrm{f}\mathrm{e}$$t_{0}$$t$$t_{1}$$\infty$set)

3. Fix a set $M$ of values of the state variables at and a set $N$ of “safe” values of the state
as large as possible of the control parameters such that all statevariables. Find a set
variables with initial values at in $M$ will have values in $N$ for all later time points (up tosome bound or ) (Control parameter set)$t_{0}$$P$$t_{0}$$t_{1}$$t$$\infty.$

Our main tool is the method of real quantifier elimination in computer algebra. This approach

was introduced into reach set computations in [29]. In a series of papers they showed how to
get exact solutions of the forward reach set problem for certain homogeneous linear differential
systems of special type with constant coefficients [23] and for associated inhomogeneous systems
with very special right hand side [24]. The exact solutions are always obtained as semialgebraic
sets described by a boolean combination of polynomial inequalities.
Here we extend this ad hoc approach for special types of differential systems to a systematic
study of the type of results obtainable by an approach via real quantifier elimination. By reducing
the approach to its bare essentials, we obtain a much wider systematic framework applicable toa considerably larger class of systems. The main observation is that all the problems mentioned
above can be reduced by exact symbolic algorithms to an implicitization problem for certain
basic transcendental functions associated with the given system. Exact solutions for implicitization problems with rational parametrizations are well-known $[8, 27]$ . Here we deal with the102corresponding problem for transcendental parametrizations that has been studied only for special
cases $e.g$ . in $[13, 20]$ .
Our main results are as follows: We associate with every parametric linear system of differa finite system $F$ of basic functions. Then for semialgebraic
ential equations
sets $M,$ $N$ all three problems can be solved exactly by real quantifier elimination relative to theimplicitization problem for the components of the functions in $F$ . Moreover the discrete point
version of these problems require only finitely many evaluations of functions in $F$ . We prove atheorem that determines the exact classes of vector-valued functions of the kind arising in linear differential systems with constant coefficients, where exact semialgebraic implicitization ispossible. As a corollary we obtain the exact limitations of the approach of $[23, 24]$ for linear
differential systems with constant coefficients and special right hand sides.
We propose several ways to overcome these limitations by approximate computations: One
way is to compute exact reach sets at a finite selection of discrete time points. This is always possible and practically quite efficient, but may lead to underestimation of the true forward reach set,
depending on the selection of time points. Another approach separates the common time variable into different time variables. This leads to an overestimation in the implicitization problem
resulting in an overestimation of the forward reach set and an underestimation of the backward
reach set and the control parameter set: So all three approximations are on the safe side.
We illustrate some problems and solution methods by examples computed in the REDLOGpackage of REDUCE [14] and QEPCAD [12]. We expect that our results can be extended to thehybrid systems with linear continuous parts.
$\dot{y}=A(t)y+b(t, \underline{r})$2 Reach sets&transcendental implicitization problem
2.1 Problem statement
We consider parametric inhomogeneous systems of linear differential systems of the form$\dot{y}=A(t)y+b(t, \underline{r})$ with an $n\cross n$ matrix $A(t)$ of real continuous functions
and a vectordefined on some interval . The inhomogeneous part isvalued real continuous function
with continuous functions : $Iarrow$assumed to be alinear combination, and real parameters . Such a system can be viewed as an continuous open-loop control
and fix an initial. Let $M$ be some subset ofsystem with control parametersof the given
time point $t_{0}\in I$ : Then we denote the set of all solution functions :, and the set of all solution functions $f\in F_{r}$, bysystem with parameterswith initial value $f(t_{0})\in M$ by $F=F_{M,r}$ .
We consider the following forward reach set problems:$S$$a_{ij}(t)$$I$$b(t, \underline{r})$$b(t, \underline{r})=\sum_{i=1}^{k}r_{i}gi(t)$$\mathrm{R}^{n}$$g_{i}$$r_{i}$$\mathrm{R}^{n}$$\underline{r}=(r_{1}, \ldots, r_{k})$$f$$\underline{r}=(r_{1}, \ldots, r_{k})$$Iarrow \mathrm{R}^{n}$$F_{r}$

discrete reach sets Compute for finitely many time points $t_{1}<\ldots<t_{m}$ insets $\{f(t_{i})|f\in F_{M,r}\}$ .

bounded reach set Compute for a given time $t_{1}>t_{0}$ in$t_{1}\}$

$I$

$I$

the union of thethe set $\{f(t)|f\in F_{M,r},$ $t_{0}\leq t\leq$.

unbounded reach set Suppose$I\supseteq[t_{0}, \infty)$, and compute the set $\{f(t)|f\in F_{M_{7}},\cdot, t_{0}\leq i\}$ .

103
All computations should be performed in explicit dependence on the control parameters .
Any solution of the discrete reach sets problem yields an lower estimate for the sets to be computed in the bounded and unbounded reach set problems.
Of equal interest are the corresponding “backward” reach set problems that are a kind of“dual” to the corresponding “forward” problems.
.
Some backward reach set problems are as follows: Let $N$ be a subset of$\underline{r}$$\mathrm{R}^{n}$backward discrete reach sets Compute for finitely many time points $t_{1}<\ldots<t_{m}$ insets $\{f(t_{0})|f(t_{1}), \ldots, f(t_{m})\in N\}$ .
backward bounded reach set Compute for a given time $t_{1}>t_{0}$ in$N$ for all
}.

$I$

$I$

the

the set $\{f(t_{0})|f(t)\in$$t_{0}\leq t\leq t_{1}$backward unbounded reach set Suppose$N$ for all}.

$I\supseteq[t_{0}, \infty)$, and compute the set $\{f(t_{0})|f(t)\in$$t_{0}\leq t$

From the viewpoint of control theory these problems have still other variants conceming the. Let $M$ as before be a subset
determination of suitable control parameter values$N$. Then we have the following natural control parameter, and let be another subset ofofset problems:$\underline{r}=(r_{1}, \ldots, r_{k})$$\mathrm{R}^{n}$$\mathrm{R}^{n}$discrete point control Compute for finitely many time points $t_{1}<\ldots<t_{m}$ infor all $f\in F_{M,r},$ $1\leq i\leq m$ }.

$I$

the set$\{\underline{r}\in$$\mathrm{R}^{k}|f(t_{i})\in N$

bounded interval control Compute for a given time $t_{1}>t_{0}$ in$N$ for all $f\in F_{M,r},$}.

the set$\{\underline{r}\in \mathrm{R}^{k}|f(t)\in$, and compute the set$\{\underline{r}\in \mathrm{R}^{k}|f(t)\in$$I$$t_{0}\leq t\leq t_{1}$unbounded interval control Suppose$N$ for all $f\in F_{M,r},$}.

$I\supseteq[t_{0}, \infty)$$t_{0}\leq t$

In order to make these problems mathematically precise, we need to specify the way in which
the input sets $M$ and $N$ , and the output sets should be described. For an approach using symbolic
computations it is natural to consider semialgebraic sets as possible inputs. These are subsets
described by a boolean combination $\varphi(x_{1,\ldots,n}x)$ of real polynomial inequalities. If inofare linear, then the set described by isaddition all the polynomials involved incalled semilinear $[16, 32]$ .
Our goal is to solve the forward and backward reach set and control parameter set problems
for semialgebraic input sets as far as possible with descriptions of semialgebraic sets as outputs.
This, however, is not always possible. Hence we consider also the computation of overestimating
the forward reach sets and underestimating the backward reach set and the control parameter sets
by suitable semialgebraic sets.
Our main tool will be a reduction of reach set and control parameter set computations tocorresponding implicitization problems for a fixed finite system of functions associated with ,associated with , andfor the homogeneous system
namely a fundamental system
special solutions of the parameter-free inhomogeneous system given by $\dot{y}=A(t)y+g_{i}(t)$for $1\leq i\leq k$ . We refer to $\{f_{1}, \ldots, f_{n}, h1, \ldots, hk\}$ as a system of basic functions for .
Implicitization problems for rational parametrizations of algebraic varieties have been widely
considered in computer algebra $[8, 27]$ . Here we have to study the corresponding problem for the, arising from the system . As these functions
vector-valued functions$\mathrm{R}^{n}$$\varphi(x_{1}, \ldots , x_{n})$$\varphi$$S$$f_{1},$$\ldots,$$S$$S_{0}$$f_{n}$$S_{i}$$h_{i}$$S$$f_{1},$$\ldots,$$f_{n},$$h_{1},$$h_{k}$$\ldots,$

$S$

104
will in general be transcendental, we refer to these problems as transcendental implicitization
problems.
More precisely, we consider the following transcendental implicitization problems for given
for $1\leq i\leq k$ :functions :$f_{i}$$Iarrow \mathrm{R}^{n}$discrete points implicitization Compute for finitely many time points $t_{1}<\ldots<t_{m}$ in.
, regarded as points invalues$I$the$\mathrm{R}^{nk}$$(f_{1}(t_{i}), \ldots f_{k}(t_{i}))$bounded implicitization Compute for a given time $t_{1}>t_{0}$ in.

$I$the set $\{(f_{1}(t), \ldots fk(t))\in$$\mathrm{R}^{nk}|t_{0}\leq t\leq t_{1}\}$

unbounded implicitization Suppose$I\supseteq[t_{0}, \infty)$$\{(f_{1}(t), \ldots fk(t))\in \mathrm{R}^{nk}|t_{0}\leq t\}$, and compute the set.

The first problem amounts to simple evaluations of the given functions. Notice that theunbounded and bounded implicitization problem for a single solution of the differential system
is in fact a special case of the unbounded and bounded forward reach set problem for ,respectively, namely for the case of a singleton set $M$ .
$S$

$S$

2.2 Reduction to implicitization problems
Next we show that all reach set computations and control parameter set computations listed
above can for semialgebraic input sets $M,$ $N$ be reduced in an exact symbolic way to one of these
implicitization problems. All these reductions require real quantifier elimination as fundamental
tool. For the case of discrete points forward and backward reach set and control parameter set
and semilinear input sets $M,$ $N$ we find moreover that the output sets are also semilinear.
be quantifier-free formulas describing the semialgeandLet$\dot{y}=Ay+b(t, \underline{r})$ with
$N$
$M$
be a
,
Let
respectively.
andbraic input sets
parametric linear system with control parameter . Let be a fundamental system of sobe a special solution of the system $\dot{y}=Ay+g_{i}(t)$ . Then by
lutions of $\dot{y}=Ay$ . Let. Notethe superposition principle, a special solution of the system is given by
may be regarded as constants or as free parameters. Then it is straightforward tothat here
write down first-order formulas describing the respective forward and backward reach sets and. . $hk$ , thecontrol parameter sets in terms of evaluations of the basic functions$\psi(x_{1,\ldots,n}x)$ and a quantifier-free formula,
given formulasset.
,
as a semialgebraic,) describing the combined range ofAll these formulas will involve several quantifiers over real numbers. By real quantifier elimination one can construct equivalent quantifier-free formulas, and thus get the desired semialgebraic
descriptions.
We will exhibit concrete first-order formulas for some reach set problems and control parameter set problem. The remaining cases are handled similarly in [5]. The forward discrete reachset problem can be described by the following formula and hence be solved by real quantifier
elimination and evaluation of the basic functions at finitely many points.
$\varphi(x_{1}, .

$\psi(x_{1}, \ldots, x_{n})$.- , x_{n})$$b(t, \underline{r})=\sum r_{i}g_{i}(t)$$S$$r_{i}$$f_{i}$$h_{i}$$S$$\sum_{i=1}^{k}r_{i}h_{i}$$r_{i}’ \mathrm{s}$$f_{1},$$\ldots$$y_{nn}$$f_{n},$ $h_{1,-}$$\mu(y_{11},$$\varphi(x_{1}, \ldots, X_{n}),$$y_{n1},$$\ldots,$$,$$\ldots,$ $y_{1n},$$(f_{1}, \ldots , f_{n}, h_{1}, \ldots , h_{k})$$\exists x_{1}\ldots\exists x_{n}(\varphi(\sum iX_{i}f_{i}+\sum_{i}rihi)(t0)\wedge[\bigwedge_{j1}^{n}=y_{j}=(\sum_{i}x_{i}f_{ij}+\sum_{i}rih_{ij}(t1))$

V. . . $\vee\bigwedge_{j=1}^{n}y_{j}=(\sum_{i^{X_{i}}}fij+\sum_{i}r_{i}h_{ij})(t_{m})])$ .

$\ldots$

105, $y_{nn’ 11}z,$,$y1n’\ldots,$
Next suppose we have a quantifier-free formulaon the interval
describing the combined range of)if and only if thisholds for $n(k+n)$ -tuple in. So
oron the given interval. Then the fortuple is in the combined range ofward bounded and unbounded reach set problem, respectively, can be described by the following
formula and hence solved by real quantifier elimination:$\mu(y_{11},$$[t_{0}, \infty)$$[t_{0}, t_{1}]$$y_{n1},$$\ldots,$$\ldots$$\ldots$$(f_{1}, \ldots , f_{n}, h_{1}, \ldots , h_{k})$$z_{1n},$ $\ldots,$ $z_{k1},$ $\ldots,$ $Z_{kn})$$\mu(y_{11}, ..

.

$\mathrm{R}^{n(kn}+$, z_{kn})$$(f_{1}, \ldots ?

f_{n}, h_{1}, \ldots , h_{k})$$\exists x_{1}\ldots\exists X_{n}[\varphi(\sum iX_{i}f_{i}+\sum_{i}rihi)(t_{0})\wedge\exists y_{11}\ldots\exists ynn\exists z11\cdots\exists z_{kn}(\mu(y11, \ldots, z_{kn})$( $\sum_{i}xiy_{ij}+\sum$ rizij) $)]$ .
$\wedge\bigwedge_{ji}^{n}=1y_{j}=$With the same formula , the backward bounded and unbounded reach set problem, respectively, can be described by the following formula and hence solved by real quantifier elimination:$\mu$$\exists x_{1}\ldots\exists x_{n}[\bigwedge_{j1}^{n}=y_{j}=(\sum_{i^{X_{i}f\sum_{i}r_{i}}}ij+hij)(t_{0}))\wedge\forall y_{11}\ldots\forall ynn\forall z11\cdots\forall zkn$.

$( \mu(y_{11}, \ldots, z_{kn})arrow\psi(\sum_{i^{X}}i\underline{yi}+\sum ir_{i^{Z}}\underline{i})(t))]$Finally, the bounded interval control problem and the unbounded interval control problem,
respectively, can be described by the following formula and hence solved by real quantifier elimination:$\exists x_{1}\ldots\exists X_{n}[\varphi(\sum ixif_{i}+\sum_{i}r_{ii}h)(t0)$A$\forall y11\cdots\forall y_{nn}\forall z_{11}\ldots\forall zkn$$( \mu(y_{11}, \ldots, z_{kn})arrow\psi(\sum_{i^{X}}i\underline{yi}+\sum iri\underline{Zi})(t))]$.

3 Exact transcendental implicitization
Here we consider cases, where the unbounded and bounded transcendental implicitization: $Iarrow \mathrm{R}^{n}(1\leq i\leq k)$ has an exact solution. Notice that the
problem for given functionsof;transcendental implicitization problem refers only to the component functions
here.
isirrelevantSo
wevector-valued
functions
intofunctionsthese
the grouping ofcomponent
may assume w.l.o.g. that $k=1$ and that we deal with a single vector-valued function $f(t)$ $:=$. Then the exact transcendental implicitization problem is to determine the(contained in .
, or a compact interval
range of $f(i)$ on an unbounded interval.
Since the is continuous, this range is always a connected subset of;for the boundedis$n=1$intervalmoreovercompact
the range is a real
In particular for
implicitization case. In the unbounded implicitization case is compact iff is bounded on
is always a, otherwise it is a closed semiinfinite interval or all of R. In particular
for
.
In
other
words
and
bounds
from
lower
upper
explicitlythat
cancomputedsetsemialgebraic
the unbounded and the bounded transcendental implicitization problem always has a positive
solution for $n=1$ .
For $n=2$ there are two well-known cases, where exact unbounded and bounded impliciti$:=$: If has components
zation is possible, namely the $\sin-\cos$ -pair and the$\cos(p(x)),$ $f2:=\sin(p(x))$ , where $p(x)$ is a real polynomial of positive degree, then the range
isincludes an unbounded interval; consequently the range of on
of $p(x)$ on$\{(x_{1},x_{2})|x_{1}^{2}+x_{2}^{2}=1\}$, the range of. On a bounded interval
exactly the unit circle$p(x)$ is again a compact interval, and so the range ofis a connected subset of the circle that canbe easily computed as semialgebraic set from the range of $p(x)$ . For the hyperbolic case, where$f_{i}$$f_{ij}(t)$$f_{i}(t)$$f_{1}(t\mathrm{I}, \ldots, fn(t))$$I$$[t_{0}, t_{1}]$$[t_{0}, \infty)$$\mathrm{R}^{n}$

$f$

$J$

$J$

$J$

$f$

$J$

$[t_{0}, \infty)$$f$$\sinh-\cosh- \mathrm{p}\mathrm{a}\mathrm{i}\mathrm{r}$$f$$f_{1}$$f$$[t_{0}, \infty)$$[t_{0}, t_{1}]$$f$$[t_{0}, \infty)$

106$f_{1}:=\cosh(p(x)),$ $f2:=\sinh(p(x))$ , the situation is analogous, except that the role of the circle

is replaces by the hyperbola $\{(x_{1}, x_{2})|x_{1^{-X_{2}^{2}}}^{2}=1\}$ .
The next theorem shows that exact transcendental implicitization is preserved under composition of functions in a very general sense:
Theorem 1 Let $f(t):=(f_{1}(t), \ldots , f_{k}(t))$ be a vector valued function such that the range ofon every compact or unbounded closed interval I is a semialgebraic set described by a quantifier. Let be a continuous real function defined on some compact orfree formula
upper semiinfinite closed interval $I’$ . Let $h_{i}(1\leq i\leq n)$ be semialgebraic real functions definedon some subset ofextending the range of . Let $\rho_{i}(x_{1,\ldots,n}x, y)$ be quantifier-free formulas$\{(X_{1,\ldots,y)}Xn’|y=h_{i}(X_{1},\ldots, Xn)\}$defining the graphof . Then the vector-valuedfunction$f^{*}(t):=(f_{1}^{*}(t), \ldots , f_{n}^{*}(t))$ with components $f_{i}^{*}(t):=h_{i}(f1(g(t)), \ldots, fn(g(t)))$for $1\leq i\leq$has a semialgebraic range described by the formula$f$$\varphi_{I}(x_{1}, \ldots, x_{k})$

$g$

$f$

$\mathrm{R}^{n}$$h_{i}$$n$,$\psi(x_{1,\ldots,n}X):=\exists y_{1}\ldots\exists yn(\varphi J(y1, \ldots, y_{n})\wedge\bigwedge_{i=1}^{n}\rho_{i}(y1, \ldots, yn’)x_{i})$

where

$J$

is the range of $g(t)$ on $I’$ .

The proof is obvious. Notice that the algorithmic quantifier elimination for the ordered fieldof real numbers this formula is required in order to transform the formula into an equivalentquantifier-free formula that describes the range of as a semialgebraic set. Typical instances ofand are real polynomials or real rational functions. The method can in particular be applied
to the situation, where consists of aor a $\sinh-\cosh$ -pair as described above. Other, whereis a Weierstrass -function [1]. Then the range
interesting examples are pairsof, on alarge enough interval is a real elliptic curve $\{(x, y)|y^{2}--4x^{3}-g2x-g\mathrm{s}\}$ . See[5] for the more examples.
$\psi$$f^{*}$$h_{i}$$g$$f$$\sin-\cos_{\mathrm{P}^{\mathrm{a}}}- \mathrm{i}_{\Gamma}$$\wp(t)$$(\wp, \wp’)$$\wp$$(\wp, \wp’)$

4 Semialgebraic implicitization for simple elementary functions
In this section we characterize those cases of linear differential systems
with constantcoefficients and “simple right hand side”, where an exact implicitization of the system of basic
functions for is possible. The condition on the right hand side $b(t)$ of the system is as follows:
All components
of $b(t)$ are -linear combinations of functions of the form,
are real numbers. Then it is, whereare non-negative integers andwell known that a special solution of the inhomogeneous system and the fundamental solutionsof the homogeneous system are again real linear combinations of functions of this kind. We
call linear systems of this form regular and functions of type
, withreal numbers simple elementary functions. In some special cases of regular systems, it
has been shown how to solve the reach set problem by an implicit semialgebraic implicitizationof functions of the following type in [23, 24, 22] : (i) real polynomials
exponential, forfunctionswith rational values of . (iii) trigonometric functions
rational .
$S$

$S$

$b_{i}(t)$$t^{d_{i}}e^{a_{i}}{}^{t}\mathrm{s}\mathrm{i}\mathrm{n}(\omega_{i}t)$$\mathrm{R}$$t^{d_{i}}e^{a_{i}}{}^{t}\mathrm{c}\mathrm{o}\mathrm{s}(\omega_{i}t)$$d_{i}$$a_{i},$$\omega_{i},$$\alpha_{i}$$t^{d}e^{at}\cos(\omega t),$ $b^{d}e^{a}\sin t(\omega t)$$a,$ $\omega,$$\alpha$$p_{i}(t),$$e^{a_{i}t}$$a_{i}$$\omega_{i}$$(\mathrm{i}\mathrm{i})$$\cos(\omega_{i}t),$$\sin(\omega_{i}t)$

107
In the following we show that for simple elementary functions there are only few more cases
which allow unbounded exact semialgebraic implicitization; all these cases are covered by Theorem 1 of the last section. In most of the remaining cases the exact semialgebraic implicitization
problem is unsolvable. In fact we provide a complete characterization of those cases, where

unbounded semialgebraic implicitization is possible.
Let $f(t):=(f_{1}(t), \ldots, fn(t))$ with non-constant, pairwise different component functions, or, whereare non-negative integers andare real numbers. Moreover we assume that the functions appear in, whenever.
$f_{i}(t):=t^{d_{i}}e^{a_{i}}{}^{t}\mathrm{c}\mathrm{o}\mathrm{s}(\omega_{i}t)$$a_{i},$$f_{i}(t):=t^{d_{i}}e^{a_{i}}{}^{t}\mathrm{s}\mathrm{i}\mathrm{n}(\omega_{i}t)$$d_{i}$$f_{i}$$\omega_{i}$$\cos-\sin-\mathrm{P}\mathrm{a}\mathrm{i}\mathrm{r}\mathrm{S}$$\omega_{i}\neq 0$

Theorem 2 Let :be as above and let $n\geq 2$ . Then the range ofsemialgebraic set iff one of the following holds:$[t_{0}, \infty)arrow \mathrm{R}^{n}$$f$

1. For all $1\leq i\leq n,$$f_{i}(t):=t^{d_{i}}$

$f$

is a

.

2. For all $1\leq i\leq n,$ $d_{i}=0,$ $f_{i}(t):=e^{a_{i}t}$ and $dim_{\mathrm{Q}}(span(a1, \ldots, an))\leq 1$ .
3. For all $1\leq i\leq n,$$d_{i}\neq 0,$ $a_{i}\neq 0,$ $f_{i}(t):=t^{d_{i}}e^{a_{i}t}$and$dim_{\mathrm{Q}}(span(a_{1,\ldots,n}a))\leq 1,$$\frac{d_{i}}{d_{1}}=\frac{a_{i}}{a_{1}}$

, and

.

4. For all $1\leq i\leq n,$ $f_{i}(t):=\cos(\omega_{i}t)$ , or $f_{i}(t):=\sin(\omega_{i}t)$ , and$dim_{\mathrm{Q}}(span(\omega_{1,\ldots,n}\omega))\leq 1$.

Moreover in these positive cases a quantifier-free formula describing the range ofcomputed algorithmically over the reals.

$f$can beIdea of the Proof. In the cases mentioned above the unbounded semialgebraic implicitizationis always achieved by the methods of the previous section, in particular Theorem 1. It remains
to show that in all other cases the range of is not a semialgebraic set. This requires a casedistinction. In each case we show that the assumption that the range of is semialgebraic leads
to a contradiction. Based on the assumption that the range of is semialgebraic we construct
new semialgebraic sets with impossible properties. Either this set is one dimensional such thatneither the set nor its complement is a finite union of intervals or it describes the graph of asemialgebraic function with an impossible rate of growth (compare [9]). See [5] for details of
the proof.
$f$

$f$

$f$

This theorem clearly shows the limitations of the approach presented in $[23, 24]$ . In fact wehave the following immediate corollary:

Corollary 3 Let $\dot{y}=Ay$ with constant $n\cross n$ -matrix be a homogeneous system of linear
differential equations. Then exact semialgebraic implicitization is possible for a fundamentalof solutions of the system iff one of the following cases holds.
$A$$s\gamma_{Sf}em$$\cdot$1. All eigenvalues of
2. All eigenvalues$dim_{\mathrm{Q}}$(span($\lambda 1,$

3. All eigenvalues$A$

are zero, i.e.

$\lambda_{1},$$\lambda_{n}$$\ldots,$$\ldots$,$\lambda_{n})$$\lambda_{1},$$\ldots,$

pairwise distinct reals$\mu_{i}$)$A$is a nilpotent matrix.

of are non-zero, pairwise distinct reals, and$\leq 1$$A$.

$\lambda_{n}ofA$

are purely, say$imagi\prime ar\}^{\backslash }$oftheform, and $dim_{\mathrm{Q}}(span(\mu 1, \ldots.\mu_{n}))\leq 1$ .

$\lambda_{i}=\mu_{i}\sqrt{-1}$with non-zero

108

5 Approximate solutions.

.

In this section we study the cases, where an exact semialgebraic unbounded or bounded
implicitization is definitely not possible. In these cases we want to find a semialgebraic supersetof the true forward reach set and a semialgebraic subset of the true backward reach set or thetrue control parameter set, both if possible such that the set difference to the true reach set orcontrol parameter set is in some sense “small enough.” Then an inspection of the reduction
formulas shows that an overestimation of the implicitization problem leads to an overestimationof the forward reach set and an underestimation of the backward reach set and of the control
parameter set $i.e$ . for “safe” estimations. Hence we are reduced to the problem of finding asemialgebraic superset of the true range of a transcendental vector valued function on a compact
or upper semiinfinite closed interval.
One strategy to find overestimations of the range is separation of variables: It comes in two
flavours: Separation of variables in different components, and separation of variables in products.

Separation of variables in different components: Let $f(t)=(f_{1}(t), \ldots, f_{n}(t))$ be definedon an interval . Then separation of variables in different components yields the function $g(t)=$$(f_{1}(t_{1}), \ldots, fn(t_{n}))$ defined on the cube
. The range of is easily
with range(g), where is the range of . Notice that this box is in fact thecomputed as a box
smallest box containing the range of .
$I$

$I^{n}$$J_{1}\cross\cdots\cross J_{n}$$\supseteq \mathrm{r}\mathrm{a}\mathrm{n}\mathrm{g}\mathrm{e}(f)$$g$$f_{i}$$J_{i}$$f$

Separation of variables in products: Suppose the component functions of the given functions
is defined on the interval . Put
are products $f_{i}(t):=f_{i,1}(t)\cdots f_{i,m}(t)$ , where each$g_{j}(t):=(f_{1,j}, \ldots, f_{n,j})^{T}$ . Then eachbe the range ,is also defined on the interval . Let$C:=B_{1}\cdots
B_{\dot{m}}$, where the multiplication is performed on the elements componentwise.
and put
Then is obviously a superset of the range of .
$I$

$f_{i,j}(t)$$I$$g_{j}$$C$

Example. 1 Let$B_{j}$$g_{j}$$f$$I$

be the upper semiinfinite interval$[0, \infty)$.

1. Let $f_{1}:=\cos(t),$ $f_{2}:=\sin(t)$ . Then the true range of is the unit circle. Separation ofvariables in different components yields as overestimation the closed unit square.
$f$

2. Let $f_{1}:=\cosh(t),$ $f_{2}:=\sinh(t)$ . Then the true range of is the hyperbola $\{(x, y)|$$x^{2}-y^{2}=1\}$ . Separation of variables in different components yields as overestimation
the “quadrant” $\{(x, y)|x, y\geq 1\}$ .
$f$

3. Let $f_{1}:=e^{t}\cos(t),$ $f_{2}:=e^{t}\sin(t)$ . Then the true range of is an expanding exponential
spiral. Separation of variables in different components yields as overestimation the full plane. Separation of variables in products yields as better overestimation the annulus $\{(x, y)|$$x^{2}+y^{2}\geq 1\}$ .
$f$$\mathrm{R}^{2}$

4. Let $f_{1}:=e^{-t}\cos(t),$ $f_{2}:=e^{-t}\sin(t)$ . Then the true range of is a contracting exponential
spiral. Separation of variables in different components yields as overestimation a closed
box $\{(x, y)|-e^{\pi}\leq x\leq 1, -e^{3\pi/2}\leq y\leq e^{\pi/2}\}$ . Separation of variables in products
yields as overestimation the closed disk $\{(x, y)|x^{2}+y^{2}\leq 1\}$ . These approximations areincomparable. So their intersection is a common improvement of both.
$f$

109

6 Complexity
In this section we briefly discuss the complexity of our algorithms. From the results on complexity of quantifier elimination in [7] we can give upper bounds for the asymptotic complexityof our approach:Discrete point reach set problems are described by purely existential formulas. Hence thecomplexity of quantifier elimination is at most simply exponential in the dimension of the differential system. For fixed dimension it the computation runs in a polynomial time. The complexityof bounded and unbounded reach set problems is the same as for the discrete reach set problem
for a fixed number $m$ of points. The backward discrete reach set problems can be solved in singly
exponential time. The complexity of backward bounded and unbounded reach set computation(generalized singly exponential). The upper complexity bounds for the control
is of typeparameter set problems are same as for the corresponding backward reach set problems.
$e^{n^{O}}(1)$7Computational example in REDLOG and QEPCAD

In this section we report on experimental results in reach set and control parameter set computation. In [5] we have presented experimental results for numerous examples that illustrate thedifferent problem types and solution methods. Here we display only one of these examples with
non-constant coefficients to show the generality of the approach. All computations are performedin the REDLOG package [14] of REDUCE 3.7 and QEPCAD [12] 1). The main algorithm employedis the linear and quadratic quantifier elimination $[25, 31]$ of REDLOG and quantifier elimination
based on cylindrical algebraic decomposition [12] of QEPCAD.

Example. 2 Consider the inhomogeneous system $\dot{y}=Ay+b$ with

$A:=,$ $b:=r_{1}$.

Then basic functions arecomputations in the$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{w}\mathrm{a}\mathrm{r}\mathrm{d}/\mathrm{b}\mathrm{a}\mathrm{c}\mathrm{k}\mathrm{w}\mathrm{a}\mathrm{r}\mathrm{d}$unbounded reach set and the control parameter set prob-

lems below (Note that we set $t_{0}=0$ ):Forward unbounded reach set: A quantifier-free formulaobtained from the following first-order formula$\bullet$$\mu(y_{11}, y_{12}, y_{21}, y_{22}, \mathcal{Z}_{11}, Z_{12})$is$\mu_{\mathit{0}}$$\mu_{\mathit{0}}=\exists u\exists v$( $u2+v^{2}=1$ A $y_{11}=v\wedge y_{12}=u$ A $y_{21}=u$ A $y_{22}=-v$ A $z_{11}=v$ A $z_{12}=0$ )by using quantifier elimination. By using$\mu:=y_{11}^{2}+y_{12}^{2}-1=0$$\mathrm{R}\mathrm{E}\mathrm{D}\mathrm{I}_{\lrcorner}\mathrm{O}\mathrm{G}$$)$

we have

A $y_{11}+y_{22}=0$ A $y_{11}-z_{11}=0$ A $y_{12}-y_{21}=0$ A $z_{12}=0$

in 10. Then we set $r_{1}=1$ and moreover $\varphi=(0\leq x_{1}\leq 1\wedge x_{2}=0)$ . Then forward
unbounded reach set problem is solved by using real quantifier elimination for the following
first-order formula freach;$\mathrm{m}\mathrm{s}$$1)\mathrm{A}\mathrm{l}1$

the computations are executed on a SUN SPARC station Ultra I$(140\mathrm{M}\mathrm{H}\mathrm{z})$.

110freachwhere

freachaux$=\exists x_{1}$($\varphi\wedge$

freachaux)$=\exists y11\exists y12\exists y_{2}1\exists y_{22}\exists Z_{1}1\exists Z12(\mu$A $y_{1}=x_{1}y_{11}+x_{2}y_{21}+r_{1}z_{11}$$\wedge y_{2}=X_{1yy_{22}}12+x_{2}+r1z_{1}2)$

By using QEPCAD for freach we obtain as an answer for the forward unbounded reach set;$y_{1}^{2}+4y_{2}^{2}-4<=0$ in 10.
$\mathrm{m}\mathrm{s}$$\bullet$

Backward unbounded reach set:$\mu$

is the same formula as in forward unbounded reach set.

first-order formula breach;breach$=\exists x_{1}\exists X_{2}$( $y_{1}=x_{2}$ A $y_{2}=x_{1}$ A breachaux)

where

breachaux$= \forall y_{11}\forall y12\wedge-\frac{11}{2}\forall y2\forall y22\forall z<x_{1}y12+x2y_{22}+r1Z_{1}11\forall z12(\muarrow(-\frac{1}{2}<_{2}<\frac{y_{1}}{2})x_{111}+x_{2}y_{21}+r_{1}z_{11}<\frac{1}{2}$

By using REDLOG for breach we obtain in 420 ms a semialgebraic description of the backward
unbounded reach set consisting of 21 atomic formulas.
$\bullet$Control parameter set: The formula$\mu$

is the same as in the reach set cases. We also set

formula pcontrol;

control$=\exists x_{1}$( A controlaux)$\varphi$

wherecontrolaux$= \forall y_{11}\forall y12\forall y2\wedge-\frac{11}{2}\forall y22\forall z11\forall z12(\mu\prec(-\frac{1}{2}<<X_{1y1}2+x_{2y22}+r1z12<\frac{y1}{2})x_{111}+x_{2}y_{21}+r_{1}z_{11}<\frac{1}{2}$

By using REDLOG for control we obtain in 70 ms a semialgebraic description of control paramby handeter set consisting of 12 atomic formulas. It can be simplified to the result-l
calculation.
$\leq r_{1}<\frac{1}{2}$8 Conclusions
In this paper we have studied forward and backward reach set and control parameter set
problems for continuous parametric open-loop systems described by a system of parametric linear differential equations with arbitrary coefficients.
The approach using quantifier elimination was introduced into reach set computations in[29]. We extend their ad hoc approach for special types of differential systems to a systematic
study of the type of results obtainable by an approach via real quantifier elimination. Thus we
obtain a much wider systematic framework applicable to a considerably larger class of systems.
The main observation is that all the problems can be reduced by exact symbolic algorithms toan implicitization problem for certain basic transcendental functions associated with the given
system.

111
We have proved a theorem that determines the exact classes of vector-valued functions of
the kind arising in linear differential systems with constant coefficients, where exact semialgebraic implicitization is possible. As a corollary we have obtained the exact limitations of theapproach of $[23, 24]$ for linear differential systems with constant coefficients and simple elementary inhomogeneous part. We have also proposed several ways to overcome these limitations byapproximate computations. The problems have been illustrated by examples computed in theof REDUCE and QEPCAD.
Further research will be concemed with an extension of these results to hybrid systems.
$\mathrm{R}\mathrm{E}\mathrm{D}\mathrm{L}\mathrm{O}\mathrm{C}-\mathrm{p}\mathrm{a}\mathrm{c}\mathrm{k}\mathrm{a}\mathrm{g}\mathrm{e}$References[1] N. L. Alling. Real elliptic curves. North-Holland, 1981.
[2] R. Alur, C. Coucoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicolin, A. Olivere,

J. Safakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3-34, 1995.
[3] H. Anai. Algebraic approach to analysis of discrete-time polynomial systems. In Proc. ofEuropean Control Conference 1999, 1999.

[4] H. Anai and S. Hara. Fixed-structure robust controller synthesis based on sign definite con-dition by a special quantifier elimination. In Proceedings $ofAmeri_{C}an$ Control Conference
2000, pages 1312-1316, 2000.
[5] H. Anai and V. Weispfenning. Reach set computation using real quantifier elimination.
Technical Report MIP-0012, FMI, Universit\"at Passau, D-94030 Passau, Germany, Oct.

2000.
[6] B. Anderson, N. Bose, and E. Jury. Output feedback stabilization and related problems
solution via decision methods. IEEE Trans. Auto. Control, $20(1):53-65,$ i975.
[7]–

S. Basu, R. Pollack, and M.-F. Roy. On the combinatorial and algebraic complexity ofquantifier elimination. J. ACM, 43(6): 1002-1045, 1996.

[8] T. Becker, V. Weispfenning, and H. Kredel. Gr\"obner Bases, a Computational Approachto Commutative Algebra, volume 141 of Graduate Texts in Mathematics. Springer, New
York, corrected second printing edition, 1998.
[9] J. Bochnak, M. Coste, and M.-F. Roy.

G\’eometrie alg\’ebrique r\’eelle.

Springer, Berlin,

Heidelberg, New York, 1987.
[10] M. Braun.

Differential Equations and Their Applications, volume 15 of Applied Mathe-

matical Science. Springer, 3rd edition, 1983.

Quantifier Elimination and Cylindrical Algebraic
Decomposition. Texts and Monographs in Symbolic Computation. Springer, Berlin, Heidelberg, New York, 1998.

[11] B. Caviness and J. Johnson, editors.

[12] G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, $12(3):299-328$ , Sept. 1991.

[13] J. Craig. Introduction to Robotics. Addison-Wesley, 1986.

112[14] A. Dolzmann and T. Sturm. REDLOG: Computer algebra meets computer logic. ACM
SIGSAM Bulletin, 31 (2):2-9, June 1997.

[15] P. Dorato, W.Yang, and C.Abdallah. Application of quantifier elimination theory to robust

multi-object feedback design. J. Symb. Comp. 11, pages 1-6, 1995.
[16] L. v. d. Dries. Tame Topology and -minimal structures. Cambridge University Press, 1998.
$\mathit{0}$[17] T. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata?

In Proceedings of the 27th Annual Symposium on Theory of Computing, STOC’95, pages
373-382. ACM Press, 1995.
[18] T. Henzinger and S. Sastry, editors. Hybrid Systems: Computation and Control, volume1386 of LNCS. Springer-Verlag, 1998.
[19] M. Jirstrand. Nonlinear control system design by quantifier elimination. Journal of $s_{ym}-$bolic Computation, 24(2): 137-152, Aug. 1997. Special issue on applications of quantifier

elimination.

Computer algebra in robot-kinematics.
In Proceeding of the workshop:
Algebra in Science and Engineering”, Bielefeld, Aug’94, pages 303-316,
Singapore, 1994. World Scientific.

[20] P. Kov\’acs.
“$c_{omp_{\mathcal{U}}er}t$[21] A. Kurzhanski and I.

$\mathrm{V}\mathrm{l}\mathrm{y}\mathrm{i}’$1997.

. Ellipsoidal Calculus for Estimation and Control. Birkh\"auser,[22] G. Lafferriere, G. Pappas, and S. Sastry. -minimal hybrid systems. Mathematics of control, Signals and Systems, 13(1): 1-21, 2000.
$\mathrm{O}$[23] G. Lafferriere, G. Pappas, and S. Yovine. A new class of decidable hybrid systems. In Hy-

brid Systems: Computation and Control, volume 1569 of LNCS, pages 137-151. Springer,

1999.
[24]

G. Lafferriere, G. Pappas, and S. Yovine. Reachability computation for linear hybrid systems. In Proceedings of the 14th IFAC World Congress, volume E, pages 7-12, Beijin,

P.R.China, 1999.

[25] R. Loos and V. Weispfenning. Applying linear quantifier elimination. The Computer Journal, $36(5):450-462$ , 1993. Special issue on computational quantifier elimination.
[26] N. A. Lynch and B. H. Krogh, editors. Proceedings Third International Workshop on Hybrid Systems: Computation and Control (HSCC 2000), Pittsburgh, PA, USA, volume 1790

of Lecture Notes in Computer Science. Springer-Verlag, Mar. 2000.
[27] D. Manocha and J. Canny.

Algorithm for implicitizing rational parametric surfaces. In
R. Bamhill and W. Boehm, editors, Computer Aided Geometric Design, volume 9. NorthHolland, 1992.

[28] D. Ne\v{s}i\v{c}. Two algorithms arising in analysis of polynomial models. In Proceedings of 1998

American Control Conference, pages 1889-1893, 1998.

[29] G. Pappas and S. Yovine. Decidable hybrid systems. Technical report, University of Cali-

fomia at Berkeley, 1998.
[30] F. Vaandrager and J. von Schuppen, editors. Hybrid Systems: Computation and Control,

volume 1569 of LNCS. Springer-Verlag, 1999.

113[31] V. Weispfenning. Quantifier elimination for real algebra–the quadratic case and beyond.
Applicable Algebra in Engineering Communication and Computing, $8(2):85-]01$ , Feb.

1997.

[32] V. Weispfenning. Semilinear motion planning in REDLOG. Technical report,$\mathrm{U}\mathrm{n}\mathrm{i}_{\mathrm{V}\mathrm{e}\Gamma \mathrm{s}}\mathrm{i}\mathrm{t}\ddot{\mathrm{a}}\mathrm{t}$Passau, D-94030 Passau, May 1999. available at the electronic proceedings of IMACSACA’99, http://math.unm.edu/aca.html.