Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes
This work provides formally verified solution methods for MDPs, addressing reliability concerns in critical applications, though it represents an incremental advance by building on existing formalizations.
The authors formally verified executable algorithms for solving infinite-horizon Markov decision processes using the Isabelle/HOL theorem prover, building on existing probability theory formalizations to analyze expected total reward and verify dynamic programming methods. They demonstrated practical performance on standard problems and showed that combining verified implementations with efficient unverified components can compete with or outperform state-of-the-art systems.
We formally verify executable algorithms for solving Markov decision processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on existing formalizations of probability theory to analyze the expected total reward criterion on infinite-horizon problems. Our developments formalize the Bellman equation and give conditions under which optimal policies exist. Based on this analysis, we verify dynamic programming algorithms to solve tabular MDPs. We evaluate the formally verified implementations experimentally on standard problems and show they are practical. Furthermore, we show that, combined with efficient unverified implementations, our system can compete with and even outperform state-of-the-art systems.