Learning Optimal Strategies for Temporal Tasks in Stochastic Games

要約

線形時相論理 (LTL) 仕様からの合成により、確率的環境や潜在的に敵対的な環境で動作するシステムに確実なコントローラーが提供されます。
ただし、自動合成ツールでは、コントローラーを構築するために環境のモデルが必要です。
この研究では、環境が完全に未知の場合でも、与えられた LTL 仕様からコントローラーを導出するモデルフリー強化学習 (RL) アプローチを導入します。
私たちは、コントローラーと敵対的環境の間の確率的ゲーム (SG) として問題をモデル化します。
次に、最悪の環境動作に対して LTL 仕様を満たす確率を最大化する最適な制御戦略を学習します。
まず、指定された LTL 仕様から変換された決定論的パリティ オートマトン (DPA) を使用してプロダクト ゲームを構築します。
DPA の受け入れ条件から個別の報酬と割引係数を導き出すことで、LTL 仕様を満たす最悪の場合の確率の最大化を、製品ゲームにおける割引報酬目標の最大化に削減します。
これにより、モデルフリーの RL アルゴリズムを使用して、最適なコントローラー戦略を学習できるようになります。
DPA の受け入れ条件 (通常は色と呼ばれる) を定義するセットの数が多い場合の一般的なスケーラビリティの問題に対処するために、個別の報酬と割引係数が必要な場合にのみ利用される遅延カラー生成方法を提案します。
コントローラーが最終的に 1 つの色のみに焦点を当てる近似的な方法。
いくつかのケーススタディでは、私たちのアプローチが広範囲の LTL 式に拡張可能であり、SG の LTL 仕様からコントローラーを学習する既存の方法よりも大幅に優れていることを示しています。

要約(オリジナル)

Synthesis from linear temporal logic (LTL) specifications provides assured controllers for systems operating in stochastic and potentially adversarial environments. Automatic synthesis tools, however, require a model of the environment to construct controllers. In this work, we introduce a model-free reinforcement learning (RL) approach to derive controllers from given LTL specifications even when the environment is completely unknown. We model the problem as a stochastic game (SG) between the controller and the adversarial environment; we then learn optimal control strategies that maximize the probability of satisfying the LTL specifications against the worst-case environment behavior. We first construct a product game using the deterministic parity automaton (DPA) translated from the given LTL specification. By deriving distinct rewards and discount factors from the acceptance condition of the DPA, we reduce the maximization of the worst-case probability of satisfying the LTL specification into the maximization of a discounted reward objective in the product game; this enables the use of model-free RL algorithms to learn an optimal controller strategy. To deal with the common scalability problems when the number of sets defining the acceptance condition of the DPA (usually referred as colors), is large, we propose a lazy color generation method where distinct rewards and discount factors are utilized only when needed, and an approximate method where the controller eventually focuses on only one color. In several case studies, we show that our approach is scalable to a wide range of LTL formulas, significantly outperforming existing methods for learning controllers from LTL specifications in SGs.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google