Formalizing Stateful Behavior Trees

要約

ビヘイビア ツリー (BT) は、さまざまな計画タスクに役立つ高レベルのコントローラーであり、ロボットのミッション計画において注目を集めています。
安全性が重要な領域で人気が高まるにつれて、その構文とセマンティクスを形式化し、そのプロパティを検証することが重要です。
この論文では、補助変数を持ち、時間の経過とともに変化する可能性のある環境で動作するステートフル ビヘイビア ツリー (SBT) と呼ばれる BT のクラスを形式化します。
SBT は、これらの補助変数を追跡する永続的な共有メモリ (ブラックボードとして知られることが多い) にアクセスできます。
我々は、黒板が数学的（つまり、無制限の）整数を格納できる場合、SBT の計算能力がチューリング マシンと同等であることを実証します。
さらに、SBT が有限状態オートマトンと同等の計算能力を持つ場合、特に補助変数が有限型である場合の構文上の仮定を特定します。
私たちは SBT を記述するためのドメイン固有言語 (DSL) を提供し、この DSL で使用できるようにツール BehaVerify を適合させます。
BehaVerify のこの新しい DSL は、Python の一般的な BT ライブラリとのインターフェイスをサポートし、Haskell コードと nuXmv モデルの生成も提供します。nuXmv モデルは、SBT の時相論理仕様のモデル チェックに使用されます。
BehaVerify が他の検証ツールを 100 倍上回るパフォーマンスを示す例とスケーラビリティの結果が含まれています。

要約(オリジナル)

Behavior Trees (BTs) are high-level controllers that are useful in a variety of planning tasks and are gaining traction in robotic mission planning. As they gain popularity in safety-critical domains, it is important to formalize their syntax and semantics, as well as verify properties for them. In this paper, we formalize a class of BTs we call Stateful Behavior Trees (SBTs) that have auxiliary variables and operate in an environment that can change over time. SBTs have access to persistent shared memory (often known as a blackboard) that keeps track of these auxiliary variables. We demonstrate that SBTs are equivalent in computational power to Turing Machines when the blackboard can store mathematical (i.e., unbounded) integers. We further identify syntactic assumptions where SBTs have computational power equivalent to finite state automata, specifically where the auxiliary variables are of finitary types. We present a domain specific language (DSL) for writing SBTs and adapt the tool BehaVerify for use with this DSL. This new DSL in BehaVerify supports interfacing with popular BT libraries in Python, and also provides generation of Haskell code and nuXmv models, the latter of which is used for model checking temporal logic specifications for the SBTs. We include examples and scalability results where BehaVerify outperforms another verification tool by a factor of 100.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google