1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization

要約

確率的モデルチェックの進歩にもかかわらず、検証方法のスケーラビリティは限られたままです。
特に、中程度の値であっても、パラメーター化されたマルコフ決定プロセス（MDP）をインスタンス化すると、状態空間が非常に大きくなることがよくあります。
そのような\ emph {巨大} MDPの合成ポリシーは、利用可能なツールの範囲を超えています。
このような巨大なMDPの合理的なポリシーを取得するための学習ベースのアプローチを提案します。
アイデアは、意思決定ツリー学習を使用して、小さなインスタンスを大規模なインスタンスにモデルチェックすることによって得られる最適なポリシーを一般化することです。
その結果、私たちの方法は、大規模なモデルの明示的な状態空間探索の必要性を回避し、状態空間爆発問題の実用的な解決策を提供します。
定量的検証ベンチマークセットから関連するモデルで広範な実験を実行することにより、アプローチの有効性を実証します。
実験結果は、モデルのサイズが最先端の分析ツールの範囲を超えて数桁である場合でも、ポリシーがうまく機能することを示しています。

要約(オリジナル)

Despite the advances in probabilistic model checking, the scalability of the verification methods remains limited. In particular, the state space often becomes extremely large when instantiating parameterized Markov decision processes (MDPs) even with moderate values. Synthesizing policies for such \emph{huge} MDPs is beyond the reach of available tools. We propose a learning-based approach to obtain a reasonable policy for such huge MDPs. The idea is to generalize optimal policies obtained by model-checking small instances to larger ones using decision-tree learning. Consequently, our method bypasses the need for explicit state-space exploration of large models, providing a practical solution to the state-space explosion problem. We demonstrate the efficacy of our approach by performing extensive experimentation on the relevant models from the quantitative verification benchmark set. The experimental results indicate that our policies perform well, even when the size of the model is orders of magnitude beyond the reach of state-of-the-art analysis tools.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google