Enabling Behaviour Tree Verification via a Translation to BIP

A formal verification method for behavior tree (BT) is proposed. The method is based on a compositional model transformation of BT into the formal component-based system design framework BIP (Behavior-Interaction-Priority). The transformation encodes each BT node as an individual BIP component that is formally defined by an extended finite state automaton (FSA), and each BT edge as a set of interactions that describes the allowed coordination between components. The correctness proof of the model transformation is presented, and a prototype tool-chain has been implemented that enables the automated verification of BT. Two practical case studies show that the tool-chain can not only verify the correctness of BT, but also detect the potential design flaws automatically.