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