Skip to Main content Skip to Navigation
Conference papers

Scalable Verification of Markov Decision Processes

Axel Legay 1 Sean Sedwards 1 Louis-Marie Traonouez 1 
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Sean Sedwards Connect in order to contact the contributor
Submitted on : Thursday, November 27, 2014 - 8:23:46 PM
Last modification on : Thursday, January 20, 2022 - 5:33:25 PM
Long-term archiving on: : Monday, March 2, 2015 - 9:31:37 AM


Files produced by the author(s)


  • HAL Id : hal-01088396, version 1


Axel Legay, Sean Sedwards, Louis-Marie Traonouez. Scalable Verification of Markov Decision Processes. 4th Workshop on Formal Methods in the Development of Software (FMDS 2014), Sep 2014, Grenoble, France. ⟨hal-01088396⟩



Record views


Files downloads