为行为树设计可运行时修正错误的监控器，支持LTL规范验证。
Verification of Behavior Trees with Contingency Monitors
- 基于LTL规范生成行为树运行时监控器，实现动态纠错。
- 生成监控器的运行开销与现有工具相当，性能稳定。
- 可轻松替换为其他监控器，适合集成到BehaVerify中使用。
行为树（BTs）作为高层控制器在机器人任务中广泛应用。随着其使用范围扩大，确保其按预期工作至关重要。为此，我们提出一种新方法，用于生成行为树的运行时监控器。这些监控器可在检测到不良行为时进行纠正，并能处理LTL规格说明。实验表明，生成的监控器在运行时间上与现有工具相当，且具备若干优势，使其在多种场景下更具实用性。此外，该方法支持以较低用户成本更换为其他监控器。最后，该方法与我们现有的工具BehaVerify无缝集成，实现了对行为树的带监控验证。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。