论文标题
behaverify：验证行为树的时间逻辑规格
BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees
论文作者
论文摘要
行为树起源于视频游戏，是一种控制NPC的方法，但此后在机器人社区中获得了吸引力，它是描述执行任务的框架。 Behaverify是一种从PY_TREE创建NUXMV模型的工具。对于标准化的复合节点，此过程是自动的，不需要其他用户输入。自动支持各种叶子节点，不需要其他用户输入，但是自定义的叶节点将需要其他用户输入才能正确建模。 Behaverify可以提供一个模板以使其更容易。 Behaverify能够创建具有100多个节点的NUXMV模型，NUXMV能够直接和通过反例来验证该模型上的各种非平凡LTL属性。有问题的模型具有并行节点，选择器和序列节点。与基于BTCompiler的模型的比较表明，由Behaverify创建的模型表现更好。
Behavior Trees, which originated in video games as a method for controlling NPCs but have since gained traction within the robotics community, are a framework for describing the execution of a task. BehaVerify is a tool that creates a nuXmv model from a py_tree. For composite nodes, which are standardized, this process is automatic and requires no additional user input. A wide variety of leaf nodes are automatically supported and require no additional user input, but customized leaf nodes will require additional user input to be correctly modeled. BehaVerify can provide a template to make this easier. BehaVerify is able to create a nuXmv model with over 100 nodes and nuXmv was able to verify various non-trivial LTL properties on this model, both directly and via counterexample. The model in question features parallel nodes, selector, and sequence nodes. A comparison with models based on BTCompiler indicates that the models created by BehaVerify perform better.
