The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates -- lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.

翻译：人工设计的模型检验器等形式化验证软件中可能存在的错误，对这些工具的根本目的构成了严重威胁。缓解该问题的成熟方法是采用证明——即对验证结果提供轻量级且易于检验的证明。本文针对具有定量可达性和期望奖励性质的马尔可夫决策过程（MDPs）模型检验，提出了一种新型证明方法。我们的方法概念简洁，几乎完全基于基本定点理论。所提出的证明适用于任意有限MDPs，并可通过标准算法以极小开销直接计算。我们在Isabelle/HOL中形式化证明了该证明方法的可靠性，并提供了经过形式化验证的证明检查器。此外，我们为概率模型检验器Storm中的现有算法增加了证明生成功能，并通过在定量验证基准集中首次完成参考结果的形式化认证，证明了该方法的实际适用性。