CAREER: Provably Correct Shared Control for Human-Embedded Autonomous Systems

拟议的工作将有助于开发人类和自主负责集体信息获取、感知、认知和决策的系统。这种集体行动既是一种必要性，也是一种增强技术。例如，在辅助机器人技术中，自主性的存在是为了支持人类用户无法执行的功能。另一方面，在人类可以充分操作平台（例如半自主无人驾驶车辆）的情况下，她有效地增强了机器人的能力。建立可证明的信任是大规模部署自治系统最紧迫的瓶颈之一。将人类作为用户、信息源或决策辅助嵌入到自主系统的操作中会增加难度。虽然人类提供的认知能力可以补充机器可实现的功能，但这种协同作用的影响取决于系统推断人类意图、偏好和局限性的能力，以及人类与自主系统之间的接口所带来的缺陷。我们期望所提出的理论、方法和工具能够跨越与人类一起工作并在人类附近工作的网络物理系统的范围。此类系统包括，仅举几例，人机交互、一系列辅助医疗设备、现代汽车中的半自动驾驶或安全增强系统以及大型工厂的控制室。拟议的工作旨在解决人类嵌入式自主系统设计的理论和工具方面的重大空白。其目标是为共享控制协议的正式规范和自动合成开发语言、算法和演示。我们的技术方法基于桥接正式方法、控制、学习和人类行为建模。它基于三个主要研究方向。 (i) 共享控制的规范和建模：在人类嵌入式自治系统中证明正确性意味着什么，以及我们如何在正式规范中表示正确性？ （ii）共享控制协议的自动合成：我们如何从数学上抽象共享控制，并从形式规范中自动合成共享控制协议？ (iii) 通过人类-自主界面的共享控制：我们如何解释人类-自主界面的表达性、精度和带宽以及协同设计控制器和界面的限制？基于数学的规范和自动合成算法将在整个设计中分散建立信任的过程，有可能减轻对纯粹经验测试的需求，并在昂贵且受限的用户研究之前诊断故障模式。这种系统性的早期集成将有助于开发自主系统，其中操作员和自主协议是同一系统的同等重要组成部分，并减少所谓的“自动化意外”。虽然我们期望所提议的工作的理论和算法结果与应用和硬件无关，但我们在特定的硬件平台中具体化了我们的研究计划。它由具有 3D 运动捕捉的现有四旋翼测试台组成；通过神经、视觉、听觉和生物电势信号进行人体监控和解码功能；以及人类自主与虚拟现实嵌入的接口。

The proposed effort will help develop systems in which humans and autonomy are responsible for collective information acquisition, perception, cognition and decision-making. Such collective operation is a necessity as much as it is an augmenting technology. In assistive robotics, for example, the autonomy exists to support functionality that the human users cannot perform. On the other hand, in cases in which a human can adequately operate a platform (e.g., semi-autonomous unmanned vehicles), she effectively augments the robot's abilities. Establishing provable trust is one of the most pressing bottlenecks in deploying autonomous systems at scale. Embedding a human as a user, information source or decision aid into the operation of autonomous systems amplifies the difficulty. While humans offer cognitive capabilities that complement machine implementable functionalities, the impact of this synergy is contingent on the system's ability to infer the intent, preferences and limitations of the human and the imperfections imposed by the interfaces between the human and the autonomous system. We expect the proposed theory, methods and tools to cut across the spectrum of cyberphysical systems that are to work with and in the vicinity of humans. Such systems include, to name a few, human-robot interactions, a range of assistive medical devices, semi-autonomous driving or safety augmentation systems in modern automobiles and control rooms of large-scale plants.The proposed effort targets a major gap in theory and tools for the design of human-embedded autonomous systems. Its objective is to develop languages, algorithms and demonstrations for the formal specification and automated synthesis of shared control protocols. Our technical approach is based on bridging formal methods, controls, learning and human behavioral modeling. It is based on three main research thrusts. (i) Specifications and modeling for shared control: What does it mean to be provably correct in human-embedded autonomous systems, and how can we represent correctness in formal specifications? (ii) Automated synthesis of shared control protocols: How can we mathematically abstract shared control, and automatically synthesize shared control protocols from formal specifications? (iii) Shared control through human-autonomy interfaces: How can we account for the limitations in expressivity, precision and bandwidth of human-autonomy interfaces, and co-design controllers and interfaces? The mathematically-based specifications and automated synthesis algorithms will diffuse the process of building trust throughout the design, have the potential to mitigate the need for purely empirical testing, and diagnose failure modes in advance of costly and restricted user studies. This systematic and early integration will help develop autonomous systems in which the operator and autonomy protocols are equally essential components of the same system and reduce the so-called ``automation surprises." While we expect the theoretical and algorithmic outcomes of the proposed effort to be application- and hardware-agnostic, we concretize our research plan in a specific hardware platform. It is composed of an existing quadrotor testbed with 3D motion capture; human monitoring and decoding functionality through neural, visual, audial and biopotential signals; and human-autonomy interfaces with virtual reality embeddings.