This presentation introduces our ongoing work on a novel lazy abstraction technique for Markov Decision Process (MDP) analysis using adaptive simulation graphs. Lazy abstraction is an abstraction technique that combines exploring the abstract state space and refining it into a single process, refining only parts of the state space on demand. As this has good synergies with partial state-space exploration techniques, we also propose combining our lazy abstraction algorithm and Bounded Real-Time Dynamic Programming to compute the numerical information on the fly while constructing the abstraction. It was presented at the Alpine Verification Meeting 2023.

September 26, 2023