What Are the Odds? Improving the foundations of Statistical Model Checking

要約

マルコフ決定プロセス（MDP）は、不確実性の下での意思決定の基本的なモデルです。
それらは、非決定的な選択と確率的不確実性を示します。
従来、検証アルゴリズムは、MDPの動作を支配する確率の正確な知識を想定しています。
この仮定は実際には非現実的であることが多いため、過去20年間に統計モデルチェック（SMC）が開発されました。
未知の遷移確率でMDPを分析し、結果にほぼ正しい（PAC）保証を提供することができます。
モデルベースのSMCアルゴリズムは、MDPをサンプルし、すべての遷移確率を推定することにより、「オッズとは何か」という質問に答えるすべての移行の確率を推定することにより、そのモデルを構築します。しかし、これまでのところ、ART SMCアルゴリズムで採用されている統計的方法は非常に重要です。
私たちの貢献は、これらの方法に対するいくつかの根本的な改善です。一方で、統計学の文献を調査し、集中の不平等を改善します。
一方、MDPの知識を活用する専門的なアプローチを提案します。
私たちの改善は、一般的に多くの種類の問題ステートメントに適用されます。なぜなら、それらは設定から​​大きく独立しているからです。
さらに、実験的評価は、それらが大幅に利益をもたらし、SMCアルゴリズムが収集しなければならないサンプルの数を最大2桁削減することを示しています。

要約(オリジナル)

Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. As this assumption is often unrealistic in practice, statistical model checking (SMC) was developed in the past two decades. It allows to analyse MDPs with unknown transition probabilities and provide probably approximately correct (PAC) guarantees on the result. Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: “What are the odds?” However, so far the statistical methods employed by the state of the art SMC algorithms are quite naive. Our contribution are several fundamental improvements to those methods: On the one hand, we survey statistics literature for better concentration inequalities; on the other hand, we propose specialised approaches that exploit our knowledge of the MDP. Our improvements are generally applicable to many kinds of problem statements because they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that the SMC algorithm has to collect by up to two orders of magnitude.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google