On Behavior Trees and their Verification

Abstract

Behavior trees are high level controllers that have gained popularity in a variety of safety critical domains such as robotics and medicine. Because of this, it is important that we be able to formally verify that behavior trees work as intended. To that end, we created a formal model for behavior trees called stateful behavior trees. A stateful behavior trees includes a behavior tree and the environment that behavior tree operates in. Furthermore, we created a tool named BehaVerify for the verification of stateful behavior trees. BehaVerify takes as input a stateful behavior tree specified using a domain specific language we created. The domain specific language allows for the use of invariant specifications, linear temporal logic specifications, and computation tree logic specifications. As output, BehaVerify produces a model for verification with nuXmv, a Python implementation, or a Haskell implementation. We compare BehaVerify against various competing tools and find that BehaVerify generally outperforms. We have expanded BehaVerify to use contingency runtime monitors. To create a contingency runtime monitor, a linear temporal logic specification is included in the input. Additionally, actions to be taken in the case of a violation are also included; this allows the behavior tree to respond to violations. With the rising power and popularity of neural networks, it is also important to be able to handle behavior trees that use neural networks. To that end, we expanded BehaVerify to handle neuro-symbolic behavior trees. We tested BehaVerify on neuro-symbolic behavior trees navigating a complex grid world environment and on a simplified version of ACASXu, an aircraft collision avoidance system. In the case of ACASXu, we verified a neuro-symbolic behavior tree that made use of 5 neural networks, each of which had 6 layers of 50 neurons each. We included a comparison of various methods to encode the neural networks in nuXmv.