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.