Stochastic model checking

被引：0

作者：

Kwiatkowska, Marta ^{[1
]}

Norman, Gethin ^{[1
]}

Parker, David ^{[1
]}

机构：

[1] Univ Birmingham, Sch Comp Sci, Birmingham B15 2TT, W Midlands, England

来源：

FORMAL METHODS FOR PERFORMANCE EVALUATION | 2007年 / 4486卷

基金：

英国工程与自然科学研究理事会;

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs). Model checking algorithms are given for verifying DTMCs and CTMCs against specifications written in probabilistic extensions of temporal logic, including quantitative properties with rewards. Example properties include the probability that a fault occurs and the expected number of faults in a given time period. We also describe the practical application of stochastic model checking with the probabilistic model checker PRISM by outlining the main features supported by PRISM and three real-world case studies: a probabilistic security protocol, dynamic power management and a biological pathway.

引用

页码：220 / +

页数：6

共 50 条

[41] Imprecise Probabilistic Model Checking for Stochastic Multi-agent Systems [J].

Termine A. ;

Antonucci A. ;

Primiero G. ;

Facchini A. .

SN Computer Science, 4 (5)

[42] PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games [J].

Ashok, Pranav ;

Kretinsky, Jan ;

Weininger, Maximilian .

COMPUTER AIDED VERIFICATION, CAV 2019, PT I, 2019, 11561 :497-519

[43] A Game-Based Approach for PCTL* Stochastic Model Checking with Evidence [J].

Liu, Yang ;

Li, Xuan-Dong ;

Ma, Yan .

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2016, 31 (01) :198-216

[44] A Game-Based Approach for PCTL* Stochastic Model Checking with Evidence [J].

Yang Liu ;

Xuan-Dong Li ;

Yan Ma .

Journal of Computer Science and Technology, 2016, 31 :198-216

[45] Using Stochastic Comparison for Efficient Model Checking of Uncertain Markov Chains [J].

Haddad, Serge ;

Pekergin, Nihal .

SIXTH INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, PROCEEDINGS, 2009, :177-+

[46] Statistical Model Checking for Verification of Rare Properties of Stochastic Hybrid System [J].

Fang, Bing-Wu ;

Huang, Zhi-Qiu ;

Xie, Jian .

Ruan Jian Xue Bao/Journal of Software, 2022, 33 (10) :3717-3731

[47] Model checking of infinite state space Markov chains by stochastic bounds [J].

Ben Mamoun, Mouad ;

Pekergin, Nihal .

ANALYTICAL AND STOCHASTIC MODELING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, 2008, 5055 :264-+

[48] PCTL* Stochastic Model Checking Label-Extended Probabilistic Petri Net System Model [J].

Liu, Yang .

2014 5TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), 2014, :287-290

[49] Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes [J].

Bortolussi, Luca ;

Gallo, Giuseppe Maria ;

Kretinsky, Jan ;

Nenzi, Laura .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 :281-300

[50] Toward Approximate Stochastic Model Checking of Computational Fields for Pervasive Computing Systems [J].

Casadei, Matteo ;

Viroli, Mirko .

2012 IEEE SIXTH INTERNATIONAL CONFERENCE ON SELF-ADAPTIVE AND SELF-ORGANIZING SYSTEMS WORKSHOPS (SASOW), 2012, :199-204

← 1 2 3 4 5 →