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.
Type de document :
Communication dans un congrès
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

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01088396
Contributeur : Sean Sedwards <>
Soumis le : jeudi 27 novembre 2014 - 20:23:46
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:31:37

Fichier

LegaySedwardsTraonouez2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

455

Téléchargements de fichiers

60