Smart sampling for lightweight verification of Markov decision processes
Markov decision processes (MDP) are useful to model optimisation problems in concurrent systems. To verify MDPs with efficient Monte Carlo techniques requires that their nondeterminism be resolved by a scheduler. Recent work has introduced the elements of lightweight techniques to sample directly from scheduler space, but finding optimal schedulers by simple sampling may be inefficient. Here we describe “smart” sampling algorithms that can make substantial improvements in performance.
Saved in:
Main Authors: | D'Argenio, Pedro Ruben, Legay, Axel, Sedwards, Sean, Traonouez, Louis-Marie |
---|---|
Format: | article biblioteca |
Language: | eng |
Published: |
2015
|
Subjects: | Statistical model checking, Sampling, Nondeterminism, |
Online Access: | http://hdl.handle.net/11086/27275 https://doi.org/10.48550/arXiv.1409.2116 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Similar Items
-
Manual of sampling and statistical methods for fisheries biology, part 1: sampling methods
by: Gulland, J.A. 162530, et al.
Published: (1966) -
Analysis of non-Markovian repairable fault trees through rare event simulation
by: Budde, Carlos E., et al.
Published: (2022) -
Sampling
by: 186383 Thompson, S.K.
Published: (2012) -
Outliers in samples from normal populations
by: Antoine, Robin
Published: (2008-11-21T14:36:30Z) -
Manuel des méthodes d'échantillonnage et des méthodes statistiques applicables à la biologie halieutique, première partie : méthodes d'échantillonnage
by: Gulland, J.A. 162530, et al.
Published: (1966)