Fardeen Bablu | October 12, 2022
Is it possible to model every action that we take as humans? Probably not. What about computers? For sure!
New developments from Bernie Serbinowski, a postdoctoral researcher here at Vanderbilt, have allowed for more efficient testing and creation of behavior trees (BT). Serbinowski is working alongside Dr. Taylor Johnson, a specialist in computer science and engineering, to create BehaVerify, a tool that generates a “checker” for BT models.
With BehaVerify, software architecture with behavior trees can be modeled before execution, saving time for developers if any issues were to arise.
After discussing the tool with Serbinowski, he stated that “The main goal of a BT is to make sure that a program has specific results after a condition is met. Anyone with a behavior tree needs it to basically test some properties they’d like to confirm”. Therefore, BehaVerify would be most useful for those wanting to design a sequential system. The applications for sequential modeling have no limits. From robots, computers, video games, software on mechanical objects, or general safety measures, BTs play a role in ensuring proper planning and execution for any type of program.
Before jumping into the software, it’s important to define a central part of this new tool. Behavior trees (BT) are models that help a system (robot, computer, program, etc) execute a set of instructions traversed in a specific order based on the environment. Following a “tree” model, after the program checks the conditions of the environment, it would then sequence through a respective “node” or block, as seen below. Simply put, a BT is a model of multiple sets of instructions should a program meet certain conditions.
The diagram below is an example of a video game with a more solid BT. We’ll call this example “sample soldier” for clarity.
Figure 1: Sample BT of a Soldier in a Video Game
First, the program starts at the root node, which is the block labeled root at the top of the sample soldier. The smaller rectangle above each node represents the condition the program has to meet to execute the larger rectangle node.
Afterward, it checks the conditions for the next set of nodes. The sample soldier represents this by a faded line, going left to right, from combat to idle. The program is simultaneously executing the root node code and constantly checks if any conditions are met in the second generation. The root nodes continue to run until a condition is met and follow through on a subsequent node.
With the diagram, for example, if the conditions for the combat node are met, then the combat node is executed. The BT model follows the same process as before for subsequent nodes. In the case of the sample soldier, the combat node is to the melee node whereas the root node is to the combat node.
BehaVerfiy is used for creating a nuXmv model, which is a model checker that verifies a BT and if it’s running correctly. The BT that is being checked by the newly created nuXmv model is created by Essentially, BehaVerify is the tool that helps create a nuXmv model checker, which checks the BT created by py_trees.
This way, BehaVerify helps make the BT verifications process more efficient, streamlining the process development process altogether.
Figure 2: Simple BehaVerify Use Diagram
In terms of real-world applications, BehaVerify could be used while programming an elevator. BehaVerify would generate a checker for an elevator BT, checking if the elevator doesn’t open when it’s moving, for instance. In this case, BehaVerify helps write down safety measures or procedures so that the elevator works as intended.
Recently, Serbinowski has been working towards improving the functionality and efficiency of BehaVerify. One of the issues that have been slowing down the process is blackboard variables or shared memory between nodes. Improving the usability of blackboard variables will allow for different parts of the tree to connect and communicate with each other.
Moreover, there are other issues and goals that Serbinowski has highlighted to make BehaVerify a useful tool. These issues include not being able to parse all of the python py_tree code, which would make the user provide input for the tree instead of it all being automated. In general, BehaVerify could be improved by making the tool more user-friendly, and accessible for all. Alongside any software tool, better code optimizations would allow the program to run faster.
Sources:
- Castro S. Introduction to behavior trees. [accessed 2022 Oct 10]. https://robohub.org/introduction-to-behavior-trees/
- Cryengine. Coordinating agents with behavior trees. Coordinating Agents with Behavior Trees. [accessed 2022 Oct 10]. https://docs.cryengine.com/display/SDKDOC4/Coordinating+Agents+with+Behavior+Trees
- Serbinowski B, Johnson TTJT. BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees. arxiv . 2022 Aug 10 [accessed 2022 Oct 11]. https://doi.org/10.48550/arXiv.2208.05360