Fixed Point Certificates for Reachability and Expected Rewards in MDPs

TL;DR

This paper introduces fixed point certificates for verifying reachability and expected rewards in finite Markov decision processes, enhancing reliability through formal verification and practical certification methods.

Contribution

It presents novel, elementary fixed point-based certificates for MDP verification, formalized in Isabelle/HOL, and integrates them into existing tools for practical certification.

Findings

Certificates are sound and formally verified.

Implementation in Storm enables practical certification.

First formal certification of Quantitative Verification Benchmark results.

Abstract

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.