Reachable set over-approximation for nonlinear systems using piecewise barrier tubes Conference Paper

Author(s): Kong, Hui; Bartocci, Ezio; Henzinger, Thomas A
Title: Reachable set over-approximation 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 over-approximating 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 over-approximate 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 over-approximation 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: 2018-07-18
Start Page: 449
End Page: 467
Copyright Statement: CC BY 4.0
Sponsor: Austrian Science Fund FWF: S11402-N23, S11405-N23, Z211-N32
DOI: 10.1007/978-3-319-96145-3_24
Open access: yes (OA journal)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Hui Kong
    9 Kong
Related IST Austria Work