Model checking

Formal verification

Automation

Reachability

Distributed computing

Curse of dimensionality

Software engineering

Engineering

Artificial intelligence

Systems engineering

SAFER

Computer science

Theoretical computer science

Computer security

Formal methods

Mechanical engineering

Annual Review of Control Robotics and Autonomous Systems

Autonomous systems are becoming pervasive in everyday life, and many of these systems are complex and safety-critical. Formal verification is important for providing performance and safety guarantees for these systems. In particular, Hamilton–Jacobi (HJ) reachability is a formal verification tool for nonlinear and hybrid systems; however, it is computationally intractable for analyzing complex systems, and computational burden is in general a difficult challenge in formal verification. In this review, we begin by briefly presenting background on reachability analysis with an emphasis on the HJ formulation. We then present recent work showing how high-dimensional reachability verification can be made more tractable by focusing on two areas of development: system decomposition for general nonlinear systems, and traffic protocols for unmanned airspace management. By tackling the curse of dimensionality, tractable verification of practical systems is becoming a reality, paving the way for more pervasive and safer automation.

Hamilton–Jacobi Reachability: Some Recent Theoretical Advances and Applications in Unmanned Airspace Management