Efficient Strategy Synthesis for MDPs via Hierarchical Block Decomposition
This provides a more efficient solution for real-world policy synthesis in software-intensive systems like robotics, though it is incremental as it builds on existing MDP methods.
The paper tackles the problem of scaling policy synthesis in large Markov decision processes (MDPs) by introducing a hierarchical block decomposition method that dynamically refines fragile regions, resulting in performance improvements of up to 2x compared to PRISM on MDPs with up to 1 million states.
Software-intensive systems, such as software product lines and robotics, utilise Markov decision processes (MDPs) to capture uncertainty and analyse sequential decision-making problems. Despite the usefulness of conventional policy synthesis methods, they fail to scale to large state spaces. Our approach addresses this issue and accelerates policy synthesis in large MDPs by dynamically refining the MDP and iteratively selecting the most fragile MDP regions for refinement. This iterative procedure offers a balance between accuracy and efficiency, as refinement occurs only when necessary. Through a comprehensive empirical evaluation comprising diverse case studies and MDPs up to 1M states, we demonstrate significant performance improvements yielded by our approach compared to the leading probabilistic model checker PRISM (up to 2x), thus offering a very competitive solution for real-world policy synthesis tasks in larger MDPs.