# Designing Behavior Trees from Goal-Oriented LTLf Formulas

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 37 references that are in the map.
- First posted on arXiv 12 Jul 2023.

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

- [Behavior Trees in Robotics and AI: An Introduction](https://mlsanity.com/paper/1709.00084/) (2017)
- [A Learning Based Approach to Control Synthesis of Markov Decision Processes for Linear Temporal Logic Specifications](https://mlsanity.com/paper/1409.5486/) (2014)
- [Stochastic Finite State Control of POMDPs with LTL Specifications](https://mlsanity.com/paper/2001.07679/) (2020)
- [On modularity in reactive control architectures, with an application to formal verification](https://mlsanity.com/paper/2008.12515/) (2020)
- [Sampling-Based Temporal Logic Path Planning](https://mlsanity.com/paper/1307.7263/) (2013)

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

- [Integrating Intent Understanding and Optimal Behavior Planning for Behavior Tree Generation from Human Instructions](https://mlsanity.com/paper/2405.07474/) (2024)
- [HBTP: Heuristic Behavior Tree Planning with Large Language Model Reasoning](https://mlsanity.com/paper/2406.00965/) (2024)
- [MRBTP: Efficient Multi-Robot Behavior Tree Planning and Collaboration](https://mlsanity.com/paper/2502.18072/) (2025)
- [Behavior Trees Enable Structured Programming of Language Model Agents](https://mlsanity.com/paper/2404.07439/) (2024)
- [CABTO: Context-Aware Behavior Tree Grounding for Robot Manipulation](https://mlsanity.com/paper/2603.16809/) (2026)

## Abstract (arXiv)

Temporal logic can be used to formally specify autonomous agent goals, but synthesizing planners that guarantee goal satisfaction can be computationally prohibitive. This paper shows how to turn goals specified using a subset of finite trace Linear Temporal Logic (LTL) into a behavior tree (BT) that guarantees that successful traces satisfy the LTL goal. Useful LTL formulas for achievement goals can be derived using achievement-oriented task mission grammars, leading to missions made up of tasks combined using LTL operators. Constructing BTs from LTL formulas leads to a relaxed behavior synthesis problem in which a wide range of planners can implement the action nodes in the BT. Importantly, any successful trace induced by the planners satisfies the corresponding LTL formula. The usefulness of the approach is demonstrated in two ways: a) exploring the alignment between two planners and LTL goals, and b) solving a sequential key-door problem for a Fetch robot.