EffBT: An Efficient Behavior Tree Reactive Synthesis and Execution Framework

Behavior Trees originate from the control of Non-Player-Characters (NPCs) and have been widely embraced in robotics because of their advantages in modularity, reactivity, and other features. Research on synthesizing BTs automatically has been strongly promoted. Reactive synthesis is a method that obtains correct-by-construction controllers from formal specifications. However, model-checking-based behavior tree reactive synthesis on general LTL suffers an EXPTIME complexity and Fragment-LTL-based (F-LTL) behavior tree synthesis needs to calculate several individual functions for each formula. Hence, we propose EffBT, an efficient behavior tree synthesis andexecution framework, which also adopts F-LTL (i.e., GR(1) formulas) as specifications, but we unify function calculations into GR(1) realizability check. Benefiting from this, we could enhance the execution efficiency of obtained BTs at the design phase by efficient modularized structure design and the adoption of Parallel nodes, while none of the prior works focused on this. We proved the soundness of EffBT and later experiments also demonstrated its effectiveness.