Author(s):

Kong, Hui; Bartocci, Ezio; Henzinger, Thomas A

Title: 
Reachable set overapproximation for nonlinear systems using piecewise barrier tubes

Title Series: 
LNCS

Affiliation 
IST Austria 
Abstract: 
We address the problem of analyzing the reachable set of a polynomial nonlinear continuous system by overapproximating the flowpipe of its dynamics. The common 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 flowpipe. The basic idea of PBT is that for each segment of a flowpipe, 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 flowpipe. The benefit of using PBT is that (1) BT is independent of time and hence can avoid being stretched and deformed by time; and (2) a small number of BTs can form a tight overapproximation for the flowpipe, which means that the computation required to decide whether the BTs intersect the unsafe set can be reduced significantly. We implemented a prototype called PBTS in C++. Experiments on some benchmark systems show that our approach is effective.

Keywords: 
Linear Programming; Computation theory; Computer aided analysis; Computer circuits; C++ (programming language); Barrier functions; Benchmark system; Continuous system; Interval arithmetic; Numerical integrations; Reachable set; Taylor expansions; Time horizons

Conference Title:

CAV: Computer Aided Verification

Volume: 
10981

Conference Dates:

14  17 July, 2018

Conference Location:

Oxford, UK

ISBN:

03029743 (ISSN); 9783319961446 (ISBN)

Publisher:

Springer

Date Published:

20180718

Start Page: 
449

End Page:

467

Copyright Statement: 
CC BY 4.0

Sponsor: 
Austrian Science Fund FWF: S11402N23, S11405N23, Z211N32

DOI: 
10.1007/9783319961453_24

Open access: 
yes (OA journal) 