可能性测度下的CTL符号化模型检测

计算机工程与科学

可能性测度下的CTL符号化模型检测

雷丽晖，郭越，张延波

（陕西师范大学计算机科学学院,陕西西安 710119）

收稿日期:2018-06-09 修回日期:2018-08-24 出版日期:2018-11-25 发布日期:2018-11-25
基金资助:
国家自然科学基金（A011404）

Symbolic CTL model checking based on possibility measure

LEI Lihui，GUO Yue，ZHANG Yanbo

（College of Computer Science,Shaanxi Normal University,Xi’an 710119,China）

Received:2018-06-09 Revised:2018-08-24 Online:2018-11-25 Published:2018-11-25

摘要/Abstract

摘要：

随着系统复杂性的增加，系统中的不确定信息亟待处理，状态爆炸问题也越来越严峻，现有的模型检测技术已不能完全适用于复杂系统的验证。
对可能性测度下CTL符号化模型检测进行了研究。首先用多终端二值决策图和布尔公式分别描述系统模型和待验证性质，然后再对系统模型进行归一化和简化，最后利用不动点计算完成系统验证。该研究是对可能性测度下的模型检测技术和符号化模型检测技术的整合，不但能处理系统的不确定信息，而且保持了符号化模型检测对计算时空要求低的优点，对于复杂系统模型检测具有重要意义。

关键词: 符号模型检测, 可能性测度, CTL, 多终端二值决策图

Abstract:

With the increasing complexity of systems, it is urgent to deal with the uncertain information in the systems. Besides, the state explosion problem is getting more and more serious. Existing model checking techniques are no longer suitable for the verification of such complex systems. We study symbolic CTL model checking based on possibility measure. Firstly, multiterminal binary decision trees (MTBDDs) and Boolean formula are respectively used to describe system models and properties to be verified. Secondly, the system models are normalized and simplified. Finally, system verification is completed by fixed point calculation. Our work is an integration of symbolic model checking and CTL model checking based on possibility measure, which can not only handle uncertain information in systems, but also maintain symbolic model checking's advantage of low demand for computation time and storage space. It is thus significant for the verification of complex systems.

Key words: symbolic model checking, possibility measure, CTL；MTBDD

雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学.

LEI Lihui，GUO Yue，ZHANG Yanbo. Symbolic CTL model checking based on possibility measure[J]. Computer Engineering & Science.

[1]	赖明澈, 吕方旭, 张庚, 许超龙. 面向112 Gbps PAM4串行接收机的低误码协同自适应均衡器[J]. 计算机工程与科学, 2023, 45(06): 951-960.
[2]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[3]	张兴兴,邓楠轶,马占有,李永明. 广义可能性互模拟及其逻辑刻画[J]. J4, 2015, 37(05): 951-957.
[4]	薛艳1，雷红轩2，李永明1. 基于可能性测度的计算树逻辑[J]. J4, 2011, 33(9): 70-75.
[5]	吴明行韩银和李晓维. 基于CTL的SOCIP核的测试技术[J]. J4, 2005, 27(4): 43-45.