Set Propagation Techniques for Reachability Analysis

TLDR

Reachability analysis computes the set of states reachable from all initial states and admissible inputs, and is fundamental for formal verification, controller synthesis, and estimation. The article aims to develop set propagation methods that compute guaranteed overapproximations of reachable sets for continuous and hybrid systems. It reviews set representations and computational techniques, then surveys state‑of‑the‑art set propagation methods for linear, nonlinear, and hybrid systems. The article concludes with examples of successful real‑world applications of reachability analysis.

Abstract

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 article focuses on a class of methods for computing a guaranteed overapproximation 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 of set representation and computation, the article presents the state of the art of set propagation techniques for reachability analysis of linear, nonlinear, and hybrid systems. It ends with a discussion of successful applications of reachability analysis to real-world problems.