A Simple and Efficient Statistical Model Checking Algorithm to Evaluate Markov Decision Processes

Benoît Delahaye 1 Axel Legay 1 Sean Sedwards 1
1 TRISKELL - Reliable and efficient component based software engineering
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We propose a simple and efficient technique that allows the application of statistical model checking (SMC) to Markov Decision Processes (MDP). Our technique finds schedulers that transform the original MDP into a purely stochastic Markov Chain, on which standard SMC can be used. A statistical search is performed over the set of possible schedulers to find the best and worst with respect to the given property. If a scheduler is found that disproves the property, a counter-example is produced. If no counter-example is found, the algorithm concludes that the property is {\em probably} satisfied, with a confidence depending on the number of schedulers evaluated. Unlike previous approaches, the efficiency of our algorithm does not depend on structural properties of the MDP. Moreover, we have devised an efficient procedure to address general classes of schedulers by using Pseudo Random Number Generators and Hash Functions. In practice, our algorithm allows the representation of general schedulers in constant space, in contrast to existing algorithms that are exponential in the size of the system. In particular, this allows our SMC algorithm for MDPs to consider memory-dependant schedulers in addition to the memoryless schedulers that have been considered by others.
Type de document :
[Technical Report] 2013
Liste complète des métadonnées

Contributeur : Benoît Delahaye <>
Soumis le : lundi 2 septembre 2013 - 11:53:30
Dernière modification le : vendredi 13 janvier 2017 - 14:21:04
Document(s) archivé(s) le : mardi 3 décembre 2013 - 11:25:22


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00856704, version 1



Benoît Delahaye, Axel Legay, Sean Sedwards. A Simple and Efficient Statistical Model Checking Algorithm to Evaluate Markov Decision Processes. [Technical Report] 2013. <hal-00856704>



Consultations de
la notice


Téléchargements du document