Smart sampling for lightweight verification of Markov decision processes

被引：31

作者：

D'Argenio, Pedro ^{[1
]}

Legay, Axel ^{[2
]}

Sedwards, Sean ^{[2
]}

Traonouez, Louis-Marie ^{[2
]}

机构：

[1] Univ Nacl Cordoba, RA-5000 Cordoba, Argentina

[2] Inria Rennes Bretagne Atlantique, Rennes, France

来源：

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER | 2015年 / 17卷 / 04期

关键词：

Statistical model checking; Sampling; Nondeterminism; REAL APPLICATIONS; INEQUALITIES;

D O I：

10.1007/s10009-015-0383-0

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：469 / 484

页数：16

共 37 条

[1] [Anonymous], 2005, THESIS CARNEGIE MELL
[2] Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1
[3] DYNAMIC PROGRAMMING
BELLMAN, R
[J]. SCIENCE, 1966, 153 (3731) : 34 - &
[4] Bianco A., 1995, Foundations of Software Technology and Theoretical Computer Science. 15th Conference. Proceedings, P499
[5] Bogdoll J, 2011, LECT NOTES COMPUT SC, V6722, P59, DOI 10.1007/978-3-642-21461-5_4
[6] Boyer Benoit., 2013, Quantitative Evaluation of Systems: 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, V10, P160, DOI DOI 10.1007/978-3-642-40196-1_12
[7] Brázdil T, 2014, LECT NOTES COMPUT SC, V8837, P98, DOI 10.1007/978-3-319-11936-6_8
[8] Clarke EM, 2009, COMMUN ACM, V52, P75, DOI 10.1145/1592761.1592781
[9] Cormen T.H., 2009, Introduction to Algorithms, V3rd ed., DOI [10.2307/2583667, DOI 10.2307/2583667]
[10] Eisner C, 2003, LECT NOTES COMPUT SC, V2725, P27

← 1 2 3 4 →