CPS: Synergy: Collaborative Research: Autonomy Protocols: From Human Behavioral Modeling to Correct-By-Construction, Scalable Control

在运输系统、化工厂和医疗设备等环境中，安全性和正确性至关重要，计算机系统越来越多地依赖于增强或取代人类操作员来控制机械设备。一个核心问题是如何验证这种部分自动化或完全自主的网络物理系统（CPS）是否值得我们信任。一种有希望的方法是通过软件工具从正式规范中合成计算机实现代码。该项目基于对人类行为模型的洞察，通过开发可扩展的、自动化的方法来合成具有可证明的正确性保证的控制协议，从而促进了这种“按构造进行更正”的方法。它的目标是：(i)当今几乎不自主、无人系统的能力与它们对我们使用金钱、劳动力和时间资源产生影响的能力水平之间的差距；以及（ii）缺乏适用于此类自主系统的规范、合成和验证的可计算、自动化、可扩展的工具。这项研究是基于模块化强化学习的人类行为模型的研究，这些模型是通过实验得出的，旨在得出人类如何在动态环境中控制复杂的交互系统的信息，包括汽车驾驶。本研究的架构见解和随机模型与基于线性时间逻辑的规范语言相结合，以指导自适应自主控制器的综合。运动规划和其他动态决策是通过基于计算引擎的算法来实现的，这些计算引擎代表了底层物理，并提供了运行时的适应性，以适应不断变化的操作和环境条件。在城市环境中的自动驾驶和动态环境中微型飞行器的多车辆自主导航的虚拟测试设施中，通过实验验证了实现该方法的工具。教育和推广活动包括让本科生和研究生参与研究，将研究纳入课程，为K-12学生进行示范，从代表性不足的人口群体中招募研究参与者。该项目开发的数据、代码和教材在网络上公开传播。

Computer systems are increasingly coming to be relied upon to augment or replace human operators in controlling mechanical devices in contexts such as transportation systems, chemical plants, and medical devices, where safety and correctness are critical. A central problem is how to verify that such partially automated or fully autonomous cyber-physical systems (CPS) are worthy of our trust. One promising approach involves synthesis of the computer implementation codes from formal specifications, by software tools. This project contributes to this "correct-by-construction" approach, by developing scalable, automated methods for the synthesis of control protocols with provable correctness guarantees, based on insights from models of human behavior. It targets: (i) the gap between the capabilities of today's hardly autonomous, unmanned systems and the levels of capability at which they can make an impact on our use of monetary, labor, and time resources; and (ii) the lack of computational, automated, scalable tools suitable for the specification, synthesis and verification of such autonomous systems.The research is based on study of modular reinforcement learning-based models of human behavior derived through experiments designed to elicit information on how humans control complex interactive systems in dynamic environments, including automobile driving. Architectural insights and stochastic models from this study are incorporated with a specification language based on linear temporal logic, to guide the synthesis of adaptive autonomous controllers. Motion planning and other dynamic decision-making are by algorithms based on computational engines that represent the underlying physics, with provision for run-time adaptation to account for changing operational and environmental conditions. Tools implementing this methodology are validated through experimentation in a virtual testing facility in the context of autonomous driving in urban environments and multi-vehicle autonomous navigation of micro-air vehicles in dynamic environments. Education and outreach activities include involvement of undergraduate and graduate students in the research, integration of the research into courses, demonstrations for K-12 students, and recruitment of research participants from under-represented demographic groups. Data, code, and teaching materials developed by the project are disseminated publicly on the Web.