# Change-Of-Bases Abstractions for Non-Linear Systems.

Sriram Sankaranarayanan
Department of Computer Science
University of Colorado, Boulder, CO, USA.
<EMAIL_ADDRESS>
###### Abstract

We present abstraction techniques that transform a given non-linear dynamical
system into a linear system or an algebraic system described by polynomials of
bounded degree, such that, invariant properties of the resulting abstraction
can be used to infer invariants for the original system. The abstraction
techniques rely on a change-of-basis transformation that associates each state
variable of the abstract system with a function involving the state variables
of the original system. We present conditions under which a given change of
basis transformation for a non-linear system can define an abstraction.
Furthermore, the techniques developed here apply to continuous systems defined
by Ordinary Differential Equations (ODEs), discrete systems defined by
transition systems and hybrid systems that combine continuous as well as
discrete subsystems.

The techniques presented here allow us to discover, given a non-linear system,
if a change of bases transformation involving degree-bounded polynomials
yielding an algebraic abstraction exists. If so, our technique yields the
resulting abstract system, as well. This approach is further extended to
search for a change of bases transformation that abstracts a given non-linear
system into a system of linear differential inclusions. Our techniques enable
the use of analysis techniques for linear systems to infer invariants for non-
linear systems. We present preliminary evidence of the practical feasibility
of our ideas using a prototype implementation.

##  1 Introduction

In this paper, we explore a class of abstractions for non-linear autonomous
systems (continuous, discrete and hybrid systems) using _Change-of-Bases_
(CoB) transformations. CoB transformations are obtained for a given system by
expressing the dynamics of the system in terms of a new set of variables that
relate to the original system variables through the CoB transformation. Such a
transformation is akin to studying the system under a new set of “bases”. We
derive conditions on the transformations such that (a) the CoB transformations
also define an _autonomous system_ and (b) the resulting system abstracts the
original system: i.e., all invariants of the abstract system can be
transformed into invariants for the original system. Furthermore, we often
seek abstract systems through CoB transformations whose dynamics are of a
simpler form, more amenable to automatic verification techniques. For
instance, it is possible to use CoB transformations that relate an ODE with
non-linear right-hand sides to an affine ODE, or transformations that reduce
the degree of a system with polynomial right-hand sides. If such
transformations can be found, then safety analysis techniques over the simpler
abstract system can be used to infer safety properties of the original system.

In this paper, we make two main contributions: (a) we define CoB
transformations for continuous, discrete and hybrid systems and provide
conditions under which a given transformation is valid; (b) we provide search
techniques for finding CoB transformations that result in a polynomial system
whose right-hand sides are degree limited by some limit $d\geq 1$.
Specifically, the case $d=1$ yields an affine abstraction; and (c) we provide
experimental evidence of the application of our techniques to a variety of
ordinary differential equations (ODEs) and discrete programs.

The results in this paper extend our previously published results that
appeared in HSCC 2011 [34]. The contributions of this paper include (a) an
extension from linearizing CoB transformations to degree-bounded polynomial
CoB transformations, (b) extending the theory from purely continuous system to
discrete and hybrid systems, and (c) an improved implementation that can
handle hybrid systems with some evaluation results using this implementation.
On the other hand, our previous work also included an extension of the theory
to differential inequalities and iterative techniques over cones. These
extensions are omitted here in favor of an extended treatment of the theory of
differential equation abstractions for continuous, discrete and hybrid
systems.

###  1.1 Motivating Examples

In this section, we motivate the techniques developed in this paper by means
of a few illustrative examples involving purely continuous ODEs and purely
discrete programs .

Our first example concerns a continuous system defined by a system of Ordinary
Differential Equations (ODEs):

######  Example 1.1.

Consider a continuous system over $\\{x,y\\}$: $\dot{x}=xy+2x,\ \
\dot{y}=-\frac{1}{2}y^{2}+7y+1$, with initial conditions given by the set
$x\in[0,1],\ y\in[0,1]$. Using the transformation
$\alpha:(x,y)\mapsto(w_{1},w_{2},w_{3})$ wherein $\alpha_{1}(x,y)=x$,
$\alpha_{2}(x,y)=xy$ and $\alpha_{3}(x,y)=xy^{2}$, we find that the dynamics
over $\vec{w}$ can be written as

$\dot{w_{1}}=2w_{1}+w_{2},\
\dot{w_{2}}=w_{1}+9w_{2}+\frac{1}{2}w_{3},\dot{w_{3}}=2w_{2}+16w_{3}$

Its initial conditions are given by $w_{1}\in[0,1],\ w_{2}\in[0,1],\
w_{3}\in[0,1]$. We analyze the system using the TimePass tool as presented in
our previous work [37] to obtain polyhedral invariants:

$\begin{array}[]{l}-w_{1}+2w_{2}\geq-1\ \land\ w_{3}\geq 0\ \land\ w_{2}\geq
0\ \land\\\ -16w_{1}+32w_{2}-w_{3}\geq-17\ \land\ 32w_{2}-w_{3}\geq-1\
\land\\\ 2w_{1}-4w_{2}+17w_{3}\geq-4\ \land\ 286w_{1}-32w_{2}+w_{3}\geq-32\
\land\\\ \cdots\end{array}$

Substituting back, we can infer polynomial inequality invariants on the
original system including,

$\begin{array}[]{l}-x+2xy\geq-1\ \land\ xy^{2}\geq 0\ \land\ -16x+32xy-
xy^{2}\geq-17\\\ x\geq 0\ \land\ 2x-4xy+17xy^{2}\geq-4\ \land\
\cdots\end{array}$

Finally, we integrate the linear system to infer the following conserved
quantity for the underlying non-linear system:

$\begin{array}[]{l}\left(\frac{e^{-9t}}{51}+\frac{1}{102}\left(50+7\sqrt{51}\right)e^{\left(-9+\sqrt{51}\right)t}+\frac{1}{102}\left(50-7\sqrt{51}\right)e^{-\left(9+\sqrt{51}\right)t}\right)\
x+\\\
\left(-\frac{1}{102}e^{-9t-\left(9+\sqrt{51}\right)t}\left(\begin{array}[]{l}7e^{9t}-\sqrt{51}e^{9t}-14e^{\left(9+\sqrt{51}\right)t}+\\\
7e^{9t+\left(-9+\sqrt{51}\right)t+\left(9+\sqrt{51}\right)t}+\\\
\sqrt{51}e^{9t+\left(-9+\sqrt{51}\right)t+\left(9+\sqrt{51}\right)t}\end{array}\right)\right)\
xy+\\\
\left(\frac{1}{204}e^{-9t-\left(9+\sqrt{51}\right)t}\left(e^{9t}-2e^{\left(9+\sqrt{51}\right)t}+e^{9t+\left(-9+\sqrt{51}\right)t+\left(9+\sqrt{51}\right)t}\right)\right)xy^{2}\end{array}$

Finally, if $x(0)\not=0$, the map $\alpha$ is invertible and therefore, the
ODE above can be integrated.

Note that not every transformation yields a linear abstraction. In fact, most
transformations will not define an abstraction. The conditions for an
abstraction are discussed in Section 2. $\blacktriangle$

⬇ proc computeP(int k) int x,y; assert( K > 0); x := y := 0; while ( y < k ){ x := x + y * y; y := y + 1; } end-function |  ⬇ proc computePAbs(int k) int x,y,y2; assert( K > 0); x := y := y2 := 0; while ( y < k ){ x := x + y2; y2 := y2 + 2 * y + 1; y := y + 1; } end-function
---|---
Figure 1: Program showing a benchmark example proposed by Petter [28] and its
abstraction obtained by a change of basis $(x\mapsto x,y\mapsto y,y2\mapsto
y^{2})$.

Next, we motivate our approach on purely discrete programs, showing how CoB
transformations can linearize a discrete program with non-linear assignments,
modeled by a _transition system_ [21]. In turn, we show how invariants of the
abstract linearized program can be transferred back.

######  Example 1.2.

Figure 1 shows an example proposed originally by Petter [28] that considers a
program that sums up all squares from $1$ to $K^{2}$ for some input $K\geq 0$.
Consider a very simple change of basis transformation wherein we add a new
variable “y2” that tracks the value of $y^{2}$ as the loop is executed. It is
straightforward to write assignments for “y2” in terms of itself, $x,y$. Doing
so for this example does not necessitate the tracking of higher degree terms
such as $y^{3},x^{2}y^{2}$ and so on. Finally, the resulting program has
affine guards and assignments, making it suitable for polyhedral abstract
interpretation [10, 16]. The polyhedral analysis yields linear invariants at
the loop head and the function exit in terms of the variables $x,y,y2$. We may
safely substitute $y^{2}$ in place of $y2$ and obtain invariants over the
original program. The non-linear invariants obtained at the function exit are
shown below:

$\begin{array}[]{c}4x+18y-7y^{2}\geq 11\ \land\ 4\leq 2x+7y-3y^{2}\ \land\
9\leq x+12y-3y^{2}\ \land\ 1\leq y\ \land\\\ 3y-y^{2}\leq 2\ \land\
5y-y^{2}\leq 6\ \land\ 6y-y^{2}\leq 9\ \land\ k=y\end{array}$

In this example, the change of basis to $y^{2}$ can, perhaps, be inferred from
the syntax of this program. However, we demonstrate other situations in this
paper, wherein the change of basis cannot be inferred from the expressions in
the program using syntactic means.

The invariant

$6x=2k^{3}+3k^{2}+k\,,$

discovered by Petter and many other subsequent works such as the complete
approach for P-solvable loops by Kovacs [18] can also be discovered by Karr’s
analysis when the term $y^{3}$ is introduced into the change-of-basis
transformations in addition to $y^{2}$. $\blacktriangle$

###  1.2 Related Work

Many different types of _discrete abstractions_ have been studied for hybrid
systems [1] including predicate abstraction [39] and abstractions based on
invariants [25]. The use of counter-example guided iterative abstraction-
refinement has also been investigated in the past (Cf. Alur et al. [2] and
Clarke et al. [6], for example). In this paper, we consider continuous
abstractions for continuous systems specified as ODEs, discrete systems and
hybrid systems using a change of bases transformation. As noted above, not all
transformations can be used for this purpose. Our abstractions for ODEs bear
similarities to the notion of topological semi-conjugacy between flows of
dynamical systems [23].

Previous work on invariant generation for hybrid system by the author
constructs invariants by assuming a desired template form (ansatz) with
unknown parameters and applying the “consecution” conditions such as _strong
consecution_ and _constant scale_ consecution [38]. Matringe et al. present
generalizations of these conditions using morphisms [22]. Therein, they
observe that strong and constant scale consecution conditions correspond to a
linear abstraction of the original non-linear system of a restrictive form.
Specifically, the original system is abstracted by a system of the form
$\frac{dx}{dt}=0$ for strong consecution, and a system of the form
$\frac{dx}{dt}=\lambda x$ for constant-scale consecution. This paper builds
upon this observation by Matringe et al. using fixed-point computation
techniques to search for a general linear abstraction that is related to the
original system by a change of basis transformation. Our work is also related
to the technique of differential invariants proposed by Platzer et al. [29].
At a high level Platzer et al. attempt to prove an invariant $p=0$ for a
continuous system (often a subsystem of a larger hybrid system) using
differential invariant rule wherein the state assertion $\frac{dp}{dt}=0$ is
established. Likewise, to prove $p\leq 0$, it seeks to establish
$\frac{dp}{dt}\leq 0$. In this paper, we may view the same process through a
CoB transformation $w\mapsto p(x)$ that allows us to write the abstract
dynamics as $\frac{dw}{dt}=0$. Going further, we seek to compute
$\vec{w}\mapsto\alpha(\vec{x})$ that maps the dynamics to an affine or a
polynomial system. On the other hand, differential invariants allow us to
reason about Boolean combinations of assertions and embed into a rich dynamic-
logic framework combining discrete and continuous actions on the state. The
work here and its extension to differential inequalities [34] can be utilized
in such a framework.

Fixed point techniques for deriving invariants of differential equations have
been proposed by the author in previous papers [37, 33] These techniques have
addressed the derivation of polyhedral invariants for affine systems [37] and
algebraic invariants for systems with polynomial right-hand sides [33]. In
this technique, we employ the machinery of fixed-points. Our primary goal is
not to derive invariants, per se, but to search for abstractions of non-linear
systems into linear systems.

##### Discrete Systems:

There has been a large body of work focused on the use of algebraic techniques
for deriving invariants of programs. Previous work by the author focuses on
deriving polynomial equality invariants for programs, automatically, by
setting up template polynomial invariants with unknown coefficients and
deriving constraints on values of these coefficients to ensure invariance [38,
35]. Carbonell et al. present loop invariant generation techniques by solving
recurrences and computing polynomial ideas to capture algebraic properties of
the reachable states [32] and subsequently using the descending abstract
interpretation over ideals with widening over ideals to ensure termination
[31]. The approach is extended to polyhedral cones generated by polynomial
inequalities to generate polynomial inequality invariants [3]. Another set of
related techniques concern the use of linear invariant generation techniques
for polynomial equality invariant generation. Müller-Olm and Seidl explore the
use of linear algebraic techniques, wherein a vector space of matrices are
used to summarize the transformation from the initial state of a program to a
given location. This space is then used to generate polynomial invariants of
the program [24]. Likewise, the work of Colón explores degree-bounded
restrictions to Nullstellensatz to enable linear algebraic techniques to
generate polynomial invariants [9]. More recently, the work of Kovacs uses
sophisticated techniques for solving recurrence equations over so-called
P-solvable loops to generate polynomial invariants for them [18].

Finally, our approach is closely related to _Carlemann embedding_ that can be
used to linearize a given differential equation with polynomial right-hand
sides [19]. The standard Carlemann embedding technique creates an infinite
dimensional linear system, wherein, each dimension corresponds to a monomial
or a basis polynomial. In practice, it is possible to create a linear
approximation with known error bounds by truncating the monomial terms beyond
a degree cutoff. Our approach for differential equation abstractions can be
_roughly_ seen as a search for a “finite submatrix” inside the infinite matrix
created by the Carleman linearization. The rows and columns of this submatrix
correspond to monomials such that the derivative of each monomial in the
submatrix is a linear combination of monomials that belong the submatrix.
Note, however, that while Carleman embedding is defined using some basis for
polynomials (usually power-products), our approach can derive transformations
that may involve polynomials as opposed to just power-products.

##### Organization:

The rest of this paper presents our approach for Ordinary Differential
Equations in Section 2. The ideas for discrete systems are presented in
Section 3 by first presenting the theory for simple loops and then extending
it to arbitrary discrete programs modeled by transition systems. The
extensions to hybrid systems are presented briefly by suitably merging the
techniques for discrete programs with those for ODEs. Finally, Section 4
presents an evaluation of the ideas presented using our implementation that
combines an automatic search for CoB transformations with polyhedral invariant
generation for continuous, discrete and hybrid systems [10, 16, 37].

##  2 Abstractions for ODEs

We first present some preliminary definitions for continuous systems defined
by Ordinary Differential Equations (ODEs).

###  2.1 Preliminaries: Continuous Systems

Let $\mathbb{R}$ denote the field of real numbers. Let $x_{1},\ldots,x_{n}$
denote a set of variables, collectively represented as $\vec{x}$. The set
$\mathbb{R}[\vec{x}]$ denotes the ring of multivariate polynomials over
$\mathbb{R}$.

A _power-product_ over $\vec{x}$ is of the form
$x_{1}^{r_{1}}x_{2}^{r_{2}}\cdots x_{n}^{r_{n}}$, succinctly written as
$\vec{x}^{\vec{r}}$, wherein each $r_{i}\in\mathbb{N}$. The _degree_ of a
monomial $\vec{x}^{\vec{r}}$ is given by
$\sum_{i=1}^{n}r_{i}=\vec{1}\cdot\vec{r}$. A _monomial_ is of the form $c\cdot
m$ where $c\in\mathbb{R}$ and $m$ is a power-product. A multivariate
polynomial $p$ is a sum of finitely many monomial terms:
$p=\sum_{\vec{r}\in\mathbb{R}^{n}}c_{r}\vec{x}^{\vec{r}}$. The degree of a
multivariate polynomial $p$ is the maximum over the degrees of all monomial
terms $m$ that _occur_ in $p$ with a non-zero coefficient.

We assume some basic familiarity with the basics of computational algebraic
geometry [11] and elementary linear algebra [17].

##### Vector Fields:

A _vector field_ $F$ over a manifold $M\subseteq\mathbb{R}^{n}$ is a map
$F:M\mapsto\mathbb{R}^{n}$ from each $\vec{x}\in M$ to a vector
$F(\vec{x})\in\mathbb{R}^{n}$, wherein $F(\vec{x})\in T_{M}(\vec{x})$, the
tangent space of $M$ at $\vec{x}$.

A vector field $F$ is continuous if the map $F$ is continuous. A _polynomial
vector field_ $F\in(\mathbb{R}[\vec{x}])^{n}$ is specified by a tuple
$F(\vec{x})=\left\langle
p_{1}(\vec{x}),p_{2}(\vec{x}),\ldots,p_{n}(\vec{x})\right\rangle$, wherein
$p_{1},\ldots,p_{n}\in\mathbb{R}[\vec{x}]$.

A system of (coupled) ordinary differential equations (ODE) specifies the
evolution of variables $\vec{x}:(x_{1},\ldots,x_{n})\in M$ over time $t$:

$\frac{dx_{1}}{dt}=p_{1}(x_{1},\ldots,x_{n}),\ \cdots,\
\frac{dx_{n}}{dt}=p_{n}(x_{1},\ldots,x_{n})\,,$

The system implicitly defines a vector field $F(\vec{x}):\left\langle
p_{1}(\vec{x}),\ldots,p_{n}(\vec{x})\right\rangle$. We assume that all vector
fields $F$ considered in this paper are (locally) Lipschitz continuous over
the domain $M$. In general, all polynomial vector fields are locally Lipschitz
continuous, but not necessarily _globally_ Lipschitz continuous over an
unbounded domain $X$. The Lipschitz continuity of the vector field $F$,
ensures that given $\vec{x}=\vec{x}_{0}$, there exists a time $T>0$ and a
unique time trajectory $\tau:[0,T)\mapsto\mathbb{R}^{n}$ such that
$\tau(t)=\vec{x}_{0}$ [23].

######  Definition 2.1.

For a vector field $F:\ \left\langle f_{1},\ldots,f_{m}\right\rangle$, the
_Lie derivative_ of a smooth function $f(\vec{x})$ is given by

$\mathcal{L}_{F}(f)=(\nabla f)\cdot
F(\vec{x})=\mathop{\sum}_{i=1}^{n}\left(\frac{\partial f}{\partial x_{i}}\cdot
f_{i}\right)$

Henceforth, wherever the vector field $F$ is clear from the context, we will
drop subscripts and use $\mathcal{L}(p)$ to denote the Lie derivative of $p$
w.r.t $F$.

######  Definition 2.2.

A continuous system over variables $x_{1},\ldots,x_{n}$ consists of a tuple
$\mathcal{S}:\left\langle X_{0},\mathcal{F},X_{I}\right\rangle$ wherein
$X_{0}\subseteq\mathbb{R}^{n}$ is the set of initial states, $\mathcal{F}$ is
a vector field over the domain represented by a manifold
$X_{I}\subseteq\mathbb{R}^{n}$.

Note that in the context of hybrid systems, the set $X_{I}$ is often referred
to as the _state invariant_ or the _domain_ manifold.

###  2.2 Change-of-Bases for Continuous Systems

In this section, we will present change-of-bases (CoB) transformations of
continuous systems and some of their properties.

Consider a map $\alpha:\mathbb{R}^{k}\mapsto\mathbb{R}^{l}$. Given a set
$S\subseteq\mathbb{R}^{k}$, let $\alpha(S)$ denote the set obtained by
applying $\alpha$ to all the elements of $S$. Likewise, the inverse map over
sets is $\alpha^{-1}(T):\ \\{s\ |\ \alpha(s)\in T\\}$. Let
$\mathcal{S}:\left\langle X_{0},\mathcal{F},X_{I}\right\rangle$ be a
continuous system over variables $\vec{x}:\ (x_{1},\ldots,x_{n})$ and
$\mathcal{T}:\left\langle Y_{0},\mathcal{G},Y_{I}\right\rangle$ be a
continuous system over variables $\vec{y}:(y_{1},\ldots,y_{m})$.

######  Definition 2.3.

We say that $\mathcal{T}$ _simulates_ $\mathcal{S}$ iff there exists a smooth
mapping $\alpha:\ \mathbb{R}^{n}\mapsto\mathbb{R}^{m}$ such that

  1. 1.

$Y_{0}\supseteq\alpha(X_{0})$ and $Y_{I}\supseteq\alpha(X_{I})$.

  2. 2.

For any trajectory $\tau:[0,T)\mapsto X_{I}$ of $\mathcal{S}$,
$\alpha\circ\tau$ is a trajectory of $\mathcal{T}$.

A simulation relation implies that any time trajectory of $\mathcal{S}$ can be
mapped to a trajectory of $\mathcal{T}$ through $\alpha$. However, since
$\alpha$ need not be invertible, the converse need not hold. I.e,
$\mathcal{T}$ may exhibit time trajectories that are not mapped onto by any
trajectory in $\mathcal{S}$.

Let $\mathcal{S}$ and $\mathcal{T}$ be defined by Lipschitz continuous vector
fields. The following theorem enables us to check given $\mathcal{S}$ and
$\mathcal{T}$, if $\mathcal{T}$ simulates $\mathcal{S}$.

######  Theorem 2.1.

$\mathcal{T}$ simulates $\mathcal{S}$ if the following conditions hold:

  1. 1.

$Y_{0}\supseteq\alpha(X_{0})$.

  2. 2.

$Y_{I}\supseteq\alpha(X_{I})$.

  3. 3.

$\mathcal{G}(\alpha(\vec{x}))=J_{\alpha}.\mathcal{F}(\vec{x})$, wherein,
$J_{\alpha}$ is the Jacobian matrix

$J_{\alpha}(x_{1},\ldots,x_{n})=\left[\begin{array}[]{rcl}\frac{\partial\alpha_{1}}{\partial
x_{1}}&\cdots&\frac{\partial\alpha_{1}}{\partial x_{n}}\\\
\vdots&\ddots&\vdots\\\ \frac{\partial\alpha_{m}}{\partial
x_{1}}&\cdots&\frac{\partial\alpha_{m}}{\partial x_{n}}\\\
\end{array}\right]\,,$

and $\alpha(\vec{x})=(\alpha_{1}(\vec{x}),\cdots,\alpha_{m}(\vec{x})),\
\alpha_{i}:\mathbb{R}^{n}\mapsto\mathbb{R}$.

###### Proof.

Let $\tau_{x}$ be a trajectory over $\vec{x}$ for system $\mathcal{S}$. Note
that at any time instant $t\in[0,t)$,
$\frac{d\tau_{x}}{dt}=\mathcal{F}(\tau(t))$.

We wish to show that $\tau_{y}(t)=\alpha(\tau_{x}(t))$ is a time trajectory
for the system $\mathcal{T}$. Since, $\tau_{x}(0)\in X_{0}$, we conclude that
$\tau_{y}(0)=\alpha(\tau_{x}(0))\in Y_{0}$. Since $\tau_{x}(t)\in X_{I}$ for
all $t\in[0,T)$, we have that $\tau_{y}(t)=\alpha(\tau_{x}(t))\in Y_{I}$.
Differentiating $\tau_{y}$ we get,

$\begin{array}[]{rclclcl}\frac{d\tau_{y}}{dt}&=&\frac{d\alpha(\tau_{x}(t))}{dt}&=&J_{\alpha}\cdot\frac{d\tau_{x}}{dt}&=&J_{\alpha}\cdot\mathcal{F}(\tau_{x}(t))\\\
&=&\mathcal{G}(\alpha(\tau_{x}(t)))&=&\mathcal{G}(\tau_{y}(t))\,.\\\
\end{array}$

Therefore $\tau_{y}=\alpha\circ\tau_{x}$ conforms to the dynamics of
$\mathcal{T}$. By Lipschitz continuity of $\mathcal{G}$, we obtain that
$\tau_{y}$ is the unique trajectory starting from $\alpha\circ\tau(0)$. ∎

Theorem 2.1 shows that the condition

$\mathcal{G}(\alpha(\vec{x}))=J_{\alpha}.\mathcal{F}(\vec{x})$

relating vector fields $\mathcal{F}$ and $\mathcal{G}$ suffices to guarantee
that time trajectories (integral curves) of $\mathcal{F}$ are related to those
in $\mathcal{G}$ through the map $\alpha$. In differential geometric terms,
this condition can be stated as $\mathcal{F}$ is $\alpha$-related to
$\mathcal{G}$ [20].

Note that, in general, a trajectory $\tau_{y}(t)=\alpha(\tau_{x}(t))$ may
exist for a longer interval of time than the interval $[0,T)$ over which
$\tau_{x}$ is assumed to be defined.

######  Theorem 2.2.

Let $\mathcal{T}$ simulate $\mathcal{S}$ through a map $\alpha$. If
$Y\subseteq Y_{I}$ is a positive invariant set for $\mathcal{T}$ then
$\alpha^{-1}(Y)\cap X_{I}$ is a positive invariant set for $\mathcal{S}$.

###### Proof.

Assuming otherwise, let $\tau_{x}$ be a time trajectory that starts from
inside $\alpha^{-1}(Y)\cap X_{I}$ and has a time instant $t$ such that
$\tau_{x}(t)\not\in\alpha^{-1}(Y)\cap X_{I}$. Since we defined time
trajectories so that $\tau_{x}(t)\in X_{I}$, it follows that
$\tau_{x}(t)\not\in\alpha^{-1}(Y)$. As a result, $\alpha(\tau_{x}(t))\not\in
Y$. Therefore, corresponding to $\tau_{x}$, we define a new trajectory
$\tau_{y}=\alpha\circ\tau_{x}$ which violates the positive invariance of $Y$.
This leads to a contradiction. ∎

Let $\varphi[\vec{y}]$ be an assertion representing an invariant of the system
$\mathcal{T}$ that simulates $\mathcal{S}$ through CoB transformation
$\alpha$. The assertion $\varphi[\vec{y}\mapsto\alpha(\vec{x})]$ obtained by
substituting $\alpha(\vec{x})$ in place of occurrences of $\vec{y}$ is an
invariant for the original system. In other words, inverting the map $\alpha$
simply boils down to substituting $\alpha(\vec{x})$ in the invariants of the
abstract system. An application of the Theorem above is illustrated in Example
1.1.

######  Example 2.1.

Consider a mechanical system $\mathcal{S}$ expressed in generalized position
coordinates $(q_{1},q_{2})$ and momenta $(p_{1},p_{2})$ defined using the
following vector field:

$F(p_{1},p_{2},q_{1},q_{2}):\left\langle\begin{array}[]{l}-2q_{1}q_{2}^{2},\
-2q_{1}^{2}q_{2},\ 2p_{1},\ 2p_{2}\end{array}\right\rangle$

with the initial conditions: $(p_{1},p_{2})\in[-1,1]\times[-1,1]\ \land\
(q_{1},q_{2}):(2,2)$. Using the transformation
$\alpha(p_{1},p_{2},q_{1},q_{2}):p_{1}^{2}+p_{2}^{2}+q_{1}^{2}q_{2}^{2}$, we
see that $\mathcal{S}$ is simulated by a linear system $\mathcal{T}$ over $y$,
with dynamics given by $\frac{dy}{dt}=0,\ y(0)\in[16,18]$.

Incidentally, the form of the system $\mathcal{T}$ above indicates that
$\alpha$ is an expression for a conserved quantity (in this case, the
Hamiltonian) of the system. $\blacktriangle$

The main goal of this work is to study CoB transformations that “simplify” the
system’s dynamics either (a) casting a non-algebraic vector field into one
defined algebraically or (b) reducing the degree of a given algebraic vector
field by means of an abstraction. A special case consists of _linearizing CoB
transformations_ that map a non-linear system to one defined by affine
dynamics.

Recall that a system $\mathcal{T}$ is algebraic if it is described by a
polynomial vector field. Furthermore, $\mathcal{T}$ is _affine_ if it is
described by an affine vector field $\frac{d\vec{y}}{dt}=A\vec{y}+\vec{b}$ for
an $m\times m$ matrix $A$ and an $m\times 1$ vector $\vec{b}$.

######  Definition 2.4.

Let $\mathcal{S}$ be a (non-linear) system. We say that $\alpha$ is an
_algebraizing CoB transformation_ if it maps $\mathcal{S}$ to an algebraic
system $\mathcal{T}$.

We say that $\alpha$ is a _linearizing CoB transformation_ if it maps each
trajectory of $\mathcal{S}$ to that of an affine system $\mathcal{T}$.

######  Example 2.2.

Consider the vector field $\mathcal{F}$

$\frac{dx}{dt}=x^{3}-2x^{2}+y^{2}+xy,\ \frac{dy}{dt}=2x-3x^{2}+2y^{3}\,.$

Let $\alpha:(x,y)\rightarrow(w_{1},w_{2},w_{3},w_{4})$ be defined as

$\alpha(x,y):(x,y,x^{2},y^{2})$

We can verify that using $\alpha$, we note that $\mathcal{F}$ is simulated by
the vector field $\mathcal{G}$:

$\begin{array}[]{ll}\frac{dw_{1}}{dt}=w_{1}w_{3}-2w_{3}+w_{4}+w_{1}w_{2},&\frac{dw_{2}}{dt}=2w_{1}-3w_{3}+2w_{2}w_{4}\\\
\frac{dw_{3}}{dt}=-4w_{1}w_{3}+2w_{3}^{2}+2w_{2}w_{3}+2w_{1}w_{4},&\frac{dw_{4}}{dt}=4w_{1}w_{2}-6w_{2}w_{3}+4w_{4}^{2}\\\
\end{array}$

Note that while $\mathcal{F}$ is a cubic vector field over $\mathbb{R}^{2}$,
$\mathcal{G}$ is a quadratic vector field over $\mathbb{R}^{4}$.
$\blacktriangle$

Example 1.1 illustrates a linearizing CoB transformation.

The above definition of an algebraizing or linearizing CoB seems useful, in
practice, only if $\alpha$ and $\mathcal{T}$ are already known. We may then
use known techniques for reasoning over algebraic systems or affine systems
for safely bounding the reachable set of an affine system, given some initial
conditions, and transform the result back through substitution to obtain a
bound on the reachable set for $\mathcal{S}$.

We now present a technique that searches for a map $\alpha$ to obtain an
algebraic system $\mathcal{T}$ that simulates a given system $\mathcal{S}$
through $\alpha$ such that the vector field describing $\mathcal{T}$ is degree
bounded by a given degree limit $d>0$. In particular, if the degree limit $d$
is set to $1$, then the resulting transformation $\alpha$ is linearizing.

We ignore the initial condition and invariant, for the time being, and simply
focus on obtaining the dynamics of $\mathcal{T}$. In other words, we will
search for a map ${\alpha}:\ (\alpha_{1},\ldots,\alpha_{m})$ that maps
$\mathbb{R}^{n}$ into $\mathbb{R}^{m}$ so that

$J_{\alpha}(\vec{x})\cdot\mathcal{F}(\vec{x})=G(\alpha(\vec{x}))\,.$

Having found such a map, we may find appropriate over-approximate initial and
invariance conditions for the simulating system $\mathcal{T}$, so that
Definition 2.3 holds. Specifically, we are interested in finding
transformations $\alpha$ that ensure that (a) $G$ is a polynomial vector field
and (b) the degrees of polynomials describing $G$ are degree bounded by the
degree limit $d>0$.

###  2.3 Multilinear Abstractions through Dimension Copying

We first show that any polynomial system of ODEs can be abstracted by a
_multilinear_ system. However, doing so may require $\alpha$ to have many
repeated components wherein $\alpha_{i}(\vec{x})=\alpha_{j}(\vec{x})$ for
$i\not=j$.

######  Definition 2.5.

A polynomial $p$ is defined to be _multilinear_ if and only if each power-
product in $p$ is of the form $x_{1}^{r_{1}}x_{2}^{r_{2}}\cdots x_{n}^{r_{n}}$
wherein each $r_{i}=0\ \mbox{or}\ 1$.

######  Example 2.3.

As an example, the polynomial $p=2x_{1}x_{2}x_{3}+x_{1}x_{3}+4x_{1}-2x_{2}-1$
is multilinear. On the other hand, the polynomial $q=2x_{2}^{2}+x_{1}+x_{3}$
is not, owing to the $x_{2}^{2}$ power product.

We first observe that any polynomial ODE may be equivalently written by means
of a multilinear system using a suitably defined $\alpha$.

######  Theorem 2.3.

Let $\mathcal{F}$ be a polynomial vector field over
$\vec{x}\in\mathbb{R}^{n}$. There is a transformation
$\alpha:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$, that maps $\mathcal{F}$ to a
multilinear system $\mathcal{G}$.

###### Proof.

Let us write $\mathcal{F}(\vec{x}):(p_{1},\ldots,p_{n})$ for multivariate
polynomials $p_{1},\ldots,p_{n}$. We will assume that the vector field
$\mathcal{F}$ is not already multi-linear. Therefore, some $p_{j}$ has a power
product that is divisible $x_{k}^{r}$ for some $r\geq 2$. The idea is to use
$r$ different functions $\alpha_{k,1}=\alpha_{k,2}=\cdots=\alpha_{k,r}=x_{k}$
so that in the transformed system the term $x_{k}^{r}$ appears as a
multilinear product $y_{k,1}y_{k,2}\cdots y_{k,r}$.

In the worst case, the transformation $\alpha$ involves $n\times K$
components, wherein

$K=\max(\mathsf{degree}(p_{1}),\ldots,\mathsf{degree}(p_{n}))\,.$

Each component $\alpha_{i,k}:x_{i}$ is simply a “copy” of the variable $x_{i}$
that ensures multilinearity of the transformed system. ∎

######  Example 2.4.

Consider the one dimensional system defined by

$\frac{dx}{dt}=2x^{5}+3x^{2}+x-5\,.$

We use the transformation $\alpha:\mathbb{R}\rightarrow\mathbb{R}^{5}$ wherein
$\alpha_{1}(x)=\alpha_{2}(x)=\cdots=\alpha_{5}(x)=x$. Using this
transformation, we derive an abstract system defined by the ODE

$\frac{dy_{j}}{dt}=2y_{1}y_{2}y_{3}y_{4}y_{5}+3y_{1}y_{2}+y_{1}-5\,,\
j=1,2,\ldots,5.$

$\blacktriangle$

Even though there are efficient algorithms for analyzing multi-linear systems
[4], the transformation in Theorem 2.3 faces two potential problems: (a) the
dimensionality of the transformed system $\mathcal{T}$ can be as large as the
dimensionality of the original system times the maximum degree of the
polynomials in the RHS of the vector field, and (b) ignoring the implicit
equality relationships between the various dimensions results in a very coarse
abstraction while taking them into account simply gives us the original system
back (albeit in a different form).

###  2.4 Independent Transformations

The rest of this paper, will focus on _independent transformations_
$\alpha:(\alpha_{1},\ldots,\alpha_{N})$ wherein each $\alpha_{i}$ cannot be
written as a linear combination of the remaining $\alpha_{j}$s for $j\not=i$.
Assuming independence automatically rules out the constructions used in
Theorem 2.3.

In general, computing independent transformations $\alpha$ for any given ODE
is a hard problem. In this paper, we will focus on solutions that involve
searching for an appropriate map $\alpha$, wherein $\alpha$ is specified to be
the linear combination of some fixed, finite set of basis functions
$g_{1},\ldots,g_{N}$. The initial basis is assumed to be given to our
algorithm by the user. Starting from this initial basis of functions, our
algorithm searches for transformations $\alpha$ whose components can be
written as linear combinations $\sum_{i=1}^{N}\lambda_{j}g_{j}$.

The basis functions could be specified implicitly as the set of all power
products over $\vec{x}$ of degree up to some limit $K>0$ or the set of all
power products involving the variables $x_{i}$ and various non-algebraic
functions $\sin(z),\cos(z)$ and $e^{z}$ applied to these power products.
Having chosen a basis $B=\\{g_{1},\ldots,g_{N}\\}$ for $\alpha$, we will cast
the search for the map $\alpha$ as a vector space iteration.

Let $\alpha(\vec{x}):(\alpha_{1}(\vec{x}),\ldots,\alpha_{m}(\vec{x}))$ be a
smooth mapping $\alpha:\mathbb{R}^{n}\mapsto\mathbb{R}^{m}$, wherein each
$\alpha_{i}:\mathbb{R}^{n}\mapsto\mathbb{R}$. Recall that
$\mathcal{L}_{F}(\alpha_{i}(\vec{x}))=(\nabla\alpha_{i})\cdot\mathcal{F}(\vec{x})$
denotes the Lie derivative of the function $\alpha_{i}(\vec{x})$ w.r.t vector
field $\mathcal{F}$.

######  Lemma 2.1.

$J_{\alpha}\cdot\mathcal{F}(\vec{x})=\left(\begin{array}[]{c}\mathcal{L}_{F}(\alpha_{1}(\vec{x}))\\\
\mathcal{L}_{F}(\alpha_{2}(\vec{x}))\\\ \vdots\\\
\mathcal{L}_{F}(\alpha_{m}(\vec{x}))\\\ \end{array}\right)$.

###### Proof.

Recall the definition of the Jacobian matrix $J_{\alpha}$:

$J_{\alpha}(x_{1},\ldots,x_{n})=\left[\begin{array}[]{rcl}\frac{\partial
y_{1}}{\partial x_{1}}&\cdots&\frac{\partial y_{1}}{\partial x_{n}}\\\
\vdots&\ddots&\vdots\\\ \frac{\partial y_{m}}{\partial
x_{1}}&\cdots&\frac{\partial y_{m}}{\partial x_{n}}\\\
\end{array}\right]=\left[\begin{array}[]{c}\nabla\alpha_{1}\\\ \vdots\\\
\nabla\alpha_{m}\\\ \end{array}\right]\,.$

Therefore,
$J_{\alpha}.\mathcal{F}=\left(\begin{array}[]{c}(\nabla\alpha_{1})\cdot(\mathcal{F})\\\
(\nabla\alpha_{2})\cdot(\mathcal{F})\\\ \vdots\\\
(\nabla\alpha_{m})\cdot(\mathcal{F})\\\
\end{array}\right)=\left(\begin{array}[]{c}\mathcal{L}_{F}(\alpha_{1}(\vec{x}))\\\
\mathcal{L}_{F}(\alpha_{2}(\vec{x}))\\\ \vdots\\\
\mathcal{L}_{F}(\alpha_{m}(\vec{x}))\\\ \end{array}\right)$. ∎

##### Note:

For the rest of this section, we will fix a vector field $\mathcal{F}$
belonging to a system $\mathcal{S}$ as the original system for which we seek
an abstraction. We will simply write $\mathcal{L}(g)$ to denote the Lie-
derivative of a given function $g$ in place of $\mathcal{L}_{F}(g)$.

###  2.5 Vector Space Closure

We first define the vector spaces that will be used in our search.

######  Definition 2.6.

Let $B=\\{g_{1},\ldots,g_{k}\\}$ be some finite set of functions wherein
$g_{i}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$ for some fixed $n,m>0$. The
_vector space_ spanned by $G$ denoted $\mathit{Span}(B)$ consists of all
functions that are linear combinations of $g_{i}$:

$\mathit{Span}(B)=\left\\{\sum_{i=1}^{k}\lambda_{i}g_{i}\ |\
\lambda_{i}\in\mathbb{R}\right\\}\,.$

We assume, without loss of generality, that the elements in $B$ are linearly
independent. I.e., no $g_{i}\in B$ can be written as a linear combination of
the remaining $g_{j}\in B$, for $j\not=i$.

Let $\mathbf{1}$ represent the constant function
$\mathbf{1}(\vec{x})=\vec{1}\in\mathbb{R}^{m}$. Given a vector space
$V=\mathit{Span}(B)$, we define the space of power products of $V$ up to a
degree limit $d\geq 1$ as

$V^{\left\langle d\right\rangle}=\mathit{Span}\left(\left\\{g_{i_{1}}\times
g_{i_{2}}\times\cdots\times g_{i_{d}}\ |\ g_{i_{1}},\ldots,g_{i_{d}}\in
B\cup\\{\mathbf{1}\\}\right\\}\right)\,.$

In particular, note that $V^{\left\langle
1\right\rangle}=\mathit{Span}(V\cup\\{\mathbf{1}\\})$.

######  Example 2.5.

Let $B=\\{x,\sin(y)\\}$ be our basis set. The vector space $V:\
\mathit{Span}(B)$ is given by $\\{a_{1}x+a_{2}\sin(y)\ |\
a_{1},a_{2}\in\mathbb{R}\\}$. The space $V^{\left\langle 2\right\rangle}$ is
the set

$\left\\{a_{0}+a_{1}x+a_{2}\sin(y)+a_{3}x\sin(y)+a_{4}x^{2}+a_{5}\sin^{2}(y)\
|\ a_{0},\ldots,a_{5}\in\mathbb{R}\right\\}\,.$

This space is generated by the functions
$\mathbf{1},x,\sin(y),x\sin(y),x^{2},\sin^{2}(y)$. It consists of all
polynomials of degree at most $2$ formed by the functions $x$, $\sin(y)$. The
purpose of adding the function $\mathbf{1}$ is to enable terms of degree $1$
and $0$ to be considered. $\blacktriangle$

Roughly, the main idea behind our approach is to find a vector space $U$ that
satisfies the following closure property:

$(\forall\ f\in U)\ \mathcal{L}(f)\in U^{\left\langle d\right\rangle}\,.$

In other words, we will search for a vector space $U$, such that taking the
Lie derivative of any element of $U$ yields an element in $U^{\left\langle
d\right\rangle}$. Such a vector space $U$ will be called $d-\mbox{closed}$.
Let $U=\mathit{Span}\left(\left\\{h_{1},\ldots,h_{m}\right\\}\right)$ be a
$d-\mbox{closed}$ vector space. We will prove that $\alpha:\
(h_{1},\ldots,h_{m})$ maps the original system $\mathcal{S}$ to an algebraic
system $\mathcal{T}$ with a vector field of degree at most $d$.

######  Definition 2.7.

A vector space $V$ is said to be $d-\mbox{closed}$ under the application of
Lie derivatives iff $(\forall\ f\in V)\ \mathcal{L}(f)\in V^{\left\langle
d\right\rangle}$.

In order to check whether a given space $V=\mathit{Span}(B)$ is
$d-\mbox{closed}$, it suffices to verify the property in Definition 2.7 for
the elements in $B$.

######  Lemma 2.2.

A vector space
$U=\mathit{Span}\left(\left\\{h_{1},\ldots,h_{m}\right\\}\right)$ be
$d-\mbox{closed}$ under Lie derivatives if and only if $\mathcal{L}(h_{i})\in
U^{\left\langle d\right\rangle}$ for $i\in\\{1,\ldots,m\\}$.

###### Proof.

If $U$ is $d-\mbox{closed}$ under Lie derivatives then by definition, the Lie
derivatives of its basis elements $h_{i}$ should lie in $U^{\left\langle
d\right\rangle}$. We will prove the reverse direction. Let $U$ be such that
for each basis element $h_{i}$, we have $\mathcal{L}(h_{i})\in U^{\left\langle
d\right\rangle}$. Any element of $U$ can be written as
$f=\sum_{j=1}^{k}a_{j}h_{j}$ for $a_{j}\in\mathbb{R}$. We have
$\mathcal{L}(f)=\sum_{j=1}^{k}a_{j}\mathcal{L}(h_{j})$. Since each
$\mathcal{L}(h_{j})\in U^{\left\langle d\right\rangle}$, we have that
$\mathcal{L}(f)\in U^{\left\langle d\right\rangle}$. This completes the proof.
∎

Next, we relate $d-\mbox{closed}$ vector spaces to algebraizing CoB
transformations. Let $B=\left\\{h_{1},\ldots,h_{m}\right\\}$ and
$U=\mathit{Span}\left(B\right)$ be a $d-\mbox{closed}$ vector space. Let
$\alpha$ be the map from $\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$ defined as
$\alpha:(h_{1},\ldots,h_{m})$.

######  Theorem 2.4.

The map $\alpha$ formed by the basis elements of a $d-$closed vector field is
an algebraizing transformation from the original system $\mathcal{S}$ to a
system $\mathcal{T}$ defined by a polynomial vector field of degree at most
$d$.

###### Proof.

Since $U$ is $d-\mbox{closed}$, we note that for each $h_{i}$ in the basis of
$U$, we have $\mathcal{L}(h_{i})\in U^{\left\langle d\right\rangle}$. In other
words, we may write $\mathcal{L}(h_{i})$ as a linear combination of power
products as shown below:

$\mathcal{L}(h_{i}):\ \sum_{j=1}^{K}a_{ij}h_{i,j,1}\times
h_{i,j,2}\times\cdots\times h_{i,j,d}\,,\ \mbox{wherein}\ h_{i,j,k}\in
B\cup\\{\mathbf{1}\\}$ (1)

We define the system $\mathcal{T}$ over variables $y_{1},\ldots,y_{m}$. We
will use variable $y_{i}$ to correspond to $h_{i}(\vec{x})$. The dynamics are
obtained as

$\frac{dy_{i}}{dt}=\sum_{j=1}^{K}a_{ij}y_{i_{1}}\times
y_{i_{2}}\times\cdots\times y_{i_{k}}\,,$

by substituting the variable $y_{j}$ wherever the function $h_{j}$ occurs in
Equation (1). Let $G$ be the resulting vector field on $\vec{y}$. It is easy
to see that (a) $G$ is a polynomial vector field and (b) of degree at most
$d$.

From Lemma 2.1, we note that
$J_{\alpha}\mathcal{F}(\vec{x})=(\mathcal{L}(h_{1}),\ldots,\mathcal{L}(h_{m}))$.
We verify that
$(\mathcal{L}(h_{1}),\ldots,\mathcal{L}(h_{m}))=G(h_{1}(\vec{x}),\ldots,h_{m}(\vec{x}))$.
This is directly evident from the construction of $G$ from Equation (1). Thus,
the key condition (3) of Theorem 2.1 is seen to hold. By finding the right
sets $Y_{0},Y_{I}$ given $\alpha$, we take care of the remaining conditions as
well. ∎

##### Note:

The trivial space $V=\mathit{Span}(\\{0\\})$ consisting of the constant
function that maps all inputs to $\vec{0}$ is always $d-$closed. This space
yields $\alpha:(0)$ that maps all states $\vec{x}$ to the zero vector. As
such, the map $\alpha$ is not very useful in practice for inferring
invariants.

######  Example 2.6.

Consider the ODE from Example 1.1 recalled below:

$\begin{array}[]{rcl}\frac{dx}{dt}&=&xy+2x\\\
\frac{dy}{dt}&=&-\frac{1}{2}y^{2}+7y+1\\\ \end{array}$

We claim that the vector space $V$ generated by the set of functions
$\\{x,xy,xy^{2}\\}$ is $1-$closed. To verify, we compute the Lie derivative of
a function of the form $c_{1}x+c_{2}xy+c_{3}xy^{2}$ to obtain

$c_{1}(xy+2x)+c_{2}(\frac{1}{2}xy^{2}+9xy+x)+c_{3}(16xy^{2}+2xy)$

which is seen to belong to $V^{\left\langle 1\right\rangle}$. As a result, we
obtain the CoB abstraction $\alpha(x,y):(x,xy,xy^{2})$ that maps the vector
field to an affine vector field (polynomial of degree $1$).

The abstract system over $(w_{1},w_{2},w_{3})\in\mathbb{R}^{3}$ has dynamics
given by

$\begin{array}[]{rcl}\frac{dw_{1}}{dt}&=&2w_{1}+w_{2}\\\
\frac{dw_{2}}{dt}&=&\frac{1}{2}w_{3}+9w_{2}+w_{1}\\\
\frac{dw_{3}}{dt}&=&16w_{3}+2w_{2}\\\ \end{array}$

The mapping between original and abstract system is given by

$w_{1}\ \mapsto\ x,\ w_{2}\ \mapsto\ xy,\ w_{3}\ \mapsto\ xy^{2}\,.$

$\blacktriangle$

###  2.6 Finding Closed Vector Spaces

We will now describe a search technique for finding a map $\alpha$ and the
associated abstraction $\mathcal{T}$, such that the dynamics of $\mathcal{T}$
are described by polynomials with degree bound $d$. If $d=1$, the dynamics of
$\mathcal{T}$ are affine. The inputs to our search procedure are

  1. 1.

The original system $\mathcal{S}$ described by a vector field $\mathcal{F}$,

  2. 2.

The degree limit $d$ for the desired vector field $\mathcal{T}$, and

  3. 3.

An initial basis $B_{0}=\\{h_{1},\ldots,h_{N}\\}$ of continuous and
differentiable functions. We may regard the linear combination

$c_{1}h_{1}(\vec{x})+c_{2}h_{2}(\vec{x})+\ldots+c_{N}h_{N}(\vec{x})\,,$

as an _ansatz_ or a template for each component $\alpha_{j}$ of the map
$\alpha:(\alpha_{1},\ldots,\alpha_{m})$, that we are searching for. However,
we do not fix the number of components $m$ of the transformation $\alpha$,
_apriori_ , or guarantee that a non-trivial $\alpha$ (with $m>0$) can be
found.

The initial basis $B_{0}$ is often specified as consisting of all power
products of the variables in $\vec{x}$ with a given degree limit $M$. This
limit $M$ is chosen independent of the limit $d$ for the desired abstraction
$\mathcal{T}$.

Our overall approach is to start with the initial vector space
$V_{0}:\mathit{Span}(B_{0})$ and iteratively refine $V_{0}$ to construct a
sequence of vector spaces

$V_{0}\supseteq V_{1}\supseteq V_{2}\cdots\supseteq V_{k}=V_{k+1}=V^{*}$

wherein, (1) $V_{j+1}\subseteq V_{j}$, for $j\in[1,k-1]$, and (2)
$V_{k}=V_{k+1}$. The iterative scheme is designed to guarantee that the
converged result $V^{*}$ is $d-$ closed. If $V^{*}$ has a non-zero basis, then
the basis elements of $V^{*}$ form the components of the map $\alpha$ and the
abstraction $\mathcal{T}$ whose dynamics have the desired form.

The main step of iteration is to derive $V_{i+1}$ from $V_{i}$. This is
performed as follows:

$~{}V_{i+1}=\\{g\in V_{i}\ |\ \mathcal{L}(g)\in V_{i}^{\left\langle
d\right\rangle}\\}\,.$ (2)

In other words, $V_{i+1}$ retains those functions $g\in V_{i}$ whose Lie
derivatives also lie inside $V_{i}^{\left\langle d\right\rangle}$.

######  Lemma 2.3.

(1) $V_{i+1}$ is a sub-space of $V_{i}$. (2) $V_{i}$ is $d-$closed iff
$V_{i}=V_{i+1}$.

###### Proof.

We prove the two parts (1) and (2) as follows.

(1) Since by Eq. (2), $V_{i+1}\subseteq V_{i}$, it suffices to show that
$V_{i+1}$ is a vector space. Let $g_{1},\ldots,g_{k}\in V_{i+1}$. We have that
$g_{1},\ldots,g_{k}\in V_{i}$. Furthermore, since $V_{i}$ is a vector space,
any linear combination $g:\ \sum_{j=1}^{k}\lambda_{j}g_{j}\in V_{i}$. The lie
derivative $\mathcal{L}(g)$ can be written as
$\sum_{j=1}^{k}\lambda_{j}\mathcal{L}(g_{j})$. Since $\mathcal{L}(g_{j})\in
V_{i}^{\left\langle d\right\rangle}$, we have
$\mathcal{L}(g)=\sum_{j=1}^{k}\lambda_{j}\mathcal{L}(g_{j})\in
V_{i}^{\left\langle d\right\rangle}$. Therefore, by definition $g\in V_{i+1}$
as well. The linear combination of any finite subset of elements from
$V_{i+1}$ also belongs to $V_{i+1}$, proving that it is a sub-space of
$V_{i}$.

(2) If $V_{i}=V_{i+1}$, it is easy to check that $V_{i}$ satisfies the
definition of being $d-$ closed. For the other direction, let us assume that
$V_{i}$ is $d-$closed. Then for each $g\in V_{i}$, we have $\mathcal{L}(g)\in
V_{i}^{\left\langle d\right\rangle}$. Thus $g\in V_{i+1}$. This proves that
$V_{i+1}\supseteq V_{i}$. Combining with the fact that $V_{i+1}\subseteq
V_{i}$, we obtain equality. ∎

We now focus on calculating $V_{i+1}$ from $V_{i}$. Let $V_{i}:\
\mathit{Span}(B_{i})$ for a finite set $B_{i}$. Any element of $V_{i}$ can be
represented as $\sum_{h_{j}\in B_{i}}c_{j}h_{j}$ for some multipliers $c_{j}$.
The Lie derivative is expressed as $\sum_{h_{j}\in
B_{i}}c_{j}\mathcal{L}(h_{j})$. The procedure for calculating $V_{i+1}$
reduces to finding the set of multipliers $(c_{1},\ldots,c_{M})$ where
$M=|B_{i}|$ such that $\sum_{h_{j}\in B_{i}}c_{j}\mathcal{L}(h_{j})\in
V_{i}^{\left\langle d\right\rangle}$.

The key challenge lies in comparing two elements of the form
$\sum_{j}c_{j}\mathcal{L}(h_{j})$ and $\sum_{k}d_{k}g_{k}$, for unknowns
$c_{j}$ and $d_{k}$, where $h_{j}\in B_{i}$ and $g_{k}\in V_{i}^{\left\langle
d\right\rangle}$. If both the functions are polynomials over $\vec{x}$, the
comparison is performed by equating the coefficients of corresponding
monomials. This is illustrated using the example below:

######  Example 2.7.

Consider once again the ODE from Example 1.1 and 2.6. We seek to find an
affine system $\mathcal{T}$ that abstracts this system. Let us consider the
space $V_{0}$ generated by the basis $B_{0}:\\{x,y,xy,x^{2},y^{2}\\}$ of all
degree $2$ monomials. Any element in $V_{0}$ can be written as

$p(c_{1},\ldots,c_{5}):\ c_{1}x+c_{2}y+c_{3}xy+c_{4}x^{2}+c_{5}y^{2}\,.$

Its Lie derivative is given by

$\begin{array}[]{l}c_{1}(xy+2x)+c_{2}(-\frac{1}{2}y^{2}+7y+1)+c_{3}x(-\frac{1}{2}y^{2}+7y+1)\\\
+c_{3}y(xy+2x)+c_{4}(2x)(xy+2x)+c_{5}(2y)(-\frac{1}{2}y^{2}+7y+1)\end{array}$

This can be simplified as

$p^{\prime}(c_{1},\ldots,c_{5}):\
\left[\begin{array}[]{l}c_{2}+(2c_{1}+c_{3})x+(7c_{2}+2c_{5})y+(c_{1}+9c_{3})xy+4c_{4}x^{2}+\\\
(14c_{5}-\frac{1}{2}c_{2})y^{2}+\frac{1}{2}c_{3}xy^{2}+2c_{4}x^{2}y-c_{5}y^{3}\end{array}\right]\,.$

We require the Lie derivative to belong to $V^{\left\langle
1\right\rangle}=\mathit{Span}(B_{0}\cup\\{1\\})$. This yields the constraints:

$(\exists d_{0},d_{1},\ldots,d_{5})\ (\forall\ x,y)\
d_{0}+d_{1}x+d_{2}y+d_{3}xy+d_{4}x^{2}+d_{5}y^{2}=p^{\prime}(c_{1},\ldots,c_{5})\,.$

We use the lemma that two polynomials are identical iff their coefficients on
corresponding power-products are. This yields the following system of linear
equations:

$\begin{array}[]{l}c_{2}=d_{0},\ 2c_{1}+c_{3}=d_{1},\ 7c_{2}+2c_{5}=d_{2},\
c_{1}+9c_{3}=d_{3},\\\ 4c_{4}=d_{4},14c_{5}-\frac{1}{2}c_{2}=d_{5},\ c_{3}=0,\
2c_{4}=0,\ c_{5}=0\\\ \end{array}$

Eliminating $d_{0},\ldots,d_{5}$, we obtain the constraints
$c_{3}=c_{4}=c_{5}=0$. The new basis $B_{1}$ is $\\{x,y\\}$. $\blacktriangle$

On the other hand, if the basis $B_{i}$ involves non-polynomials
(trigonometric or exponential functions), then encoding equality by matching
up coefficients of syntactically identical terms is _incomplete_ : I.e, not
all solutions can be found by equating coefficients of matching terms. In
general, deciding if two expressions involving trigonometric functions is
identically zero is undecidable 111 This follows from Richardson’s theorem
[27].. In practice, we may continue to handle trigonometric functions using
the same syntactic matching technique that is complete for polynomials. If a
$d-$closed basis is discovered this way, then it may be used to derive a valid
abstraction. On the other hand, the process may be unable to find a vector
space starting from the initial set of functions even if one such exists.

######  Example 2.8.

Consider a simple example with the ODE

$\frac{dx}{dt}=\sin(x+y),\ \ \ \frac{dy}{dt}=x+y\,.$

Consider the space $V$ spanned by the basis

$B=\\{x,y,\sin(x),\sin(y),\cos(x),\cos(y)\\}\,.$

Our goal is to check if $V$ is $3-$closed. Any element of $V$ can be written
as

$c_{1}x+c_{2}y+c_{3}\sin(x)+c_{4}\sin(y)+c_{5}\cos(x)+c_{6}\cos(y)\,.$

Its Lie derivative can be written as

$\begin{array}[]{c}c_{1}\sin(x+y)+c_{2}(x+y)+c_{3}\cos(x)\sin(x+y)+c_{4}\cos(y)(x+y)\\\
-c_{5}\sin(x)\sin(x+y)-c_{6}\sin(y)(x+y)\end{array}\,.$

Our goal is to check if the Lie derivative belongs to $V^{\left\langle
3\right\rangle}$. We note that a syntactic check for membership yields the
constraints $c_{1}=c_{3}=c_{5}=0$. On the other hand, substituting the
trigonometric identity

$\sin(x+y)\equiv\sin x\cos y+\sin y\cos x\,,$

we may indeed verify that the Lie derivative of any element of $V$ belongs to
$V^{\left\langle 3\right\rangle}$. This yields a degree $3$ algebraization
given by $\alpha(x,y):(x,y,\sin(x),\sin(y),\cos(x),\cos(y))$ with the abstract
system having the dynamics

$\begin{array}[]{rcl}\frac{dw_{1}}{dt}&=&w_{3}w_{6}+w_{4}w_{5}\\\
\frac{dw_{2}}{dt}&=&w_{1}+w_{2}\\\
\frac{dw_{3}}{dt}&=&w_{3}w_{5}w_{6}+w_{5}^{2}w_{4}\\\
\frac{dw_{4}}{dt}&=&w_{6}w_{1}+w_{6}w_{2}\\\
\frac{dw_{5}}{dt}&=&-w_{3}^{2}w_{6}-w_{3}w_{4}w_{5}\\\
\frac{dw_{6}}{dt}&=&-w_{4}w_{1}-w_{4}w_{2}\\\ \end{array}$

Here $w_{1},\ldots,w_{6}$ correspond to the components of the map $\alpha$
above. $\blacktriangle$

######  Theorem 2.5.

Given an initial vector space $V_{0}$ and vector field $\mathcal{F}$, the
iterative procedure using Eqn. (2) converges in finitely many steps to a
subspace $V^{*}\subseteq V_{0}$. Let $\alpha_{1},\ldots,\alpha_{m}$ be the
basis functions that generate $V^{*}$.

  1. 1.

The transformation $\alpha:(\alpha_{1},\ldots,\alpha_{m})$ generated by the
basis functions of the final vector space leads to an abstract system whose
dynamics are described by polynomials of degree at most $d$.

  2. 2.

For every CoB transformation $\beta:(\beta_{1},\ldots,\beta_{k})$, wherein
each $\beta_{i}\in V_{0}$ and $\beta$ yields a polynomial abstraction of
degree at most $d$, it follows that $\beta_{i}\in V^{*}$.

###### Proof.

Let us represent the iterative sequence as

$V_{0}\supseteq V_{1}\supseteq V_{2}\cdots$

The convergence of the iteration follows from the observation that if
$V_{i+1}\subset V_{i}$, the dimension of $V_{i+1}$ is at least one less than
that of $V_{i}$. Since $V_{0}$ is finite dimensional, the number of iterations
is upper bounded by the number of basis functions in $V_{0}$.

Statement 1 follows directly from Theorem 2.4.

Finally, us assume that a transformation $\beta$ exists such that
$\beta_{i}\in V_{0}$. We note that the space $U$ generated by
$\mathbf{1},\beta_{1},\ldots,\beta_{k}$ is a subset of $V_{0}$ and is
$d-$closed. We can now prove by induction that $U\subseteq V_{i}$ for each
$i$. The base case is true since $U\subseteq V_{0}$.

Next, we show that if $U\subseteq V_{i}$ then $U\subseteq V_{i+1}$. This
follows from Eq. 2 since for each $p\in U$, we have $p\in V_{i}$ and
$\mathcal{L}(p)\in U^{\left\langle d\right\rangle}$. This gives us
$\mathcal{L}(p)\in V_{i}^{\left\langle d\right\rangle}$. Therefore, $p\in
V_{i+1}$.

As a result, we prove by induction that $U\subseteq V_{i}$ for each $i$. This
also means that $U\subseteq V^{*}$. ∎

Note that it is possible for the converged result $V^{*}$ to be trivial. I.e,
it is generated by the constant function $\mathbf{1}$.

######  Example 2.9.

Consider the Vanderpol oscillator whose dynamics are given by

$\dot{x}=y,\ \dot{y}=\mu(y-\frac{1}{3}y^{3}-x)\,.$

Our search for polynomials ($\mu=1$) of degree up to 20 did not yield a non-
trivial linearizing transformation.

For a trivial system, the resulting affine system $\mathcal{T}$ is
$\frac{dy}{dt}=0$ under the map $\alpha(\vec{x})=0$. Naturally, this situation
is not quite interesting but will often result, depending on the system
$\mathcal{S}$ and the initial basis chosen $V_{0}$. We now discuss common
situations where the vector space $V^{*}$ obtained as the result is guaranteed
to be non-trivial.

###  2.7 Strong and Constant Scale Consecution

The notion of “strong” consecution, “constant scale” consecution and
“polynomial scale” consecution were defined for equality invariants of
differential equations in our previous work [38] and subsequently expanded
upon by Matringe et al. [22] using the notion of morphisms. We now show that
the techniques presented in this section can generalize strong and constant
scale consecutions, ensuring that all the systems handled by the techniques
presented in our previous work [38] can be handled by the techniques here (but
not vice-versa).

######  Definition 2.8.

A function $f$ satisfies the _strong scale_ consecution requirement for a
vector field $\mathcal{F}$ iff $\mathcal{L}_{F}(f)=0$. In other words, $f$ is
a conserved quantity. Similarly, $f$ satisfies the _constant scale_
consecution iff $\exists\lambda\in\mathbb{R},\ \mathcal{L}_{F}(f)=\lambda f$.

The following theorem is a corollary of Theorem 2.5 and shows that the ideas
presented in this section can capture the notion of strong and constant scale
consecution without requiring quantifier elimination, solving an eigenvalue
problem [38] or finding roots of a univariate polynomial [22].

######  Theorem 2.6.

The result of the iteration $V^{*}$ starting from an initial space $V_{0}$
contains all the strong and constant scale invariant functions in $V_{0}$.

###### Proof.

This is a direct consequence of Theorem 2.5 by noting that for a constant
scale consecuting function $f$, the subspace $U\subseteq V_{0}$ spanned by $f$
is closed under Lie derivatives. ∎

Furthermore, if such functions exist in $V_{0}$ the result after convergence
$V^{*}$ is guaranteed to be a non-trivial vector space (of positive
dimension). Finally, constant scale and strong scale functions can be
extracted by computing the affine equality invariants of the linear system
$\mathcal{T}$ that can be extracted from $V^{*}$.

####  2.7.1 Stability

We briefly address the issue of deducing stability (or instability) of a
system $\mathcal{S}$ using an abstraction to a system $\mathcal{T}$. Since
$\alpha$ satisfies the identity

$\mathcal{G}(\alpha(\vec{x}))=J_{\alpha}.\mathcal{F}(\vec{x})\,.$

Every equilibrium of $\mathcal{S}$ ($\mathcal{F}(\vec{x})=0$) maps onto an
equilibrium of $\mathcal{T}$ ($\mathcal{G}(\vec{x})=0$), but not vice-versa.
Furthermore, the map $\alpha(\vec{x})=(\mathbf{0},\ldots,\mathbf{0})$ is an
abstraction from any non-linear system to one with an equilibrium at origin.
Therefore, unless restrictions are placed on $\alpha$, we are unable to draw
conclusions on liveness properties for $\mathcal{S}$ based on $\mathcal{T}$.
If $\alpha$ has a continuous inverse, then $\mathcal{T}$ is topologically
diffeomorphic to $\mathcal{S}$ [23]. This allows us to correlate equilibria of
$\mathcal{T}$ with those of $\mathcal{S}$. The preservation of stability under
mappings of state variables has been studied by Vassilyev and Ul’yanov [41].
We are currently investigating restrictions that will allow us to draw
conclusions about liveness properties of $\mathcal{S}$ from those of
$\mathcal{T}$.

The issue of stability preserving maps between continuous and hybrid systems
was recently addressed by the work of Prabhakar et al. [30].

###  2.8 Affine CoB Abstraction: Existence

We will now focus on the special case of CoB transformations that lead to
linear abstractions of the form $\frac{d\vec{w}}{dt}=A\vec{w}$ (and affine
abstractions of the form $\frac{d\vec{w}}{dt}=A\vec{w}+\vec{b}$).

Let $\mathcal{S}$ be a non-linear system over $\vec{x}$ that has a CoB
transformation $\alpha:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$ with $m>0$
that maps to a linear system $\frac{d\vec{w}}{dt}=A\vec{w}$.

######  Lemma 2.4.

The system $\mathcal{S}$ has $m$ conserved quantities given by the components
of the vector valued function $e^{-tA}\alpha(\vec{x})$.

###### Proof.

Our goal is to prove that the Lie derivative of each component of
$e^{-tA}\alpha(\vec{x})$ equals zero. Since $\alpha$ is a linearizing CoB, we
have $\mathcal{L}(\alpha(\vec{x}))=A\alpha(\vec{x})$.

The Lie derivative of $e^{-tA}\alpha(\vec{x})$ is given by

$e^{-tA}\mathcal{L}(\alpha(\vec{x}))+\partial_{t}e^{-tA}\alpha(\vec{x})=e^{-tA}A\alpha(\vec{x})-e^{-tA}A\alpha(\vec{x})=0\,.$

Thus we see that the Lie derivative of $e^{-tA}\alpha(\vec{x})$ vanishes.
Therefore, each component of $e^{-tA}\alpha(\vec{x})$ is a conserved quantity.
∎

Conversely, whenever the original system $\mathcal{S}$ has conserved
quantities, it trivially admits the linearization $\frac{d\vec{w}}{dt}=0$
using a transformation $\alpha$ that is formed by its conserved quantity.

######  Theorem 2.7.

A system $\mathcal{S}$ has an independent, linearizing CoB transformation
$\alpha:\mathbb{R}^{n}\mapsto\mathbb{R}^{m}$ if and only if it has $m$
linearly independent conserved quantities.

The theorem extends to affine CoB transformations that yield abstract systems
of the form $\frac{d\vec{w}}{dt}=A\vec{w}+\vec{b}$. While conservative
mechanical and electromagnetic systems naturally have conserved quantities
(eg., conservation of momentum, energy, charge, mass), many systems
encountered are dissipative. Such cases are handled by extending the approach
presented here to differential inequality abstractions [34].

Furthermore, even in a setting where conservative quantities exist, the
advantages of searching for a CoB transformation as opposed to directly
searching for a conserved quantity from an ansatz are not clear at a first
glance. The advantage of the techniques presented here lies in the fact that
existing techniques that search for conserved quantities focus for the most
part on finding polynomial conserved quantities. Whereas, searching for a CoB
transformation allows us to implicitly obtain conserved quantities that may
involve exponentials, sines and cosines in addition to polynomial conserved
quantities by focusing purely on reasoning with vector spaces generated by
polynomials.

######  Example 2.10.

We observed the following conserved quantity for the system in Example 1.1

$\begin{array}[]{l}\left(\frac{e^{-9t}}{51}+\frac{1}{102}\left(50+7\sqrt{51}\right)e^{\left(-9+\sqrt{51}\right)t}+\frac{1}{102}\left(50-7\sqrt{51}\right)e^{-\left(9+\sqrt{51}\right)t}\right)\
x+\\\
\left(-\frac{1}{102}e^{-9t-\left(9+\sqrt{51}\right)t}\left(\begin{array}[]{l}7e^{9t}-\sqrt{51}e^{9t}-14e^{\left(9+\sqrt{51}\right)t}+\\\
7e^{9t+\left(-9+\sqrt{51}\right)t+\left(9+\sqrt{51}\right)t}+\\\
\sqrt{51}e^{9t+\left(-9+\sqrt{51}\right)t+\left(9+\sqrt{51}\right)t}\end{array}\right)\right)\
xy+\\\
\left(\frac{1}{204}e^{-9t-\left(9+\sqrt{51}\right)t}\left(e^{9t}-2e^{\left(9+\sqrt{51}\right)t}+e^{9t+\left(-9+\sqrt{51}\right)t+\left(9+\sqrt{51}\right)t}\right)\right)xy^{2}\end{array}$

This is one of the three conserved quantities obtained by computing
$e^{-tA}\alpha(\vec{x})$, where

$\alpha:(x,xy,xy^{2})\ \mbox{and}\ A=\left(\begin{array}[]{ccc}2&1&0\\\
1&9&\frac{1}{2}\\\ 0&2&16\\\ \end{array}\right)\,.$

We are unaware of techniques that can directly generate such conserved
quantities. $\blacktriangle$

Finally, we conclude by noting that conserved quantities such as the one
described above seem less useful for reasoning about the dynamics of the
underlying system when compared to the CoB transformation and the resulting
abstraction that gave rise to them.

##  3 Abstractions for Discrete and Hybrid Systems

In this section, we will discuss how the techniques of the previous sections
can be extended to find CoB transformations of purely discrete programs. In
particular, our focus will be on transforming loops in programs to infer
abstractions that are of a simpler form. Our presentation will first focus on
simple loops consisting of a single location. The combination of loops with
multiple locations and continuous dynamics will be handled in the subsequent
section.

###  3.1 Transition System Models

We will first define transition system models and the action of CoB
transformations on these models. Let $\vec{x}\in X$ represent real valued
system variables, where $X\subseteq\mathbb{R}^{n}$. Transition systems will
form our basic models for loops in programs [21].

######  Definition 3.1.

A _transition system_ $\Pi$ is defined by a tuple $\left\langle
X,L,\mathcal{T},X_{0},\ell_{0}\right\rangle$, wherein,

  1. 1.

$X\subseteq\mathbb{R}^{n}$ represents the continuous state-space. We will
denote the system variables by $\vec{x}\in\mathbb{R}^{n}$.

  2. 2.

$L$ denotes a finite set of _locations_.

  3. 3.

$\mathcal{T}$ represents a finite set of _transitions_. Each transition
$t_{j}\in\mathcal{T}$ is a tuple
$\left\langle\ell_{j},m_{j},G_{j},F_{j}\right\rangle$, where

     * •

$\ell_{j}\in L$ is the pre-location of the transition, and $m_{j}\in L$ is the
post-location.

     * •

$G_{j}\subseteq\mathbb{R}^{n}$ is the guard condition on the system variables
$\vec{x}$.

     * •

$F_{j}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$ is the update function.

  4. 4.

$X_{0}\subseteq X$ represents the possible set of initial values and
$\ell_{0}\in L$ represents the starting location.

$\ell_{0}$$t_{1}$$t_{2}$$\begin{array}[]{rclp{.5cm}rcl}\vec{x}&:&(x,y,k)\\\
L&:&\\{\ell_{0}\\}\\\ \mathcal{T}&:&\left\\{\begin{array}[]{l}t_{1}:\
(\ell_{0},\ell_{0},G_{1},F_{1}),\\\ t_{2}:\
(\ell_{0},\ell_{0},G_{2},F_{2})\end{array}\right\\}\\\ X_{0}&:&\\{(x,y,k)\ |\
x=y=0\ \land\ k>0\\}\,.\\\\[5.0pt] G_{1}&:&\\{(x,y,k)\ |\
y<k\\}&&G_{2}&:&\\{(x,y,k)\ |\ y\geq k\\}\\\ F_{1}&:&\lambda(x,y,k).\
(x+y^{2},y+1,k)&&F_{2}&:&\lambda(x,y,k).\ (x,y,k)\\\ \end{array}$ Figure 2:
Transition system model for the loop in Example 1.2.

######  Example 3.1.

Figure 2 shows an example of a transition system derived from a simple program
that computes the sum of the first $k$ squares. The transition system consists
of a single location $\ell_{0}$, transitions
$t_{1}:(\ell_{0},\ell_{0},G_{1},F_{1})$ and
$t_{2}:(\ell_{0},\ell_{0},G_{2},F_{2})$. $\blacktriangle$

A _state_ of the transition system is a tuple
$\sigma:\left\langle\ell,\vec{x}\right\rangle$ where $\ell$ is the _current_
location and $\vec{x}\in X$ are the values of the continuous variables.

A _run_ is a finite or infinite sequence of states

$\sigma_{0}\xrightarrow{t_{0}}\sigma_{1}\xrightarrow{t_{1}}\cdots\rightarrow\sigma_{j}\xrightarrow{t_{j}}\sigma_{j+1}\cdots\,,$

where each $\sigma_{j}:(\ell_{j},\vec{x}_{j})$ is a state and $t_{j}$ a
transition, satisfying the following conditions:

  1. 1.

The starting state $\sigma_{0}:(\ell_{0},\vec{x}_{0})$ is initial. I.e.,
$\ell_{0}$ is the initial location of $\Pi$ and $\vec{x}_{0}\in X_{0}$.

  2. 2.

The state $\sigma_{i+1}:(\ell_{i+1},\vec{x}_{i+1})$ is related to the state
$\sigma_{i}:(\ell_{i},\vec{x}_{i})$ in the following way:

    1. (a)

The transition $t_{i}\in\mathcal{T}$ is of the form
$(\ell_{i},\ell_{i+1},G_{i},F_{i})$, leading from $\ell_{i}$ to $\ell_{i+1}$.

    2. (b)

The valuation $\vec{x}_{i}$ of the continuous variables satisfy the guard
$G_{i}$ and the valuation $\vec{x}_{i+1}$ is obtained by executing the
assignments in $F_{i}$ on $\vec{x}_{i}$:

$\vec{x}_{i}\in G_{i}\;\mbox{and}\;\vec{x}_{i+1}=F_{i}(\vec{x}_{i})\,.$

A special class of “simple loop” transition systems that have a single
location are defined below.

######  Definition 3.2.

A transition system $\Pi$ is called a _simple loop_ if it has a single
location. I.e., $L=\\{\ell\\}$. All transitions of a simple loop are self-
loops around this location $\ell$.

The transition system in Example 3.1 is a simple loop. It consists of a single
location. In general, simple loops can have multiple transitions that “loop”
around this single location.

We will now discuss the pre-image operator fpre induced by a transition. Let
$g(\vec{x})$ be some function over the state variables and $t:\ (\ell,m,G,F)$
be a transition.

######  Definition 3.3.

The _functional pre-image_ $\mbox{{fpre}}(g,t)$ is defined as $g(F(\vec{x}))$.

##### Note:

The standard precondition operator works over assertions over the state
variables, involving computing the pre-image using $F$ and computing the
intersection of the result with the guard. The functional precondition defined
here is defined over functions $g(\vec{x})$ over the state variables.

######  Example 3.2.

Consider the transition

$t:(\ell,m,G,F),\ \mbox{wherein}\ G:\ \\{(x,y)\ |\ x\geq y\\},F:\
\lambda(x,y).\ (x^{2},y^{2}-x^{2}))\,.$

The functional pre-image of the function $g(x,y):x+y$, denoted
$\mbox{{fpre}}(x+y,t)$, is given by

$\mbox{{fpre}}(x+y,t):\ (x^{2})+(y^{2}-x^{2})=y^{2}\,.$

To contrast with the standard pre-condition operator, which applies to
assertions over states, let us consider the assertion $x+y\geq 0$. We have

$\mbox{{pre}}(x+y\geq 0,t):\ y^{2}\geq 0\ \land\ x\geq y\,.$

$\blacktriangle$

We now show that fpre is a linear operator over functions.

######  Lemma 3.1.

For any transition $t$ and functions $g_{1},g_{2},g$ over $\vec{x}$, we have
$\mbox{{fpre}}(g_{1}+g_{2},t)=\mbox{{fpre}}(g_{1},t)+\mbox{{fpre}}(g_{2},t)$
and further, $\mbox{{fpre}}(\lambda g)=\lambda\mbox{{fpre}}(g)$ for any
$\lambda\in\mathbb{R}$.

###### Proof.

Proof follows by directly applying Def. 3.3. ∎

Let us consider any run of the transition system

$r:\sigma_{0}\xrightarrow{t_{0}}\sigma_{1}\rightarrow\cdots\rightarrow\sigma_{i}\xrightarrow{t_{i}}\sigma_{i+1}\cdots\,.$

Let $t_{i}:(\ell_{i},\ell_{i+1},G_{i},F_{i})$ denote the transition between
$\sigma_{i}:(\ell_{i},\vec{x}_{i})$ and
$\sigma_{i+1}:(\ell_{i+1},\vec{x}_{i+1})$. Finally, let $g(\vec{x})$ be any
function over the state variables of the transition system.

######  Lemma 3.2.

The following identity holds for all successive pairs of states
$(\ell_{i},\vec{x}_{i})\xrightarrow{t_{i}}(\ell_{i+1},\vec{x}_{i+1})$
encountered in a run of the transition system and for all functions
$g(\vec{x})$:

$\mbox{{fpre}}(g,t_{i})(\vec{x}_{i})\equiv g(\vec{x}_{i+1})\,$

###### Proof.

We may write $\mbox{{fpre}}(g,t_{i})(\vec{x}_{i})=g(F(\vec{x}_{i}))$. We know
that $\vec{x}_{i+1}=F(\vec{x}_{i})$. Therefore,
$g(\vec{x}_{i+1})=g(F(\vec{x}_{i}))=\mbox{{fpre}}(g,t_{i})(\vec{x}_{i})$. ∎

We will now discuss change-of-basis abstractions for transition systems. The
discussion will focus on defining change-of-basis abstractions for simple
loops, which are represented by a transition system with a single location
$\ell$ (Cf. Definition 3.2). The subsequent sections will extend this concept
to arbitrary transition systems.

###  3.2 CoB Abstractions For Simple Loops

Consider a simple loop $\Pi$ over $\vec{x}\in\mathbb{R}^{n}$ with a single
location $\ell$, transitions $\\{t_{1},\ldots,t_{k}\\}$, and initial condition
$X_{0}$. We seek to abstract $\Pi$ with another simple loop $\Xi$ over
$\vec{y}\in\mathbb{R}^{l}$ with a single location $m$, transitions
$\\{t_{1}^{\prime},\ldots,t_{k}^{\prime}\\}$ and initial condition $Y_{0}$.

######  Definition 3.4.

Simple loop $\Xi$ is a CoB abstraction of $\Pi$ iff there is a continuous
function $\alpha:\mathbb{R}^{n}\rightarrow\mathbb{R}^{l}$ such that

  1. 1.

The initial condition $Y_{0}\supseteq\alpha(X_{0})$,

  2. 2.

For each transition $t_{i}:(\ell,\ell,G_{i},F_{i})$ in $\Pi$, there is a
corresponding transition $t_{i}^{\prime}:(m,m,G_{i}^{\prime},F_{i}^{\prime})$
in $\Xi$ such that

    1. (a)

$G_{i}^{\prime}\supseteq\alpha(G_{i})$,

    2. (b)

$\forall\ \vec{x}\ F_{i}^{\prime}(\alpha(\vec{x}))=\alpha(F_{i}(\vec{x}))$.

We will now present an example of CoB abstraction for simple loops.

######  Example 3.3.

Consider the simple loop from Example 3.1 (also Fig. 2). We note that the map

$\alpha:\mathbb{R}^{3}\rightarrow\ \mathbb{R}^{4},\ \mbox{where}\
\alpha=\lambda(x,y,k).(x,y,k,y^{2})\,,$

yields an abstract transition system $\Xi$ over variables
$\vec{w}:(w_{1},w_{2},w_{3},w_{4})$. Informally, the variables
$(w_{1},w_{2},w_{3},w_{4})$ are place holders for the expressions
$(x,y,k,y^{2})$, respectively. The resulting transition system $\Xi$ is

$\begin{array}[]{rcl}\vec{w}&:&(w_{1},\ldots,w_{4})\\\ L&:&\\{m\\}\\\
\mathcal{T}&:&\\{t_{1}^{\prime}:\
(m,m,G_{1}^{\prime},F_{1}^{\prime}),t_{2}^{\prime}:(m,m,G_{2}^{\prime},F_{2}^{\prime})\\}\\\
X_{0}&:&w_{1}=w_{2}=w_{4}=0\ \land\ w_{3}\geq 1\\\
G_{1}^{\prime}&:&\\{\vec{w}\ |\ w_{2}<w_{3}\\}\\\ G_{2}^{\prime}&:&\\{\vec{w}\
|\ w_{2}\geq w_{3}\\}\\\ F_{1}^{\prime}&:&\lambda\ \vec{w}.\
(w_{1}+w_{4},w_{2}+1,w_{3},w_{4}+2w_{2}+1)\\\ F_{2}^{\prime}&:&\lambda\
\vec{w}.\ \vec{w}\\\ \end{array}$

The various requirements laid out in Definition 3.4 can be easily verified. We
will verify the requirement for $F_{1}^{\prime}$:
$F_{1}^{\prime}(\alpha(x,y,k))=\alpha(F_{1}(x,y,k))$, as follows:

$\begin{array}[]{rclcl}F_{1}^{\prime}(\alpha(x,y,k))&=&F_{1}^{\prime}(x,y,k,y^{2})&=&(\underset{w_{1}+w_{4}}{\underbrace{x+y^{2}}},\underset{w_{2}+1}{\underbrace{y+1}},\underset{w_{3}}{\underbrace{k}},\underset{w_{4}+2w_{2}+1}{\underbrace{y^{2}+2y+1}})\\\\[5.0pt]
&=&\alpha(x+y^{2},y+1,k)&=&\alpha(F_{1}(x,y,k))\\\ \end{array}\,.$

$\blacktriangle$

The definition of CoB abstraction immediately admits the following key
theorem.

######  Theorem 3.1.

For any run

$\sigma_{0}:(\ell,\vec{x}_{0})\xrightarrow{t_{0}}(\ell,\vec{x}_{1})\xrightarrow{t_{1}}(\ell,\vec{x}_{2})\xrightarrow{t_{2}}\cdots$

the corresponding sequence of $\Xi$-states

$\gamma_{0}:(m,\alpha(\vec{x}_{0}))\xrightarrow{t_{0}^{\prime}}(m,\alpha(\vec{x}_{1}))\xrightarrow{t_{1}^{\prime}}(m,\alpha(\vec{x}_{2}))\xrightarrow{t_{2}^{\prime}}\cdots\,,$

is a run of $\Xi$.

###### Proof.

Proof uses the property that whenever the move
$(\ell,\vec{x}_{j})\xrightarrow{t_{j}}(\ell,\vec{x}_{j+1})$ is enabled in
$\Pi$ then the move
$(m,\alpha(\vec{x}_{j}))\xrightarrow{t_{j}^{\prime}}(m,\alpha(\vec{x}_{j+1}))$
is enabled in $\Xi$.

Let $t_{j}$ be described by the guard $G_{j}$ and the functional update
$F_{j}$. Likewise, let $t_{j}^{\prime}$ be described by $G_{j}^{\prime}$ and
$F_{j}^{\prime}$. We note that $\alpha(G_{j})\subseteq G_{j}^{\prime}$. Since
$\vec{x}_{j}$ satisfies the guard of $t_{j}$, $\alpha(\vec{x}_{j})$ satisfies
that of $t_{j}^{\prime}$. The state obtained after the transition is given by

$F^{\prime}(\alpha(\vec{x}_{j}))=\alpha(F(\vec{x}_{j}))=\alpha(\vec{x}_{j+1})\,.$

We have proved that whenever the move
$(\ell,\vec{x}_{j})\xrightarrow{t_{j}}(\ell,\vec{x}_{j+1})$ is possible in
$\Pi$ then the move
$(m,\alpha(\vec{x}_{j}))\xrightarrow{t_{j}^{\prime}}(m,\alpha(\vec{x}_{j+1}))$
is possible in $\Xi$. The rest of the proof extends this to trace containment
through induction over prefixes of the traces. ∎

As a direct consequence, we may state a theorem that corresponds to Theorem
2.2 for the case of vector fields.

######  Theorem 3.2.

Let $[[\varphi]]$ be an invariant set for the abstract system $\Xi$. Then,
$\alpha^{-1}([[\varphi]])$ is an invariant of the original system $\Pi$.

###### Proof.

First, we note from Theorem 3.1 that if $(\ell,\vec{x})$ is reachable in $\Pi$
then $(m,\alpha(\vec{x}))$ is reachable in $\Xi$. Since $\varphi$ is an
invariant for $\Xi$, we have $(m,\alpha(\vec{x}))\in[[\varphi]]$. Therefore
for any reachable state $(\ell,\vec{x})$ in $\Pi$, we have
$(\ell,\vec{x})\in\alpha^{-1}([[\varphi]])$. Thus $\alpha^{-1}([[\varphi]])$
is an invariant set for $\Pi$. ∎

Given an invariant $\varphi[\vec{y}]$ for $\Xi$ in the form of an assertion,
the invariants for the original system are obtained simply by substituting
$\alpha(\vec{x})$ in the place of $\vec{y}$ in $\varphi$.

######  Example 3.4.

Consider the transition system $\Pi$ from Example 3.1 and its abstraction
$\Xi$ in Example 3.3. We note that $\Xi$ has affine guards and updates.
Therefore, we may use a standard polyhedral analysis tool to compute
invariants over $\Xi$ [10, 16, 36]. Some of the invariants obtained include

$\begin{array}[]{l}13w_{4}\leq 9w_{1}+24w_{2}\ \land\ 7w_{4}\leq
6w_{1}+11w_{2}\ \land\ 4w_{1}+7w_{2}-7w_{4}+11w_{3}\geq 11\\\
2w_{1}+3w_{2}-3w_{4}+4w_{3}\geq 4\ \land\ w_{4}\leq 2w_{1}+w_{2}\ \land\
3w_{4}\leq w_{1}+12w_{2}\\\ 9-w_{1}-3w_{2}+3w_{4}-9w_{3}\leq 0\ \land\
w_{2}\geq 0\ \land\ 1\leq w_{3}\ \land\ w_{2}-w_{3}\leq 0\\\ \end{array}$

By substituting $w_{1}\mapsto x,w_{2}\mapsto y,w_{3}\mapsto k,w_{4}\mapsto
y^{2}$ on these invariants, we conclude invariants for the original system.
For instance, we conclude facts such as

$13y^{2}-24y-9x\geq 0\ \land\ 7y^{2}-11y-6x\geq 0\ \land\ 11k-7y^{2}+7y+4x\geq
11\,.$

$\blacktriangle$

The goal, once again, is to find an abstraction $\alpha$ and an abstract
system $\Xi$ starting from a description of the system $\Pi$. Furthermore, we
require that the update functions $F_{j}^{\prime}$ in $\Xi$ are all
polynomials whose degrees are smaller than some given limit $d>0$. In
particular, if we set $d=1$, we are effectively requiring all the updates in
$\Xi$ to be affine functions over $\vec{y}$.

Our strategy will be to find a map
$\alpha:\mathbb{R}^{n}\rightarrow\mathbb{R}^{k}$. For convenience, we will
write $\alpha$ as $(\alpha_{1},\ldots,\alpha_{k})$, wherein each component
function $\alpha_{j}:\mathbb{R}^{n}\rightarrow\mathbb{R}$. Let $V$ be the
vector space spanned by the components of $\alpha$, i.e,
$V=\mathit{Span}(\\{\alpha_{1},\ldots,\alpha_{k}\\})$. Our goal will be to
ensure that for each transition $t$ in $\Pi$ and for each $\alpha_{i}$,

$\forall\ \vec{x},\ \mbox{{fpre}}(\alpha_{i}(\vec{x}),t)\ \in\ V^{\left\langle
d\right\rangle}\,.$ (3)

Let $V$ be a vector space that satisfies Eq. (3) for each transition $t$ in
$\Pi$. We will say that the space $V$ is _$d$ -closed_ w.r.t $\Pi$.

######  Theorem 3.3.

Let $V:\mathit{Span}(g_{1},\ldots,g_{k})$ be $d$-closed w.r.t $\Pi$ for
continuous functions $g_{1},\ldots,g_{k}$. The map
$\alpha:(g_{1},\ldots,g_{k})$ is a CoB transformation defining an abstract
system $\Xi$, wherein each transition of $\Xi$ has a polynomial update
function involving polynomials of degree at most $d$.

###### Proof.

We construct the abstract system $\Xi$ with variables $w_{1},\ldots,w_{k}$
representing the functions $g_{1},\ldots,g_{k}$ that are the components of
$\alpha$. $\Xi$ has a single location $m$ and for each transition
$t_{i}\in\Pi$, we construct a corresponding transition $t_{i}^{\prime}\in\Xi$
as follows.

Let $G_{i},F_{i}$ be the guard set and update function for $t_{i}$,
respectively. The guard set for $t_{i}^{\prime}$ is given by $\alpha(G_{i})$
or an over-approximation thereof. Likewise, the update $F_{i}^{\prime}$ for
$t_{i}^{\prime}$ is derived as follows. We note that

$\mbox{{fpre}}(g_{j},t_{i})=\sum_{r}c_{r_{1},r_{2},\ldots,r_{k}}g_{1}^{r_{1}}g_{2}^{r_{2}}\cdots
g_{k}^{r_{k}}\,,$

wherein $0\leq r_{1}+r_{2}+\ldots+r_{k}\leq d$. The corresponding update for
$w_{j}$ in the abstract system is given by

$F_{i}^{\prime}(w_{j})=\sum_{r}c_{r_{1},r_{2},\ldots,r_{k}}w_{1}^{r_{1}}w_{2}^{r_{2}}\cdots
w_{k}^{r_{k}}\,.$

Note that each function $F_{i}^{\prime}(w_{j})$ is a polynomial of degree at
most $d$ over $w_{1},\ldots,w_{k}$. ∎

Since the operator fpre used to define the closure in Eq. (3) is a linear
operator (Cf. Lemma 3.1), we may check the closure property for a given vector
space $V$ by checking if its basis functions satisfy the property.

######  Lemma 3.3.

The vector space $V:\mathit{Span}(\\{g_{1},\ldots,g_{k}\\})$ is $d$-closed
w.r.t $\Pi$ iff for each basis element $g_{i}$ of $V$, and for each transition
$t$ in $\Pi$, $\mbox{{fpre}}(g_{i},t)\in V^{\left\langle d\right\rangle}$.

###### Proof.

For the non-trivial direction, let $V$ be a space where for each basis element
$g_{i}$ of $V$, and for each transition $t$ in $\Pi$,
$\mbox{{fpre}}(g_{i},t)\in V^{\left\langle d\right\rangle}$. An arbitrary
element $g\in V$ can be written as a linear combination of its basis elements:
$g=\sum_{j}\lambda_{j}g_{j}$. We have
$\mbox{{fpre}}(g,t)=\sum_{j}\lambda_{j}\mbox{{fpre}}(g_{j},t)$ from Lemma 3.1.
Since $\mbox{{fpre}}(g_{j},t)\in V^{\left\langle d\right\rangle}$, which is a
vector space itself, we have that $\mbox{{fpre}}(g,t)$ is a linear combination
of elements in $V^{\left\langle d\right\rangle}$ and thus
$\mbox{{fpre}}(g,t)\in V^{\left\langle d\right\rangle}$. Thus $V$ is
$d$-closed. ∎

######  Example 3.5.

Once again, consider the system $\Pi$ in Example 3.1 and the map
$\alpha:(x,y,k,y^{2})$ from Example 3.3. The components of this map are the
functions $\alpha_{1}:x,\alpha_{2}:y,\alpha_{3}:k,\mbox{and}\
\alpha_{4}:y^{2}$. We may verify that the vector space
$V:\mathit{Span}(\\{x,y,k,y^{2}\\})$ satisfies the closure property in Eq. (3)
for $d=1$. The table below shows the results of applying fpre on each of the
basis elements.

$\begin{array}[]{|l|l|l|}\hline\cr\mbox{Basis function}\
g_{j}&\mbox{{fpre}}(g_{j},t_{1})&\mbox{{fpre}}(g_{j},t_{2})\\\ \hline\cr
x&x+y^{2}&x\\\ y&y+1&y\\\ k&k&k\\\ y^{2}&y^{2}+2y+1&y^{2}\\\
\hline\cr\end{array}$

Thus, $\mbox{{fpre}}(g_{j},t_{k})$ belongs to $V^{\left\langle
1\right\rangle}=\mathit{Span}(\\{1,x,y,k,y^{2}\\})$. $\blacktriangle$

##### Searching for Abstractions:

The procedure for finding abstractions is identical to that used for vector
fields with the caveat that closure under Lie-derivative is replaced by
closure under $\mbox{{fpre}}(\cdot,t_{j})$ for every transition $t_{j}$ in the
system. The procedure takes as input an initial basis of functions $B_{0}$ and
iteratively refines the vector space $V_{i}:\mathit{Span}(B_{i})$ by removing
all the functions that do not satisfy the closure property.

######  Example 3.6.

Consider the system $\Pi$ in Example 3.1 and the initial basis consisting of
all monomials of degree at most $2$ over variables $x,y,k$. We obtain the
basis $B_{0}:\\{x,y,k,x^{2},y^{2},k^{2},xy,yk,xk\\}$ and the space
$V_{0}:\mathit{Span}(B_{0})$. An element of $V_{0}$ can be written as

$p:\
\left[\begin{array}[]{c}c_{1}x+c_{2}y+c_{3}k+c_{4}x^{2}+c_{5}y^{2}+c_{6}k^{2}\\\
+c_{7}xy+c_{8}yk+c_{9}xk\,.\end{array}\right]$

We consider the transition $t_{1}$ with update
$F_{1}:\lambda(x,y,k).(x+y^{2},y+1,k)$. Transition $t_{2}$ is ignored as its
update is simply the identity relation. We have $\mbox{{fpre}}(p,t_{1})$ as

$\mbox{{fpre}}(p,t_{1}):\
\left[\begin{array}[]{c}(c_{2}+c_{5})+(c_{1}+c_{7})x+(c_{2}+2c_{5})y+(c_{3}+c_{8})k+c_{4}x^{2}+\\\
(c_{1}+c_{5}+c_{7})y^{2}+c_{6}k^{2}+c_{7}xy+c_{7}y^{3}+c_{4}y^{4}+2c_{4}xy^{2}+\\\
c_{8}yk+c_{9}xk+c_{9}y^{2}k\end{array}\right]$

The “overflow” terms $c_{7}y^{3}$, $c_{4}y^{4}$, $c_{9}y^{2}k$ immediately
yield the constraints $c_{4}=c_{7}=c_{9}=0$. The refined basis is
$B_{1}:\\{x,y,k,y^{2},k^{2},yk\\}$. The iterative process converges with
$V_{1}:\mathit{Span}(B_{1})$ yielding a linearization. $\blacktriangle$

###  3.3 Abstractions for General Transition Systems

Thus far, we have presented CoB abstractions for simple loops consisting of a
single location. The ideas seamlessly extend to systems with multiple
locations with a few generalizations that will be described in this section.

Let $\Pi$ be a system with a set of locations
$L=\\{\ell_{1},\ldots,\ell_{k}\\}$ and transitions $\mathcal{T}$. We will
assume that $|L|\geq 2$ so that the system is no longer a simple loop. The
main idea behind change of basis (CoB) transformations for systems with
multiple locations is to allow a different map for each location. In other
words, the abstraction is defined by a maps $\alpha_{\ell}(\vec{x})$ for each
location $\ell\in L$.

The maps for two different locations $\ell_{1}$ and $\ell_{2}$ are of the type
$\alpha_{\ell_{1}}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m_{1}}$ and
$\alpha_{\ell_{2}}:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m_{2}}$. In general,
we may assume that $m_{1}\not=m_{2}$. This discrepancy can be remedied by
padding each $\alpha_{\ell_{i}}$ with extra components that map to the
constant function $0$. While, this transformation violates the linear
independence requirement between the various components in $\alpha$, it makes
the resulting abstract system easier to describe. Without loss of generality,
we assume that all the maps $\alpha_{\ell}$ for each $\ell\in L$ are of the
form $\alpha_{\ell}:\ \mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$ for a fixed
$m>0$.

######  Definition 3.5.

A system $\Xi$ is a CoB abstraction of $\Pi$ through a collection of maps
$\alpha_{\ell_{1}},\ldots,\alpha_{\ell_{k}}$ each of the type
$\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$, corresponding to locations
$\ell_{1},\ldots,\ell_{k}$, iff

  1. 1.

$\Xi$ has locations $m_{j}$ corresponding to $\ell_{j}\in L$ for $1\leq j\leq
k$ , and transitions $t_{i}^{\prime}$ corresponding to transition
$t_{i}\in\mathcal{T}$.

  2. 2.

For each transition
$t_{i}:\left\langle\ell_{pre},\ell_{post},G_{i},F_{i}\right\rangle$ in $\Pi$,
the corresponding transition $t_{i}^{\prime}:\left\langle
m_{pre},m_{post},G_{i}^{\prime},F_{i}^{\prime}\right\rangle$ is such that

    1. (a)

$m_{pre}$ and $m_{post}$ correspond to $\ell_{pre}$ and $\ell_{post}$,
respectively,

    2. (b)

$G_{i}^{\prime}\supseteq\alpha_{\ell_{pre}}(G_{i})$,

    3. (c)

$(\forall\ \vec{x})\
F_{i}^{\prime}(\alpha_{\ell_{pre}}(\vec{x}))=\alpha_{post}(F_{i}(\vec{x}))$.

We note that for a simple loop with a single location, the definition above is
identical to Def. 3.4.

⬇ int x,y,z; // .. initialize.. while (x + y - z <= 100){ (x,y):=( x + z * (x - y) , y + z * (y - x)); // x,y,z unmodified here (x,y,z) := (z+1 , x+y -1 , z+x+y -1 ); } |  $\ell_{1}$$\ell_{2}$$\ell_{3}$$t_{1}$$t_{3}$$t_{2}$$\begin{array}[]{rcl}L&:&\\{\ell_{1},\ell_{2},\ell_{3}\\}\\\ \mathcal{T}&:&\\{t_{1},t_{2},t_{3}\\}\\\ t_{1}&:&\left\langle\ell_{1},\ell_{2},G_{1},F_{1}\right\rangle\\\ t_{2}&:&\left\langle\ell_{2},\ell_{1},G_{2},F_{2}\right\rangle\\\ t_{3}&:&\left\langle\ell_{1},\ell_{3},G_{3},F_{3}\right\rangle\\\\[5.0pt] G_{1}&:&\\{(x,y,z)\ |\ x+y-z\leq 100\\}\\\ F_{1}&:&\left(x+zx-zy,y+zy-zx,z\right)\\\\[5.0pt] G_{2}&:&\mathbb{Z}^{3}\\\ F_{1}&:&\left(z+1,x+y-1,z+x+y-1\right)\\\\[5.0pt] G_{3}&:&\\{(x,y,z)\ |\ x+y-z>100\\}\\\ F_{3}&:&(x,y,z)\end{array}$
---|---
Figure 3:  An example program fragment with multiple locations and its
transition system.

######  Example 3.7.

Figure 3 shows an example of a transition system with multiple locations.
Consider the following CoB transformation:

$\begin{array}[]{rcl}\alpha_{\ell_{1}}&:&(z^{2},yz,xz,z,y^{2},xy,y,x^{2},x)\\\
\alpha_{\ell_{2}}&:&(z^{2},yz+xz,z,y,y^{2}+2xy+x^{2},x,0,0,0)\\\
\alpha_{\ell_{3}}&:&(z^{2},yz,xz,z,y^{2},xy,y,x^{2},x)\\\ \end{array}$

The transformation yields an abstraction $\Xi$ of the original system. The
abstract system has $9$ variables $w_{0},\ldots,w_{8}$. The structure of $\Xi$
mirrors that of $\Pi$ with three locations $m_{1},m_{2},m_{3}$ corresponding
to $\ell_{1},\ell_{2},\ell_{3}$, respectively and three transitions
$t_{1}^{\prime},t_{2}^{\prime}$ and $t_{3}^{\prime}$ corresponding to
$t_{1},t_{2}$ and $t_{3}$ in $\Pi$. The guards and updates of the transition
$t_{1}^{\prime}$ are

$\begin{array}[]{rcl}G_{1}^{\prime}&:&\\{(w_{0},\ldots,w_{8})\ |\
w_{8}+w_{6}-w_{3}\leq 100\\},\\\
F_{1}^{\prime}&:&(w_{0},w_{1}+w_{2},w_{3},w_{1}-w_{2}+w_{6},w_{4}+2w_{5}+w_{7},-w_{1}+w_{2}+w_{8},0,0,0)\\\
\end{array}$

We verify the key condition that ensures that $t_{1}^{\prime}$ is an
abstraction of $t_{1}$:

$\alpha_{\ell_{2}}(F_{1}(x,y,z))=F_{1}^{\prime}(\alpha_{\ell_{1}}(x,y,z))\,.$

The LHS $\alpha_{\ell_{2}}(F_{1}(x,y,z))=\alpha_{\ell_{2}}(x+zx-zy,y+zy-zx,z)$
is given by

$(z^{2},zx+zy,z,y+zy-zx,x^{2}+2xy+y^{2},x+zx-zy,0,0,0)\,.$

The RHS
$F_{1}^{\prime}(\alpha_{\ell_{1}}(x,y,z))=F_{1}^{\prime}(z^{2},yz,xz,z,y^{2},xy,y,x^{2},x)$
is given by

$(z^{2},xz+yz,z,y-zx+zy,y^{2}+2xy+x^{2},x+zx-zy,0,0,0)\,.$

The identity of LHS and RHS is thus verified. $\blacktriangle$

Our goal once again is to search of a collection of transformations
$\alpha_{\ell}$, for each $\ell\in L$ such that the resulting system is
described by polynomial updates of degree at most $d$. The case where $d=1$
corresponds to affine updates. Once again, we generalize the notion of a
$d-$closed vector space. Consider a collection of vector spaces
$V_{\ell}:\mathit{Span}(B_{\ell})$ for each location $\ell\in L$.

######  Definition 3.6.

We say that the collection $V_{\ell},\ell\in L$ is $d-$closed for transition
system $\Pi$ if and only if for each transition
$t_{j}:\left\langle\ell_{pre},\ell_{post},G_{j},F_{j}\right\rangle$ and for
each element $p\in V_{post}$, we have $\mbox{{fpre}}(p,t_{j})\in
V_{pre}^{\left\langle d\right\rangle}$.

The notion of $d-$closed vector spaces can be related to CoB transformations
and resulting abstractions whose updates are defined by means of polynomials
of degree at most $d$.

######  Theorem 3.4.

Let $V_{\ell},\ell\in L$ be a collection of vector spaces that are $d-$closed
for a system $\Pi$. The basis elements of $V_{\ell}$ yields a collection of
maps $\alpha_{\ell},\ \ell\in L$ that relate $\Pi$ to a CoB abstraction $\Xi$.
The update maps of $\Xi$ are all polynomials of degree at most $d$.

######  Example 3.8.

Consider the transition system described in Example 3.7 and Figure 3. We wish
to discover an affine abstraction for this system automatically. Starting from
the initial collection of vector spaces that maps each location to the space
of all polynomials of degree at most $2$ over $x,y,z$, we obtain the
transformations $\alpha_{\ell_{1}},\alpha_{\ell_{2}},\alpha_{\ell_{3}}$
described in the same example. This yields an abstract system over variables
$w_{0},\ldots,w_{8}$.

###  3.4 Combining Discrete and Continuous Systems

As a final step, we extend our approach to hybrid systems that combine
discrete and continuous dynamics. We define hybrid systems briefly and extend
the results from Sections 2 and 3 to address hybrid systems.

######  Definition 3.7.

A hybrid system consists of a discrete transition system $\Pi:\left\langle
X,L,\mathcal{T},X_{0},\ell_{0}\right\rangle$ and a mapping that associates
each location $\ell_{i}\in L$ with a continuous subsystem
$\mathcal{S}_{i}:\left\langle\mathcal{F}_{i},X_{i}\right\rangle$ over the
state-space $X$, consisting of a vector field $\mathcal{F}_{i}$ and location
invariant $X_{i}$.

A state $\sigma$ of the hybrid system consists of a tuple
$\left\langle\ell,\vec{x},T\right\rangle$ where $\ell\in L$ is the current
location, valuations to the continuous variables $\vec{x}\in X$ and the
current time $T\geq 0$.

Given a time $\delta\geq 0$, we write
$\left\langle\ell,\vec{x},T\right\rangle\ \underset{\delta}{\leadsto}\
\left\langle\ell,\vec{y},T+\delta\right\rangle$ to denote that starting from
state $\left\langle\ell,\vec{x},T\right\rangle$ the hybrid system _flows_
continuously according to the continuous subsystem $\mathcal{S}_{\ell}$
corresponding to the location $\ell$. Likewise, we write
$\left\langle\ell,\vec{x},T\right\rangle\xrightarrow{t_{j}}\left\langle\ell^{\prime},\vec{x}^{\prime},T\right\rangle$
to denote a _jump_ between two states upon taking a discrete transition
$t_{j}$ from $\ell$ to $\ell^{\prime}$. Note that no time elapses upon taking
a jump.

A run $R$ of the hybrid system is given by a countable sequence of alternating
flows (evolution according to the ODE inside a location) and jumps (discrete
transition to a different location) starting from an initial state:

$\sigma_{0}:\left\langle\ell_{0},\vec{x}_{0},0\right\rangle\underset{\delta_{0}}{\leadsto}\sigma_{0}^{\prime}:\left\langle\ell_{0},\vec{y}_{0},\delta_{0}\right\rangle\xrightarrow{t_{1}}\
\sigma_{1}:\left\langle\ell_{1},\vec{x}_{1},\delta_{0}\right\rangle\underset{\delta_{1}}{\leadsto}\
\sigma_{1}^{\prime}:\left\langle\ell_{1},\vec{y}_{0},\delta_{0}+\delta_{1}\right\rangle\xrightarrow{t_{2}}\cdots$

To avoid Zenoness, we require that the summation of the dwell times in the
individual modes $\sum_{j=0}^{\infty}\delta_{j}$ diverges.

We now define CoB abstractions for hybrid systems. Our definitions simply
combine aspects of the definition for transition systems 3.5 and continuous
systems 2.3.

A CoB abstraction of the hybrid system is obtained through a collection of
maps $\alpha_{\ell_{1}},\ldots,\alpha_{\ell_{k}}$ corresponding to the
locations $\ell_{1},\ldots,\ell_{k}$ of the hybrid system. It is assumed that
by padding with $0$s, we obtain each $\alpha_{\ell_{i}}$ as a function
$\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$.

######  Definition 3.8.

A system $\Xi$ is a CoB abstraction of $\Pi$ through a collection of maps
$\alpha_{\ell_{1}},\ldots,\alpha_{\ell_{k}}$ each of the type
$\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}$, corresponding to locations
$\ell_{1},\ldots,\ell_{k}$, iff

  1. 1.

$\Xi$ has locations $m_{j}$ corresponding to $\ell_{j}\in L$ for $1\leq j\leq
k$ , and transitions $t_{i}^{\prime}$ corresponding to transition
$t_{i}\in\mathcal{T}$. Each location $m_{j}$ in $\Xi$ has an associated
continuous system $\mathcal{T}_{j}$.

  2. 2.

For each corresponding location pair $\ell_{j},m_{j}$, the system
$\mathcal{T}_{j}$ is a CoB abstraction of $\mathcal{S}_{j}$ through the
transformation $\alpha_{\ell_{j}}$.

  3. 3.

For each transition
$t_{i}:\left\langle\ell_{pre},\ell_{post},G_{i},F_{i}\right\rangle$ in $\Pi$,
the corresponding transition $t_{i}^{\prime}:\left\langle
m_{pre},m_{post},G_{i}^{\prime},F_{i}^{\prime}\right\rangle$ are such that

    1. (a)

$m_{pre}$ and $m_{post}$ correspond to $\ell_{pre}$ and $\ell_{post}$,
respectively,

    2. (b)

$G_{i}^{\prime}\supseteq\alpha_{\ell_{pre}}(G_{i})$,

    3. (c)

$(\forall\ \vec{x})\
F_{i}^{\prime}(\alpha_{\ell_{pre}}(\vec{x}))=\alpha_{post}(F_{i}(\vec{x}))$.

Once again, we focus on searching for an abstraction $\Xi$ of a given hybrid
system wherein the continuous abstraction for each location and that of each
transition is expressed by means of polynomials degree bounded by some fixed
bound $d$. The case where the bound is $d=1$ specifies an affine hybrid
abstraction $\Xi$. We translate this into a $d-$closure condition for vector
spaces. Consider a collection of vector spaces
$V_{\ell}:\mathit{Span}(B_{\ell})$ for each location $\ell\in L$.

######  Definition 3.9.

We say that the collection $V_{\ell},\ell\in L$ is $d-$closed for hybrid
system $\Pi$ if and only if

  1. 1.

For each location $\ell\in L$, the corresponding vector space $V_{\ell}$ is
$d$-closed w.r.t to the vector field $\mathcal{F}_{\ell}$ for the continuous
subsystem $\mathcal{S}_{\ell}$.

  2. 2.

For each transition
$t_{j}:\left\langle\ell_{pre},\ell_{post},G_{j},F_{j}\right\rangle$ and for
each element $p\in V_{post}$, we have $\mbox{{fpre}}(p,t_{j})\in
V_{pre}^{\left\langle d\right\rangle}$.

Once again, the approach for finding a $d$-closed collection $V_{\ell},\
\ell\in L$ starts from an initial basis $V_{\ell}^{(0)}$ at each location
$\ell$ and refines the basis. Two types of refinements are applied (a)
refinement of $V_{\ell}$ to enforce closure w.r.t the Lie derivative of its
basis elements for the vector field $\mathcal{F}_{\ell}$ and (b) refinement of
$V_{m}$ w.r.t a transition $t:\left\langle\ell,m,G,F\right\rangle$ incoming at
location $m$.

##  4 Implementation and Evaluation

We have implemented the ideas described in this paper to derive affine
abstractions for (a) continuous systems described by ODEs with polynomial
right-hand sides, (b) discrete systems with assignments that have polynomial
RHS and (b) hybrid systems with polynomial ODEs and discrete transition
updates. Our approach takes as inputs the system description, a degree limit
$k>0$ that is used to construct the initial basis. Starting from this initial
basis, our approach iteratively applies refinement until convergence. Upon
convergence, we print the basis inferred along with the resulting abstraction.

Currently, our implementation does not abstract the guard sets of the
transitions and the invariant sets of the ODEs. However, once the basis is
inferred, the abstractions for the guards of the transition and mode
invariants are obtained using quantifier elimination techniques (which is
quite expensive in practice) [7, 8, 13] or optimization techniques such as
Linear programming or SOS programming [26]. Our implementation currently
relies on manual translation of invariant and guard assertions into the new
basis to form the abstract transition system.

If a non-trivial abstraction is discovered by our iterative scheme, we may use
a linear invariant generator on the resulting affine system to infer
invariants that relate to the original transition system.

Our implementation and the benchmarks used in the evaluation presented in this
section may be obtained upon request.

###  4.1 Continuous Systems

We first describe experimental results obtained for continuous systems
described by ODEs. Figure 4 summarizes the results on continuous system
benchmarks. We collected nearly $15$ benchmark systems and ran our
implementation to search for a linearizing CoB transformation. We report on
the degree of the monomials in the initial basis, time taken to converge and
the number of polynomials in the final basis that form the transformation to
the abstract system.

##### Trivial Transformations Found:

Some of the benchmarks attempted resulted in trivial final transformations.
Examples include the well-known Fitzhugh-Nagumo neuron model, the vanderpol
oscillators and similar small but complex systems that are known to be non-
integrable.

We now highlight some of the interesting results, while summarizing all
benchmarks in Table 4.

##### Toda Lattice with Boundary Particles:

The Toda lattice models an infinite array of point particles such that the
position and velocity of the $n^{th}$ particle are affected by its neighbors
the $(n-1)^{th}$ and $(n+1)^{th}$ particle for $n\in\mathbb{Z}$ 222See
description by Göktas and Hereman [15] and references therein.. We consider a
finite version of this lattice with $2$ fixed boundary particles that are
constrained to have a fixed position and zero velocity and $K$ particles in
the middle. The dynamics for $K=2$ non-fixed particles are given by position
variables $y_{1},y_{2}$, velocities $v_{1},v_{2}$ and extra state variables
$u_{1},u_{2}$ to model the interaction with neighbors.

$\begin{array}[]{rcl rcl rcl
}\frac{dx_{1}}{dt}&=&v_{1}&\frac{dv_{1}}{dt}&=&v_{1}(u_{1}-u_{2})&\frac{du_{1}}{dt}&=&-v_{1}\\\
\frac{dx_{2}}{dt}&=&v_{2}&\frac{dv_{2}}{dt}&=&v_{2}u_{2}&\frac{du_{2}}{dt}&=&v_{1}-v_{2}\\\
\end{array}$

In addition, we add time $t$ as a variable to the model with dynamics
$\frac{dt}{dt}=1$. Our approach initialized with polynomials of degree $2$
discovers a basis with $10$ polynomials:

$\begin{array}[]{l}w_{1}:\ -2v_{2}-2v_{1}-u_{2}^{2}+2x_{1}u_{1}+x_{2}^{2},\\\
w_{2}:\
-2v_{2}-2v_{1}-u_{2}^{2}+u_{1}u_{2}+x_{2}u_{1}+x_{1}u_{2}+x_{1}u_{1}+x_{1}x_{2}\\\
w_{3}:\ -2v_{2}-2v_{1}+2u_{1}u_{2}+2x_{2}u_{2}+2x_{2}u_{1}+x_{2}^{2},\ w_{4}:\
u_{1}+x_{1},\\\ w_{5}:\ 2v_{2}+2v_{1}+u_{1}^{2}+u_{2}^{2},\ w_{6}:\
u_{2}+x_{2}-x_{1},\ w_{7}:\ t,\\\ w_{8}:\ u_{1}t+x_{1}t,\ w_{9}:\
u_{2}t+u_{1}t+x_{2}t,\ w_{10}:\ t^{2}\end{array}$

The resulting abstract system has linear dynamics given by:

$\frac{dw_{j}}{dt}=0,\ 1\leq j\leq 6,\ \frac{dw_{7}}{dt}=1,\
\frac{dw_{8}}{dt}=w_{4},\ \frac{dw_{9}}{dt}=w_{4}+w_{6},\
\frac{dw_{10}}{dt}=2w_{7}\,.$

Results for larger instances are reported in Table 4.

##### Quadratic Fermi-Pasta-Ulam-Tsingou System:

Consider a system considered by Fermi et al. [14]. The system consists of a
chain of particles at positions $x_{1},\ldots,x_{N}$ with fixed boundary
particles $x_{0}=0$ and $x_{N+1}=N+1$. The dynamics are given by

$\frac{d^{2}x_{i}}{dt^{2}}=(x_{i+1}+x_{i-1}-2x_{i})+\alpha((x_{i+1}^{2}-x_{i}^{2})-(x_{i}-x_{i-1})^{2})\,,\
1\leq i\leq N$

We consider an instantiation with $N=3$, searching for CoB transformations
with an initial basis of monomials of degree up to $4$. We obtain a
transformation representing a conserved quantity

$\begin{array}[]{c}\frac{1}{2}(v_{1}^{2}+v_{2}^{2}+v_{3}^{2})+x_{1}^{2}+x_{2}^{2}+x_{3}^{2}-3x_{3}(1+3a-ax_{3})\\\
-x_{2}x_{3}(1+ax_{3}-ax_{2})-x_{1}x_{2}(1+ax_{2}-ax_{1})\end{array}\,.$

The abstract system is given by $\frac{dw_{1}}{dt}=0$.

##### Two Mass Spring System:

Consider the dynamics of two masses connected by a spring to each other and to
two fixed walls. The state variables are $(x_{1},x_{2},v_{1},v_{2})$
indicating the position and velocity of the masses while the spring constant
$k$ is a parameter. The dynamics are given by

$\begin{array}[]{rcl
rcl}\frac{dx_{1}}{dt}&=&v_{1}&\frac{dx_{2}}{dt}&=&v_{2}\\\
\frac{dv_{1}}{dt}&=&kx_{2}-2kx_{1}&\frac{dv_{2}}{dt}&=&k(x_{1}-x_{2})\\\
\end{array}$

Our procedure yields a change of basis transformation

$w_{1}:\ v_{2}^{2}+v_{1}^{2}+kx_{2}^{2}-2kx_{1}x_{2}+2kx_{1}^{2},\ w_{2}:\
v_{1}v_{2}-\frac{1}{2}v_{1}^{2}-\frac{1}{2}kx_{2}^{2}+2kx_{1}x_{2}-\frac{3}{2}kx_{1}^{2}$

Both $w_{1},w_{2}$ represent conserved quantities, yielding the abstraction

$\frac{dw_{1}}{dt}=\frac{dw_{2}}{dt}=0\,.$

##### Biochemical reaction network:

We consider a biochemical reaction network benchmark from Dang et al. [12].
The ODE along with the values are parameters in our model coincide with those
used by Dang et al. The ODE consists of $12$ variables and roughly $14$
parameters. Our search for degree bound $\leq 3$ discovers a transformation
generated by five basis functions (in roughly $3$ seconds).

##### Collision Avoidance

We consider the algebraic abstraction of the roundabout mode of a collision
avoidance system analyzed recently by Platzer et al. [29] and earlier by
Tomlin et al. [40]. The two airplane collision avoidance system consists of
the variables $(x_{1},x_{2})$ denoting the position of the first aircraft,
$(y_{1},y_{2})$ for the second aircraft, $(d_{1},d_{2})$ representing the
velocity vector for aircraft 1 and $(e_{1},e_{2})$ for aircraft $2$.
$\omega,\theta$ abstract the trigonometric terms. In addition, the parameters
$a,b,r_{1},r_{2}$ are also represented as system variables. The dynamics are
modeled by the following differential equations:

$\begin{array}[]{ccccccccc}x_{1}^{\prime}=d_{1}&x_{2}^{\prime}=d_{2}&d_{1}^{\prime}=-\omega
d_{2}&d_{2}^{\prime}=\omega d_{1}\\\
y_{1}^{\prime}=e_{1}&y_{2}^{\prime}=e_{2}&e_{1}^{\prime}=-\theta
e_{2}&e_{2}^{\prime}=\theta e_{1}\\\
a^{\prime}=0&b^{\prime}=0&r_{1}^{\prime}=0&r_{2}^{\prime}=0\\\ \end{array}$

A search for transformations of degree $2$ yields a closed vector space with
27 basis functions within $0.2$ seconds. The basis functions include
$a,b,r_{1},r_{2}$ and all degree two terms involving these. Removing these
from the basis, gives us $14$ basis functions that yield a transformation to a
$14$ dimensional affine ODE.

ID | #V | Deg. | #B0 | Time | #B* | #B0 | Time | #B*
---|---|---|---|---|---|---|---|---
Brusselator | 2 | 3 | 3 | 0.01 | 0 | 25 | 2.8 | 0
Fitz-Nagumo | 2 | 3 | 3 | 0.01 | 0 | 25 | 2.6 | 0
Vanderpol | 2 | 3 | 3 | 0.01 | 0 | 25 | 1.9 | 0
Proj-drag | 4 | 2 | 3 | 0.02 | 8 | 10 | 9.7 | 64
Circular | 4 | 2 | 3 | 6 | 0.01 | 10 | 10.6 | 83
Hamiltonian | 5 + 1 | 2 | 3 | 0.02 |  5$\dagger$ | 5 | 1.3 |  20$\dagger$
Two-spring | 4 + 1 | 2 | 3 | 0.03 |  2$\dagger$ | 5 | 0.5 |  6$\dagger$
Toda-2 | 7 | 2 | 3 | 0.1 | 22 | 5 | 4.6 | 82
Toda-3 | 10 | 2 | 3 | 0.5 | 38 | 5 | 95 | 169
Toda-5 | 16 | 2 | 3 | 6 | 90 | 5 | 6373 | 559
Toda-10 | 31 | 2 | 3 | 301.5 | 375 | 5 | dnf
FPUT-3 | 6 + 1 | 3 | 3 | 0.05 |  0$\dagger$ | 5 | 3.7 |  2 $\dagger$
FPUT-5 | 10 + 1 | 3 | 3 | 0.4 | 0 | 5 | 231 | 2
Bio-network | 13 | 2 | 3 | 0.07 | 5 | 5 | 4800 | 20
Roundabout | 10 + 4 | 2 | 3 | 1.5 |  68$\dagger$ | 5 | 890 | $\geq 600\ \dagger$
Figure 4: Experimental evaluation results on non linear polynomial ODE
benchmarks at a glance. Legend: #V denotes number of system variables +
parameters, Deg.: max. degree of the RHS, #B0: degree limit for monomials in
the initial basis, Time: timing in seconds, #B*: number of elements in the
final basis, $\dagger$: some elements of the basis involving just the
parameters were discarded from the count and dnf: did not finish in 2hrs or
out of memory crash.

###  4.2 Discrete Systems

We now describe experimental results on some discrete programs. We used a set
of benchmark programs that require non-linear invariants to prove correctness
compiled by Enric Carbonell 333The benchmark instances are available on-line
at http://www.lsi.upc.edu/~erodri/webpage/polynomial_invariants/list.html..
Our evaluation focuses on a subset of benchmarks that have non-linear
assignments or guards in them. The methods presented here converge in a single
step with the initial basis whenever the program being considered already has
affine updates.

⬇ int fermat(int N, int R) pre (N >= 0 && R >= 0); int u,v,r; u := 2*R -1; v := 1; r := R*R -N; 1: while ( r != 0 ){ 2: while (r > 0) (r,v) := (r-v, v+2); 3: while (r < 0) (r,v) := (r+u, u+2); } end |  $\begin{array}[]{l}-4r-v^{2}-4Nv+2v+u^{2}-2u\ \leq\ 0\ \land\\\ -r-Nu\ \leq\ 0\ \land\ 1-v^{2}\ \leq\ 0\ \land\\\ 1-uv\ \leq\ 0\ \land\ -Rv+R\ \leq\ 0\ \land\\\ 1-v\ \leq\ 0\ \land\ 1-u^{2}\ \leq\ 0\ \land\\\ -Ru+2R^{2}+R\ \leq\ 0\ \land\ -Nu\ \leq\ 0\ \land\\\ 1-u\ \leq\ 0\ \land\ -R^{2}\ \leq\ 0\ \land\ -NR\ \leq\ 0\ \land\\\ -R\ \leq\ 0\ \land\ -N^{2}\ \leq\ 0\ \land\\\ v^{2}-2v-u^{2}+2u\ \leq\ 0\ \land\\\ 1+r-u-R^{2}\ \leq\ 0\ \land\ 1+4r-u^{2}\ \leq\ 0\ \land\\\ 4r+v^{2}-2v-u^{2}+2u\ \leq\ 0\ \land\\\ 2+6r-uv-u^{2}-2R^{2}\ \leq\ 0\ \land\\\ 4r+v^{2}-2v-u^{2}+2u+4N=0\end{array}$
---|---
Figure 5: Fermat’s algorithm for prime factorization taken from Bressoud [5]
and invariants computed at location 1 using polyhedral analysis of the
linearization.

##### Fermat Factorization:

Figure 5 shows a program for finding a factor of a number $N$ near its square
root taken from a book by Bressoud [5]. Our analysis initialized with
monomials of degree up to $2$ over the program variables yields a final basis
consisting of $17$ polynomials. The resulting affine system is analyzed by a
polyhedral analyzer using abstract interpretation to yield invariants. Some of
the invariants obtained at the loop head are shown in Figure 5. The equality
invariant

$4r+v^{2}-2v-u^{2}+2u+4N=0$

is obtained at locations $1,2$ and $3$ in the program. This forms a key part
of the program’s partial correctness proof.

⬇ int productBR(int x, int y) pre (x >= 0 && y >= 0); int a,b,p,q; (a,b,p,q) := (x,y,1,0); 1: while ( a >= 1 && b >= 1 ){ if ( a mod 2 == 0 && b mod 2 == 0) (a,b,p) := (a/2, b/2, 4 * p); elsif (a mod 2 == 1 && b mod 2 == 0) (a,q) := (a-1, q+ b*p); elsif (a mod 2 == 0 && b mod 2 == 1) (b,q) := (b-1, q + a*p); else (a,b,p) := (a-1, b-1, q + (a+b-1)*p); } end |  $\begin{array}[]{l}1-p^{2}\leq 0\ \land\ -yp+y\leq 0\ \land\\\ -xp+x\leq 0\ \land\ 1-p\leq 0\ \land\\\ -1-b\leq 0\ \land\ -1-a\leq 0\ \land\\\ -y\leq 0\ \land\ -x\leq 0\ \land\\\ 2ap-xp-2a+x\leq 0\ \land\\\ 7ap-xp-7a-14x\leq 0\ \land\\\ 7ap-xp+8a-14x\leq 0\ \land\\\ 16ap-3xp-16a-12x\leq 0\ \land\\\ 2bp-yp-2b+y\leq 0\ \land\\\ 7bp-yp-7b-14y\leq 0\ \land\\\ 7bp-yp+8b-14y\leq 0\ \land\\\ 16bp-3yp-16b-12y\leq 0\end{array}$
---|---
Figure 6: A multiplication algorithm and loop invariant computed using
polyhedral analysis on the linearization.

##### Product of Numbers:

Consider the benchmark shown in Figure 6 that seeks to compute the product of
its arguments $x,y$. Our approach initialized using degree $2$ monomials
computes an abstract system with $20$ basis polynomials that in turn yields an
affine transition system with $20$ variables. Figure 6 shows the invariants
computed using polyhedral abstract interpretation. The invariant $q-abp=0$
cannot be established by our technique with degree $2$ monomials. On the other
hand, it can be established by considering degree $3$ monomials in the initial
basis. The resulting system however has $60$ variables, making polyhedral
analysis of the system as a whole hard.

⬇ int geoSum(int a, int r, int n ) int s := 0; int p := a; int k := 0; while (k < n) s := s + p; p := p * r; k := k + 1; end |  $\begin{array}[]{l}-k^{2}+k\ \leq\ 0\ \land\ -2-k^{2}+3k\ \leq\ 0\ \land\\\ -6-k^{2}+5k\ \leq\ 0\ \land\ -9-k^{2}+6k\ \leq\ 0\ \land\\\ -k\ \leq\ 0\ \land\ -r^{2}\ \leq\ 0\ \land\ -n\ \leq\ 0\ \land\\\ -1+k-n\ \leq\ 0\ \land\ -p+s-rs+a=0\end{array}$
---|---
Figure 7: Geometric summation program and computed loop invariant.

##### Geometric Summation:

Consider the geometric summation program in Figure 7. Our approach computes a
linearization with $5$ variables in the abstract system. Polyhedral analysis
of the resulting program yields the invariant $(1-r)s=a-p$. This invariant
together with the invariant $p=ar^{k}$ (which cannot be obtained through
algebraic reasoning) suffices to prove the partial correctness of the program.

System | Linearization | Analysis
---|---|---
ID | #V | #Trs | Deg | B0 | #B* | Time | Time | #I
Petter2 | 2 | 1 | 2 | 2 | 3 | 0.02 |  $\leq$ 0.01 | 10
Petter3 | 2 | 1 | 2 | 3 | 1 | 0.02 |  $\leq$ 0.01 | 2
Petter3 | 2 | 1 | 3 | 3 | 4 | 0.02 |  $\leq$ 0.01 | 25
Geo | 6 | 2 | 2 | 2 | 6 | 0.02 |  $\leq$ 0.01 | 9
Fermat | 5 | 6 | 2 | 2 | 17 | 0.04 | 0.5 | 26
Prodbr | 7 | 5 | 2 | 2 | 20 | 0.06 | 2.0 | 19
Euclidex1 | 11 | 5 | 2 | 2 | 51 | 0.66 | DNF
Figure 8: Timings for computing abstractions of discrete systems and analyzing
the resulting abstractions. Legend: #V denotes number of system variables,
#Trs: number of transitions, Deg.: max. degree of the RHS, B0: degree limit
for monomials in the initial basis, Time: timing in seconds, #B*: number of
elements in the final basis, #I: invariants computed and DNF: did not finish
in 2hrs or out of memory crash.

##  5 Conclusion and Future Directions

Thus far, we have presented an approach that uses Change-Of-Bases
transformation for inferring abstractions of continuous, discrete and hybrid
systems. We have explored the theoretical underpinnings of our approach, its
connections to various invariant generation techniques presented earlier. Our
previous work presents an extension of the approach presented in this paper to
infer differential inequality abstractions [34]. Similar extensions for
discrete systems remain unexplored. Furthermore, the use of the abstractions
presented here to establish termination for transition systems is also a
promising line of future research. Future research will also focus on the use
of Lie symmetries to reduce the size of the ansatz or templates used in the
search for conserved quantities and CoB transformations [15].

## References

  * Alur et al. [2000] R. Alur, T. A. Henzinger, G. Lafferriere, and G. Pappas.  Discrete abstractions of hybrid systems.  _Proc. of IEEE_ , 88(7):971–984, 2000.
  * Alur et al. [2003] R. Alur, T. Dang, and F. Ivančić.  Counter-example guided predicate abstraction of hybrid systems.  In _TACAS_ , volume 2619 of _LNCS_ , pages 208–223. Springer, 2003.
  * Bagnara et al. [2005] R. Bagnara, E. Rodríguez-Carbonell, and E. Zaffanella.  Generation of basic semi-algebraic invariants using convex polyhedra.  In _12th International Symposium on Static Analysis (SAS’05)_ , volume 3672 of _Lecture Notes in Computer Science_ , pages 19–34. Springer-Verlag, Sept. 2005.
  * Berman et al. [2007] S. Berman, A. Halasz, and V. Kumar.  MARCO: a reachability algorithm for multi-affine systems with applications to biological systems.  In _Hybrid Systems: Computation and Control_ , volume 4416, pages 76–89. Springer–Verlag, 2007.
  * Bressoud [1989] D. M. Bressoud.  _Factoring and Primality Testing_.  Springer-Verlag (Undergraduate Texts in Mathematics), 1989.
  * Clarke et al. [2003] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith.  Counterexample-guided abstraction refinement for symbolic model checking.  _J. ACM_ , 50(5):752–794, 2003.
  * Collins [1975] G. Collins.  Quantifier elimination for real closed fields by cylindrical algebraic decomposition.  In H.Brakhage, editor, _Automata Theory and Formal Languages_ , volume 33 of _LNCS_ , pages 134–183. Springer, 1975.
  * Collins and Hong [1991] G. E. Collins and H. Hong.  Partial cylindrical algebraic decomposition for quantifier elimination.  _Journal of Symbolic Computation_ , 12(3):299–328, sep 1991.
  * Colón [2004] M. Colón.  Approximating the algebraic relational semantics of imperative programs.  In _$11^{th}$ Static Analysis Symposium (SAS’2004)_, volume 3148 of _LNCS_. Springer, 2004.
  * Cousot and Halbwachs [1978] P. Cousot and N. Halbwachs.  Automatic discovery of linear restraints among the variables of a program.  In _POPL’78_ , pages 84–97, Jan. 1978.
  * Cox et al. [1991] D. Cox, J. Little, and D. O’Shea.  _Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra_.  Springer-Verlag, 1991.
  * Dang et al. [2010] T. Dang, O. Maler, and R. Testylier.  Accurate hybridization of nonlinear systems.  In _HSCC ’10_ , pages 11–20. ACM, 2010.
  * Dolzmann and Sturm [1997] A. Dolzmann and T. Sturm.  REDLOG: Computer algebra meets computer logic.  _ACM SIGSAM Bulletin_ , 31(2):2–9, June 1997\.
  * Fermi et al. [1955] E. Fermi, J. Pasta, and S. Ulam.  Studies of non-linear problems.  Document LA-140, Los Alamos National Laboratories, 1955.
  * Göktas and Hereman [2011] Ü. Göktas and W. A. Hereman.  Symbolic computation of conservation laws, generalized symmetries, and recursion operators for nonlinear differential-difference equations.  In _Dynamical Systems and Methods_. Springer–Verlag, 2011.
  * Halbwachs et al. [1997] N. Halbwachs, Y.-E. Proy, and P. Roumanoff.  Verification of real-time systems using linear relation analysis.  _Formal Methods in System Design_ , 11(2):157–185, 1997.
  * Halmos [1974] P. Halmos.  _Finite-Dimensional Vector Spaces_.  Springer-Verlag, 1974.
  * Kovács [2008] L. Kovács.  Reasoning algebraically about p-solvable loops.  In _Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_ , volume 4963 of _Lecture Notes in Computer Science_ , pages 249–264. Springer, 2008.
  * Kowalski and Steeb [1991] K. Kowalski and W.-H. Steeb.  _Non-Linear Dynamical Systems and Carleman Linearization_.  World Scientific, 1991.
  * Lee [2003] J. M. Lee.  _Introduction to Smooth Manifolds_.  Graduate Texts in Mathematics. Springer–Verlag, 2003.
  * Manna and Pnueli [1995] Z. Manna and A. Pnueli.  _Temporal Verification of Reactive Systems: Safety_.  Springer, New York, 1995.
  * Matringe et al. [2009] N. Matringe, A. V. Moura, and R. Rebiha.  Morphisms for non-trivial non-linear invariant generation for algebraic hybrid systems.  In _HSCC_ , volume 5469 of _LNCS_ , pages 445–449, 2009.
  * Meiss [2007] J. D. Meiss.  _Differential Dynamical Systems_.  SIAM publishers, 2007.
  * Müller-Olm and Seidl [2004] M. Müller-Olm and H. Seidl.  Precise interprocedural analysis through linear algebra.  In _Principles Of Programming Languages (POPL)_ , pages 330–341. ACM, 2004.  ISBN 1-58113-729-X.
  * Oishi et al. [2008] M. Oishi, I. Mitchell, A. M. Bayen, and C. J. Tomlin.  Invariance-preserving abstractions of hybrid systems: Application to user interface design.  _IEEE Trans. on Control Systems Technology_ , 16(2), Mar 2008.
  * Parillo [2003] P. A. Parillo.  Semidefinite programming relaxation for semialgebraic problems.  _Mathematical Programming Ser. B_ , 96(2):293–320, 2003.
  * Petkovsek et al. [1996] M. Petkovsek, H. S. Wilf, and D. Zeilberger.  _A=B_.  A.K. Peters/ CRC Press, 1996.
  * Petter [2004] M. Petter.  _Berechnung von polynomiellen invarianten (German)_.  PhD thesis, Technische Universität München, October 2004.  Cf. http://www2.cs.tum.edu/~petter/da/da.pdf .
  * Platzer and Clarke [2009] A. Platzer and E. Clarke.  Computing differential invariants of hybrid systems as fixedpoints.  _Formal Methods in Systems Design_ , 35(1):98–120, 2009.
  * Prabhakar et al. [2012] P. Prabhakar, G. Dullerud, and M. Viswanathan.  Pre-orders for reasoning about stability.  In _Hybrid Systems: Computation and Control (HSCC)_. ACM Press, 2012\.  to appear (April 2012).
  * Rodríguez-Carbonell and Kapur [2004a] E. Rodríguez-Carbonell and D. Kapur.  An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants.  In _International Symposium on Static Analysis (SAS 2004)_ , volume 3148 of _Lecture Notes in Computer Science_ , pages 280–295. Springer-Verlag, 2004a.
  * Rodríguez-Carbonell and Kapur [2004b] E. Rodríguez-Carbonell and D. Kapur.  Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations.  In _International Symposium on Symbolic and Algebraic Computation 2004 (ISSAC04)_ , pages 266–273. ACM Press, 2004b.
  * Sankaranarayanan [2010] S. Sankaranarayanan.  Automatic invariant generation for hybrid systems using ideal fixed points.  In _Hybrid Systems: Computation and Control_ , pages 211–230. ACM Press, 2010.
  * Sankaranarayanan [2011] S. Sankaranarayanan.  Automatic abstraction of non-linear systems using change of bases transformations.  In _Hybrid Systems: Computation and Control (HSCC)_ , pages 143–152. ACM, 2011.
  * Sankaranarayanan et al. [2004] S. Sankaranarayanan, H. Sipma, and Z. Manna.  Non-linear loop invariant generation using Gröbner bases.  In _ACM Principles of Programming Languages (POPL)_ , pages 318–330. ACM Press, 2004.
  * Sankaranarayanan et al. [2006a] S. Sankaranarayanan, M. A. Colón, H. Sipma, and Z. Manna.  Efficient strongly relational polyhedral analysis.  In _VMCAI’06_ , volume 3855/2006 of _LNCS_ , pages 111–125, 2006a.
  * Sankaranarayanan et al. [2006b] S. Sankaranarayanan, H. B. Sipma, and Z. Manna.  Fixed point iteration for computing the time-elapse operator.  In _HSCC_ , LNCS. Springer, 2006b.
  * Sankaranarayanan et al. [2008] S. Sankaranarayanan, H. Sipma, and Z. Manna.  Constructing invariants for hybrid systems.  _Formal Methods in System Design_ , 32(1):25–55, 2008.
  * Tiwari [2008] A. Tiwari.  Abstractions for hybrid systems.  _Formal Methods in Systems Design_ , 32:57–83, 2008.
  * Tomlin et al. [1998] C. J. Tomlin, G. J. Pappas, and S. Sastry.  Conflict resolution for air traffic management: A study in multi-agent hybrid systems.  _IEEE Trans. on Aut. Control_ , 43(4):509–521, April 1998.
  * Vassilyev and Ul’yanov [2009] S. Vassilyev and S. Ul’yanov.  Preservation of stability of dynamical systems under homomorphisms.  _Differential Equations_ , 45:1709–1720, 2009.