统计算法选择对统计模型检测效率的影响分析

摘要

Recently,statistical model checking technology has been widely used,and different statistical algorithms have different effects on the performance of the statistical model checking.This paper mainly compared the running time of different statistical algorithms,thus analyzed the applicable environment of the algorithms.The statistical algorithms include Chernoff algorithm,sequential algorithm,smart aim-listed probability estimation algorithm,smart content testing algorithm and Monte Carlo algorithm.Models are the Wireless LAN (WLAN) and the Dining Philosophers problem,using PLASMA model checking tool for validation.The result shows that different statistical algorithms have different influences on the efficiency of model checking when the environment is different.Sequential algorithm is fit for verifying the reachability of state,and the time performance is the best.Smart content testing algorithm and Monte Carlo algorithm are fit for verifying complex models.This conclusion can help the selection of statistical algorithms in model checking,in order to improve the efficiency of model checking.%近年来,统计模型检测技术已经得到了广泛的应用,不同的统计算法对统计模型检测的性能有所影响.主要对比不同统计算法对统计模型检测的时间开销影响,从而分析算法的适用环境.选择的统计算法包括切诺夫算法、序贯算法、智能概率估计算法、智能假设检验算法及蒙特卡罗算法.采用无线局域网协议验证和哲学家就餐问题的状态可达性验证为实例进行分析,使用PLASMA模型检测工具进行验证.实验结果表明,不同的统计算法在不同的环境中对模型检测的效率有不同的影响.序贯算法适用于状态可达性性质的验证,时间性能最优;智能假设检验算法与蒙特卡罗算法适合验证复杂模型.这一结论有助于在模型检测时对统计算法的选择,从而提高模型检测的效率.