形式化无状态行为树
机器人学
2024-11-22 v1
摘要
行为树（Behavior Trees, BTs）是一种高层次控制器，在各种规划任务中具有广泛应用前景，并在机器人任务规划中日益受到关注。随着其在安全关键领域的流行，对于形式化其语法和语义以及验证其属性至关重要。本文我们提出了一类称为无状态行为树（Stateful Behavior Trees, SBTs）的行为树，该类行为树包含额外变量，并在随时间可能变化的环境中运行。SBTs 能够访问持久的共享内存（常称为黑板），用于跟踪这些额外变量。我们展示，当黑板能够存储数学（即无限）整数时，SBTs 的计算能力等价于图灵机。我们进一步识别了若干语法假设条件下，SBTs 的计算能力等价于有限状态自动机，具体条件为额外变量为有限类型。我们提出了一种用于编写 SBTs 的领域特定语言（DSL），并改造了工具 BehaVerify 以适用于该 DSL。该新的 BehaVerify DSL 支持与 Python 中流行的行为树库进行接口，同时提供 Haskell 代码和 nuXmv 模型的生成，后者用于对 SBTs 的时序逻辑规范进行模型检查。我们包含示例和可扩展性结果，表明 BehaVerify 在验证效率上超过另一款工具 100 倍。
引用
@article{arxiv.2411.14165,
title = {Formalizing Stateful Behavior Trees},
author = {Serena S. Serbinowska and Preston Robinette and Gabor Karsai and Taylor T. Johnson},
journal= {arXiv preprint arXiv:2411.14165},
year = {2024}
}
备注
In Proceedings FMAS2024, arXiv:2411.13215