CSR: Small: Human-Centered Synthesis of Provably Correct Controllers for Hybrid Systems

混合系统是一种数学框架，已被广泛用于建模工程和自然系统，其动态具有连续和离散方面。应用范围从现代的“电传操纵”飞机到细胞生物学。用于混合动力系统的控制器观察系统的执行，并在混合动力系统中发出输入信号和/或触发事件，以便满足系统的目标和安全要求。 针对复杂混杂系统控制器综合方法存在计算量大的问题，本研究试图以一种新的方法解决混杂系统控制器设计的高计算量问题。该方法的新奇在于使用以人为中心的计算（众包），同时确保获得的控制器是正确的。该项目的预期成果是数学理论和算法，这将使上述想法适用于广泛的问题，包括涉及非线性系统和随机事件的问题。这些结果将进一步在模拟器计算机游戏中实现，这些游戏将在线部署。 可以通过众包潜在地收获的计算资源的量非常高。早期的众包应用程序，如reCAPTCHA、FoldIt和维基百科，已经记录了人类贡献者数十亿小时的努力。除了解决控制器综合问题，该项目的成果可以导致新的方法来利用这一资源来解决新的问题。该项目的更广泛的影响包括改善各种工程系统的安全性。 该项目还有一个教育推广计划，涉及K-12学生和教育工作者的前沿多学科研究。独特的是，游戏主题是一个理想的工具，从事大学预科学生在科学和工程。

Hybrid systems are a mathematical framework that has been widely used to model engineering and natural systems whose dynamics have both continuous and discrete aspects. Applications range from modern "fly-by-wire" airplanes to cellular biology. A controller for a hybrid system observes the execution of the system and issues input signals and/or trigger events in the hybrid system so as to meet the system's goals and safety requirements. An outstanding problem is that for complex hybrid systems existing methods for controller synthesis require exceedingly large computational resources.This project seeks to address the high computational demands of constructing controllers for hybrid systems in a new way. The novelty of the approach lies in using human-centered computing (crowdsourcing), while ensuring that the obtained controller is correct. The expected outcomes of this project are mathematical theory and algorithms that will enable the idea above for a wide range of problems, including those involving nonlinear systems and random events. These results are further implemented in simulator computer games, which will be deployed online. The amount of computing resource that can be potentially be harvested through crowdsourcing is very high. Earlier crowdsourcing applications such as reCAPTCHA, FoldIt, and Wikipedia have recorded billions of hours of effort by their human contributors. Beyond solving the controller synthesis problem, the outcomes of this project can lead to new ways to tap into this resource for solving new problems.The broader impacts of this project include improvements in the safety of a wide range of engineered systems. The project also has an educational outreach program involving K-12 students and educators in cutting edge multidisciplinary research. Uniquely, the gaming theme is an ideal vehicle to engage pre-college students in science and engineering.