在 Event-B 中验证行为树的安全性
机器人学
2022-09-29 v1 人工智能
摘要
行为树（Behavior Trees, BT）在机器人学界日益流行。BT 工具非常适用于决策应用，使机器人能够执行复杂行为，同时也便于人类理解。验证所用 BT 针对安全性与可靠性需求是否构建良好至关重要，尤其对于在关键环境中运行的机器人。在本工作中，我们提出行为树的形式化规约以及一种证明已用树不变量的方法，同时为最终用户保持树形式化的简洁性。允许测试行为树的特定实例而无需了解形式化更抽象的层次。
引用
@article{arxiv.2209.14045,
title = {Verifying Safety of Behaviour Trees in Event-B},
author = {Matteo Tadiello and Elena Troubitsyna},
journal= {arXiv preprint arXiv:2209.14045},
year = {2022}
}
备注
In Proceedings FMAS2022 ASYDE2022, arXiv:2209.13181