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 fr...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: D'Argenio, Pedro Ruben, Legay, Axel, Sedwards, Sean, Traonouez, Louis-Marie
Formato: article
Lenguaje:Inglés
Publicado: 2022
Materias:
Statistical model checking
Sampling
Nondeterminism
Acceso en línea:http://hdl.handle.net/11086/27275
https://doi.org/10.48550/arXiv.1409.2116
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-27275
record_format dspace
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic Statistical model checking
Sampling
Nondeterminism
spellingShingle Statistical model checking
Sampling
Nondeterminism
D'Argenio, Pedro Ruben
Legay, Axel
Sedwards, Sean
Traonouez, Louis-Marie
Smart sampling for lightweight verification of Markov decision processes
topic_facet Statistical model checking
Sampling
Nondeterminism
description 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.
format article
author D'Argenio, Pedro Ruben
Legay, Axel
Sedwards, Sean
Traonouez, Louis-Marie
author_facet D'Argenio, Pedro Ruben
Legay, Axel
Sedwards, Sean
Traonouez, Louis-Marie
author_sort D'Argenio, Pedro Ruben
title Smart sampling for lightweight verification of Markov decision processes
title_short Smart sampling for lightweight verification of Markov decision processes
title_full Smart sampling for lightweight verification of Markov decision processes
title_fullStr Smart sampling for lightweight verification of Markov decision processes
title_full_unstemmed Smart sampling for lightweight verification of Markov decision processes
title_sort smart sampling for lightweight verification of markov decision processes
publishDate 2022
url http://hdl.handle.net/11086/27275
https://doi.org/10.48550/arXiv.1409.2116
work_keys_str_mv AT dargeniopedroruben smartsamplingforlightweightverificationofmarkovdecisionprocesses
AT legayaxel smartsamplingforlightweightverificationofmarkovdecisionprocesses
AT sedwardssean smartsamplingforlightweightverificationofmarkovdecisionprocesses
AT traonouezlouismarie smartsamplingforlightweightverificationofmarkovdecisionprocesses
bdutipo_str Repositorios
_version_ 1764820391552876544

Ejemplares similares