CSR-EHCS(EHS), SM: A formal approach to control of hybrid systems with applications to mobile robotics

在正式验证中，计算机程序或数字电路的有限模型要根据时间逻辑属性进行检查，比如安全性（坏事永远不会发生）和活跃性（好事最终会发生）。虽然形式验证受到了很多关注，但形式综合的双重问题，其重点是构建一个可证明正确的系统（例如，通过设计安全）仍然处于起步阶段。此外，大多数系统，如无人驾驶车辆模型，都是混合的，将车辆动力学的连续模型与嵌入式控制器和通信协议建模的有限状态自动机相结合。该项目开发了理论框架和计算工具，用于综合混合系统和分布式混合系统的可证明正确的控制和通信策略，这些策略来自丰富的类人语言规范。在这个项目中，方法的核心是抽象的概念，它用于构建控制系统的有限描述。这样的抽象允许使用（改编的）时态逻辑作为规范语言，使用来自形式验证和时态逻辑游戏的工具来进行分析和控制，以及使用受并发理论中的同步启发的技术来综合通信策略。本项目开发的计算工具以用户友好的软件包形式实现，并在微型移动机器人实验平台上进行了测试。这项研究与一个全面的教育和推广计划紧密结合，其中包括本科生和研究生课程，本科生和高中生参与研究，以及PI作为高中机器人竞赛的评委和组织者参与。

In formal verification, finite models of computer programs or digital circuits are checked against temporal logic properties such as safety (something bad never happens) and liveness (something good eventually happens). While formal verification received a lot of attention, the dual problem of formal synthesis, where the focus is to construct a provably correct system (e.g., safe by design) is still in its infancy. In addition, most systems, such as models of unmanned vehicles, are hybrid, combining continuous models of vehicle dynamics with finite state automata that model embedded controllers and communication protocols.This project develops theoretical frameworks and computational tools for synthesis of provably-correct control and communication strategies for hybrid systems and distributed hybrid systems from specifications given in rich, human-like language. Central to the approach in this project is the notion of abstraction, which is used to construct finite descriptions of control systems. Such abstractions allow for the use of (adapted) temporal logics as specification languages, tools from formal verification and temporal logic games for analysis and control, and techniques inspired from synchronization in concurrency theory for synthesis of communication strategies.The computational tools developed in this project are implemented as user-friendly software packages and tested in a miniature mobile robotics experimental platform. This research is closely integrated with a comprehensive educational and outreach plan, which includes undergraduate and graduate classes, involvement of undergraduate and high school students in research, and the participation of the PI as a judge and organizer in high school robotics competitions.