Dissertation Talk: High Dimensional Reachability Analysis: Addressing the Curse of Dimensionality in Formal Verification

Seminar | May 5 | 10-11 a.m. | 405 Soda Hall

 Mo Chen, UC Berkeley EECS

 Electrical Engineering and Computer Sciences (EECS)

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. Computational burden is in general a difficult challenge in formal verification.

In this seminar, we show that high-dimensional verification can be made more tractable by imposing traffic protocols in multi-agent systems and decomposing complex systems into subsystems. These recent advances are demonstrated through unmanned airspace management experiments with NASA, high-dimensional HJ reachability theory, and modular combination of reachability with fast path or trajectory planners. By tackling the curse of dimensionality, tractable verification of practical systems is becoming a reality, paving the way towards more pervasive and safer automation.