Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks

要約

最近、線形時間論理 (LTL) によって捕捉される複雑なミッションを担う、未知の確率的ダイナミクスを備えた自律エージェントのニューラル ネットワーク (NN) コントローラーを学習するためのいくつかの方法が提案されています。
これらの作業の大部分はサンプル効率が悪いため、LTL 仕様をより小さなサブタスクに分解する構成学習方法が提案されています。
次に、元のタスクを満たすために個別のコントローラーが学習および構成されます。
これらのアプローチの主な課題は、多くの場合、安全性の保証が欠けているか、提供される保証が非実用的であることです。
この文書は、この課題に対処することを目的としています。
特に、未知の確率的ダイナミクスと LTL エンコードされたタスクを備えた自律システムを考慮します。
システムには、訓練された NN フィードバック コントローラーによってモデル化された基本スキルの有限セットが装備されていると仮定します。
私たちの目標は、トレーニングされた NN コントローラーの時間的構成が存在するかどうかを確認し、存在する場合はそれを計算し、割り当てられた LTL タスクを確率 1 で満たす複合システムの動作を生成することです。
我々は、オートマトン理論と NN 制御の確率システム向けのデータ駆動型到達可能性分析ツールの新しい統合に依存する新しいアプローチを提案します。
結果として得られるニューロシンボリック コントローラーにより、エージェントはその基本スキルを活用して、目に見えない複雑な時相論理タスクに対する安全な動作をゼロショット方式で生成できます。
提案された方法の正しさを示し、それが完了するための条件を提供します。
私たちの知る限り、これは未知の確率システムに対する NN コントローラーの検証済みの時間構成を設計した最初の研究です。
最後に、提案された方法を実証するために、ロボット ナビゲーション タスクに関する広範な数値シミュレーションとハードウェア実験を提供します。

要約(オリジナル)

Several methods have been proposed recently to learn neural network (NN) controllers for autonomous agents, with unknown and stochastic dynamics, tasked with complex missions captured by Linear Temporal Logic (LTL). Due to the sample-inefficiency of the majority of these works, compositional learning methods have been proposed decomposing the LTL specification into smaller sub-tasks. Then, separate controllers are learned and composed to satisfy the original task. A key challenge within these approaches is that they often lack safety guarantees or the provided guarantees are impractical. This paper aims to address this challenge. Particularly, we consider autonomous systems with unknown and stochastic dynamics and LTL-encoded tasks. We assume that the system is equipped with a finite set of base skills modeled by trained NN feedback controllers. Our goal is to check if there exists a temporal composition of the trained NN controllers – and if so, to compute it – that will yield a composite system behavior that satisfies the assigned LTL task with probability one. We propose a new approach that relies on a novel integration of automata theory and data-driven reachability analysis tools for NN-controlled stochastic systems. The resulting neuro-symbolic controller allows the agent to generate safe behaviors for unseen complex temporal logic tasks in a zero-shot fashion by leveraging its base skills. We show correctness of the proposed method and we provide conditions under which it is complete. To the best of our knowledge, this is the first work that designs verified temporal compositions of NN controllers for unknown and stochastic systems. Finally, we provide extensive numerical simulations and hardware experiments on robot navigation tasks to demonstrate the proposed method.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google