"Nonlinear Algorithms for Verification, Control, Design and Analysis of Nonlinear Continuous and Hybrid Systems"

我建议开发数值算法和实现，用于验证、控制和设计系统，这些系统的动力学最好用非线性连续或混合（连续和离散的混合）模型来描述。每当数字计算机与外部世界交互时，这种系统就会出现，随着计算机嵌入到我们周围环境中的设备中，它们也因此变得越来越普遍。本研究计划的基础将是研究连续系统的各种可达性算法，包括基于参数和非参数可达集表示的网格和轨迹。这些技术的应用可以减少不良行为的可能性，但对于非线性连续和混合系统，这很少是可能的，或者需要可达性专家的干预。为了将这些形式化分析方法引入工业实践，两个不同的应用领域将为这个研究项目提供信息：机器人的安全协同控制，以及鲁棒模拟和混合信号集成电路的设计。为了在没有形式化方法专家干预的情况下解决实际问题，该程序还将解决另外两个关键需求：基于领域专家通常使用的描述构建系统和待解决问题的数学模型，并将验证结果转换为解决这些专家关注的形式。对于特定领域的工具链，必要时，对于核心可达性算法，我将创建并发布灵活、高效、健壮且文档完备的实现，这些实现将为这些技术做水平集方法工具箱为时间相关的汉密尔顿-雅可比方程所做的事情：允许工业界和学术界的其他研究人员复制、利用和扩展已发表的结果。学员将获得数值算法、强大的软件开发实践、集成电路和/或机器人技术方面的经验，这些领域都有积极的就业前景。最后，选择不同的应用领域将引导自动化形式化分析扩展到显示连续和混合动态的其他领域。

I propose to develop numerical algorithms and implementations for the verification, control and design of systems whose dynamics are best described by nonlinear continuous or hybrid (a mixture of continuous and discrete) models. Such systems arise whenever a digital computer interacts with the external world, and they are hence becoming ever more widespread as computers are embedded into devices throughout our environment. The foundation of this research program will be the study of a variety of reachability algorithms for continuous systems, including both grid and trajectory based with both parametric and nonparametric reach set representations. Application of these techniques can reduce the likelihood of undesirable behaviours, but for nonlinear continuous and hybrid systems it has rarely been possible or it has required the intervention of reachability experts. With the long-term goal of bringing these formal analysis methods into industrial practice, two distinct application domains will inform this program of research: safe collaborative control of robots, and design of robust analog and mixed-signal integrated circuits. In order to solve real problems without the intervention of experts in formal methods, this program will also address two other key needs: construction of the mathematical model of the system and problem to be solved based on descriptions typically used by domain experts, and conversion of the verification results into a form which addresses those experts' concerns. For the domain specific toolchains and, where necessary, for the core reachability algorithms I will create and release flexible, efficient, robust and well-documented implementations that will do for these techniques what the Toolbox of Level Set Methods has done for time-dependent Hamilton-Jacobi equations: permit other researchers in industry and academia to reproduce, utilize and extend published results. Trainees will gain experience in numerical algorithms, robust software development practices, integrated circuits and/or robotics, all areas with positive job prospects. Finally, the choice of distinct application areas will guide the extension of automated formal analysis into other domains exhibiting continuous and hybrid dynamics.