A three-valued model abstraction framework for PCTL* stochastic model checking
A three-valued model abstraction framework for PCTL* stochastic model checking
复制标题
DOI：
10.1007/s10515-022-00327-z
复制
发表时间：
2022-03
影响因子：
3.4
通讯作者：
Yang Liu;Yan Ma;Yongsheng Yang
中科院分区：
文献类型：
--
作者：
Yang Liu;Yan Ma;Yongsheng Yang
随机模型检测是一种基于系统模型的形式化验证技术，可以对具有随机行为的软件驱动自治系统进行自动验证和分析。在处理大系统时，状态空间爆炸问题非常严重。模型抽象是缓解这一问题的一种潜在技术。目前，在随机模型检测的实际模型抽象中，只能保留概率计算树逻辑(PCTL)所规定的概率安全性、概率可达性等少数性质，它们是PCTL(概率计算树逻辑)性质的真子集。针对这一问题，本文提出了一种有效、高效的三值模型抽象框架，用于完全PCTL*随机模型检测。我们提出了一个新的抽象模型来保持不确定和概率系统的全部PCTL*性质，该模型将转移的区间概率和非确定系统的博弈正交地结合在一起。提出了一种基于博弈的三值PCTL*随机模型检验算法来验证抽象模型，并设计了一种结合样本学习的二进制粒子群优化算法来求精三值PCTL*随机模型检验抽象模型的不确定结果。证明了当三值随机模型检验的结果是确定的时，完全的PCTL*性质是保持的，并通过一些大型案例证明了该框架的有效性。
Stochastic model checking can automatically verify and analyse the software-driven autonomous systems with stochastic behaviors, which is a formal verification technique based on system models. When coping with large-scale systems, it suffers from state space explosion problem very seriously. Model abstraction is a potential technique for mitigating this problem. At present, only a few properties specified by PCTL (Probabilistic Computation Tree Logic), such as probabilistic safety and probabilistic reachability, can be preserved in the practical model abstraction of stochastic model checking, which are the proper subset of PCTL* (Probabilistic Computation Tree Logic*) properties. For dealing with this, an effective and efficient three-valued model abstraction framework for full PCTL* stochastic model checking is proposed in this paper. We propose a new abstract model to preserve full PCTL* properties for nondeterministic and probabilistic system, which orthogonally integrates interval probability of transition and game for nondeterminism. A game-based three-valued PCTL* stochastic model checking algorithm is developed to verify abstract model, and a BPSO (binary particle swarm optimization) algorithm integrated with sample learning is designed to refine the indefinite result of three-valued PCTL* stochastic model checking abstract model. It is proved that full PCTL* properties are preserved when the result of three-valued stochastic model checking is definite, and the efficiency of this framework is demonstrated by some large cases.