Lightweight Verification of Markov Decision Processes with Rewards

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 are useful models of concurrency optimisation problems, but are often intractable for exhaustive verification methods. Recent work has introduced lightweight approximative techniques that sample directly from scheduler space, bringing the prospect of scalable alternatives to standard numerical algorithms. The focus so far has been on optimising the probability of a property, but many problems require quantitative analysis of rewards. In this work we therefore present lightweight verification algorithms to optimise the rewards of Markov decision processes. We provide the statistical confidence bounds that this necessitates and demonstrate our approach on standard case studies.
Type de document :
Rapport
[Research Report] INRIA Rennes - Bretagne Atlantique. 2014
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01088684
Contributeur : Sean Sedwards <>
Soumis le : vendredi 28 novembre 2014 - 14:02:31
Dernière modification le : mardi 16 janvier 2018 - 15:54:23
Document(s) archivé(s) le : vendredi 14 avril 2017 - 23:09:07

Fichier

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

Identifiants

  • HAL Id : hal-01088684, version 1

Citation

Axel Legay, Sean Sedwards, Louis-Marie Traonouez. Lightweight Verification of Markov Decision Processes with Rewards. [Research Report] INRIA Rennes - Bretagne Atlantique. 2014. 〈hal-01088684〉

Partager

Métriques

Consultations de la notice

348

Téléchargements de fichiers

82