Tags:Barrier Certificates, Reachability analysis of nonlinear systems and Reachable set over-approximation
Abstract:
We address the problem of analysing the reachable set of a nonlinear continuous system by computing or approximating the flow pipe of its dynamics. The most widely employed approach to tackle this problem is to perform a numerical integration over a given time horizon based on Taylor expansion and interval arithmetic. However, this method results to be very conservative when there is a large difference in speed between trajectories as time progresses. In this paper, we propose to use combinations of barrier functions, which we call piecewise barrier tube (PBT), to overapproximate flow pipe. The basic idea of PBT is that for each segment of a flow pipe, a coarse box which is big enough to contain the segment is constructed using sampled simulation and then in the box we compute by linear programming a set of barrier functions (called barrier tube or BT for short) which work together to form a tube surrounding the flow pipe. The benefit of using PBT is that (1) is independent of time and hence can avoid being stretched and deformed by time (2) a small number of BTs can form a tight overapproximation for the flow pipe, which means that the computation required to decide whether the BTs intersect the unsafe set can be reduced significantly. We implemented a prototype tool called PBTS in C++. Experiment on some benchmark systems show that our approach is effective.
Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes