Verification of Behavior Trees with Contingency Monitors

TL;DR

A new methodology by which to create Runtime Monitors for BTs, which can be used by the BT to correct when undesirable behavior is detected and are capable of handling LTL specifications.

Abstract

Behavior Trees (BTs) are high level controllers that have found use in a wide range of robotics tasks. As they grow in popularity and usage, it is crucial to ensure that the appropriate tools and methods are available for ensuring they work as intended. To that end, we created a new methodology by which to create Runtime Monitors for BTs. These monitors can be used by the BT to correct when undesirable behavior is detected and are capable of handling LTL specifications. We demonstrate that in terms of runtime, the generated monitors are on par with monitors generated by existing tools and highlight certain features that make our method more desirable in various situations. We note that our method allows for our monitors to be swapped out with alternate monitors with fairly minimal user effort. Finally, our method ties in with our existing tool, BehaVerify, allowing for the verification of BTs with monitors.

Figures (9)

• Figure 1: Example Leaf and Decorator Nodes.
• Figure 2: A $\mathit{BT}$ consisting of a sequence node (a) with two actions (b, d) and a check (c). We use the ternary operator $i?j:k$ to mean if $i$ then $j$ else $k$. Tick indicates the number of times the tree has been ticked. At each timestep $t$, the variable $x$ is updated based on the active node. If a node is finished, then it returns one of $\mathit{S}$, $\mathit{F}$, or $\mathit{R}$.
• Figure 3: Diagram of how BehaVerify generates Python code for $\mathit{BT}$s with monitors. LTL2BA is a tool for converting an LTL specification to a $BA$. Spin is a model checker, and a Never Claim can be checked using Spin. Solid blue arrows mark new contributions.
• Figure 4: Diagram of how BehaVerify generates .smv files for $\mathit{BT}$s with monitors that can be verified using nuXmv. LTL2BA is a tool for converting an LTL specification to a $BA$. Spin is a model checker, and a Never Claim can be checked using Spin. Solid blue arrows mark new contributions.
• Figure 5: Images representing some of the grids used for the scaling experiments. The upper grids are sparse and were randomly generated. The lower grids are dense and were created by copying a 5 by 5 grid repeatedly. The left grids are 10 by 10 and the right grids are 50 by 50. Black squares are obstacles, the blue square is the drone, and the green square is the destination.