A formal implementation of Behavior Trees to act in robotics

要約

行動ツリー（BT）は、自律的なロボットシステムの作用コンポーネントとして非常に人気があります。
これらのBTが実行される間にランタイム検証と同様に、BTで書かれたプログラムの検証を実行できるようにする正式な言語にそれらを変換することにより、BTに正式なセマンティクスを定義することを提案します。
これにより、BTプログラマーが正式な言語を習得することを要求することなく、モジュール性、柔軟性、および再利用性などの最も貴重な機能を侵害することなく、BT正確性を正式に検証できます。
使用する正式なフレームワークを紹介します。
Tina、そのモデルチェックツールとHippo、ランタイム検証エンジン。
次に、BTからFiacreへの翻訳が自動的にどのように行われるか、オフラインで確認できる正式なLTLおよびCTLプロパティのタイプ、および通常のBTエンジンの代わりにオンラインで正式なモデルを実行する方法を示します。
2つのRoboticsアプリケーションでアプローチを説明し、FAIARの正式なフレームワーク（状態変数、時間など）で利用可能な他の機能にBTがどのように利益をもたらすことができるかを示します。

要約(オリジナル)

Behavior Trees (BT) are becoming quite popular as an Acting component of autonomous robotic systems. We propose to define a formal semantics to BT by translating them to a formal language which enables us to perform verification of programs written with BT, as well as runtime verification while these BT execute. This allows us to formally verify BT correctness without requiring BT programmers to master formal language and without compromising BT most valuable features: modularity, flexibility and reusability. We present the formal framework we use: Fiacre, its langage and the produced TTS model; Tina, its model checking tools and Hippo, its runtime verification engine. We then show how the translation from BT to Fiacre is automatically done, the type of formal LTL and CTL properties we can check offline and how to execute the formal model online in place of a regular BT engine. We illustrate our approach on two robotics applications, and show how BT could benefit of other features available in the Fiacre formal framework (state variables, time, etc).

arxiv情報

提供元, 利用サービス

arxiv.jp, Google