A verified interpreter for Behavior Trees. This package contains a compiler that generates the interpreter that execute a given Behavior Tree. The interpreted can be executed in any C/C++ code or as SmartSoft component.

The goal of this package it to provide an execution engine for Behavior Trees which can be integrated into the SmartSoft framework and which provably conforms to the operational semantics for BTs (as defined in the deliverable D3.2  of the ITP CARVE, Syntax and Semantic of Behavior Trees for Robotics). In order to achieve this goal we translated the abstract operational semantics into a concrete algorithm written in Gallina, the language of the Coq proof assistant. This algorithm is then extracted into actual executable code (written in the OCaml programming language) using Coq's program extraction mechanism. Finally, the generated OCaml code is compiled into a shared library which can be called from the SmartSoft runtime.

The input to the compiler is a BT described using the Groot (https://github.com/BehaviorTree/Groot) syntax as xml.

This work is conformant to the RobMoSys Task-Skill metamodel. The BT interpreter is an engine for a Task, described using a Behavior Tree syntax. Leaves within a BT represent Skills.

Behavior Trees can be designed using the Groot editor, because the syntax used to generate the interpreter is compatible. The BehaviorTree C++ library is an alternative execution engine for behavior Trees.

• Code and installation instructions are available on the GitHub page: https://github.com/CARVE-ROBMOSYS/BTCompiler
• Code for executing the engine within SmartSoft is available here: https://github.com/CARVE-ROBMOSYS/Yarp-SmartSoft-Integration/tree/master/BehaviorTree
• Check out CARVE official website for information on the project and how the BT engine has been used with the R1 humanoid robot to solve navigation and grasping task.
• Robotic Behavior Metamodel
• Skill Definition Metamodel