What Is Reachability Analysis?

Reachability analysis is a formal method for computing the set of all states that a dynamical system can occupy over a given time horizon, starting from a specified set of initial conditions and subject to a defined set of inputs or disturbances. By characterizing this reachable set, engineers and researchers can determine whether a system will ever enter a region of state space designated as unsafe, thereby providing a mathematically rigorous basis for safety certification. The technique applies to continuous systems governed by differential equations, discrete systems described by difference equations, and hybrid systems that combine both continuous dynamics and discrete mode switching.

Reachability analysis draws on control theory, formal methods in computer science, and computational geometry. It became increasingly practical as computational tools and set-representation methods improved through the 1990s and 2000s, and now underpins safety verification workflows for automotive, aerospace, robotics, and power systems applications.

Set-Based Reachability Computation

The core computational challenge in reachability analysis is representing and propagating a set of states through system dynamics, rather than simulating individual trajectories from individual initial conditions. Several geometric data structures have been developed to make this tractable. Polytopes represent reachable sets exactly for linear systems but grow in complexity as the number of faces increases with time steps. Zonotopes, a subclass of polytopes defined by a center point and a set of generator vectors, offer efficient computation because they are closed under linear transformations and Minkowski sums, which correspond directly to the operations needed to propagate state sets under linear dynamics and add disturbance sets. Hybrid zonotope methods extend these representations to hybrid systems, encoding the union of many convex reachable sets arising from different discrete modes within a single compact structure. Ellipsoidal and support-function approaches provide alternatives that scale better to high-dimensional systems at the cost of some tightness in the enclosure.

Safety Verification and Hybrid Systems

The primary application of reachability analysis is safety verification: confirming that the reachable set does not intersect with an unsafe region. For hybrid systems, which combine continuous differential equations with discrete guard conditions and mode transitions, reachability analysis must track how the state set evolves within each continuous mode and how it maps across guard surfaces when a transition fires. This coupling of continuous and discrete behavior makes the problem significantly harder than pure continuous or discrete verification, and the reachable set can become non-convex even when individual mode dynamics are linear. Safety verification for neural network-controlled systems, such as autonomous vehicles, requires computing the reachable set of the closed-loop system formed by the nonlinear neural network controller and the physical plant. Reachability analysis and safety verification for neural network control systems develops linear programming-based methods for estimating the output range of feedforward networks and combining these estimates with plant dynamics to bound the closed-loop reachable set.

Computational Scalability and Tools

A persistent challenge in reachability analysis is the curse of dimensionality: the complexity of representing and computing reachable sets grows rapidly with the number of state variables, making exact analysis of large systems infeasible. Approximate methods address this by computing outer approximations, enclosures guaranteed to contain the true reachable set, at the cost of conservatism. Hamilton-Jacobi reachability approaches solve a partial differential equation whose zero-sublevel set characterizes the reachable tube; this method handles general nonlinear systems but faces exponential grid-size growth with dimension. High-dimensional reachability analysis methods developed at UC Berkeley address this limitation by decomposing large systems into coupled low-dimensional subsystems. Software tools such as CORA, SpaceEx, and Flow* automate the application of these algorithms to user-specified system models.

Applications

Reachability analysis has applications in a wide range of disciplines, including:

• Autonomous vehicle safety certification, verifying that planned trajectories remain collision-free under uncertainty
• Air traffic management, ensuring aircraft maintain mandated separation under wind disturbances
• Power system stability analysis, confirming that generator states remain within acceptable operating bounds after faults
• Robotic motion planning, computing configuration-space regions reachable from a given state
• Biomedical device verification, certifying that closed-loop drug delivery systems stay within therapeutic bounds