Thursday, September 28, 2017
Speaker: Goran Frehse
Venue: IST Austria
Reachability analysis is a useful tool for checking whether a cyber-physical system satisfies a given safety property. For instance, one could ask whether an electro-magnetic braking system brings a car to a standstill within a given time frame. In set-based reachability, one takes a given set of initial states (ranges for the position and speed of the car) and computes the image of the set of states as it evolves over time. Even for simple types of systems, this so-called reach set can only be computed approximately, and accuracy comes at an extremely steep cost. A highly scalable way to approximate the reach set is known for the special case of linear dynamics. It is based on template polyhedra, which are polyhedra (sets bounded by linear constraints) with normal vectors from a given finite set. Simple instances of template polyhedra are boxes or octagons. A template instance that tightly bounds the reach set is found by solving a set of optimization problems. The accuracy of the approximation can be improved by adding more normal vectors to the template.
In this talk, we propose an approach that extends this idea from linear to nonlinear dynamics. We linearize the system around a reference trajectory and solve ODEs to obtain templates that bound the reach set. The ODEs are particular in that they involve an optimization problem constrained by the template itself. We show how, similarly to the linear case, the template can be adapted over time to match the dynamics of the system. For both static and dynamic templates, we identify conditions that guarantee convergence. The potential of the approach is discussed on several benchmarks.