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.