Designing Behavior Trees from Goal-Oriented LTLf Formulas

要約

時間論理を使用して自律エージェントの目標を正式に指定することはできますが、目標の満足を保証するプランナーを合成するには、計算量が法外に多くなる可能性があります。
このペーパーでは、有限トレースの線形時間論理 (LTL) のサブセットを使用して指定された目標を、成功したトレースが LTL の目標を満たすことを保証するビヘイビア ツリー (BT) に変換する方法を示します。
達成目標に役立つ LTL 式は、達成指向のタスク ミッション文法を使用して導き出すことができ、LTL 演算子を使用して結合されたタスクで構成されるミッションにつながります。
LTL 式から BT を構築すると、幅広いプランナーが BT にアクション ノードを実装できる、緩和された動作合成問題が生じます。
重要なのは、プランナーによって誘導された成功したトレースは、対応する LTL 式を満たしていることです。
このアプローチの有用性は 2 つの方法で実証されます。a) 2 人のプランナーと LTL 目標の間の整合性を調査すること、および b) フェッチ ロボットの連続キードア問題を解決することです。

要約(オリジナル)

Temporal logic can be used to formally specify autonomous agent goals, but synthesizing planners that guarantee goal satisfaction can be computationally prohibitive. This paper shows how to turn goals specified using a subset of finite trace Linear Temporal Logic (LTL) into a behavior tree (BT) that guarantees that successful traces satisfy the LTL goal. Useful LTL formulas for achievement goals can be derived using achievement-oriented task mission grammars, leading to missions made up of tasks combined using LTL operators. Constructing BTs from LTL formulas leads to a relaxed behavior synthesis problem in which a wide range of planners can implement the action nodes in the BT. Importantly, any successful trace induced by the planners satisfies the corresponding LTL formula. The usefulness of the approach is demonstrated in two ways: a) exploring the alignment between two planners and LTL goals, and b) solving a sequential key-door problem for a Fetch robot.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google