行为树在机器人学中的形式化实现

行为树（BT）正日益成为自主机器人系统中执行组件的热门选择。我们提出通过将行为树翻译为形式化语言来定义其形式语义，从而使我们能够对用 BT 编写的程序进行验证，以及在 BT 执行时进行运行时验证。这使得我们可以在不要求 BT 程序员掌握形式化语言的情况下形式化验证 BT 的正确性，同时不损害 BT 最有价值的特性：模块化、灵活性和可复用性。我们展示了所使用的形式化框架：Fiacre、其语言及生成的 TTS 模型；Tina、其模型检验工具；以及 Hippo、其运行时验证引擎。随后我们展示了如何自动完成从 BT 到 Fiacre 的翻译、可以离线检验何种形式的 LTL 和 CTL 性质，以及如何在线执行形式化模型以替代常规 BT 引擎。我们在两个机器人学应用上展示了我们的方法，并展示了如何通过状态变量、求值节点、节点求值结果以及 Fiacre 形式化框架中其他可用特性（如时间）来扩展 BT。