A Lazy Abstraction Algorithm for Markov Decision Processes: Theory and Initial Evaluation

TL;DR

This paper introduces a lazy abstraction algorithm for Markov Decision Processes that combines adaptive simulation graphs with BRTDP, aiming to improve efficiency in state space exploration and verification.

Contribution

The paper proposes a novel lazy abstraction method for MDPs that selectively refines the state space, enhancing partial exploration techniques like BRTDP.

Findings

Initial experiments show improved state space merging.

The method reduces computational complexity.

Combines lazy abstraction with BRTDP effectively.

Abstract

Analysis of Markov Decision Processes (MDP) is often hindered by state space explosion. Abstraction is a well-established technique in model checking to mitigate this issue. This paper presents a novel lazy abstraction method for MDP analysis based on adaptive simulation graphs. Refinement is performed only when new parts of the state space are explored, which makes partial exploration techniques like Bounded Real-Time Dynamic Programming (BRTDP) retain more merged states. Therefore, we propose a combination of lazy abstraction and BRTDP. To evaluate the performance of our algorithm, we conduct initial experiments using the Quantitative Verification Benchmark Set.