Formal Verification Based Synthesis for Behavior Trees

Behavior trees (BTs) have been extensively applied in the area of both computer games and robotics, as the control architectures. However, the construction of BTs is labor-expensive, time-consuming, and even impossible as the complexity of task increases. In this work, we propose a formal verification based synthesis method to automatically construct BTs whose behaviors satisfy the given Linear Temporal Logic (LTL) specifications. Our method first explores candidate BTs by a grammar-based Monte Carlo Tree Search (MCTS), then the explored BTs are transformed into Communicating Sequential Processes (CSP) models. After that, we invoke the verifier to check the models’ correctness w.r.t. specifications, and provide feedback based on the verification result for guiding the search process. The application of our method on several representative robotic missions indicates its promising.