Félix Ingrand.

The BT2Fiacre tool takes a Behavior Tree (BT) as input and produces an equivalent Fiacre formal model, which can then be used with the Tina toolbox (to prove some formal properties using model checking), but also with the Hippo engine to execute the equivalent formal model of the BT.

To perform the translation from BT to Fiacre, a number of clarifications in the BT semantics had to be made. This is in fact one advantage of transforming the BT in a formal model, one needs to make explicit some of the unspecified behaviors of BT, and thus clarify what was often left to the implementer choice. For example, what should be done with running branches when a Parallel node has succeeded or failed. Should we wait for those running branches? halt them? Similarly, for ReactiveSequence node, if a branch fails, while there are other following branches still running.