Skip to Main content Skip to Navigation
New interface
Reports (Technical report)

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.
Document type :
Reports (Technical report)
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download
Contributor : Benoît Delahaye Connect in order to contact the contributor
Submitted on : Monday, September 2, 2013 - 11:53:30 AM
Last modification on : Wednesday, October 26, 2022 - 8:14:02 AM
Long-term archiving on: : Tuesday, December 3, 2013 - 11:25:22 AM


Files produced by the author(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⟩



Record views


Files downloads