Scholarlink

<p>Computing reachability probabilities and expected rewards for Markov decision processes is a core feature of probabilistic model checkers. Value iteration (VI) is the predominantly implemented approach but occasionally yields vastly incorrect results. Interval iteration (II), sound value iteration (SVI), and optimistic value iteration (OVI) are recently proposed variants of VI that produce sound approximations of the desired values. Hartmanns and Kaminski (CAV (2), pp.&#xa0;488–511, <CitationRef CitationID="CR9">2020</CitationRef>) empirically compared the three approaches using implementations in the model checker <span>mcsta</span> and a broad selection of benchmarks. They concluded that OVI is faster than II and SVI for the majority of instances. We replicate these research results using implementations in the model checker <span>Storm</span>. The key insight is that OVI still mostly outperforms II and SVI, but the competition becomes tighter.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

What is the best algorithm for MDP model checking?

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年5月13日

查看全文
  • Tim Quatmann

摘要

Computing reachability probabilities and expected rewards for Markov decision processes is a core feature of probabilistic model checkers. Value iteration (VI) is the predominantly implemented approach but occasionally yields vastly incorrect results. Interval iteration (II), sound value iteration (SVI), and optimistic value iteration (OVI) are recently proposed variants of VI that produce sound approximations of the desired values. Hartmanns and Kaminski (CAV (2), pp. 488–511, 2020) empirically compared the three approaches using implementations in the model checker mcsta and a broad selection of benchmarks. They concluded that OVI is faster than II and SVI for the majority of instances. We replicate these research results using implementations in the model checker Storm. The key insight is that OVI still mostly outperforms II and SVI, but the competition becomes tighter.