Verifying Safety of Behaviour Trees in Event-B

TL;DR

This paper introduces a formal specification and verification methodology for Behavior Trees in robotics, ensuring safety and reliability in critical environments while maintaining user-friendly complexity.

Contribution

It presents a novel formalization of Behavior Trees and a practical approach to verify their safety invariants without requiring deep formal knowledge from users.

Findings

Enables formal verification of Behavior Trees for safety.

Allows testing specific trees without complex formalization.

Supports deployment in safety-critical robotic applications.

Abstract

Behavior Trees (BT) are becoming increasingly popular in the robotics community. The BT tool is well suited for decision-making applications allowing a robot to perform complex behavior while being explainable to humans as well. Verifying that BTs used are well constructed with respect to safety and reliability requirements is essential, especially for robots operating in critical environments. In this work, we propose a formal specification of Behavior Trees and a methodology to prove invariants of already used trees, while keeping the complexity of the formalization of the tree simple for the final user. Allowing the possibility to test the particular instance of the behavior tree without the necessity to know the more abstract levels of the formalization.