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
4th Workshop on Formal Methods in the Development of Software (FMDS 2014), Sep 2014, Grenoble, France. 2014, Lecture Notes in Computer Science
Liste complète des métadonnées

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-01088396
Contributor : Sean Sedwards <>
Submitted on : Thursday, November 27, 2014 - 8:23:46 PM
Last modification on : Friday, November 16, 2018 - 1:39:28 AM
Document(s) archivé(s) le : Monday, March 2, 2015 - 9:31:37 AM

File

LegaySedwardsTraonouez2014.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01088396, version 1

Citation

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. 2014, Lecture Notes in Computer Science. 〈hal-01088396〉

Share

Metrics

Record views

505

Files downloads

76