# Verifying Safety of Behaviour Trees in Event-B

arXiv: https://arxiv.org/abs/2209.14045 · HTML: https://mlsanity.com/paper/2209.14045/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 21 references that are in the map.
- First posted on arXiv 28 Sep 2022.

## Builds on (most cited first, 3 of 3)

- [Behavior Trees in Robotics and AI: An Introduction](https://mlsanity.com/paper/1709.00084/) (2017)
- [The Marathon 2: A Navigation System](https://mlsanity.com/paper/2003.00368/) (2020)
- [Learning of Behavior Trees for Autonomous Agents](https://mlsanity.com/paper/1504.05811/) (2015)

## Built on by (most cited first, 2 of 2)

- [Behavior Trees Enable Structured Programming of Language Model Agents](https://mlsanity.com/paper/2404.07439/) (2024)
- [Execution Semantics of Behavior Trees in Robotic Applications](https://mlsanity.com/paper/2408.00090/) (2024)

## Abstract (arXiv)

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.