EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution Framework

Behavior Trees (BTs), originated from the control of Non-Player-Characters (NPCs), have been widely embraced in robotics and software engineering communities due to their modularity, reactivity, and other beneficial characteristics. It is highly desirable to synthesize BTs automatically. The consequent challenges are to ensure the generated BTs semantically correct, well-structured, and efficiently executable. To address these challenges, in this paper, we present a novel reactive synthesis method for BTs, namely EffBT, to generate correct and efficient controllers from formal specifications in GR(1) automatically. The idea is to construct BTs soundly from the intermediate strategies derived during the algorithm of GR(1) realizability check. Additionally, we introduce pruning strategies and use of Parallel nodes to improve BT execution, while none of the priors explored before. We prove the soundness of the EffBT method, and the experimental results demonstrate its effectiveness in various scenarios and datasets.

Authors

Institutions

Publication Details

Published
2025-04-26
DOI
https://doi.org/10.1109/icse55347.2025.00225
Primary Topic
Formal Methods in Verification
Type
article
Field-Weighted Citation Impact
0.00
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution Framework

Peishan Huang, Zeping Wu, Minglong Li, Ji Wang et al.
Formal Methods in Verification
article

EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution Framework

Peishan Huang, Zeping Wu, Minglong Li, Ji Wang, Yu Huang, Shanghua Wen
article en

Abstract

Behavior Trees (BTs), originated from the control of Non-Player-Characters (NPCs), have been widely embraced in robotics and software engineering communities due to their modularity, reactivity, and other beneficial characteristics. It is highly desirable to synthesize BTs automatically. The consequent challenges are to ensure the generated BTs semantically correct, well-structured, and efficiently executable. To address these challenges, in this paper, we present a novel reactive synthesis method for BTs, namely EffBT, to generate correct and efficient controllers from formal specifications in GR(1) automatically. The idea is to construct BTs soundly from the intermediate strategies derived during the algorithm of GR(1) realizability check. Additionally, we introduce pruning strategies and use of Parallel nodes to improve BT execution, while none of the priors explored before. We prove the soundness of the EffBT method, and the experimental results demonstrate its effectiveness in various scenarios and datasets.

National University of Defense Technology (CN)
Openalex Percentile: Top 84%
Formal Methods in Verification
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution Framework — Peishan Huang, Zeping Wu, et al. · (2025) | TGRS Research Map | TGRS