Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A formal implementation of Behavior Trees to act in robotics

Felix Ingrand

TL;DR

The paper tackles the need for formal semantics and verification of Behavior Trees in robotics by translating BTs into Fiacre, enabling both offline model checking (via Tina) and online runtime verification (via Hippo). The BT2Fiacre workflow yields executable Fiacre models with time, state variables, and external C/C++ bindings, allowing rigorous proofs of properties (e.g., safety, reachability) and faithful live execution. The approach is demonstrated on UAV and ROS2 Nav2 BTs, showing scalable offline verification results and real-time, color-coded runtime monitoring. The work positions Fiacre/Tina/Hippo as a unified framework to increase trust in BT-based robotic actuation, while outlining limitations (state explosion, dynamic BTs) and paths for future enhancement (time modeling, richer data types, environment modeling). Overall, the method provides a rigorous bridge between BT programming and formal verification, with potential impact on safety-critical robotic systems.

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

A formal implementation of Behavior Trees to act in robotics

TL;DR

The paper tackles the need for formal semantics and verification of Behavior Trees in robotics by translating BTs into Fiacre, enabling both offline model checking (via Tina) and online runtime verification (via Hippo). The BT2Fiacre workflow yields executable Fiacre models with time, state variables, and external C/C++ bindings, allowing rigorous proofs of properties (e.g., safety, reachability) and faithful live execution. The approach is demonstrated on UAV and ROS2 Nav2 BTs, showing scalable offline verification results and real-time, color-coded runtime monitoring. The work positions Fiacre/Tina/Hippo as a unified framework to increase trust in BT-based robotic actuation, while outlining limitations (state explosion, dynamic BTs) and paths for future enhancement (time modeling, richer data types, environment modeling). Overall, the method provides a rigorous bridge between BT programming and formal verification, with potential impact on safety-critical robotic systems.

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

Paper Structure

This paper contains 47 sections, 17 figures.

Table of Contents

  1. Introduction and motivation
  2. State of the art and proposed approach
  3. BT in robotics
  4. Implementation considerations
  5. BT and planning
  6. BT and formal models
  7. Proposed approach
  8. A Formal Framework for Offline and Runtime Verification: The Fiacre Language, Models, and Tools
  9. Terminology, Models, Languages, and Tools
  10. Fiacre Semantics
  11. Offline Formal Verification
  12. H-Fiacre Runtime Extensions
  13. Runtime (Online) Verification
  14. The mapping of BT in Fiacre
  15. The general mapping
  16. ...and 32 more sections

Figures (17)

  • Figure 1: The Fiacre processes modeling the Fiacre specification on Listing \ref{['lst:ftct']}p\ref{['lst:ftct']}.
  • Figure 2: Illustration of the H-Fiacre program on Listing \ref{['lst:ftch']}p\ref{['lst:ftch']}.
  • Figure 3: The BT2Fiacre ( Hippo/ Tina) workflow. Only the data in the blue boxes need to be provided by the programmer. The BT2Fiacre tool (in light red) synthesizes the two models, the rest is fully automated. In light green, the workflow for the Hippo runtime verification version, and in light purple, the workflow for the Tina offline verification version.
  • Figure 4: Preamble and postamble of BT nodes in Fiacre.
  • Figure 5: The Fiacre process modeling the Condition node for the verification ( Tina) model.
  • ...and 12 more figures