Set Propagation Techniques for Reachability Analysis

Overview & Synopsis

Reachability analysis consists in computing the set of states that are reachable by a dynamical system from all initial states and for all admissible inputs and parameters. It is a fundamental problem motivated by many applications in formal verification, controller synthesis, and estimation, to name only a few. This paper focuses on a class of methods for computing a guaranteed over-approximation of the reachable set of continuous and hybrid systems, relying predominantly on set propagation: starting from the set of initial states, these techniques iteratively propagate a sequence of sets according to the system dynamics. After a review on set representation and computation, the paper presents the state of the art on set propagation techniques for reachability analysis of linear, nonlinear, and hybrid systems. The paper ends with a discussion on successful applications of reachability analysis to real world-problems. Contents