Verification of Behavior Trees with Contingency Monitors

TL;DR

This paper introduces a new methodology for creating runtime monitors for Behavior Trees that can detect and correct undesirable behaviors, handle LTL specifications, and integrate with existing verification tools.

Contribution

The paper presents a novel approach to generate runtime monitors for Behavior Trees, enabling correction of behaviors and compatibility with LTL specifications, enhancing verification and reliability.

Findings

Monitors perform comparably to existing tools in runtime.

The method allows easy swapping of monitors with minimal user effort.

Integration with BehaVerify facilitates BT verification with monitors.

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.