要約
ビヘイビア ツリーは、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.
arxiv情報
| 著者 | Serena S. Serbinowska,Taylor T. Johnson |
| 発行日 | 2024-02-20 05:07:18+00:00 |
| arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google