Sound, Automated, and scalable, Synthesis of Digital Controllers for Physical Systems

简要描述研究背景，包括潜在影响：验证和控制之间的联系为基于SAT/SMT理论的合成CPS的符号方法和自动化技术的发展奠定了基础。该项目将采用强大的技术，从有界模型检查和归纳综合（CEGIS和SyGuS），以自动设计合理的数字控制器的物理工厂（1,2）。该方法允许设计和综合现代控制体系结构，在数字设备（如fpga）上实现，使用正确的自动程序。对于与物理工厂使用数字架构相关的完整近似范围，包括：时间离散化，量化和饱和效应，以及带舍入误差的有限精度算法，合成是合理的。目的和目标：该项目的最终目标是为开发一种新的、自动化的、健全的和可扩展的框架做出贡献，改善工业相关的数字控制系统的最新成果。研究方法的新颖性：最近(3)采用了CEGIS体系结构来自动和健全地合成控制系统的李雅普诺夫控制函数，成功地使用神经网络作为李雅普诺夫函数的模板。这个项目试图将这项工作扩展到物理系统的综合控制器。与EPSRC的战略和研究领域保持一致：该项目将与EPSRC在验证、正确性和控制工程方面的研究领域保持一致。(1) A. Abate， I. Bessa， D. Cattaruzza， L. Cordeiro， C. David， P. Kesseli， D. Kroening， E. Polgreen，状态空间物理对象的自动形式综合，vol . 17, vol . 26, pp 462-482, 2017。(2) A. Abate， I. Bessa， D. Cattaruzza， L. Cordeiro， C. David， P. Kesseli， D. Kroening， E. Polgreen，连续装置可证明安全数字控制器的自动形式合成，信息学报，出版，2020。(3)刘建平，李亚鹏，李亚鹏，李亚鹏，李亚鹏，李亚鹏，李亚鹏，李亚鹏，李亚鹏，李亚鹏，李亚鹏。

Brief description of the context of the research including potential impact: Connections between verification and control underpin work on the development of symbolic methods and automated techniques based on SAT/SMT theory for the synthesis of CPS.This project will employ powerful techniques from bounded model checking and inductive synthesis (CEGIS and SyGuS) to automatically design sound digital controllers for physical plants (1,2). The approach allows for the design and synthesis of modern control architectures, implemented over digital devices such as FPGAs using automatic procedures that are correct by construction. The synthesis is sound with respect to the complete range of approximates related to utilising digital architectures for physical plants including: time discretisation, quantisation and saturation effects, and finite-precision arithmetics with rounding errors.Aims and Objectives: The end-goal of this project is to contribute towards the development of a new, automated, sound and scalable framework, improving industrially relevant state-of-the-art results in digital control systems. Novelty of the Research Method: Recently (3) has employed the CEGIS architecture to automatically and soundly synthesise Lyapunov control functions for control systems, successfully using neural networks as templates for Lyapunov functions. This project seeks to extend this work to synthesisng controllers of physical systems. Alignment to EPSRC's strategies and research areas: This project will be in line with EPSRC's research areas in Verification and correctness and control engineering.(1) A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening and E. Polgreen, Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants, CAV17, LNCS 10426, pp 462-482, 2017.(2) A. Abate, I. Bessa, D. Cattaruzza, L. Cordeiro, C. David, P. Kesseli, D. Kroening and E. Polgreen, Automated Formal Synthesis of Provably Safe Digital Controllers for Continuous Plants, Acta Informatica, In Press, 2020.(3) D. Ahmed, A. Peruffo and A. Abate, Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers, TACAS20, To Appear, 2020.