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

对研究背景的简要描述，包括潜在的影响：验证和控制之间的联系是开发基于SAT/SMT理论的CP合成的符号方法和自动化技术的基础工作。该项目将利用来自有界模型检查和归纳综合(CEGIS和SyGuS)的强大技术，为物理工厂自动设计声音数字控制器(1，2)。该方法允许设计和综合现代控制体系结构，这些体系结构在数字器件(如FPGA)上实现，使用的是通过构造正确的自动程序。综合考虑到与利用物理工厂的数字架构相关的全部近似，包括：时间离散化、量化和饱和效应，以及具有舍入误差的有限精度算术。目的和目标：本项目的最终目标是促进新的、自动化的、健全的和可扩展的框架的开发，改善数字控制系统中与工业相关的最先进的结果。研究方法的新颖性：最近，(3)利用CEGIS体系结构自动和合理地综合控制系统的Lyapunov控制函数，成功地使用神经网络作为Lyapunov函数的模板。该项目旨在将这项工作扩展到物理系统的综合控制器。与EPSRC的战略和研究领域保持一致：本项目将与EPSRC在验证和正确性以及控制工程方面的研究领域保持一致。(1)A.Abate，I.Bessa，D.Cattaruzza，L.Cordeiro，C.David，P.Kesseli，D.Kroning和E.Polgreen，状态空间物理工厂数字控制器的自动化形式综合，CAV17，LNCS 10426，第462-482页，2017年。(2)A.Abate，I.Bessa，D.Cattaruzza，L.Cordeiro，C.David，P.Kesseli，D.Kroning和E.Polgreen，《连续工厂可证明安全的数字控制器的自动化形式综合》，《信息学报》，出版社，2020年。(3)D.Ahmed，A.Peruffo和A.Abate，《用SMT解算器自动和合理地合成Lyapunov函数》，TACAS20，将于2020年出版。

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.