Specification-guided behavior tree synthesis and execution for coordination of autonomous systems

This paper develops an automatic online Behavior Tree (BT) synthesis and execution technique to guide an autonomous agent to accomplish a series of missions expressed in Fragmented-Linear Temporal Logic (F-LTL). For this purpose, a novel top-down, divide-and-conquer method is developed to decompose the original F-LTL formulas into simpler sub-formulas, followed by synthesizing the corresponding sub-BTs. Then, the safe and reachable regions are calculated to identify the winning set for the sub-BTs and the associated winning paths. If the computed winning set is non-empty, the sub-BTs are composed to form a coordinator whose execution guarantees the satisfaction of the original F-LTL formulas. The correctness of the proposed method is proved. Unlike most existing methods which manually design BTs and suffer from high computation cost, the proposed method can automatically synthesize the BTs on-the-fly for F-LTL formulas with polynomial complexity in the size of the formula and the environment. The developed method is applied to several scenarios with different missions and sizes of the environment using a physics-based simulator. The simulation results demonstrate the capability of the proposed method to handle missions described by F-LTL formulas and the scalability of the approach in terms of the size of the environment.