Fixed Point Certificates for Reachability and Expected Rewards in MDPs
Krishnendu Chatterjee, Tim Quatmann, Maximilian Sch\"affeler,, Maximilian Weininger, Tobias Winkler, Daniel Zilken

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
