1 Introduction

Hybrid systems [17] are widely used to model dynamical systems which exhibit both discrete and continuous behaviors. The reachability analysis of hybrid systems has been a challenging problem over the last few decades. The hard core of this problem lies in dealing with the continuous behavior of systems that are described by ordinary differential equations (ODEs). Although there are currently several quite efficient and scalable approaches for reachability analysis of linear systems [8,9,10, 14, 16, 19, 20, 26, 34], nonlinear ODEs are much harder to handle and the current approaches can be characterized into the following groups.

Invariant Generation [18, 21, 22, 27, 28, 36, 37, 39]. An invariant I for a system S is a set such that any trajectory of S originating from I never escapes from I. Therefore, finding an invariant I such that the initial set \(I_0\subseteq I\) and the unsafe set \(U\cap I=\emptyset \) indicates the safety of the system. In this way, there is no need to compute the flowpipe. The main problem with invariant generation is that it is hard to define a set of high quality constraints which can be solved efficiently.

Abstraction and Hybridization [2, 11, 24, 31, 35]. The basic idea of the abstraction-based approach is first constructing a linear model which over-approximates the original nonlinear dynamics and then applying techniques for linear systems to the abstraction model. However, how to construct an abstraction with the fewest discrete states and sufficiently high accuracy is still a challenging issue.

Satisfiability Modulo Theory (SMT) Over Reals [6, 7, 23]. This approach encodes the reachability problem for nonlinear systems as first-order logic formulas over the real numbers. These formulas can be solved using for example \(\delta -\)complete decision procedures that overcome the theoretical limits in nonlinear theories over the reals, by choosing a desired precision \(\delta \). An SMT implementing such procedures can return either unsat if the reachability problem is unsatisfiable or \(\delta \)-sat if the problem is satisfiable given the chosen precision. The \(\delta \)-sat verdict does not guarantee that the dynamics of the system will reach a particular region. It may happens that by increasing the precision the problem would result unsat. In general the limit of this approach is that it does not provide as a result a complete and comprehensive description of the reachability set.

Bounded Time Flowpipe Computation [1, 3,4,5, 25, 32]. The common technique to compute a bounded flowpipe is based on interval method or Taylor model. Interval-based approach is quite efficient even for high dimensional systems [29], but it suffers the wrapping effect of intervals and can quickly accumulate over-approximation errors. In contrast, the Taylor-model-based approach is more precise in that it uses a vector of polynomials plus a vector of small intervals to symbolically represent the flowpipe. However, for the purpose of safety verification or reachability analysis, the Taylor model has to be further over-approximated by intervals, which may bring back the wrapping effect. In particular, the wrapping effect can explode easily when the flowpipe segment over a time interval is stretched drastically due to a large difference in speed between individual trajectories. This case is demonstrated by the following example.

Example 1

(Running example). Consider the 2D system [30] described by \(\dot{x} = y\) and \(\dot{y} = x^2\). Let the initial set \( X_0 \) be a line segment \( x\in [1.0,1.0]\) and \(y\in [-1.05,-0.95]\), Fig. 1a shows the simulation result on three points in \( X_0 \) over time interval [0, 6.6]. The reachable set at \(t = 6.6\) s is a smooth curve connecting the end points of the three trajectories. As can be seen, the trajectory originating from the top is left far behind the one originating from the bottom, which means that the tiny initial line segment is being stretched into a huge curve very quickly, while the width of the flowpipe is actually converging to 0. As a result, the interval over-approximation of this huge curve can be extremely conservative even if its Taylor model representation is precise, and reducing the time step size is not helpful. To prove this point, we computed with Flow* [3] a Taylor model series for the time horizon of 6.6 s which consists of 13200 Taylor models. Figure 1b shows the interval approximation of the Taylor model series, which apparently starts exploding.

Fig. 1.
figure 1

(a) Simulation for Example 1 showing flowpipe segment being extremely stretched and deformed, (b) Interval over-approximation of the Taylor model computed by Flow* [3].

Full size image

In this paper, we propose to use piecewise barrier tubes (PBTs) to over-approximate flowpipes of polynomial nonlinear systems, which can avoid the issue caused by the excessive stretching of a flowpipe segment. The idea of PBT is inspired from barrier certificate [22, 33]. A barrier certificate \(B(\varvec{x})\) is a real-valued function such that (1) \(B(\varvec{x}) \ge 0\) for all \(\varvec{x}\) in the initial set \( X_0 \); (2) \(B(\varvec{x}) < 0\) for all \(\varvec{x}\) in the unsafe set \( X_U \); (3) no trajectory can escape from \(\{\varvec{x}\in \mathbb {R} ^n \mid B(\varvec{x}) \ge 0 \}\) through the boundary \(\{\varvec{x}\in \mathbb {R} ^n \mid B(\varvec{x}) = 0 \}\). A sufficient condition for this constraint is that the Lie derivative of \(B(\varvec{x})\) w.r.t the dynamics \(\dot{\varvec{x}} = \varvec{f}\) is positive all over the invariant region, i.e., \(\mathcal {L}_{\varvec{f}} B(\varvec{x}) > 0\), which means that all the trajectories must move in the increasing direction of the level sets of \(B(\varvec{\varvec{x}})\).

Barrier certificates can be used to verify safety properties without computing the flowpipe explicitly. The essential idea is to use the zero level set of \(B(\varvec{x})\) as a barrier to separate the flowpipe from the unsafe set. Moreover, if the unsafe set is very close to the boundary of the flowpipe, the barrier has to fit the shape of the flowpipe to make sure that all components of the constraint are satisfied. However, the zero level set of a polynomial of fixed degree may not have the power to mimic the shape of the flowpipe, which means that there may exist no solution for the above constraints even if the system is safe. This problem might be addressed using piecewise barrier certificate, i.e., cutting the flowpipe into small pieces so that every piece is straight enough to have a barrier certificate of simple form. Unfortunately, this is infeasible because we know nothing about the flowpipe locally. Therefore, we have to find another way to proceed.

Instead of computing a single barrier certificate, we propose to compute barrier tubes to piecewise over-approximate the flowpipe. Concretely, in the beginning, we first construct a containing box, called enclosure, for the initial set using interval approach [29] and simulation, then, using linear programming, we compute a group of barrier functions which work together to form a tight tube (called barrier tube) around the flowpipe. Similarly, taking the intersection of the barrier tube and the boundary of the box as the new initial set, we repeat the previous operations to obtain successive barrier tubes step by step. The key point here is how to compute a group of tightly enclosing barriers around the flowpipe without a constraint on the unsafe set inside the box. Our basic idea is to construct a group of auxiliary state sets U around the flowpipe and then, for each \(U_i\in U\), we compute a barrier certificate between \(U_i\) and the flowpipe. If a barrier certificate is found, we expand \(U_i\) towards the flowpipe iteratively until no more barrier certificate can be found; otherwise, we shrink \(U_i\) away from the flowpipe until a barrier certificate is found. Since the auxiliary sets are distributed around the flowpipe, so is the barrier tube. The benefit of such piecewise barrier tubes is that they are time independent, and hence can avoid the issue of stretched flowpipe segments caused by speed differences between trajectories. Moreover, usually a small number of BTs can form a tight over-approximation of the flowpipe, which means that less computation is needed to decide the intersection of PBT and the unsafe set.

The main contributions of this paper are as follows:

  1. 1.

    We transform the constraint-solving problem for barrier certificates into a linear programming problem using Handelman representation [15];

  2. 2.

    We introduce PBT to over-approximate the flowpipe of nonlinear systems, thus dealing with flowpipes independent of time and hence avoiding the error explosion caused by stretched flowpipe segments;

  3. 3.

    We implement a prototype in C++ to compute PTB automatically and we show the effectiveness of our approach by providing a comparison with the state-of-the-art tools for reachability analysis of polynomial nonlinear systems such as CORA [1] and Flow* [3].

The paper is organized as follows. Section 2 is devoted to the preliminaries. Section 3 shows how to compute barrier certificates using Handelman representation, while in Sect. 4 we present a method to compute Piecewise Barrier Tubes. Section 5 provides our experimental results and we conclude in Sect. 6.

2 Preliminaries

In this section, we recall some concepts used throughout the paper. We first clarify some notation conventions. If not specified otherwise, we use boldface lower case letters to denote vectors, we use \(\mathbb {R} \) for the real number field and \(\mathbb {N} \) for the set of natural numbers, and we consider multivariate polynomials in \(\mathbb {R} [\varvec{x}]\), where the components of \(\varvec{x}\) act as indeterminates. In addition, for all the polynomials \(B(\varvec{u} ,\varvec{x} )\), we denote by \(\varvec{u} \) the vector composed of all the \(u_i\) and denote by \(\varvec{x} \) the vector composed of all the remaining variables \(x_i\) that occur in the polynomial. We use \(\mathbb {R} _{\ge 0}\) and \(\mathbb {R} _{>0}\) to denote the domain of nonnegative real number and positive real number respectively.

Let \(P\subseteq \mathbb {R} ^n\) be a convex and compact polyhedron with non-empty interior, bounded by linear polynomials \(p_1,\cdots ,p_m \in \mathbb {R} [\varvec{x}]\). Without lose of generality, we may assume \(P=\{\varvec{x}\in \mathbb {R} ^n \mid p_i(\varvec{x})\ge 0, i=1,\cdots ,m\}\).

Next, we present the notation of the Lie derivative, which is widely used in the discipline of differential geometry. Let \(\varvec{f}: \mathbb {R}^n \rightarrow \mathbb {R}^n\) be a continuous vector field such that \(\dot{x}_i = f_i(\varvec{x})\) where \(\dot{x}_i\) is the time derivative of \(x_i(t)\).

Definition 1

(Lie derivative). For a given polynomial \(p\in \mathbb {R} [\varvec{x} ]\) over \(\varvec{x} =(x_1,\dots ,x_n)\) and a continuous system \(\dot{\varvec{x}} = \varvec{f} \), where \(\varvec{f} =(f_1,\dots ,f_n)\), the Lie derivative of \(p\in \mathbb {R} [\varvec{x} ]\) along \(\varvec{f}\) of order k is defined as follows.

$$\begin{aligned} \mathcal {L}_{\varvec{f}} ^{k} p {\mathop {=}\limits ^{\text {def}}} \left\{ \begin{array}{lc} p, &{} k = 0\\ {\mathop {\sum }\nolimits _{i=1}^n} \frac{\partial {\mathcal {L}_{\varvec{f}} ^{k-1} p}}{\partial {x_i}} \cdot f_i, &{} k \ge 1 \end{array}\right. \end{aligned}$$

Essentially, the k-th order Lie derivative of p is the k-th derivative of p w.r.t. time, i.e., reflects the change of p over time. We write \(\mathcal {L}_{\varvec{f}} p\) for \(\mathcal {L}_{\varvec{f}} ^{1} p\).

In this paper, we focus on semialgebraic nonlinear systems, which are defined as follows.

Definition 2

(Semialgebraic system). A semialgebraic system is a triple \(M {\mathop { = }\limits ^{\text {def}}} \langle X, \varvec{f}, X_0 , I\rangle \), where

  1. 1.

    \(X \subseteq \mathbb {R}^n\) is the state space of the system \(M \),

  2. 2.

    \(\varvec{f} \in \mathbb {R} [\varvec{x} ]^n\) is locally Lipschitz continuous vector function,

  3. 3.

    \( X_0 \subseteq X\) is the initial set, which is semialgebraic [40],

  4. 4.

    I is the invariant of the system.

The local Lipschitz continuity guarantees the existence and uniqueness of the differential equation \(\varvec{\dot{x}}=\varvec{f} \) locally. A trajectory of a semialgebraic system is defined as follows.

Definition 3

(Trajectory). Given a semialgebraic system \(M \), a trajectory originating from a point \(\varvec{x} _0\in X_0 \) to time \(T>0\) is a continuous and differentiable function \(\varvec{\zeta } (\varvec{x}_0,t):[0, T)\rightarrow \mathbb {R}^n\) such that (1) \(\varvec{\zeta } (x_0,0)=\varvec{x} _0\) , and (2) \(\forall \tau \in [0,T)\): \(\frac{d\varvec{\zeta }}{dt}\big |_{t=\tau } = \varvec{f} (\varvec{\zeta } (\varvec{x}_0,\tau ))\). T is assumed to be within the maximal interval of existence of the solution from \(\varvec{x} _0\).

For ease of readability, we also use \(\zeta (t)\) for \(\zeta (\varvec{x}_0,t)\). In addition, we use \(Flow_{\varvec{f}}( X_0 )\) to denote the flowpipe of initial set \( X_0 \), i.e.,

$$\begin{aligned} Flow_{\varvec{f}}( X_0 ) {\mathop {=}\limits ^{\text {def}}} \{\varvec{\zeta }(\varvec{x}_0,t) \mid \varvec{x}_0\in X_0 , t\in \mathbb {R} _{\ge },\dot{\varvec{\zeta }} = \varvec{f}(\varvec{\zeta }) \} \end{aligned}$$
(1)

Definition 4

(Safety). Given an unsafe set \( X_U \subseteq X\), a semialgebraic system \(M = \langle X, \varvec{f}, X_0 , I\rangle \) is said to be safe if no trajectory \(\varvec{\zeta } (\varvec{x}_0,t)\) of \(M \) satisfies that \(\exists \tau \in \mathbb {R}_{\ge 0}:\varvec{x} (\tau )\in X_U \), where \(\varvec{x}_0\in X_0 \).

3 Computing Barrier Certificates

Given a semialgebraic system \(M \), a barrier certificate is a real-valued function \(B(\varvec{x})\) such that (1) \(B(\varvec{x}) \ge 0\) for all \(\varvec{x}\) in the initial set; (2) \(B(\varvec{x}) < 0\) for all \(\varvec{x}\) in the unsafe set; (3) no trajectory can escape from the region of \(B(\varvec{x} ) \ge 0\). Then, the hyper-surface \(\{\varvec{x}\in \mathbb {R} ^n \mid B(\varvec{x}) = 0\}\) forms a barrier separating the flowpipe from the unsafe set. To compute such a barrier certificate, the most common approach is template based constraint solving, i.e., firstly figure out a sufficient condition for the above condition and then, set up a template polynomial \(B(\varvec{u},\varvec{x})\) of fixed degree, and finally solve the constraint on \(\varvec{u}\) derived from the sufficient condition on \(B(\varvec{u},\varvec{x})\). There are a couple of sufficient conditions available for this purpose [13, 22, 27]. In order to have an efficient constraint solving method, we adopt the following condition [33].

Theorem 1

Given a semialgebraic system \(M \), let \( X_0 \) and U be the initial set and the unsafe set respectively, the system is guaranteed to be safe if there exists a real-valued function \(B(\varvec{x})\) such that

$$\begin{aligned}&\forall \varvec{x}\in X_0 : B(\varvec{x}) > 0 \end{aligned}$$
(2)
$$\begin{aligned}&\forall \varvec{x}\in I: \mathcal {L}_f B > 0 \end{aligned}$$
(3)
$$\begin{aligned}&\forall \varvec{x}\in X_U : B(\varvec{x}) < 0 \end{aligned}$$
(4)

In Theorem 1, the condition (3) means that all the trajectories of the system always point in the increasing direction of the level sets of \(B(\varvec{x})\) in the region I. Therefore, no trajectory starting from the initial set would cross the zero level set. The benefit of this condition is that it can be solved more efficiently than other existing conditions [13, 22] although it is relatively conservative. The most widely used approach is to transform the constraint-solving problem into a sum-of-squares (SOS) programming problem [33], which can be solved in polynomial time. However, a serious problem with SOS programming based approach is that automatic generation of polynomial templates is very hard to perform. We now show an example to demonstrate the reason. For simplicity, we assume that the initial set, the unsafe set and the invariant are defined by the polynomial inequalities \( X_0 (\varvec{x}) \ge 0\), \( X_U (\varvec{x} ) \ge 0\) and \(I(\varvec{x} ) \ge 0\) respectively, then the SOS relaxation of Theorem 1 is that the following polynomials are all SOS

$$\begin{aligned}&B(\varvec{x}) - \mu _1(\varvec{x}) X_0 (\varvec{x}) + \epsilon _1 \end{aligned}$$
(5)
$$\begin{aligned}&\mathcal {L}_f B - \mu _2(\varvec{x}) I(\varvec{x}) + \epsilon _2 \end{aligned}$$
(6)
$$\begin{aligned}&-B(\varvec{x}) - \mu _3(\varvec{x}) X_U (\varvec{x}) + \epsilon _3 \end{aligned}$$
(7)

where \(\mu _i(\varvec{x}), i=1,\cdots ,3\) are SOS polynomials as well and \(\epsilon _i > 0, i=1,\cdots ,3\). Suppose the degrees of \( X_0 (\varvec{x})\), \(I(\varvec{x})\) and \( X_U (\varvec{x})\) are all odd numbers. Then, the degree of the template for \(B(\varvec{x})\) must be an odd number too. The reason is that, if deg(B) is an even number, in order for the first and third polynomials to be SOS polynomials, deg(B) must be greater than both \(deg(\mu _3 X_U )\) and \(deg(\mu _1 X_0 )\), which are odd numbers. However, since the first and third condition contain \(B(\varvec{x})\) and \(-B(\varvec{x})\) respectively, their leading monomials must have the opposite sign, which means that they cannot be SOS polynomial simultaneously. Moreover, the degrees of the templates for the auxiliary polynomials \(\mu _1(\varvec{x}), \mu _3(\varvec{x})\) must also be chosen properly so that \(deg(\mu _1 X_0 ) = deg(\mu _3 X_U )= deg(B)\), because only in this way the leading monomials (which has an odd degree) of (5) and (7) have the chance to be resolved so that the resultant polynomial can be a SOS. Similarly, in order to make the second polynomial a SOS as well, one has to choose an appropriate degree for \(\mu _2(\varvec{x})\) according to the degree of \(\mathcal {L}_f B\) and \(I(\varvec{x})\). As a result, the tangled constraints on the relevant template polynomials reduce the power of SOS programming significantly.

Due to the above reason, inspired by the work [38], we use Handelman representation to relax Theorem 1. We assume that the initial set \( X_0 \), the unsafe set \( X_U \) and the invariant I are all convex and compact polyhedra, i.e., \( X_0 = \{\varvec{x}\in \mathbb {R} ^n \mid p_1(\varvec{x})\ge 0,\cdots ,p_{m_1}(\varvec{x})\ge 0\}\), \(I = \{\varvec{x}\in \mathbb {R} ^n \mid q_1(\varvec{x})\ge 0,\cdots ,q_{m_2}(\varvec{x})\ge 0\}\) and \( X_U = \{\varvec{x}\in \mathbb {R} ^n \mid r_1(\varvec{x})\ge 0,\cdots ,r_{m_3}(\varvec{x})\ge 0\}\), where \(p_i(\varvec{x}),q_j(\varvec{x}),r_k(\varvec{x})\) are linear polynomials. Then, we have the following theorem.

Theorem 2

Given a semialgebraic system \(M \), let \( X_0 \), \( X_U \) and I be defined as above, the system is guaranteed to be safe if there exists a real-valued polynomial function \(B(\varvec{x})\) such that

$$\begin{aligned} B(\varvec{x})&\equiv \sum _{|\varvec{\alpha }|\le M_1} \lambda _{\varvec{\alpha }}p_1^{\alpha _1}\cdots p_{m_1}^{\alpha _{m_1}} + \epsilon _1 \end{aligned}$$
(8)
$$\begin{aligned} \mathcal {L}_f B&\equiv \sum _{|\varvec{\beta }|\le M_2} \lambda _{\varvec{\beta }}q_1^{\beta _1}\cdots q_{m_2}^{\beta _{m_2}} + \epsilon _2 \end{aligned}$$
(9)
$$\begin{aligned} -B(\varvec{x})&\equiv \sum _{|\varvec{\gamma }|\le M_3} \lambda _{\varvec{\gamma }}r_1^{\gamma _1}\cdots r_{m_3}^{\gamma _{m_3}} + \epsilon _3 \end{aligned}$$
(10)

where \(\lambda _{\varvec{\alpha }}, \lambda _{\varvec{\beta }}, \lambda _{\varvec{\gamma }}\in \mathbb {R} _{\ge 0}\), \(\epsilon _i \in \mathbb {R} _{>0}\) and \(M_i\in \mathbb {N}, i=1,\cdots ,3\).

Theorem 2 provides us with an alternative to SOS programming to find barrier certificate \(B(\varvec{x})\) by transforming it into a linear programming problem. The basic idea is that we first set up a template \(B(\varvec{u} ,\varvec{x} )\) of fixed degree as well as the appropriate \(M_i, i=1,\cdots ,3\) that make the both sides of the three identities (8)–(10) have the same degree. Since (8)–(10) are identities, the coefficients of the corresponding monomials on both sides must be identical as well. Thus, we derive a system S of linear equations and inequalities over \(\varvec{u} , \lambda _{\varvec{\alpha }}, \lambda _{\varvec{\beta }}, \lambda _{\varvec{\gamma }}\). Now, finding a barrier certificate is just to find a feasible solution for S, which can be solved by linear programming. Compared to SOS programming based approach, this approach is more flexible in choosing the polynomial template as well as other parameters. We consider now a linear system to show how it works.

Example 2

Given a 2D system defined by \(\dot{x} = 2x + 3y, \dot{y} = -4x + 2y\), let \( X_0 =\{(x,y)\in \mathbb {R} ^2\mid p_1 = x + 100 \ge 0, p_2= -90 - x \ge 0, p_3 = y + 45 \ge 0, p_4 = -40 - y \ge 0\}\), \(I =\{(x,y)\in \mathbb {R} ^2\mid q_1 = x\,+\,110 \ge 0, q_2 = -80\,-\,x \ge 0, q_3 = y\,+\,45 \ge 0, q_4 = -20 - y \ge 0\}\) and \( X_U =\{(x,y)\in \mathbb {R} ^2\mid r_1 = x + 98 \ge 0, r_2 = -90 - x \ge 0, r_3 = y + 24 \ge 0, r_4 = -20 - y \ge 0\}\). Assume \(B(\varvec{u},\varvec{x}) = u_1 + u_2x + u_3y\), \(M_i = \epsilon _i = 1\) for \(i=1,\cdots ,3\), then we obtain the following polynomial identities according to Theorem 2

$$\begin{aligned}&u_1 + u_2x + u_3y - \sum _{i=1}^4 \lambda _{1i} p_i -\epsilon _1 \equiv 0\\&u_2 (2x + 3y) + u_3(-4x + 2y) - \sum _{j=1}^4 \lambda _{2j} q_j -\epsilon _2 \equiv 0\\&-(u_1 + u_2x + u_3y) - \sum _{k=1}^4 \lambda _{3k} r_k -\epsilon _3 \equiv 0 \end{aligned}$$

where \(\lambda _{ij}\ge 0\) for \(i=1,\cdots ,3\), \(j=1,\cdots ,4\). By collecting the coefficients of x, y in the above polynomials, we obtain a system S of linear polynomial equations and inequalities over \(u_i, \lambda _{jk}\). By solving S using linear programming, we obtain a feasible solution and Fig. 2a shows the computed linear barrier certificate. Note that, for the aforementioned reason, it is impossible to find a linear barrier certificate using SOS programming for this example.

Fig. 2.
figure 2

(a) Linear barrier certificate (straight red line) for Example 2. Rectangle in green: initial set, rectangle in red: unsafe set. (b) PBT for the running Example 5, consisting of 45 BTs. (c) Enclosure (before bloating) for flowpipe of Example 3 (green shadow region). (d) Enclosure (after bloating) for flowpipe of Example 3. (Color figure online)

Full size image

4 Piecewise Barrier Tubes

In this section, we introduce how to construct PBTs for nonlinear polynomial systems. The basic idea of constructing PBT is that, for each segment of the flowpipe, an enclosure box is first constructed and then, a BT is constructed to form a tighter over-approximation for the flowpipe segment inside the box.

4.1 Constructing an Enclosure Box

Given an initial set, the first task is to construct an enclosure box for the initial set and the following segment of the flowpipe. As pointed out in Sect. 1, one principle to construct an enclosure box is to simplify the shape of the flowpipe segment, or in other words, to approximately bound the twisting of trajectories by some \(\theta \) in the box, where the twisting of a trajectory is defined as follows.

Definition 5

(Twisting of a trajectory). Let \(M\) be a continuous system and \(\zeta (t)\) be a trajectory of \(M\). Then, \(\zeta (t)\) is said to have a twisting of \(\theta \) on the time interval \(I = [T_1, T_2]\), written as \(\xi _I(\zeta )\), if it satisfies that \(\xi _I(\zeta ) = \theta \), where \( \xi _I(\zeta ) {\mathop {=}\limits ^{\text {def}}} \sup _{t_1,t_2 \in I} \arccos \bigg (\frac{\langle \dot{\zeta }(t_1),\,\dot{\zeta }(t_2) \rangle }{\Vert \zeta (t_1)\Vert \Vert \zeta (t_2)\Vert }\bigg )\).

The basic idea to construct an enclosure box is depicted in Algorithm 1.

figure a

Remark 1

In Algorithm 1, we use interval arithmetic [29] and simulation to construct an enclosure box E for a given initial set and its following flowpipe segment. Meanwhile, we obtain a coarse range of the intersection of the flowpipe and the boundary of the enclosure, which helps to accelerate the construction of barrier tube. To be simple, the enclosure is constructed in a way such that the flowpipe gets out of the box through a single facet. Given an initial set \( X_0 \), we first sample a set \(S_0\) of points from \( X_0 \) for simulation. Then, we select a point \(\varvec{x}_0\) from \(S_0\) and do \((\theta ,d)\)-simulation on \(\varvec{x}_0\) to obtain a time step \(\varDelta T\). A \((\theta ,d)\)-simulation is a simulation that stops either when the twisting of the simulation reaches \(\theta \) or when the distance between \(x_0\) and the end point reaches d. On the one hand, by using a small \(\theta \), we aim to achieve a straight flowpipe segment. On the other hand, by specifying a maximal distance d, we make sure that the simulation can stop for a long and straight flowpipe. At each iteration of the while loop in line 5, we first try to construct an enclosure box by interval arithmetic over \(\varDelta T\). If such an enclosure box is created, we then perform a simulation (see line 8) for all the points in \(S_0\) to find out the plane P of facet which intersects with the most of the simulations. The idea behind line 9 is that in order to better over-approximate the intersection of the flowpipe with the boundary of the box using intervals, we push the other planes outwards to make P the only plane where the flowpipe get out of the box. Certainly, simply by simulation we cannot guarantee that the flowpipe does not intersect the other facets. Therefore, we have the following theorem for the decision.

Theorem 3

Given a semialgebraic system \(M\) and an initial set \( X_0 \), a box E is an enclosure of \( X_0 \) and \(F_i\) is a facet of E. Then, \((Flow_f( X_0 ) \cap E) \cap F_i = \emptyset \) if there exists a barrier certificate \(B_i(\varvec{x})\) for \( X_0 \) and \(F_i\) inside E.

Remark 2

According to the definition of barrier certificate, the proof of Theorem 3 is straightforward, which is ignored here. Therefore, to make sure that the flowpipe does not intersect the facet \(F_i\), we only need to find a barrier certificate, which can be done using the approach presented in Sect. 3. Moreover, if no barrier certificate can be found, we further bloat the facet. Next, we still use the running Example 1 to demonstrate the process of constructing an enclosure.

Example 3

(running example). Consider the system in Example 1 and the initial set \(x =1.0, -1.05 \le y \le -0.95\), let the bounding twisting of simulation be \(\theta = \pi /18\), then the time step size we computed for interval evaluation is \(\varDelta T = 0.2947\). The corresponding enclosure computed by interval arithmetic is shown in Fig. 2c. Furthermore, by simulation, we know that the flowpipe can reach both left facet and top facet. Therefore, we have two options to bloat the facet: bloat the left facet to make the flowpipe intersects the top facet only or bloat the top facet to make the flowpipe intersects left facet only. In this example, we choose the latter option and the bloated enclosure is shown in Fig. 2d. In this way, we can over-approximate the intersection of the flowpipe and the facet by intervals if we can obtain its boundary on every side. This can be achieved by finding barrier tube.

4.2 Compute a Barrier Tube Inside a Box

An important fact about the flowpipe of continuous system is that it tends to be straight if it is short enough, given that the initial set is straight as well (otherwise, we can split it). Suppose there is a small box E around a straight flowpipe, it will be easy to compute a barrier certificate for a given initial set and unsafe set inside E. A barrier tube for the flowpipe in E is a group of barrier certificates which form a tube around a flowpipe inside E. Formally,

Definition 6

(Barrier Tube). Given a semialgebraic system \(M\), a box E and an initial set \( X_0 \subseteq E\), a barrier tube is a set of real-valued functions \(BT = \{B_i(\varvec{x}), i=1,\cdots ,m\}\) such that for all \(B_i(\varvec{x})\in BT\): (1) \(\forall \varvec{x}\in X_0 : B_i(\varvec{x}) > 0\) and, (2) \(\forall \varvec{x}\in E: \mathcal {L}_f B_i > 0\).

According to Definition 6, a barrier tube BT is defined by a set of real-valued functions and every function inequality \(B_i(\varvec{x})>0\) is an invariant of \(M\) in E and so do their conjunction. The property of a barrier tube BT is formally described in the following theorem.

Theorem 4

Given a semialgebraic system \(M\), a box E and an initial set \( X_0 \subseteq E\), let \(BT = \{B_i(\varvec{x}): i=1,\cdots ,m\}\) be a barrier tube of \(M\) and \(\varOmega = \{\varvec{x}\in \mathbb {R} ^n \mid \bigwedge B_i(\varvec{x})>0, B_i \in BT\}\), then \(Flow_{\varvec{f}}( X_0 ) \cap E \subseteq \varOmega \cap E\).

Remark 3

Theorem 4 states that an arbitrary barrier tube is able to form an over-approximation for the reach pipe in the box E. Compared to a single barrier certificate, multiple barrier certificates could over-approximate the flowpipe more precisely. However, since there is no constraint on unsafe sets in Definition 6, a barrier tube satisfying the definition could be very conservative. In order to obtain an accurate approximation for the flowpipe, we choose to create additional auxiliary constraints.

Auxiliary Unsafe Set (AUS). To obtain an accurate barrier tube, there are two main questions to be answered: (1) How many barrier certificates are needed? and (2) How do we control their positions to make the tube well-shaped to better over-approximate the flowpipe? The answer for the first question is quite simple: the more, the better. This will be explained later on. For the second question, the answer is to construct a group of properly distributed auxiliary state sets (AUSs). Each set of the AUSs is used as an unsafe set \(U_i\) for the system and then we compute a barrier certificate \(B_i\) for \(U_i\) according to Theorem 2. Since the zero level set of \(B_i\) serves as a barrier between the flowpipe and \(U_i\), the space where a barrier could appear is fully determined by the position of \(U_i\). Roughly speaking, when \(U_i\) is far away from the flowpipe, the space for a barrier to exist is wide as well. Correspondingly, the barrier certificate found would usually locate far away from the flowpipe as well. Certainly, as \(U_i\) gets closer to the flowpipe, the space for barrier certificates also contracts towards the flowpipe accordingly. Therefore, by expanding \(U_i\) towards the flowpipe, we can get more precise over-approximations for the flowpipe.

Why Multiple AUS? Although the accuracy of the barrier certificate over-approximation can be improved by expanding the AUS towards the flowpipe, the capability of a single barrier certificate is very limited because it can erect a barrier which only matches a single profile of the flow pipe. However, if we have a set U of AUSs which are distributed evenly around the flowpipe and there is a barrier certificate \(B_i\) for each \(U_i\in U\), these barrier certificates would be able to over-approximate the flowpipe from a number of profiles. Therefore, increasing the number of AUSs can increase the quality of the over-approximation as well. Furthermore, if all these auxiliary sets are connected, all the barriers would form a tube surrounding the flowpipe. Therefore, if we can create a series of boxes piecewise covering the flowpipe and then construct a barrier tube for every piece of the flowpipe, we obtain an over-approximation for the flowpipe by PBT.

Based on the above idea, we provide Algorithm 2 to compute barrier tube.

figure b

Remark 4

In Algorithm 2, for an n-dimensional flowpipe segment, we aim to build a barrier tube composed of \(2(n-1)\) barrier certificates, which means we need to construct \(2(n-1)\) \(\mathtt {AUS}\)s. According to Algorithm 1, we know that the plane \(\mathtt {P}\) is the only exit of the flowpipe from the enclosure \(\mathtt {E}\) and \(\mathtt {G}\) is roughly the region where they intersect. Let \(F^G\) be the facet of \(\mathtt {E}\) that contains \(\mathtt {G}\), then for every facet \(F_{ij}^G\) of \(F^G\), we can take an \((n-1)\)-dimensional rectangle between \(F_{ij}^G\) and \(G_{ij}\) as an \(\mathtt {AUS}\), where \(G_{ij}\) is the facet of G adjacent to \(F_G^{ij}\). Therefore, enumerating all the facets of G in line 1 would produce \(2(n-1)\) positions for \(\mathtt {AUS}\). The loop in line 3 is attempting to find a polynomial barrier certificate of different degrees in D. In the while loop 5, we iteratively compute the best barrier certificate by adjusting the width of \(\mathtt {AUS}\) through binary search until the difference in width between two successive \(\mathtt {AUS}\)s is less than the specified threshold \(\epsilon \).

Example 4

(Running example). Consider the initial set and the enclosure computed in Example 3, we use Algorithm 2 to compute a barrier tube. The initial set is \( X_0 = [1.0,1.0]\times [-1.05, -0.95]\) and the enclosure of \( X_0 \) is \(E = [0.84,1.01] \times [-1.1,-0.75]\), \(G = [0.84,0.84]\times [-0.91,-0.80]\), the plane P is \(x=0.84\), \(D = \{2\}\) and \(\epsilon = 0.001\). The barrier tube consists of two barrier certificates. As shown in Fig. 3, each of the barrier certificates is derived from an \(\mathtt {AUS}\) (red line segment) which is located respectively on the bottom-left and top-left boundary of E.

Fig. 3.
figure 3

Computing process of BT for Example 4. Blue line segment: initial set, red line segment: \(\mathtt {AUS}\). Figure a–l show how intermediate barrier certificates changed with the width of the \(\mathtt {AUS}\)s and Fig. l shows the final BT (shadow region in green). (Color figure online)

Full size image

4.3 Compute Piecewise Barrier Tube

During the computation of a barrier tube by Algorithm 2, we create a series of \(\mathtt {AUS}\)s around the flowpipe, which build up a rectangular enclosure for the intersection of the flowpipe and the facet of the enclosure box. As a result, such a rectangular enclosure can be taken as an initial set for the following flowpipe segment and then Algorithm 2 can be applied repeatedly to compute a PBT. The basic procedure to compute PBT is presented in Algorithm 3.

figure c

Remark 5

In Algorithm 3, initially a box that contains the initial set \(X_0\) is constructed using Algorithm 1. The loop in line 2 consists of 3 major parts: (1) In lines 3–6, a barrier tube BT is firstly computed using Algorithm 2. The while loop keeps shrinking the box until a barrier tube is found; (2) In line 8, the initial set \( X_0 \) is updated for the next box; (3) In line 9, a new box is constructed to contain \( X_0 \) and the process is repeated.

Example 5

(Running example). Let us consider again the running example. We set the length of PBT to 45 and the PBT we obtained is shown in Fig. 2b. Compared to the interval over-approximation of the Taylor model obtained using Flow*, the computed PBT consists of a significantly reduced number of segments and is more precise for the absence of stretching.

Safety Verification Based on PBT. The idea of safety verification based on PBT is straightforward. Given an unsafe set \( X_U \), for each intermediate initial set \( X_0 \) and the corresponding enclosure box E, we first check whether \( X_U \cap E = \emptyset \). If not empty, we would further find a barrier certificate between \( X_U \) and the flowpipe of \( X_0 \) inside E. If empty or barrier found, we continue to compute longer PBT. The refinement of PBT computation can be achieved by using smaller E and higher d for template polynomial.

5 Implementation and Experiments

We have implemented the proposed approach as a C++ prototype called Piecewise Barrier Tube Solver (PBTS), choosing Gurobi [12] as our internal linear programming solver. We have also performed some experiments on a benchmark of four nonlinear polynomial dynamical systems (described in Table 1) to compare the efficiency and the effectiveness of our approach w.r.t. other tools. Our experiments were performed on a desktop computer with a 3.6 GHz Intel Core i7-7700 8 Core CPU and 32 GB memory. The results are presented in Table 2.

Table 1. Model definitions
Full size table
Table 2. Tool Comparison on Nonlinear Systems. #var: number of variables; T: computing time; NFS: number of flowpipe segments; DEG: candidate degrees for template polynomial (only for PBTS); TH: time horizon for flowpipe (only for Flow* and CORA). FAIL: failed to terminate under 30 min.
Full size table

Remark 6

There are a number of outstanding tools for flowpipe computation  [1, 3,4,5]. Since our approach is to perform flowpipe computation for polynomial nonlinear systems, we pick two of the most relevant state-of-the-art tools for comparison: CORA [1] and Flow* [3]. Note that a big difference between our approach and the other two approaches is that PBTS is time-independent, which means that we cannot compare PBTS with CORA or Flow* over the exactly same time horizon. To be fair enough, for Flow* and CORA, we have used the same time horizon for the flowpipe computation, while we have computed a slightly longer flowpipe using PBTS. To guide the reader, we have also used different plotting colors to visualize the difference between the flowpipes obtained from the three different tools.

Evaluation. As pointed out in Sect. 1, a common problem with the bounded-time integration based approaches is that the flowpipe segment of a dynamics system can be extremely stretched with time so that the interval over-approximation of the flowpipe segment is very conservative and usually the solver has to stop prematurely due to the error explosion. This fact can be found easily from the figures Fig. 4, 5, 6 and 7. In particular, for Controller 2D, Flow* can give quite nice result in the beginning but started producing an exploding flowpipe very quickly (Note that Flow* offers options to produce better plotting which however is expensive and was not used for safety verification. CORA even failed to give a result after over 30 min of running). This phenomenon reappeared with both Flow* and CORA for Controller 3D. Notice that most of the time horizons used in the experiment are basically the time limits that Flow* and CORA can reach, i.e., a slightly larger value for the time horizon would cause the solvers to fail. In comparison, our tool has no such problem and can survive a much longer flowpipe before exploding or even without exploding as shown in Fig. 4a.

Fig. 4.
figure 4

Flowpipe for Controller 2D.

Full size image
Fig. 5.
figure 5

Flowpipe for Van der Pol Oscillator.

Full size image
Fig. 6.
figure 6

Flowpipe for Lotka-Volterra.

Full size image
Fig. 7.
figure 7

Flowpipe (projection) for Controller 3D.

Full size image

Another important factor of the approaches is the efficiency. As is shown in Table 2, our approach is more efficient on the first three examples but slower on the last example than the other two tools. The reason for this phenomenon is that the degree d of the template polynomial used in the last example is higher than the others and increasing d led to an increase in the number of decision variables in the linear constraint. This suggests that using smaller d on shorter flowpipe segment would be better. In addition, we can also see in Table 2 that the number of the flowpipe segments produced by PBTS is much fewer than that produced by Flow* and CORA. In this respect, PBTS would be more efficient on safety verification.

6 Conclusion

We have presented PBTS, a novel approach to over-approximate flowpipes of nonlinear systems with polynomial dynamics. The benefit of using BTs is that they are time-independent and hence cannot be stretched or deformed by time. Moreover, this approach only results in a small number of BTs which are sufficient to form a tight over-approximation for the flowpipe, hence the safety verification with PBT can be very efficient.