用形式化语言让行为树可验证，提升机器人程序可靠性。
A formal implementation of Behavior Trees to act in robotics
- 将行为树转为Fiacre语言，实现形式化建模。
- 支持离线检查LTL/CTL性质，运行时可实时验证正确性。
- 保留行为树模块化优势，适合需高可靠性的机器人开发。
行为树（BT）在自主机器人系统中作为决策组件日益流行。本文提出一种形式化语义框架，通过将行为树翻译为形式化语言Fiacre，实现程序的正式验证与运行时验证，无需编程者掌握形式化语言，同时保持行为树的模块化、灵活性和可复用性。我们采用Fiacre语言及其生成的TTS模型，结合其模型检测工具Tina与运行时验证引擎Hippo。展示自动将行为树转化为Fiacre的方法，支持离线验证LTL和CTL性质，并可在运行时以形式化模型替代传统行为树引擎执行。在两个机器人应用中验证该方法，证明可通过扩展状态变量、评估节点、节点结果及利用时间等特性增强行为树功能。
原文摘要 · Abstract (English)
Behavior Trees (BT) are becoming quite popular as an Acting component of autonomous robotic systems. We propose to define a formal semantics to BT by translating them to a formal language which enables us to perform verification of programs written with BT, as well as runtime verification while these BT execute. This allows us to formally verify BT correctness without requiring BT programmers to master formal languages and without compromising BT most valuable features: modularity, flexibility and reusability. We present the formal framework we use: Fiacre, its language and the produced TTS model; Tina, its model checking tools and Hippo, its runtime verification engine. We then show how the translation from BT to Fiacre is automatically done, the type of formal LTL and CTL properties we can check offline and how to execute the formal model online in place of a regular BT engine. We illustrate our approach on two robotics applications, and show how BT can be extended with state variables, eval nodes, node evaluation results and benefit of other features available in the Fiacre formal framework (e.g., time).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。