A Game-Based Approach for PCTL＊ Stochastic Model Checking with Evidence

作     者：Yang Liu Xuan-Dong Li Yan Ma 

作者机构：State Key Laboratory for Novel Software Technology Nanjing University Nanjing 210046 China Department of Computer Science School of Computing National University of Singapore Singapore 117417 Singapore College of Computer Science and Technology Nanjing University of Aeronautics and Astronautics Nanjing 210016 China 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2016年第31卷第1期

页      面：198-216页

核心收录：

学科分类：070801[理学-固体地球物理学] 07[理学] 0839[工学-网络空间安全] 08[工学] 0708[理学-地球物理学] 0816[工学-测绘科学与技术] 

基　　金：The work was supported by the National Natural Science Foundation of China under Grant Nos. 61303022 and 61472179  the China Postdoctoral Science Foundation under Grant No. 2013M531328  the Natural Science Foundation of Shandong Province of China under Grant No. ZR2012FQ013  the Project of Shandong Province Higher Educational Science and Technology Program under Grant No. J13LN10  and the Science and Technology Program of Taian of China under Grant No. 201330629. This work was partially supported by Jiangsu Collaborative Innovation Center of Novel Software Technology and Industrialization of China 

主　　题：PCTL* stochastic model checking game semantics strategy evidence 

摘      要：Stochastic model checking is a recent extension and generalization of the classical model checking, which focuses on quantitatively checking the temporal property of a system model. PCTL＊ is one of the important quantitative property specification languages, which is strictly more expressive than either PCTL （probabilistic computation tree logic） or LTL （linear temporal logic） with probability bounds. At present, PCTL＊ stochastic model checking algorithm is very complicated, and cannot provide any relevant explanation of why a formula does or does not hold in a given model. For dealing with this problem, an intuitive and succinct approach for PCTL＊ stochastic model checking with evidence is put forward in this paper, which includes： presenting the game semantics for PCTL＊ in release-PNF （release-positive normal form）, defining the PCTL＊ stochastic model checking game, using strategy solving in game to achieve the PCTL＊ stochastic model checking, and refining winning strategy as the evidence to certify stochastic model checking result. The soundness and the completeness of game-based PCTL＊ stochastic model checking are proved, and its complexity matches the known lower and upper bounds. The game-based PCTL＊ stochastic model checking algorithm is implemented in a visual prototype tool, and its feasibility is demonstrated by an illustrative example.