SHF: EAGER: Closing the gap in Controller Synthesis

自动控制器综合算法有望产生按结构更正的系统，从而消除了昂贵的事后验证的需要。然而，目前控制器综合的理论基础与其在硬件和软件平台上的实际实现之间存在着差距。该项目解决了缩小控制合成方面的差距的挑战。特别是，我们考虑了两个基本问题。首先，我们考虑了控制器实现的复杂性问题。虽然理论结果主要集中在控制器的最优存储要求上，但在实践中，控制器实现可能具有其他几个最优要求，例如实现(组合和顺序)电路的大小、计算控制动作的复杂性和频率以及感测和执行带宽。相应地，我们研究了在这些度量下构造最优控制器的算法。其次，我们考虑了控制器中的容错问题，其中我们考虑了控制器实现中的(可能是随机的)误差的影响。虽然纠错码和冗余等传统容错技术可以直接应用，但我们的论文认为，容错和控制器综合算法的更紧密结合可以以比传统技术更低的成本实现容错设计。例如，通过区分信号对控制目标的“重要性”，可以降低与纠错和冗余相关的成本，同时对控制目标的影响可以忽略不计。在这个项目中进行的研究是更广泛地采用按构造更正技术的先决条件。在这个项目中开发的工具和技术有可能显著增强我们生产健壮的计算机物理系统的能力，从而影响到计算机科学和控制工程领域以外的几个大型应用领域。实践证明，研究结果将为控制器综合提供更好的工具。从理论上讲，这项研究将汇集交叉技术，从逻辑和控制算法的理论基础，到优化技术、实时系统和硬件和软件综合。此外，通过促进软件基础、控制基础和硬件综合基础之间的合作，该项目将在网络物理系统的形式技术这一新兴而重要的领域培训研究生和本科生。

Automatic controller synthesis algorithms hold the promise of producing correct-by-construction systems, obviating the need for costly post facto verification. However, there is currently a gap between theoretical foundations of controller synthesis and their practical implementations on hardware and software platforms. This project addresses challenges in closing the gap in control synthesis. In particular, we consider two fundamental problems. First, we consider the problem of implementation complexity of controllers. While theoretical results have focused on the optimal memory requirements for controllers, in practice, a controller implementation may have several other optimality requirements such as the size of the implementing (combinational and sequential) circuit, the complexity and frequency of computing the control action, and the sensing and actuation bandwidth. Accordingly, we study algorithms for the construction of optimal controllers under these metrics. Second, we consider the problem of fault tolerance in controllers, in which we consider effects of (possibly stochastic) errors in controller implementations. While traditional fault tolerance techniques such as error-correcting codes and redundancy can be applied directly, our thesis is that a closer interaction of fault tolerance with controller synthesis algorithms can lead to fault tolerant designs at costs lower than traditional techniques. For example, by distinguishing the "importance" of signals to the control objective, the costs associated with error-correction and redundancy can be decreased while having a negligible effect on the control objective. The research performed in this project is prerequisite for a more widespread adoption of correct-by-construction techniques.The tools and techniques developed in this project have the potential to significantly enhance our ability to produce robust cyber-physical systems, thus affecting several large-scale application areas beyond the computer science and control engineering domains. Practically, the results of the research will lead to better controller synthesis tools. Theoretically, the research will bring together cross-cutting techniques, ranging from theoretical foundations in logics and algorithms for control, to optimization techniques, real-time systems, and hardware and software synthesis. In addition, by fostering collaboration between software foundations, control foundations, and hardware synthesis foundations, the project will train graduate and undergraduate students in the emerging and important domain of formal techniques for cyber-physical systems.