A formal implementation of Behavior Trees to act in robotics

TL;DR

This paper introduces a formal semantics for Behavior Trees in robotics by translating them into a formal language, enabling verification and runtime analysis without sacrificing modularity or flexibility.

Contribution

It presents a novel formal framework translating Behavior Trees into Fiacre, allowing verification and execution in robotics applications.

Findings

Automated translation from BT to Fiacre is feasible.

Formal verification of BT properties is possible offline.

Runtime verification can be integrated with BT execution.

Abstract

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