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

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