《基于形式化方法的多机器人系统规划与规范》2022博士论文

机器人系统正在进入舞台。在硬件组件和软件技术进步的推动下，机器人越来越能够在工厂外运作，协助人类，并与人类一起工作。机器人扩张的限制因素仍然是机器人系统的编程。由于建立一个多机器人系统需要许多不同的技能，只有最大的组织能够在机器人提供的服务空间中进行创新。

只有最大的组织能够在机器人提供的服务空间中进行创新。为了使开发新的机器人服务更容易，我在这篇论文中提出了一个规划模型，在这个模型中，用户（程序员）给出了需要完成的声明性规范，然后一个后台系统确保该规范被安全、可靠地执行。我介绍了Antlab，一个这样的后端系统。Antlab接受来自多个用户的线性时态逻辑（LTL）规范，并使用一组不同能力的机器人来执行它们。

在实施Antlab的经验基础上，我确定了由所提出的规划模型产生的问题。这些问题分为两大类：规范和规划。

在规范问题的类别中，我解决了从正反两方面的例子中推断LTL公式的问题，以及仅从一组正面例子中推断LTL公式的问题。在这些解决方案的基础上，我开发了一种方法来帮助用户将他们的意图转移到正式的规范中。本论文所采取的方法是将来自单个演示的意图信号和用户给出的自然语言描述结合起来。通过将问题编码为命题逻辑的可满足性问题，推断出一组候选规范。通过与用户的互动，这组规格被缩小到一个单一的规格；用户批准或拒绝对机器人在不同情况下的行为进行的模拟。

在规划问题类别中，我首先解决了目前正在执行任务的机器人的规划问题。在这种情况下，不清楚应该把什么作为规划的初始状态。我通过考虑多个推测的初始状态来解决这个问题。从这些状态出发的路径是根据一个质量函数来探索的，该函数反复估计规划时间。第二个问题是奖励函数为非马尔科夫时的强化学习问题。建议的解决方案包括反复学习代表奖励函数的自动机，并使用它来指导探索。