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

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

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.