CAREER: Analysis and Synthesis of Systems over Finite Alphabets: Theoretical Foundations, Analytical Methods and Algorithmic Tools

摘要：从高科技汽车到智能基础设施，由硬件与控制和计算单元交互组成的网络物理系统无处不在。模拟动力学和离散动力学之间的紧密相互作用导致了复杂的验证和综合问题。为这些系统综合设计正确的控制器仍然是一个艰巨的挑战。该提案提出了一个雄心勃勃的研究议程，致力于从根本和整体上解决这一挑战。具体地说，我们建议开发一个统一的框架，围绕使用有限状态自动机作为物理和计算过程的名义模型。智力价值：拟议的研究解决了控制理论、计算机科学和数学之间的基本问题，潜在地导致了变革性的突破。预期的理论贡献包括理解使用有限记忆模型来近似无限记忆系统的基本限制，以及开发用于建立先验和后验误差界限的分析方法。预期的算法贡献包括开发用于构建近似模型的高效递归方案以及用于解决特定组合优化问题的高效技术。最后，希望通过理论和算法开发的结合使用，最终克服普遍存在的可伸缩性问题。广泛的影响：拟议的研究项目将产生一种计算机辅助方法，用于以可验证的正确方式系统地综合网络物理系统，自由分布的软件工具箱集合，以及一组精心设计的基准问题，可用于评估和指导进一步的研究进展。这项拟议的研究将推动本科控制教育的新课程的开发，使用有限状态自动机作为引入先进控制概念的工具。研究成果将被纳入关于混合系统的新的研究生水平课程和手稿的开发中。

Abstract:Cyber-physical systems comprising hardware interacting with control and computational units are omnipresent in our lives from high-tech cars to smart infrastructure. The tight interaction between analog and discrete dynamics gives rise to complex verification and synthesis problems. The challenge of synthesizing correct-by-design controllers for these systems remains daunting. This proposal presents an ambitious research agenda dedicated to fundamentally and holistically addressing this challenge. Specifically, we propose to develop a unifying framework built around the use of finite state automata as nominal models of both physical and computing processes. Intellectual Merit:The proposed research addresses fundamental problems at the interface of control theory, computer science and mathematics, potentially leading to transformative breakthroughs. Anticipated theoretical contributions include understanding the fundamental limitations of using finite memory models to approximate infinite memory systems, and developing analytical methods for establishing both a priori and a posteriori error bounds. Anticipated algorithmic contributions include developing efficient recursive schemes for constructing the approximate models as well as efficient techniques for solving specific combinatorial optimization problems. Finally, it is the hope that the ubiquitous problem of scalability can be finally overcome through the combined use of theoretical and algorithmic developments.Broader Impacts:The proposed research project would result in a computer-aided approach for systematically synthesizing cyber-physical systems in a verifiably correct manner, a freely distributed collection of software toolboxes, and a carefully crafted set of benchmark problems that can be used to evaluate and guide further research progress. The proposed research will drive the development of a new curriculum for undergraduate control education employing finite state automata as vehicles for introducing advanced control concepts. The research results will be incorporated in the development of a new graduate level course and manuscript on hybrid systems.