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

共 50 条

[1] Smart sampling for lightweight verification of Markov decision processes
Pedro D’Argenio
Axel Legay
Sean Sedwards
Louis-Marie Traonouez
International Journal on Software Tools for Technology Transfer, 2015, 17 : 469 - 484
[2] Scalable Verification of Markov Decision Processes
Legay, Axel
Sedwards, Sean
Traonouez, Louis-Marie
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2014, 2015, 8938 : 350 - 362
[3] Incremental Quantitative Verification for Markov Decision Processes
Kwiatkowska, Marta
Parker, David
Qu, Hongyang
2011 IEEE/IFIP 41ST INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS (DSN), 2011, : 359 - 370
[4] Active Learning of Markov Decision Processes for System Verification
Chen, Yingke
Nielsen, Thomas Dyhre
2012 11TH INTERNATIONAL CONFERENCE ON MACHINE LEARNING AND APPLICATIONS (ICMLA 2012), VOL 2, 2012, : 289 - 294
[5] Approximate planning and verification for large Markov decision processes
Lassaigne, Richard
Peyronnet, Sylvain
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2015, 17 (04) : 457 - 467
[6] Approximate planning and verification for large Markov decision processes
Richard Lassaigne
Sylvain Peyronnet
International Journal on Software Tools for Technology Transfer, 2015, 17 : 457 - 467
[7] Verification of Markov Decision Processes Using Learning Algorithms
Brazdil, Tomas
Chatterjee, Krishnendu
Chmelik, Martin
Forejt, Vojtech
Kretinsky, Jan
Kwiatkowska, Marta
Parker, David
Ujma, Mateusz
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2014, 2014, 8837 : 98 - 114
[8] An adaptive sampling algorithm for solving Markov decision processes
Chang, HS
Fu, MC
Hu, JQ
Marcus, SI
OPERATIONS RESEARCH, 2005, 53 (01) : 126 - 139
[9] Verification of Markov Decision Processes with Risk-Sensitive Measures
Cubuktepe, Murat
Topcu, Ufuk
2018 ANNUAL AMERICAN CONTROL CONFERENCE (ACC), 2018, : 2371 - 2377
[10] Learning Weighted Assumptions for Compositional Verification of Markov Decision Processes
He, Fei
Gao, Xiaowei
Wang, Miaofei
Wang, Bow-Yaw
Zhang, Lijun
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2016, 25 (03)

← 1 2 3 4 5 →