FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes

Authors: Hui Kong, Ezio Bartocci and Tom Henzinger

Paper Information

Title:Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes
Authors:Hui Kong, Ezio Bartocci and Tom Henzinger
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Reachability analysis of nonlinear systems, Reachable set over-approximation, Barrier Certificates
Abstract:

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.

Pages:19
Talk:Jul 15 11:00 (Session 103A: Runtime Verification, Hybrid and Timed Systems)
Paper: