A Game-Based Approach for PCTL* Stochastic Model Checking with Evidence
A Game-Based Approach for PCTL* Stochastic Model Checking with Evidence
复制标题
基于游戏的 PCTL* 随机模型验证方法
DOI：
10.1007/s11390-016-1621-y
复制
发表时间：
2016-01
影响因子：
0.7
通讯作者：
Yan Ma
中科院分区：
文献类型：
--
作者：
Yang Liu;Xu;ong Li;Yan Ma
随机模型检查是经典模型检查的最新延伸和概括，其重点是定量检查系统模型的时间属性。 PCTL* 是重要的定量属性规范语言之一，严格来说，它比具有概率界限的 PCTL（概率计算树逻辑）或 LTL（线性时态逻辑）更具表现力。目前，PCTL*随机模型检验算法非常复杂，无法对某个公式在给定模型中成立或不成立的原因提供任何相关解释。针对这一问题，本文提出了一种直观、简洁的PCTL*随机模型检验有证据的方法，包括：以release-PNF（释放正范式）形式给出PCTL*的博弈语义，定义PCTL*随机模型检验博弈，利用博弈中的策略求解实现PCTL*随机模型检验，并细化获胜策略作为证明随机模型检验结果的证据。 基于游戏的PCTL*随机模型检验算法在可视化原型工具中实现，并通过示例证明了其可行性。
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 game-based PCTL* stochastic model checking algorithm is implemented in a visual prototype tool, and its feasibility is demonstrated by an illustrative example.
登录
查看更多内容
影响因子：
7.4
作者：
Baier, C;Haverkort, B;Katoen, JP
通讯作者：
Katoen, JP
DOI：
--
发表时间：
2008-04
期刊：
--
影响因子：
--
作者：
C. Baier;J. Katoen
通讯作者：
C. Baier;J. Katoen
影响因子：
7.4
作者：
Aljazzar, Husain;Leue, Stefan
通讯作者：
Leue, Stefan
DOI：
10.1016/j.peva.2009.07.002
发表时间：
2010-09
期刊：
Perform. Evaluation
影响因子：
--
作者：
Harald Fecher;M. Huth;Nir Piterman;Daniel Wagner
通讯作者：
Harald Fecher;M. Huth;Nir Piterman;Daniel Wagner
影响因子：
0.7
作者：
Yang Liu;Huai-kou Miao;Hong-wei Zeng;Yan Ma;Pan Liu
通讯作者：
Yang Liu;Huai-kou Miao;Hong-wei Zeng;Yan Ma;Pan Liu