Scalable Verification of Markov Decision Processes
Legay, Axel;Sedwards, Sean;Traonouez, Louis-Marie
(2014) 4th Workshop on Formal Methods in the Development of Software (FMDS 2014) (2.September.2014)
Files
No attached file found for this publication.
Details
Authors
Legay, AxelUCLouvain
Author
Sedwards, Sean
Author
Traonouez, Louis-Marie
Author
Abstract
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 MDPs, using an O(1) memory representation of history-dependent schedulers. We thus facilitate scalable learning techniques and the use of massively parallel verification.
Legay, A., Sedwards, S., & Traonouez, L.-M. (2014). Scalable Verification of Markov Decision Processes. 4th Workshop on Formal Methods in the Development of Software (FMDS 2014). https://hdl.handle.net/2078.5/172936