Scalable Verification of Markov Decision Processes
This addresses the scalability problem for researchers and practitioners in concurrent process optimization, though it appears incremental as it builds on existing approximative approaches.
The paper tackled the intractability of verifying Markov decision processes (MDPs) by introducing a scalable method using an O(1) memory representation for history-dependent schedulers, enabling the use of scalable learning techniques and massively parallel verification.
Markov decision processes (MDP) are useful to model concurrent process optimisation problems, but verifying them with numerical methods is often intractable. Existing approximative approaches do not scale well and are limited to memoryless schedulers. Here we present the basis of scalable verification for MDPSs, using an O(1) memory representation of history-dependent schedulers. We thus facilitate scalable learning techniques and the use of massively parallel verification.