High Dimensional Reachability Analysis: Addressing the Curse of Dimensionality in Formal Verification
High Dimensional Reachability Analysis: Addressing the Curse of Dimensionality in Formal Verification
复制标题
高维可达性分析：解决形式验证中的维数灾难
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Mo Chen
中科院分区：
文献类型：
--
作者：
Mo Chen
作者：Chen，Mo|顾问：Tomlin，Claire J|摘要：自动化在日常生活中变得越来越普遍，许多自动化系统，如无人驾驶航空系统，自动汽车和许多类型的机器人，都是复杂和安全关键的。正式的验证工具对于为这些系统提供性能和安全保证至关重要。特别是，可达性分析以前已成功地应用于小规模控制系统的一般非线性动态的影响下的干扰。然而，其指数级的计算复杂性使得分析更复杂的大规模系统变得棘手。减轻计算负担是形式化验证面临的主要挑战，本文从多个方面提出了解决这种“维数灾难”的方法，使复杂实用系统（如无人机系统、自动汽车和机器人以及生物系统）的易处理验证更接近现实。理论上的贡献属于哈密尔顿-雅可比（HJ）的可达性分析，与无人机系统的应用。此外，本文还探索了HJ可达性的两个前沿，通过结合可达性的形式保证与优化和机器学习的计算优势，并与机器人技术中常用的快速运动规划算法。理论进步的潜力和好处在许多实际应用中得到了证明。
Author(s): Chen, Mo | Advisor(s): Tomlin, Claire J | Abstract: Automation is becoming pervasive in everyday life, and many automated systems, such as unmanned aerial systems, autonomous cars, and many types of robots, are complex and safety-critical. Formal verification tools are essential for providing performance and safety guarantees for these systems. In particular, reachability analysis has previously been successfully applied to small scale control systems with general nonlinear dynamics under the influence of disturbances. Its exponentially scaling computational complexity, however, makes analyzing more complex, large scale systems intractable. Alleviating computation burden is in general a primary challenge in formal verification.This thesis presents ways to tackle this "curse of dimensionality" from multiple fronts, bringing tractable verification of complex, practical systems such as unmanned aerial systems, autonomous cars and robots, and biological systems closer to reality. The theoretical contributions pertain to Hamilton-Jacobi (HJ) reachability analysis, with applications to unmanned aerial system. In addition, this thesis also explores two frontiers of HJ reachability by combining the formal guarantees of reachability with the computational advantages of optimization and machine learning, and with fast motion planning algorithms commonly used in robotics. The potential and benefits of the theoretical advances are demonstrated in numerous practical applications.