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

“用于非线性连续和混合系统验证、控制、设计和分析的非线性算法”

• 批准号: 298211-2012
• 负责人: Mitchell, Ian
• 金额: $ 1.6万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2014
• 资助国家: 加拿大
• 起止时间: 2014-01-01 至 2015-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=548263
• 关键词: Nonlinear; Algorithms; Verification; Control; Design

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.

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