  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.
