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
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.