Learning Algorithms for Verification of Markov Decision Processes

要約

学習アルゴリズムとヒューリスティック ガイダンスをマルコフ意思決定プロセス (MDP) の検証に適用するための一般的なフレームワークを紹介します。
私たちの技術の主な目的は、状態空間の徹底的な探索を回避し、代わりにヒューリスティックに基づいてシステムの特に関連する領域に焦点を当てることでパフォーマンスを向上させることです。
私たちの研究は、Br{\'{a}}zdil らの以前の結果に基づいており、それを大幅に拡張するとともに、いくつかの詳細を改良し、エラーを修正しています。
提示されたフレームワークは、検証における中心的な問題である確率的到達可能性に焦点を当てており、2 つの異なるシナリオでインスタンス化されます。
1 つ目は、MDP の完全な知識、特に正確な遷移確率が利用可能であることを前提としています。
ヒューリスティックに基づいてモデルの部分探索を実行し、必要な確率の正確な下限と上限を生成します。
2 つ目は、正確な遷移ダイナミクスを知らずに MDP をサンプリングするだけの場合に取り組みます。
ここでも、下限と上限の両方に関して確率的な保証が得られ、近似の効率的な停止基準が提供されます。
特に、後者は、MDP の無制限プロパティに対する統計モデル検査 (SMC) の拡張です。
他の関連アプローチとは対照的に、私たちは時間制限のある (有限地平線) プロパティや割引されたプロパティに注意を限定したり、MDP の特定の構造プロパティを想定したりしません。

要約(オリジナル)

We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{\'{a}}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google