Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees

Serena S. Serbinowska, Taylor T. Johnson

TL;DR

BehaVerify tackles the lack of practical verification tools for Behavior Trees by automatically converting PyTrees into nuXmv SMV models for LTL model checking. It introduces Leaf and Total encodings (with a BTCompiler-based baseline) and demonstrates that Total_v3 offers the best runtime and memory performance across Checklist and BlueROV case studies. The tool supports Blackboard variables and memory-enabled composites, broadening verifiable BT applications in robotics. This work advances verification efficiency and practicality for BT-based control, enabling rigorous safety guarantees and accessible counterexamples.

Abstract

Behavior Trees, which originated in video games as a method for controlling NPCs but have since gained traction within the robotics community, are a framework for describing the execution of a task. BehaVerify is a tool that creates a nuXmv model from a py_tree. For composite nodes, which are standardized, this process is automatic and requires no additional user input. A wide variety of leaf nodes are automatically supported and require no additional user input, but customized leaf nodes will require additional user input to be correctly modeled. BehaVerify can provide a template to make this easier. BehaVerify is able to create a nuXmv model with over 100 nodes and nuXmv was able to verify various non-trivial LTL properties on this model, both directly and via counterexample. The model in question features parallel nodes, selector, and sequence nodes. A comparison with models based on BTCompiler indicates that the models created by BehaVerify perform better.

BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees

TL;DR

BehaVerify tackles the lack of practical verification tools for Behavior Trees by automatically converting PyTrees into nuXmv SMV models for LTL model checking. It introduces Leaf and Total encodings (with a BTCompiler-based baseline) and demonstrates that Total_v3 offers the best runtime and memory performance across Checklist and BlueROV case studies. The tool supports Blackboard variables and memory-enabled composites, broadening verifiable BT applications in robotics. This work advances verification efficiency and practicality for BT-based control, enabling rigorous safety guarantees and accessible counterexamples.

Abstract

Behavior Trees, which originated in video games as a method for controlling NPCs but have since gained traction within the robotics community, are a framework for describing the execution of a task. BehaVerify is a tool that creates a nuXmv model from a py_tree. For composite nodes, which are standardized, this process is automatic and requires no additional user input. A wide variety of leaf nodes are automatically supported and require no additional user input, but customized leaf nodes will require additional user input to be correctly modeled. BehaVerify can provide a template to make this easier. BehaVerify is able to create a nuXmv model with over 100 nodes and nuXmv was able to verify various non-trivial LTL properties on this model, both directly and via counterexample. The model in question features parallel nodes, selector, and sequence nodes. A comparison with models based on BTCompiler indicates that the models created by BehaVerify perform better.
Paper Structure (26 sections, 29 equations, 9 figures, 2 tables)

This paper contains 26 sections, 29 equations, 9 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Background
  4. The Blackboard
  5. Related Work
  6. Strengths and Uses of BTs
  7. Expanded BTs
  8. Verification of BTs
  9. Overview of Approach
  10. Encodings
  11. Leaf
  12. Total
  13. BTCompiler
  14. Results
  15. Checklist and Parallel-Checklist
  16. ...and 11 more sections

Figures (9)

  • Figure 1: Composite Nodes in PyTrees.
  • Figure 2: A simple BT
  • Figure 3: A selector node with many children.
  • Figure 4: Timing and memory results for verifying LTL specifications in nuXmv for Checklist and Parallel-Checklist. Timeout is set to 5 minutes. If a timeout occurred, a value of 350 is used for timing and -1000 for memory. After 3 timeouts, the remaining tests for the version are skipped. BTC is based on BTCompiler, Leaf_v2 is a model based on the Leaf encoding, and Total_v2 and Total_v3 are models based on the Total encoding.
  • Figure 5: Two examples with 3 children.
  • ...and 4 more figures