BehaVerify：验证行为树的时序逻辑规约
机器人学
2024-02-21 v2
摘要
行为树起源于电子游戏中对 NPC 的控制方法，但此后在机器人学界获得关注，是一种描述任务执行的框架。BehaVerify 是一个从 py_tree 创建 nuXmv 模型的工具。对于标准化的复合节点，该过程是自动的，无需额外用户输入。多种叶节点被自动支持且无需额外用户输入，但自定义叶节点需要额外用户输入才能被正确建模。BehaVerify 可提供模板以简化此过程。BehaVerify 能够创建具有超过 100 个节点的 nuXmv 模型，且 nuXmv 能够在该模型上验证各种非平凡的 LTL 性质，包括直接验证与通过反例验证。所述模型具有并行节点、选择节点与序列节点。与基于 BTCompiler 的模型比较表明，BehaVerify 创建的模型性能更优。
引用
@article{arxiv.2208.05360,
title = {BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees},
author = {Serena S. Serbinowska and Taylor T. Johnson},
journal= {arXiv preprint arXiv:2208.05360},
year = {2024}
}