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).

翻译：行为树（BT）作为自主机器人系统的执行组件正日益普及。我们提出通过将BT转换为形式化语言来定义其形式语义，这使得我们能够对使用BT编写的程序进行验证，并在BT执行时进行运行时验证。这种方法允许我们形式化验证BT的正确性，同时无需BT程序员掌握形式化语言，也不会损害BT最宝贵的特性：模块化、灵活性和可重用性。我们介绍了所使用的形式化框架：Fiacre及其语言和生成的TTS模型；Tina及其模型检测工具；以及Hippo运行时验证引擎。随后展示了如何自动完成从BT到Fiacre的转换，可离线验证的LTL与CTL形式化属性类型，以及如何在线执行形式化模型以替代常规BT引擎。我们通过两个机器人应用案例阐释该方法，并展示如何通过状态变量、评估节点、节点评估结果扩展BT功能，以及如何利用Fiacre形式化框架的其他特性（如时间处理）。