We use cookies to improve your experience with our site.

一种基于博弈的带有证据的PCTL*随机模型检验方法

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

  • 摘要: 随机模型检验是经典模型检验理论的延伸和推广,其可以定量验证系统模型的时序逻辑性质。PCTL*是一种重要的定量性质规约语言,它的描述能力严格大于PCTL(probabilistic computation tree logic)和带有概率界的LTL(linear temporal logic)。目前,PCTL*随机模型检验算法非常复杂,并且不可以提供任何支撑验证结果的相关信息。为了处理这一问题,本文给出了一种直观简洁的PCTL*随机模型检验方法,并且可以提供支持验证结果的证据。它具体包括:给出release-PNF (release-positive normal form) PCTL*的博弈语义,定义PCTL*随机模型检验博弈,使用博弈的策略求解实现PCTL*随机模型检验,并且用精化的获胜策略作为支撑验证结果的证据。该方法的正确性和完备性均给出了证明,与目前的PCTL*算法相比,其算法复杂性的上界和下界并没有增加。基于博弈的PCTL*随机模型检验算法的原型工具已经实现,并通过一个例子演示了其可行性。

     

    Abstract: 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.

     

/

返回文章
返回