LTL概率模型检验工具的实现与优化

计算机工程与科学

LTL概率模型检验工具的实现与优化

林哲超，董威

（国防科学技术大学计算机学院,湖南长沙 410073）

收稿日期:2015-10-14 修回日期:2015-12-02 出版日期:2017-05-25 发布日期:2017-05-25

Implementation and optimization of

LTL probabilistic model checker

LIN Zhe-chao，DONG Wei

（College of Computer,National University of Defense Technology,Changsha 410073,China）

Received:2015-10-14 Revised:2015-12-02 Online:2017-05-25 Published:2017-05-25

摘要/Abstract

摘要：

概率模型检验建立在非概率模型检验技术的基础上，不仅能够对系统进行定性的验证，还能够定量判断系统满足相关性质的概率，具有广泛的适用性。LTL概率模型检验算法的复杂度较高,达到双重指数级别，现有的工具如PRISM与MRMC均不支持对LTL性质的验证。针对这个问题，通过对原有的LTL概率模型检验算法进行优化，实现了一个高效的LTL概率模型检验工具。通过对比实验验证了该工具的有效性。

关键词: LTL, 概率模型检验, 优化

Abstract:

Probabilistic model checking is one model checking technology, which cannot only verify the system qualitatively but also judge if the system satisfies quantitative properties. The complexity for LTL probabilistic model checking can be up to a double exponential level. Existing tools such as PRISM and MRMC do not support the validation of LTL properties. We optimize the LTL probabilistic model checking algorithm and implement an efficient LTL model checker. The proposed tool is evaluated via some comparative experiments.

Key words: LTL, probabilistic model checking, optimization

林哲超，董威. LTL概率模型检验工具的实现与优化[J]. 计算机工程与科学.

LIN Zhe-chao，DONG Wei.

Implementation and optimization of

LTL probabilistic model checker

[J]. Computer Engineering & Science.

[1]	陈侨安1，李峰1，曹越1，龙明盛1,2. 基于运行数据分析的Spark任务参数优化[J]. J4, 20160101, 38(01): 11-19.
[2]	周兰凤1，赵鹏飞1，彭俊杰2. 基于云环境下一种小文件传输策略研究[J]. J4, 20160101, 38(01): 20-27.
[3]	施禹, 董攀, 张利军. 一种不规则稀疏矩阵的SpMV方法[J]. 计算机工程与科学, 2024, 46(07): 1175-1184.
[4]	王堃, 李少波, 何玲, 周鹏. 基于改进北方苍鹰优化随机配置网络的网络流量预测模型[J]. 计算机工程与科学, 2024, 46(07): 1245-1255.
[5]	张永智, 何可人, 戈珏. 改进YOLOv7网络在低空遥感图像目标检测中的应用[J]. 计算机工程与科学, 2024, 46(07): 1269-1277.
[6]	徐慧玲, 刘升, 李安东. 基于双向局部开发和黄金正弦的异构导向的鲸鱼优化算法[J]. 计算机工程与科学, 2024, 46(06): 1128-1140.
[7]	王颍超. 鲸鱼优化算法研究与应用进展[J]. 计算机工程与科学, 2024, 46(05): 881-896.
[8]	卢明妤, 李陶深, 吕品. 无线携能通信下mmWave协作通信小单元的能效最优策略[J]. 计算机工程与科学, 2024, 46(04): 626-634.
[9]	梁昔明, 史兰艳, 龙文. 基于混合策略改进的蛇优化算法及其应用[J]. 计算机工程与科学, 2024, 46(04): 693-706.
[10]	刘向举, 李金贺, 方贤进, 王宇. 移动边缘计算中计算卸载与资源分配联合优化策略[J]. 计算机工程与科学, 2024, 46(03): 416-426.
[11]	刘振超, 苑迎春, 王克俭, 何晨. 融合特征权重与改进粒子群优化的特征选择算法[J]. 计算机工程与科学, 2024, 46(02): 282-291.
[12]	李雨恒, 高尚, 孟祥宇. 基于精英引导的改进哈里斯鹰优化算法[J]. 计算机工程与科学, 2024, 46(02): 363-373.
[13]	季俊豪, 张玉书, 赵若宇, 温文媖, 董理. 基于智能进化算法的可见水印对抗攻击[J]. 计算机工程与科学, 2024, 46(01): 63-71.
[14]	李中华, 袁杰, 郭振宇. 基于信息启发的目标导向Bi-RRT机器人路径规划[J]. 计算机工程与科学, 2023, 45(12): 2237-2245.
[15]	许文俊, 王锡淮. 基于变尺度黑洞和种群迁徙的粒子群优化算法[J]. 计算机工程与科学, 2023, 45(11): 2036-2046.