Fixed Point Certificates for Reachability and Expected Rewards in MDPs
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912196432232448 |
|---|---|
| author | Chatterjee, Krishnendu Quatmann, Tim Schäffeler, Maximilian Weininger, Maximilian Winkler, Tobias Zilken, Daniel |
| author_facet | Chatterjee, Krishnendu Quatmann, Tim Schäffeler, Maximilian Weininger, Maximilian Winkler, Tobias Zilken, Daniel |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_11467 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Fixed Point Certificates for Reachability and Expected Rewards in MDPs Chatterjee, Krishnendu Quatmann, Tim Schäffeler, Maximilian Weininger, Maximilian Winkler, Tobias Zilken, Daniel Logic in Computer Science Discrete Mathematics Systems and Control 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. |
| title | Fixed Point Certificates for Reachability and Expected Rewards in MDPs |
| topic | Logic in Computer Science Discrete Mathematics Systems and Control |
| url | https://arxiv.org/abs/2501.11467 |