Automatic Dynamic Parallelotope Bundles for Reachability Analysis of Nonlinear Systems.

Reachable set computation is an important technique for the verification of safety properties of dynamical systems. In this paper, we investigate parallelotope bundle based reachable set computation for discrete nonlinear systems. The algorithm relies on computing an upper bound on the supremum of a nonlinear function over a rectangular domain, traditionally done using Bernstein polynomials. We strive to remove the manual step of parallelotope template selection to make the method fully automatic. Further, we show that changing templates dynamically during computations can improve accuracy. We investigate two techniques for generating the template directions. The first technique approximates the dynamics as a linear transformation and generates templates using this linear transformation. The second technique uses Principle Component Analysis (PCA) of sample trajectories for generating templates. We have implemented our approach in a Python based tool called Kaa and improve its performance by two main enhancements. The tool is modular and use two types of global optimization solvers, the first using Bernstein polynomials and the second using NASA's Kodiak nonlinear optimization library. Second, we leverage the natural parallelism of the reachability algorithm and parallelize the Kaa implementation. We demonstrate the improved accuracy of our approach on several standard nonlinear benchmark systems.