Formalizing Stateful Behavior Trees

TL;DR

This paper presents a domain specific language (DSL) for writing SBTs and adapt the tool BehaVerify for use with this DSL, and identifies syntactic assumptions where SBTs have computational power equivalent to finite state automata, specifically where the auxiliary variables are of finitary types.

Abstract

Behavior Trees (BTs) are high-level controllers that are useful in a variety of planning tasks and are gaining traction in robotic mission planning. As they gain popularity in safety-critical domains, it is important to formalize their syntax and semantics, as well as verify properties for them. In this paper, we formalize a class of BTs we call Stateful Behavior Trees (SBTs) that have auxiliary variables and operate in an environment that can change over time. SBTs have access to persistent shared memory (often known as a blackboard) that keeps track of these auxiliary variables. We demonstrate that SBTs are equivalent in computational power to Turing Machines when the blackboard can store mathematical (i.e., unbounded) integers. We further identify syntactic assumptions where SBTs have computational power equivalent to finite state automata, specifically where the auxiliary variables are of finitary types. We present a domain specific language (DSL) for writing SBTs and adapt the tool BehaVerify for use with this DSL. This new DSL in BehaVerify supports interfacing with popular BT libraries in Python, and also provides generation of Haskell code and nuXmv models, the latter of which is used for model checking temporal logic specifications for the SBTs. We include examples and scalability results where BehaVerify outperforms another verification tool by a factor of 100.

Figures (9)

• Figure 1: A $\mathit{BT}$ for the Collatz conjecture (hailstone sequence) consisting of a selector node (a), a sequence node (b), a check (c), and two actions (d, e). We use the ternary operator $i?j:k$ to mean if $i$ then $j$ else $k$. We use % for modulo. Tick indicates the number of times the tree has been ticked. $t$ is used to track the number of times we have changed active nodes. Active is used to track where we are in the tree. Returns indicates what the active node returns; a - indicates the node did not return. If a node is finished, then it returns one of $\mathit{S}$, $\mathit{F}$, or $\mathit{R}$.
• Figure 2: Assume that $f(sym, st) = (sym^{\prime}, st^{\prime}, dir)$, where $f$ is the transition function for the Turing Machine. Then this means that if the Turing Machine is in state $st$ and reads $sym$ from the tape head, it will write $sym^{\prime}$ to the tape head, transition to $st^{\prime}$, and move the tape head according to $dir$. The subtree captures this behavior.
• Figure 3: (L) 3 node tree. (R) total encoding. Note: $x?y:z$ means if $x$, then $y$, else $z$.
• Figure 4: Here $\textcolor{BehaviorTreeBlackboardColor}{x}$ is a blackboard variable and $\textcolor{BehaviorTreeEnvironmentColor}{y}$ is an environment variable (an input). The input changes between ticks, so $\textcolor{BehaviorTreeEnvironmentColor}{y_1}$ does not appear in the tree. The upper table shows what stepping through the tree one node at a time would look like. The lower table shows what fastforwarding looks like. The tree itself includes stage subscripts that were added for readability; the user would normally create a tree without knowledge of the stages, as BehaVerify handles stage creation. Note that when fastforwarding, the value of $\textcolor{BehaviorTreeBlackboardColor}{x_2}$ is set to that of $\textcolor{BehaviorTreeBlackboardColor}{x_1}$ if (d) does not execute. Furthermore, note that the value of $\textcolor{BehaviorTreeBlackboardColor}{x}$ at the end of the tick ($\textcolor{BehaviorTreeBlackboardColor}{x_2}$) is the value of $\textcolor{BehaviorTreeBlackboardColor}{x}$ at the start of the next tick ($\textcolor{BehaviorTreeBlackboardColor}{x_0}$).
• Figure 5: Left is original, right is reworked for MoVe4BT. Number of nodes is counted using right tree (10 in this case). $\textcolor{BehaviorTreeBlackboardColor}{f}$ is the size of the 'biggest fish' so far. Each check returns $\mathit{S}$ if the $\textcolor{BehaviorTreeBlackboardColor}{f}$ is equal to its number and $\mathit{F}$ otherwise. If any check returns $\mathit{S}$, the left half of the tree returns $\mathit{S}$ and $\textcolor{BehaviorTreeBlackboardColor}{f}$ is incremented.