通过对话消除歧义以修正自由飞行机器人不可综合的控制器

在栖息地建造、空间站巡检或协同探索等情境中，团队对环境或任务的不正确假设可能导致任务失败。因此，在执行指令任务之前，解决队友间关于任务的任何歧义十分重要。形式化方法所保证的安全机制可用于为机器人使用线性时序逻辑综合构造即正确的反应式控制器。若机器人给定指令后未能综合出控制器，则显然环境假设和/或所描述的交互中存在逻辑不一致。然而，这些规约通常用验证框架特有的语言编写，要求人类协作者精通用于构建它的软件工具。此外，若控制器综合失败，可能难以轻松修复该规约。语言是利用现代符号接地技术生成这些规约的自然媒介。使用语言使非专家人类能够向机器人队友描述任务，同时保留形式化验证的优势。此外，对话可用于在任务执行前告知机器人环境信息和/或消除任何歧义。本文引入一种使用符号表示的自然语言交互架构，该架构为线性时序逻辑中规约的构建提供信息。该方法的新颖之处在于，它提供了一种通过假设对规约的修正并通过人机对话验证来解决综合失败的机制。所提架构的实验通过使用在国际空间站中导航的Astrobee机器人仿真进行演示。