CAREER: Designing Robust Cyber-Physical Systems: Logics, Automata, Optimization, and Heuristic Methods

该项目的影响是在涉及汽车、医疗设备、航空电子、电网和自主代理等领域的更可靠、更安全、性能更好的下一代网络物理系统（CPS）的工程设计。由于这些系统在不能总是完美预测/建模的环境中运行，因此从设计阶段开始，将鲁棒性作为主要目标至关重要。该项目的新颖之处在于开发了可扩展且严格的形式化算法方法，以促进这种强大的CPS工程。这些方法推进了经典的离散算法技术，用于CPS操作的定量环境。该项目的研究方面与研究生和本科生课程的创建相辅相成，这些课程向即将进入劳动力市场的科学家和工程师教授核心逻辑和算法分析技能。对CPS进行算法分析的第一步是对系统的预期正确行为进行正式规范。信号时间逻辑（Signal Temporal Logic， STL）是度量时间逻辑（Metric Temporal Logic）的信号变体，是目前比较流行的一种区分CPS行为好坏的形式。不幸的是，STL不能指定许多工程师感兴趣的属性。该项目正在用其他时态操作符（如freeze操作符）对STL进行扩充，以便拥有更具表现力的规范形式化，解决STL的缺点。这种增强是由高效算法、启发式方法和工具的开发指导的，并且是与它们一起完成的，这样新的逻辑就可以在工业CPS环境中易于使用，例如，在测试生成中。为了找到易于处理的新CPS逻辑类，正在探索规范表达性增强与算法复杂性增加之间的权衡。同样重要的是，在空间和时间领域中，在这些新形式主义之上建立定量稳健性理论的项目推力。研究小组正在通过同行评议的会议和期刊出版物、会议演讲和研究访问广泛传播结果。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The project's impact is the engineering of more reliable, safer, and better performing next generation Cyber-Physical Systems (CPS) arising in domains involving automotive vehicles, medical devices, avionics, power grids, and autonomous agents. As these systems operate in environments that cannot always be perfectly anticipated/modeled, it is crucial that robustness be a prime objective right from the design phase. The project's novelty is the development of scalable and rigorous formal algorithmic approaches for facilitating such robust CPS engineering. These approaches advance classical discrete algorithmic techniques for use in quantitative environments in which CPS operates. The research aspect of the project is complemented with the creation of graduate and undergraduate courses teaching core logical and algorithmic analyses skills to scientists and engineers about to enter the workforce.The first step toward algorithmic analysis of CPS is a formal specification of the expected correct behaviors of the system. Signal Temporal Logic (STL), the signal variant of Metric Temporal Logic, is currently a popular formalism for classifying good/bad CPS behaviors. Unfortunately, STL cannot specify many properties of interest to engineers. The project is augmenting STL with other temporal operators, such as the freeze operator, in order to have more expressive specification formalisms, addressing the shortcomings of STL. This augmentation is guided by, and done in tandem with, the development of efficient algorithms, heuristic methods, and tools so that the new logics will be tractable to use in industrial CPS contexts, for instance, in test generation. The tradeoff between increased specification expressivity and resulting increased algorithm complexity is being explored to find tractable classes of new CPS logics. Of equal importance is the project thrust that builds a theory of quantitative robustness over these new formalisms, both in the space and in the time domain. Broad dissemination of results is being done by the research team through peer reviewed conference and journal publications, conference talks, and through research visits.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.