In situations such as habitat construction, station inspection, or cooperative exploration, incorrect assumptions about the environment or task across the team could lead to mission failure. Thus it is important to resolve any ambiguity about the mission between teammates before embarking on a commanded task. The safeguards guaranteed by formal methods can be used to synthesize correct-by-construction reactive controllers for a robot using Linear Temporal Logic. If a robot fails to synthesize a controller given an instruction, it is clear that there exists a logical inconsistency in the environmental assumptions and/or described interactions. These specifications however are typically crafted in a language unique to the verification framework, requiring the human collaborator to be fluent in the software tool used to construct it. Furthermore, if the controller fails to synthesize, it may prove difficult to easily repair the specification. Language is a natural medium to generate these specifications using modern symbol grounding techniques. Using language empowers non-expert humans to describe tasks to robot teammates while retaining the benefits of formal verification. Additionally, dialogue could be used to inform robots about the environment and/or resolve any ambiguities before mission execution. This paper introduces an architecture for natural language interaction using a symbolic representation that informs the construction of a specification in Linear Temporal Logic. The novel aspect of this approach is that it provides a mechanism for resolving synthesis failure by hypothesizing corrections to the specification that are verified through human-robot dialogue. Experiments involving the proposed architecture are demonstrated using a simulation of an Astrobee robot navigating in the International Space Station.

翻译：在栖息地建设、空间站检查或协同探索等场景中，团队成员对环境或任务的错误假设可能导致任务失败。因此，在执行受命任务前，解决团队成员间关于任务的任何歧义至关重要。形式化方法提供的安全保障可用于利用线性时态逻辑为机器人综合出正确性有保证的反应式控制器。若机器人在给定指令后未能综合出控制器，则表明环境假设和/或所描述交互中存在逻辑不一致性。然而，这些规约通常以验证框架特有的语言编写，要求人类协作者熟练掌握用于构建规约的软件工具。此外，若控制器综合失败，可能难以轻易修正规约。语言是一种自然的媒介，可通过现代符号接地技术生成这些规约。使用语言能使非专业人类向机器人队友描述任务，同时保留形式化验证的优势。此外，对话可用于在任务执行前向机器人提供环境信息并/或解决任何歧义。本文提出一种基于符号表示的自然语言交互架构，该架构可指导线性时态逻辑规约的构建。该方法的新颖之处在于提供了一种机制，通过假设对规约的修正（经由人机对话验证）来解决综合失败问题。在模拟国际空间站中Astrobee机器人导航的实验中，展示了所提架构的效果。