Under-Approximating Backward Reachable Sets by Polytopes

Abstract

Under-approximations are useful for falsification of safety properties for nonlinear (hybrid) systems by finding counter-examples. Polytopic under-approximations enable analysis of these properties using reasoning in the theory of linear arithmetic. Given a nonlinear system, a target region of the simply connected compact type and a time duration, we in this paper propose a method using boundary analysis to compute an under-approximation of the backward reachable set. The under-approximation is represented as a polytope. The polytope can be computed by solving linear program problems. We test our method on several examples and compare them with existing methods. The results show that our method is highly promising in under-approximating reachable sets. Furthermore, we explore some directions to improve the scalability of our method.

B. Xue—This work is based on Bai Xue’s Ph.D. thesis from Beihang University [1].

Z. She— The work of Zhikun She was partly supported by NSFC-11422111 and NSFC-11371047.

1 Introduction

Reachability analysis, which involves constructing reachable sets, is a central component of model checking. It plays an important role in automatic verification and falsification of safety properties for continuous nonlinear and hybrid systems [2, 3]. It has been utilized in diverse applications such as artificial pancreas [4, 5] and robotic systems [6]. Over the past few years, a lot of attention has been given to construct over-approximations of reachable sets of nonlinear systems, i.e., abstraction methods [7, 8], simulation based methods [9] and Taylor series expansions [10, 11]. Nevertheless, much less attention has been given to the problem of finding under-approximations. Actually, under-approximations of reachable sets are also important to compute because of a variety of applications in engineering domains. For example, they can be used for designing robust artificial pancreas [5, 12]. Computing under-approximations of backward reachable sets can help find a set of feasible states such that every trajectory originating from it will definitely enter a specified region (e.g., normal blood glucose ranges) at a specified time instant. They can be used to prove attractive properties by checking if all the trajectories originating from them will stay in them forever and eventually enter some specified desired sets [13]. They can also be used for falsification by checking if the under-approximation intersects the unsafe sets¹ [3]. Also, under- and over-approximations of reachable sets can provide an indication of the precision of an estimate of the exact reachability region [4]. In contrast to over-approximation problems, methods for computing under-approximations are far from being developed. One of main reasons may lie in the fact that the problem is more difficult than the one of computing over-approximations [14].

We in this paper propose a linear programming based approach combining validated numerical methods for ordinary differential equations for finding polytopic under-approximations of backward reachable sets, under the assumption that the target region is a simply connected compact set. The basic procedure for computing the under-approximation mainly consists of three steps. The first step is to compute an enclosure of the boundary of the backward reachable set based on validated numerical techniques for ordinary differential equations. The second step is to obtain a polytope, which contains the enclosure obtained in the first step, and the last step is to shrink this polytope based on linear programming to yield an under-approximation of the backward reachable set. The contributions of this paper are summarized as follows:

• 1. We show how a polytopic under-approximation of the backward reachable set can be obtained by solving linear programming problems. We first construct a polytopic over-approximation of the reachable set based on the reachable set’s boundary and validated numerical techniques for ordinary differential equations, then contract this over-approximation to obtain a polytopic under-approximation by solving linear programs.

• 2. We implement our approach based on linear programming solver GLPK² and the validated ordinary differential equation solver VNODE-LP [24], test and compare it with the method of Korda et al. [22] based on several examples. The experiment results show that our approach is highly promising in under-approximating reachable sets for some cases. Furthermore, we explore some directions toward making our method scale well based on an example involving a seven-dimensional biological system.

Related Work

Several techniques have been proposed for computing under-approximations of reachable sets for linear systems, e.g., [14–16]. However, they cannot be easily extended to handle non-linear systems. Under-approximations of reachable sets for nonlinear systems have been discussed elsewhere (e.g., [17] and [21]), but a feasible solution is not given. Recently, some methods have been proposed to compute under-approximations of reachable sets for nonlinear systems.

Sum-of-squares programming based methods are proposed to compute inner approximations of reachable sets for polynomial dynamical systems in [22, 37]. Unfortunately, the present status of semi-definite programming solvers is not so advanced. The numerical problems produced by these solvers often lead to unreliable results for some cases. On the contrary, our method relies on linear programming and validated numerical methods for ordinary differential equations, thus making our method more reliable. A Taylor model backward flowpipe method is presented to compute under-approximations in [23]. However, the algorithm in [23], in which an interval constraint propagation technique is employed to verify the connectedness of an already obtained basic semi-algebraic set, for finding implicit Taylor models such that the semi-algebraic set formed by them is simply-connected³ is not complete generally⁴. In our method, the procedure employing interval constraint propagation techniques to enclose the boundary of the reachable set is complete.

As mentioned previously, polytopic under-approximations permits the analysis of some specified properties such as the falsification of safety properties using reasoning in the theory of linear arithmetic. Interval under-approximations received increasing attention recently [18, 19]. A method based on modal intervals with affine forms is proposed to under-approximate reachable sets using intervals for continuous nonlinear systems modelled by ordinary differential equations [20]. However, our method provides a way to characterize under-approximations of reachable sets using general polytopes, reducing the conservativeness induced by interval representations in the construction of reachable sets.

The structure of this paper is as follows. Some basic definitions related to backward reachable sets as well as an introduction to convex polytopes is introduced in Sect. 2. Our approach of computing under-approximations, together with its computational complexity, is presented in Sect. 3. Several numerical examples with a detailed discussion of our approach and comparison with the method in [22] are provided in Sect. 4. Finally, we conclude our paper in Sect. 5.

2 Preliminary

In this paper, the following notations are used. Vectors are denoted by boldface letters (e.g., $\varvec{x}$). For a set $\varDelta$, its complement, interior, closure and boundary are denoted by $\varDelta ^c$, $\varDelta ^{\circ }$, $\overline{\varDelta }$ and $\partial \varDelta$ respectively. Further, $\mathbb {U}(\varvec{x};\epsilon )=\{\varvec{y}: \Vert \varvec{y}-\varvec{x}\Vert <\epsilon , \epsilon >0\}$ represents an $\epsilon -$neighbourhood of the vector $\varvec{x}$.

2.1 Backward Reachable Sets

Consider a nonlinear system of the form

$$\begin{aligned} \dot{\varvec{x}}=\varvec{f}(\varvec{x}), \end{aligned}$$

(1)

where $\varvec{x}=(x_1,\cdots ,x_n)'\in \mathbb {R}^n$, and $\varvec{f}(\varvec{x})$: $\mathbb {R}^n\rightarrow \mathbb {R}^n$ is $(p-1)$-time continuously differentiable and $p\ge 1$. We also assume $\varvec{f}$ is locally Lipschitz continuous. Thus for a given set $\mathcal {X}$ that is a simply connected compact set, the existence and uniqueness of the trajectory with $\varvec{x}(0)=\varvec{x}_0$ and $\varvec{x}_0\in \mathcal {X}$ will be assured over some time interval $[-\sigma _\mathcal {X}, \sigma _{\mathcal {X}}]$ with $\sigma _{\mathcal {X}}>0$. Further, the trajectory of System (1) is defined to be $\varvec{\phi }(t;\varvec{x}_0)=\varvec{x}(t)$, where $\varvec{x}(t)$ is the solution of System (1) satisfying the initial condition $\varvec{x}(0)=\varvec{x}_{0}$. Furthermore, the backward and forward reachable sets of a simply connected compact set $\mathtt {TR}$ for the time duration T are defined as follows.

Definition 1

Given System (1), a set $\mathtt {TR}$ that is a simply connected compact set and a finite time duration $T\le \sigma _{TR}$, the backward reachable set of $\mathtt {TR}$ for the time duration T is defined to be $\varOmega _b(T;\mathtt {TR},\varvec{f})=\{\varvec{x}_0|\varvec{\phi }(T;\varvec{x}_0)\in \mathtt {TR}\}$ and the forward reachable set of $\mathtt {TR}$ for the time duration T is defined to be $\varOmega _f(T;\mathtt {TR},\varvec{f})=\{\varvec{x}|\varvec{x}=\varvec{\phi }(T;\varvec{x}_0)~\text {and}~\varvec{x}_0\in \mathtt {TR}\}$.

Remark 1

According to Definition 1, the map $\varvec{\phi }(t;\cdot ): \mathtt {TR}\subseteq \mathbb {R}^n\rightarrow \varOmega _f(t;\mathtt {TR},\varvec{f})$ $(\text {or},~\varOmega _b(t;\mathtt {TR},\varvec{f})\rightarrow \mathtt {TR})$ is bijective and continuous for $t\in [0,T]$ under the Lipschitz condition of $\varvec{f}$.

It is intractable to obtain these reachable sets for nonlinear systems since they generally do not have a closed-form solution. However, as mentioned previously, it is sufficient to consider an under-approximation of the backward reachable set, denoted as $\mathtt {UAB}$, for certain applications such as artificial pancreas [12].

Definition 2

Given System (1), a set $\mathtt {TR}$ that is a simply connected compact set and a finite time duration T, an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration T is a nonempty subset of $\varOmega _b(T;\mathtt {TR},\varvec{f})$.

Obviously, all trajectories originating from $\mathtt {UAB}$ will definitely enter $\mathtt {TR}$ after a time duration T, although there may be trajectories not in $\mathtt {UAB}$ that also enter $\mathtt {TR}$ after the time duration T. The under-approximation is equivalent to a region attracting to a target region, but a variant of the classical region of attraction containing an equilibrium.

2.2 Convex Polytopes

Convex polyhedra over reals (rationals) are a natural representation of sets of states for the verification of hybrid systems [25–27]. A convex polytope is a set in $\mathbb {R}^l$ that can be regarded as the set of solutions to the system of linear inequalities $A\varvec{w}+C\le B$,⁵ where $A=(a_{ij})_{m\times l}$ is a $m\times l$ matrix, $\varvec{w}=(w_1,\ldots ,w_l)'$ is a $l\times 1$ vector, $C=(c_1,\ldots ,c_m)'$ and $B=(b,\ldots ,b)'$ are both $m\times 1$ vectors.

A convex polytope $P=\{\varvec{w}:A\varvec{w}+C\le B\}$ has the following property, where the matrix A is full row rank.

Property 1

Let P be compact and its interior $P^{\circ }$ be not empty, then P and $P^{\circ }$ are both simply connected sets with the same boundary $\partial P=\{\varvec{w}\in P:\vee _{i=1}^m[\sum _{j=1}^l a_{ij}w_j+c_i=b]\}$.

Based on Property 1, the following two lemmas can be obtained, which are further illustrated in Fig. 1.

Lemma 1

Assume $P=\{\varvec{w}:A\varvec{w}+C\le B\}$ is a compact convex polytope. If U is a compact set such that its boundary is a subset of the compact convex polytope P, then P is an over-approximation of the set U.

Proof

Since U is a compact set, there exists $\varvec{y}_i=(y_{i1},\ldots ,y_{il})' \in U$ such that $\sum _{j=1}^l a_{ij} w_{j}+c_i$ reaches its maximum value $\mathtt {MAX}_i$ in U at this point, where $i=1,\ldots ,m$. Obviously, $U\subseteq P$ is equivalent to $\mathtt {MAX}_i\le b$ for $i=1,\ldots ,m$. Thus it is enough to prove that $\mathtt {MAX}_i\le b$ for $i=1,\ldots ,m$.

Assuming that there exists an index $i\in \{1,\ldots ,m\}$ such that $\mathtt {MAX}_i>b$, we derive a contradiction as follows. Since $\partial U\subseteq P$ and $A\varvec{w}+C\le B$ for $\forall \varvec{w}\in P$, then $\varvec{y}_i\in U^{\circ }$. If $U^{\circ }=\emptyset$, a contradiction is obtained; Otherwise, let $\varOmega =\{\varvec{w}:A\varvec{w}+C\le \mathtt {MAX}\}$, where $\mathtt {MAX}=(\mathtt {MAX}_i,\ldots ,\mathtt {MAX}_i)'$. By Property 1, we obtain that $\varvec{y}_i\in \partial \varOmega$. Thus for an arbitrary but fixed positive number $\epsilon$, there exists $\varvec{z}=(z_1,\ldots , z_l)'\in \mathbb {U}(\varvec{y}_i;\epsilon )$ such that $\sum _{j=1}^la_{ij}z_j+c_i>\mathtt {MAX}_i$. Also, since $\varvec{y}_i\in U^{\circ }$, there exist $\epsilon _1>0$ and $\varvec{w}_0=(w_{01},\ldots , w_{0l})'\in \mathbb {U}(\varvec{y}_i;\epsilon _1)\subseteq U$ such that $\sum _{j=1}^la_{ij}w_{0j}+c_i>\mathtt {MAX}_i$, contradicting the fact that $\sum _{j=1}^l a_{ij}w_{j}+c_i$ reaches its maximum $\mathtt {MAX}_i$ in U at the point $\varvec{y}_i$. Thus, $\mathtt {MAX}_i\le b$ for $i=1,\ldots ,m$. That is, P is an over-approximation of the set U.

Lemma 2

Assume O is a simply connected compact set and $P=\{\varvec{w}:A\varvec{w}+C\le B\}$ is a compact convex polytope. If the boundary of the set O is a subset of the enclosure of the complement of the polytope P, and the intersection of the interior of the set O and the interior of the set P is not empty, then the set P is an under-approximation of the set O.

Proof

Since $P=\{\varvec{w}:A\varvec{w}+C\le B\}$ is compact, $P^{\circ }$ and P are simply connected sets with the same boundary $\partial P=\{\varvec{w}\in P: \vee _{i=1}^m\sum _{j=1}^l a_{ij}w_j+c_i=b\}$.

Assuming that $\varvec{y}\in P$ is a point such that $\varvec{y}\notin O$, we derive a contradiction as follows.

• Case 1: $\varvec{y}\in P^{\circ }$. Since $O^{\circ }\cap P^{\circ }\ne \emptyset$, there exists $\varvec{y}_0\in O^{\circ }\cap P^{\circ }$. Thus there exists a path q in $P^{\circ }$, connecting $\varvec{y}$ and $\varvec{y}_0$. Due to the assumption that $\varvec{y}\notin O$, there exists $\varvec{y}_1\in q$ such that $\varvec{y}_1\in \partial O$ and $\varvec{y}_1\in P^{\circ }$, contradicting the assumption that $\partial O\subseteq \overline{P^{c}}$.

• Case 2: $\varvec{y}\in \partial P$. Since $\varvec{y}\notin O$ and O is compact, there exists a $\delta >0$ such that $P^{\circ }\cap \mathbb {U}(\varvec{y};\delta )\ne \emptyset$ and $\mathbb {U}(\varvec{y};\delta )\cap O=\emptyset$. Thus there exists $\varvec{z}_1$ such that $\varvec{z}_1\in P^{\circ }\cap \mathbb {U}(\varvec{y};\delta )$ and $\varvec{z}_1\notin O$. Then, similar to the above case, a contradiction is derived.

Thus, we conclude that the set P is an under-approximation of the set O.

Fig. 1.

An illustration for Lemmas 1 and 2. (blue curve – the boundary of the set O in Lemma 1; red curve – the boundary of the convex polytope P; black curve – the boundary of the set U in Lemma 2.) (Color figure online)

Based on the above two lemmas, an approach to compute a polytopic $\mathtt {UAB}$ is proposed in the section that follows.

3 Under-Approximating Backward Reachable Sets

In this section an approach is proposed to compute an $\mathtt {UAB}$ of a compact simply connected target region $\mathtt {TR}$ after the time duration T. The $\mathtt {UAB}$ is represented by a polytope.

3.1 Computing Under-Approximations

In this subsection an approach for computing an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration T is detailed. The framework to compute an $\mathtt {UAB}$ of a simply connected compact set $\mathtt {TR}$ for the time duration T in our method involves the following steps,

• 1. a time grid $0=t_0<t_1<\ldots <t_N=T$ is adopted with a step size h;

• 2. starting with $U_{0}=\mathtt {TR}$, we compute a compact polytope $U_{1}$, which is an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration h;

• 3. starting from the $k^{th}$ $\mathtt {UAB}$, we advance our approximation to a compact polytopic $\mathtt {UAB}$ $U_{{k+1}}$;

• 4. $U_{N}$ is what we want to obtain.

Assume that we have already obtained a compact polytope $U_{k}$, where $U_{k}$ is an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration $t_k$. A compact polytopic $\mathtt {UAB}$ for the time duration ${k+1}$ is constructed through the following steps:

• (a) compute a set $\varOmega _{{k+1}}$, which is an union of a collection of intervals, such that $\partial \varOmega _b(h;U_{k},\varvec{f})\subseteq \varOmega _{{k+1}}$, as discussed below;

• (b) compute a compact polytope $O_{{k+1}}=\{\varvec{x}:A\varvec{x}+C\le B\}$ such that $\varOmega _{{k+1}}\subseteq O_{{k+1}}$;

• (c) contract $O_{{k+1}}$ to obtain $U_{{k+1}}=\{\varvec{x}:A\varvec{x}+C\le B^u\}$ such that $\varOmega _{{k+1}} \subseteq \overline{{U_{{k+1}}^{c}}}$ and ${U_{{k+1}}^{\circ }}\cap ({\varOmega _b(h;U_{{k}},\varvec{f})})^{\circ }\ne \emptyset$.

In order to prove that $U_{{k+1}}$ obtained by the steps (a) $\sim$ (c) is also a simply connected compact set and is a subset of $\varOmega _b(h;U_{{k}},\varvec{f})$, we first introduce a fundamental theorem behind our method based on the fact that $\varvec{\phi }(t;\cdot ): \varOmega _b(t;\varDelta ,\varvec{f})\mapsto \varDelta$ is a homeomorphism between two topological spaces $(\varDelta ,\mathcal {T}_{\varDelta })$ and $(\varOmega _b(t;\varDelta ,\varvec{f}), \mathcal {T}_{\varOmega _b(t;\varDelta ,\varvec{f})})$.

Theorem 1

[28, 29] If $\varDelta \subseteq \mathbb {R}^n$ is a simply connected compact set, then $\varOmega _b(t;\varDelta ,\varvec{f})$ is also a simply connected compact set and $\partial \varOmega _b(t;\varDelta ,\varvec{f})$=$\varOmega _b(t;\partial \varDelta , \varvec{f})$.

Based on Theorem 1, we have the following lemma stating that $U_{{k+1}}$ is a simply connected compact $\mathtt {UAB}$ of $\mathtt {U_{k}}$ for the time duration h.

Lemma 3

If $U_{k}$ is a simply connected compact set, then $U_{{k+1}}$ obtained by our framework is also a simply connected compact set satisfying $U_{{k+1}}\subseteq \varOmega _b(h;U_{{k}},\varvec{f})$.

Proof

Since $U_{k}$ is a simply connected compact set, $\varOmega _b(h;U_{k},\varvec{f})$ is also a simply connected compact set according to Theorem 1. Also, since $O_{{k+1}}$ in our framework is a simply connected compact set, we obtain that $U_{{k+1}}$ is a simply connected compact set.

Regarding $\partial \varOmega _b(h;U_{k},\varvec{f})\subseteq \varOmega _{{k+1}}\subseteq \overline{U_{{k+1}}^c}$ and $U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{{k}}, \varvec{f}))^{\circ }\ne \emptyset$, we conclude that $U_{{k+1}}\subseteq \varOmega _b(h;U_{{k}},\varvec{f})$ according to Lemma 2.

From Lemma 3, we can deduce that $U_{N}$ is an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration T, as stated in Theorem 2.

Theorem 2

Given a nonlinear system of the form (1), if $U_{0}=\mathtt {TR}$ is a simply connected compact set, $U_{N}$ obtained by our computational framework is an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration $t=T$.

In the sections that follow, we detail how to compute $\varOmega _{{k+1}}$, $O_{{k+1}}$ and $U_{{k+1}}$ in the steps (a) $\sim$ (c).

3.1.1 Computing $\varOmega _{{k+1}}$ and $O_{{k+1}}$

In this subsection, we describe how to compute $\varOmega _{{k+1}}$ and $O_{{k+1}}$ in the steps (a) and (b) respectively in our computational framework.

Firstly, we introduce a proposition stating that the backward reachable set of System (1) can be obtained by computing the corresponding forward reachable set of its reverse system, as described in the following.

Proposition 1

 [21] $\varOmega _f(h;\mathcal {X},-\varvec{f})$=$\varOmega _b(h;\mathcal {X},\varvec{f})$, where $\mathcal {X}\subseteq \mathbb {R}^n$.

From Proposition 1, we observe that $\varOmega _f(h;U_{k},-\varvec{f})$ instead of $\varOmega _b(h;U_{k},\varvec{f})$ can be used for performing computations in our computational framework, where $k=0,\ldots ,N-1$. Thus, we can equivalently compute a set $\varOmega _{{k+1}}$ such that $\partial \varOmega _f(h;U_{k},-\varvec{f}) \subseteq \varOmega _{{k+1}}$. Also, the fact that the boundary of $\varOmega _f(h;U_{k},-\varvec{f})$ corresponds to the boundary of $U_{k}$ under the map $\varvec{\phi }(h;\cdot )$ according to Theorem 1 is observed. Thus $\varOmega _{{k+1}}$ is obtained based on $\partial U_{{k}}$. According to these observations, an approach to computing $\varOmega _{{k+1}}$ is presented, as described in the following.

• 1. For a given $\epsilon _{M}$, we use the interval Branch and Bound methods (e.g., [30]) to obtain a set of compact intervals $\{s_{j},j=1,\ldots ,M_k\}$ such that $\partial U_{{k}}\subseteq \cup _{j=1}^{M_k}s_{j}$, where $M_k$ is the number of intervals and each interval $s_{j}$ is of the form $[\underline{x}_1,\overline{x}_1]\times \ldots \times [\underline{x}_n,\overline{x}_n]$ satisfying $|\overline{x}_l-\underline{x}_l|\le \epsilon _{M}$.

• 2. For $j=1,\ldots ,M_k$, we use interval reachability analysis based methods (e.g., [24]) to obtain a compact interval $I_{j}$ such that $\varOmega _f(h;s_{j},-\varvec{f})\subseteq I_{j}$. Thus, $\varOmega _{{k+1}}=\cup _{j=1}^{M_k}I_{j}$ is what we want.

The above procedure for computing $\varOmega _{{k+1}}$ is denoted by $\mathtt {Boundary}(h,U_{k},\epsilon _M)$.

Remark 2

In the procedure $\mathtt {Boundary}(h,U_{k},\epsilon _M)$, $\epsilon _{M}$ is used to restrict the size of boxes enclosing $\partial U_{k}$. As $\epsilon _M$ becomes smaller, the volume of the obtained boxes becomes smaller and the resulting $\varOmega _{{k+1}}$ becomes less conservative, but the computational burden increases.

The procedure $\mathtt {Boundary}(h,U_{k},\epsilon _M)$ for computing $\varOmega _{{k+1}}$ is illustrated through the following example.

Example 1

Consider a model of an electromechnical oscillation of s synchronous machine [31],

$$\begin{aligned} \left\{ \begin{aligned}&\dot{x_1}=x_2\\&\dot{x_2}=0.2-0.7sinx_1-0.05x_2\\ \end{aligned} \right. , \end{aligned}$$

where $\mathtt {TR}=[-0.1,0.1] \times [2.9,3.1]$ and $T=0.5$.

Computing $\varOmega _1$ when $h=0.5$ and $\epsilon _{M}=0.05$ is illustrated in Fig. 2.

Fig. 2.

An illustration for computing $\varOmega _1$. (red boxes – $\varOmega _1$ including $\partial \varOmega _b(T;\mathtt {TR},\varvec{f})$; green points – $\partial \varOmega _b(T;\mathtt {TR},\varvec{f})$ obtained by simulation methods; black points – some simulation trajectories originating from $\varOmega _b(T;\mathtt {TR},\varvec{f})$ over the time interval [0, 0.5]; purple curve – $\partial \mathtt {TR}$; blue boxes – $\cup _{j} s_{j}$ including $\partial TR$.) (Color figure online)

Next, we compute a convex hull $O_{{k+1}}$ such that $O_{{k+1}}\supseteq \varOmega _{{k+1}}$, where $\varOmega _{{k+1}}=\cup _{j=1}^{M_{k}}I_{j}$. Let $v_{j}$ be the set of vertices of the interval $I_{j}$ and $v=\cup _{j=1}^{M_{k}}v_{j}$. We get a polytope $O_{{k+1}}=\{\varvec{x}:A\varvec{x}+C\le B\}$ of v using convex hull algorithm (e.g., [33]), where $A=(a_{ij})_{m\times n}$ and $B=(b,\ldots ,b)'$. This procedure for computing $O_{{k+1}}$ is denoted by $\mathtt {Polytope}(\varOmega _{{k+1}})$.

Since $I_{j}$ is compact for $j=1,\ldots ,M_k$, v is a bounded set, and as a consequence $O_{{k+1}}$ is bounded and thus compact. Also, since every box $I_{j}$ is also a convex hull of $v_{j}$, every $\varvec{x} \in I_{j}$ can be formulated as $\sum _{l=1}^{2^n} \lambda _l\varvec{v}_{j,l}$, where $\varvec{v}_{j,l}\in v_{j}$, $\lambda _{l}\ge 0$ for $l=1,\ldots ,2^n$ and $\sum _{l=1}^{2^n}\lambda _{l}=1$. Thus $\varvec{x}\in O_{{k+1}}$ holds, implying that $\cup _{j=1}^{M_{k}}I_{j}\subseteq O_{{k+1}}$. Now we conclude that $O_{{k+1}}$ in the step (b) is computed.

Remark 3

According to Lemma 1 in Subsect. 2.2, the convex hull $O_{{k+1}}$ is an over-approximation of the backward reachable set of $U_{k}$ for the time duration h.

3.1.2 Computing an Under-Approximation $U_{{k+1}}$

This section focuses on computing a polytopic under-approximation $U_{{k+1}}$ (step (c) in our computational framework) by solving linear programming problems.

After obtaining $\varOmega _{{k+1}}=\cup _{j=1}^{M_{k}}I_{j}$ and $O_{{k+1}}=\{\varvec{x}:A\varvec{x}+C\le B\}$ in steps (a) and (b) based on the method in Subsect. 3.1, we shrink $O_{{k+1}}$ to yield $U_{{k+1}}$ by solving linear programming problems. The computations consist of two steps, as described below.

• 1. For $j=1,\ldots ,M_k$, we solve the following linear optimization problem:

  $$\begin{aligned} \begin{array}{ll} &{}\text {minimize} \quad b_{j}\\ &{}\text {s. t. } \quad A\varvec{x}+C\le B_{j},\\ &{} \qquad \qquad ~~ b_{j}\le b,\\ &{} \qquad \qquad ~~ \varvec{x}\in I_{j}, \end{array} \end{aligned}$$

  (2)

  where $B_{j}=(b_{j},\ldots ,b_{j})'$. Since $b_j\le b$, we can obtain that $\{\varvec{x}: A\varvec{x}+C\le B_j\}\subseteq \{\varvec{x}: A\varvec{x}+C\le B\}$.

• 2. We denote $min\{b_{j},j=1,\ldots ,M_{k}\}$ by $b^u$ and $(b^u,\ldots ,b^u)'$ by $B^u$ respectively. If $\{\varvec{x}:A\varvec{x}+C\le B^u\}\ne \emptyset$, it is denoted by $U_{{k+1}}$. The case that $U_{{k+1}}$ is empty is discussed in Sect. 4. Note that $U_{{k+1}}$ is just a candidate of what we want.

The above procedure for $U_{{k+1}}$ is denoted by $\mathtt {Contraction}(\varOmega _{{k+1}},O_{{k+1}})$, which is illustrated in the following example.

Example 2

For Example 1, computing $U_{1}$ when $\epsilon _{M}=0.05$ and $h=0.5$ is illustrated in Fig. 3, where $T=0.5$.

Fig. 3.

An illustration for computing $\varOmega _1$. (red boxes – $\varOmega _1$ including $\partial \varOmega _b(T;\mathtt {TR},\varvec{f})$; green curve – $\partial O_{1}$; black curve – $\partial U_1$.) (Color figure online)

Since $U_{{k+1}}\subseteq O_{{k+1}}$, $U_{{k+1}}$ is compact. However, we cannot conclude that $U_{k+1}$ is an $\mathtt {UAB}$ of $U_k$ for the time duration h. In order to further ensure that $U_{{k+1}}$ is an under-approximation of $\varOmega _b(h;U_{{k}}, \varvec{f})$, we need to verify whether $U_{{k+1}}$ satisfies the condition as described in the step (c) in our computational framework, i.e., verify whether $\varOmega _{{k+1}} \subseteq \overline{{U_{{k+1}}^{c}}}$ and ${U_{{k+1}}^{\circ }}\cap ({\varOmega _b(h;U_{{k}},\varvec{f})})^{\circ }\ne \emptyset$ holds.

For the constraint $\varOmega _{{k+1}} \subseteq \overline{{U_{{k+1}}^{c}}}$, we can ensure it by the following lemma.

Lemma 4

$\varOmega _{{k+1}}\subseteq \overline{U_{{k+1}}^{c}}$, where $\varOmega _{{k+1}}$ and $U_{{k+1}}$ are respectively obtained based on the procedures $\mathtt {Boundary}(h,U_{k},\epsilon _M)$ and $\mathtt {Contraction}(\varOmega _{{k+1}},O_{{k+1}})$.

Proof

Since $U_{{k+1}}=\{\varvec{x}: A\varvec{x}+C\le B^u\}$, where $A=\big (a_{ij}\big )_{m\times n}$, $C=(c_{1},\ldots ,c_{m})'$, $B^u=(b^u,\ldots ,b^u)'$, $b^u=\min \{b_{j},j=1,\ldots ,M_{k}\}$ and $b_{j}$ is obtained by solving the optimization problem (2), we can obtain that for every $\varvec{x}=(x_1,\ldots ,x_n)'\in \cup _{j=1}^{M_k}I_{j}$, there exists an index $i\in \{1,\ldots ,m\}$ such that $\sum _{j=1}^n a_{ij}x_j+c_{i}\ge b^u$, implying that $\varvec{x}\notin \{\varvec{x}:A\varvec{x}+C<B^u\}$. Thus, $\varOmega _{{k+1}}=\cup _{j=1}^{M_{k}} I_{j}\subseteq \overline{{U_{{k+1}}^{c}}}$.

In order to check whether $U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ }\ne \emptyset$ holds, we first take a point $\varvec{x}\in U_{{k+1}}^{\circ }=\{\varvec{x}:A\varvec{x}+C< B^u\}$, then apply interval methods (e.g., [24]) to get an interval enclosure $s_{\varvec{x}}$ of $\varvec{\phi }(h;\varvec{x})$, and check whether $s_{\varvec{x}}\subseteq U_{{k}}$ holds. If the answer is positive, $U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ }\ne \emptyset$ holds, as stated in Lemma 5. The procedure for checking $U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ }\ne \emptyset$ is denoted by $\mathtt {Verification}(U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ })$.

Lemma 5

If $s_{\varvec{x}}\subseteq U_{{k}}$, then $\varvec{x}$ ⁶ $\in U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ }$ holds, where $s_{\varvec{x}}$ and $U_{{k+1}}$ are respectively computed based on the procedures $\mathtt {Verification}(U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ })$ and $\mathtt {Contraction}(\varOmega _{{k+1}},O_{{k+1}})$.

Proof

Since $s_{\varvec{x}}\subseteq U_{{k}}$, $\varvec{x}\in \varOmega _f(h;U_{k},-\varvec{f})$ and thus $\varvec{x}\in \varOmega _b(h;U_{k},\varvec{f})$ holds. Also, according to the fact that $\partial \varOmega _b(h;U_{k},\varvec{f})\subseteq \varOmega _{k+1}$ and $\varOmega _{{k+1}}\subseteq \overline{U_{{k+1}}^{c}}$, we obtain that $U_{{k+1}}^{\circ } \cap \partial \varOmega _b(h;U_{k},\varvec{f})=\emptyset$, implying that $\varvec{x}\notin \partial \varOmega _b(h;U_{k},\varvec{f})$. Thus, $\varvec{x}\in U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ }$.

Thus, if the boolean value returned by $\mathtt {Verification}(U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ })$ is true, i.e., $U_{{k+1}}^{\circ }\cap (\varOmega _b(h;U_{k},\varvec{f}))^{\circ }\ne \emptyset$, then $U_{{k+1}}$ obtained by the procedure $\mathtt {Contraction}(\varOmega _{{k+1}},O_{{k+1}})$ is an $\mathtt {UAB}$ of $\varOmega _b(h;U_{k},\varvec{f})$.

Remark 4

In the procedure $\mathtt {Contraction}(\varOmega _{{k+1}},O_{{k+1}})$, $|\frac{b-b^u}{b-d}|$ can be used to evaluate the obtained $\mathtt {UAB}$ $U_{k}$, where d is the supremum such that $\{\varvec{x}:A\varvec{x}+C<D\}=\emptyset$ and $D=(d,\ldots ,d)'$ ⁷. As it approaches one, the under-approximation becomes increasingly conservative.

Thus our approach for computing a compact polytopic $\mathtt {UAB}$ is elucidated. We formally formulate our approach for computing an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration T as Algorithm 1.

Remark 5

Our method, as formalised in Algorithm 1, can be applied to under-approximate forward reachable sets by performing forward computations on initial sets.

In order to enhance the understanding of our approach, an example is employed to illustrate Algorithm 1 as follows.

Example 3

Consider a model of an electromechanical oscillation of s synchronous machine,

$$\begin{aligned} \left\{ \begin{aligned}&\dot{x_1}=x_2\\&\dot{x_2}=0.2-0.7sinx_1-0.05x_2\\ \end{aligned} \right. , \end{aligned}$$

where $\mathtt {TR}=[-0.1,0.1] \times [2.9,3.1]$ and $T=3$.

Let $h=3$, $\epsilon _{M}=0.0001$ and $\epsilon =0.5$. Firstly, we compute $\varOmega _1=\cup _{j} I_{j}$ such that $\partial \varOmega _b(T;\mathtt {TR},\varvec{f})\subseteq \varOmega _1$ based on the procedure $\mathtt {Boundary}(h,\mathtt {TR},\epsilon _M)$ in Subsect. 3.1, where $I_{j}$ is of the interval form. Secondly, we compute $O_1$ based on the procedure $\mathtt {Polytope}(\varOmega _{1})$ in Subsect. 3.1 such that $\varOmega _1\subseteq O_1$. Thirdly, we contract $O_1$ to obtain $U_1$ based on the procedure $\mathtt {Contraction}(\varOmega _{1},O_{1})$ in Subsect. 3.1. Finally, we find a point $\varvec{x}=(-8.08,2.52) \in U_1^{\circ }$ and obtain $s_{\varvec{x}}=[0.0082,0.0083] \times [3.0181,3.0182]$ based on the procedure $\mathtt {Verification}(U_{{1}}^{\circ }\cap (\varOmega _b(h;\mathtt {TR},\varvec{f}))^{\circ })$ in Subsect. 3.1. Since $s_{\varvec{x}}\subseteq \mathtt {TR}$ and $|\frac{b-b^u}{b-d}|\approx 0.246621\le \epsilon$, where $b=0$, $b^u=-0.008260$ and $d=-0.0334927$, $U_{1}$ is an $\mathtt {UAB}$ of $\mathtt {TR}$ for the time duration $T=3$. The boundary of $U_1$ is depicted in Fig. 4.

Fig. 4.

An $\mathtt {UAB}$ for Example 3. (left: red boxes – $\varOmega _1$ including $\partial \varOmega _b(3;\mathtt {TR},\varvec{f})$; green curve – $\partial O_{1}$; black curve – $\partial U_{1}$; right: a zoomed-in portion of the left figure.) (Color figure online)

3.2 Computational Complexity

In this subsection, the computational complexity of Algorithm 1 is discussed briefly. In the $k^{th}$ step, the branch-and-bound method for the problem of yielding some interval subdivisions to enclose $\partial U_{k}$ is of exponential complexity $\mathcal {O}(\xi ^n)$, where $\xi =\mathcal {O}(\frac{1}{\epsilon _{M}})$. The underlying interval Taylor series method is of polynomial complexity: the work is $\mathcal {O}(p^2)$ to compute the Taylor coefficients, where p is the order of the used Taylor expansion, and $\mathcal {O}(n^3)$ for performing linear algebra [32]. The complexity of applying simplex algorithms to solve the linear program (2) is $\mathcal {O}(nm_k)$ generally, where $m_k$ is the number of linear constraints. The computational complexity of the convex hull algorithm (e.g., [33]) is $\mathtt {Con_k}=\mathcal {O}(2^n M_k~logr)$ for $n\le 3$ and $\mathcal {O}(2^n M_k f_r/r+f_r)$ when $n>3$, where $r\le 2^n M_k$ is the number of vertices of $O_{{k+1}}$, $f_r=\mathcal {O}(r^{\lfloor \frac{n}{2}\rfloor }/{\lfloor \frac{n}{2}\rfloor }!)$ and $\lfloor \frac{n}{2}\rfloor$ is the floor function of $\frac{n}{2}$. Therefore, the total computational complexity of our method is $\sum _{k=0}^{N-1}\big ({\mathcal {O}(\xi _k^n)}+M_k(\mathcal {O}(p^2)+\mathcal {O}(n^3))+M_k \mathcal {O}(n m_k)+ \mathtt {Con_k}\big )$.

4 Examples, Discussions and Comparisons

Our approach is implemented based on the floating point linear programming solver GLPK running the Simplex algorithm and the validated ordinary differential equation solver VNODE-LP [24]. We evaluate it using five examples and compare it with the method of Korda et al. [22]. The results for Examples 4–7 can be found in Figs. 5, 6, 7 and 8 respectively. Table 1 presents details on parameters that control our approach. All these computations are performed on an i5-3337U 1.8 GHz CPU with 4 GB RAM running Ubuntu Linux 13.04.

4.1 Examples and Discussions

In this subsection our approach is evaluated using Examples 4–8, and parameters that control our approach are discussed using the first four examples. The results are illustrated in Figs. 4, 5, 6 and 7. Regarding the computational complexity analysis in Subsect. 3.2, our approach suffers from dimensional curse. In order to overcome this problem, we explore some future directions to make our approach more practical through Example 8.

Table 1. Performance of Algorithm 1 on Examples. Each benchmark is indexed by its example number. $\mathtt {TR}$: target region, $\epsilon _{M}$: bound for the size of intervals in the procedure $\mathtt {Boundary}(h,U_{{k}},\epsilon _M)$; $\epsilon$: bound for $|\frac{b-b^u}{b-d}|$ in the procedure $\mathtt {Contraction}(\varOmega _{{k+1}},O_{{k+1}})$; h: step size; T : a specified time duration for $\mathtt {UAB}$; Time: CPU time cost (seconds).

Example 4

Consider the system in Example 1 again

$$\begin{aligned} \left\{ \begin{aligned}&\dot{x_1}=x_2\\&\dot{x_2}=0.2-0.7sinx_1-0.05x_2\\ \end{aligned} \right. . \end{aligned}$$

Example 5

Consider the Brusselator model [10],

$$\begin{aligned} \left\{ \begin{aligned}&\dot{x_1}=1+x_1^2x_2-1.5x_1-x_1\\&\dot{x_2}=1.5x_1-x_1^2x_2\\ \end{aligned} \right. , \end{aligned}$$

Example 6

Consider the Van-der-Pol system,

$$\begin{aligned} \left\{ \begin{aligned}&\dot{x_1}=x_2\\&\dot{x_2}=-0.2(x_1^2-1)x_2-x_1\\ \end{aligned} \right. . \end{aligned}$$

Example 7

Consider the 3D-Lotka-Volterra System,

$$\begin{aligned} \left\{ \begin{aligned}&\dot{x_1}=x_1x_2-x_1x_3\\&\dot{x_2}=x_2x_3-x_2x_1\\&\dot{x_3}=x_3x_1-x_3x_2\\ \end{aligned} \right. . \end{aligned}$$

Note that $\varOmega _b(2.5;\mathtt {TR},\varvec{f})\subseteq$ $O_{1}$ in Fig. 8 according to Remark 3.

Fig. 5.

$\partial \mathtt {UAB}$ for Example 4.(blue points – $\partial \varOmega _b(10;\mathtt {TR},\varvec{f})$ obtained by Runge-Kutta methods; red curve – $\partial U_{20}$ when $\epsilon _{M}=0.0002$; green curve – $\partial U_{20}$ when $\epsilon _{M}=0.001$.) (Color figure online)

Fig. 6.

$\partial \mathtt {UAB}$ for Example 5. (blue points – $\partial \varOmega _b(1.1;\mathtt {TR},\varvec{f})$ obtained by Runge-Kutta methods; red curve – $\partial U_{22}$ when $\epsilon _{M}=0.0002$; green curve – $\partial U_{22}$ when $\epsilon _{M}=0.001$.) (Color figure online)

Fig. 7.

$\partial \mathtt {UAB}$ for Example 6. (blue points – $\partial \varOmega _b(10;\mathtt {TR},\varvec{f})$ obtained by Runge-Kutta methods; red curve – $\partial U_{20}$ when $\epsilon _{M}=0.0001$; green curve - $\partial U_{20}$ when $\epsilon _{M}=0.001$.) (Color figure online)

Fig. 8.

$\partial \mathtt {UAB}$ for Example 7. (black curve – $\partial O_{1}$ when $h=2.5$; red curve – $\partial U_{1}$ when $h=2.5$; green curve – $\partial U_{5}$ when $h=0.5$.) (Color figure online)

From the above four examples, we first observe that polytopes can represent reachable sets well for some nonlinear systems, e.g., Examples 4–7. Also, we observe that (1) when h is fixed, the resulting $\mathtt {UAB}$ becomes less conservative as $\epsilon _{M}$ becomes smaller (Examples 4–6); (2) when $\epsilon _{M}$ is fixed, a smaller h may lead to large errors. The underlying reason is that the under-approximation error in every iterative step will propagate through the computations (Example 7), similar to the well known wrapping effect in over-approximating reachable sets. The errors in the construction of under-approximations of reachable sets using our method result from three parts in every iteration. The first one is the computation of interval boxes enclosing the boundary of the target region. The second one is the computation of interval boxes enclosing the boundary of the backward reachable set based on the interval Taylor-series method and the last one is the computation of an polytopic under-approximation. It is well known that reachable sets of nonlinear systems are in general far from being convex, the last one contributes to the total error mainly. Especially, for the case that the returned under-approximation is empty in some iterative step, we could try a smaller $\epsilon _M$ and/or a different time step h. A smaller $\epsilon _M$, which mitigates the error from the first source, will help to obtain a tighter $\varOmega _{{k+1}}$, eventually leading to a less conservative $\mathtt {UAB}$. However, the computational cost increases. Therefore, in order to obtain a tighter $\varOmega _{{k+1}}$, reachability analysis methods which better control the wrapping effect should be considered (e.g., [10, 27]). This corresponds to the reduction of the error from the second source. As to the last error source resulting from polytopic approximations, an under-approximation of the semi-algebraic form instead of the polytopic form will be contemplated in our future study.

Example 8

Consider a seven-domensional biological system⁸,

$$\begin{aligned} \left\{ \begin{array}{ll} \dot{x}_1=-0.4x_1+5x_3x_4\\ \dot{x}_2=0.4x_1-x_2\\ \dot{x}_3=x_2-5x_3x_4\\ \dot{x}_4=5x_5x_6-5x_3x_4\\ \dot{x}_5=-5x_5x_6+5x_3x_4\\ \dot{x}_6=0.5x_7-5x_5x_6\\ \dot{x}_7=-0.5x_7+5x_5x_6\\ \end{array} \right. . \end{aligned}$$

Using an interval hull rather than a convex hull in every iterative step of Algorithm 1, we obtain that an $\mathtt {UAB}$ for the time duration $t=0.2$ is $[-0.0152,0.000] \times [-0.0169,0.0011] \times [-0.0140,0.0030] \times [-0.0141,0.0001] \times [-0.0141,0.0001] \times [-0.0138,0.0014] \times [-0.0155,0.000]$.

From Example 8, we observe that our approach scales well to systems with a large number of variables by using an interval hull instead of a convex hull in every iteration. However, this results in more conservative results, compared to that based on polytopic representations. In order to reduce the conservativeness brought by interval representations, while making our approach scale well, we will explore using oriented rectangular hulls [25], zonotopes [15] or symbolic orthogonal projections [34] to construct under-approximations in our future work. Furthermore, regarding that the boundary of a polytope is piecewise of the zonotope form, therefore the exact boundary of the polytope rather than interval subdivisions enveloping it obtained by Branch and Bound methods in every iteration can be used for computations directly using methods in [11, 27], thereby reducing the computational cost and further improving the scalability of our method.

4.2 Comparisons

In this section we will compare our method with the method of Korda et al. [22]. Due to a lot of input parameters such as sum-of-squares multipliers being coordinated in the method of Korda et al. [22], it is not trivial to find an optimal combination, thereby making fair comparisons difficult. Therefore, we try to explore some potential benefits of our method by comparing with this method.

Firstly, the method of Korda et al. [22] aims to compute inner approximations of the region of attraction for polynomial dynamical systems by solving sum-of-squares programming problems. The region of attraction is the set of all states that end in the target set at a given time without leaving a constraint set. In contrast, our method is not restricted to polynomial dynamical systems. That is, our method can deal with more general nonlinear systems such as Example 4 in Subsect. 4.1. Secondly, we compare the performances of the two methods based on Examples 5–8. Assume that the specified constraint sets for the four examples are $\{\varvec{x}: 1.25^2-(x_1+0.75)^2-(x_2-0.65)^2\ge 0\}$, $\{\varvec{x}: 4-x_1^2-x_2^2\ge 0\}$, $\{\varvec{x}:0.04-x_1^2-x_2^2-x_3^2\ge 0\}$ and $\{\varvec{x}:0.0125^2-\sum _{i=1}^7(x_i+0.0075)^2\ge 0\}$ respectively. Actually, they are respectively the over-approximations of backward reachable sets of the target regions for these four examples. Using the method of Korda et al. [22], we can not obtain feasible solutions to any of the above examples based on the sum-of-squares programming solver YALMIP [35] with Sedumi [36]. Since there are a lot of sum-of-squares multipliers that are coordinated in advance, their degrees should be determined in advance for computations, improper mixing will result in unreliable results. The main underlying reason is that the present status of semi-definite programming solvers is not so advanced, as pointed out in [37]. The numerical problems produced by these solvers often result in unreliable results for some cases. We use Example 5 to illustrate this. Although the solver YALMIP returns a “feasible" solution as shown in Fig. 9 for some mixing of sum-of-squares multipliers, the result is incorrect actually. On the contrary, our method relies on Interval methods to locate the boundary of the backward reachable set and linear programs to obtain an under-approximation in every iterative step, making our method more reliable.

Fig. 9.

An incorrect $\mathtt {UAB}$ for Example 5 obtained by the method of Korda et al. [22] due to numerical problems. (black curve – $\{\varvec{x}: 1.25^2-(x_1+0.75)^2-(x_2-0.65)^2\ge 0\}$; red curve – the boundary of an incorrect under-approximation of $\varOmega _b(1.1,\mathtt {TR},\varvec{f})$; green curve - $\partial \mathtt {TR}$; blue points – $\partial \varOmega _b(1.1,\mathtt {TR},\varvec{f})$ obtained by Runge Kutta methods.) (Color figure online)

5 Conclusion

Given a nonlinear system and a target region of the simply connected compact type, we in this paper proposed a method by performing boundary analysis to obtain an $\mathtt {UAB}$ of the target region for a specified time duration. The $\mathtt {UAB}$ is represented as a polytope. The polytope can be obtained by combining validated numerical methods for ordinary differential equations and linear programs. Numerical results and comparisons with the method of Korda et al. [22] based on five examples were given to illustrate the benefits of our approach. The results show that our method has some significant benefits in under-approximating reachable sets for some cases. Furthermore, we explore some directions toward improving the scalability of our method.

Extending our method to compute under-approximations of reachable sets for nonlinear systems with time delay (e.g., [38]) is considered in our future work. Moreover, computing a bounded error approximation of the solution over a bounded time is another interesting investigation towards addressing under-approximation problems [39].