具有多值决策过程的广义可能性计算树逻辑模型检测

计算机工程与科学

具有多值决策过程的广义可能性计算树逻辑模型检测

袁申,魏杰林,李永明

(陕西师范大学计算机科学学院，陕西西安 710119)

收稿日期:2018-07-15 修回日期:2018-09-12 出版日期:2019-01-25 发布日期:2019-01-25
基金资助:
国家自然科学基金（11671244）

Model checking of generalized possibilistic

computation tree logic with multi-valued decision process

YUAN Shen,WEI Jielin,LI Yongming

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

Received:2018-07-15 Revised:2018-09-12 Online:2019-01-25 Published:2019-01-25

摘要/Abstract

摘要：

模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证，在可能性理论、多值逻辑的基础上，研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法，及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型，用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法，该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题，给出一个具体的应用实例。

关键词: 模型检测, 多值计算树逻辑, 广义可能性测度, 多值决策过程

Abstract:

Model checking is an effective technique for automatically verifying the behavior of hardware and software systems. To formally verify a concurrent system that contains non-deterministic and inconsistent information, based on the possibility theory and multivalued logic, we propose a generalized possibilistic multivalued model checking algorithm for computation tree logic with multi-valued decision process (MvDP), and apply it to non-deterministic system verification. Firstly, an MvDP is constructed to specify the behaviour of the system as a formal system model. Then a multi-valued computation tree logic (MvCTL) is introduced to describe system properties and the model checking algorithm of generalized possibilistic MvCTL with MvDP is presented. The algorithm converts the model checking problem into polynomialtime fuzzy matrix calculations. Finally, we give a specific application example to deal with model checking problems of nondeterministic multi-valued systems.

Key words: model checking, multi-valued computation tree logic, generalized possibilistic measure, multivalued decision process

袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学.

YUAN Shen,WEI Jielin,LI Yongming.

Model checking of generalized possibilistic

computation tree logic with multi-valued decision process

[J]. Computer Engineering & Science.

[1]	刘子源, 马占有, 李霞, 高滢囡, 何娜娜, 黄瑞祺. 基于模糊测度的模糊分支时态逻辑模型检测[J]. 计算机工程与科学, 2024, 46(04): 676-683.
[2]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[3]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[4]	钟小妹，肖美华，李伟，谌佳，李娅楠. RFID超轻量级认证协议RCIA形式化分析与改进[J]. 计算机工程与科学, 2018, 40(12): 2183-2192.
[5]	王亚鹏，雷丽晖. 基于CTL模型检测的胃腺癌核心路径形式化验证[J]. 计算机工程与科学, 2018, 40(12): 2280-2286.
[6]	雷丽晖，郭越，张延波. 可能性测度下的CTL符号化模型检测[J]. 计算机工程与科学, 2018, 40(11): 2008-2014.
[7]	肖美华1，梅映天1,2，李伟1，李娅楠1，钟小妹1，宋子繁1. 基于时间戳私钥签名技术的Nayak-T协议安全性分析[J]. 计算机工程与科学, 2017, 39(12): 2252-2259.
[8]	袁红娟1,2,马艳芳3,潘海玉1,2. 模糊交互时态逻辑的模型检测[J]. 计算机工程与科学, 2017, 39(12): 2290-2296.
[9]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.
[10]	程道雷,肖美华,刘欣倩,梅映天,李伟. 运用SPIN对开放授权协议OAuth 2.0的分析与验证[J]. J4, 2015, 37(11): 2121-2127.
[11]	马占有1，2，李永明1. 广义可能性决策过程的计算树逻辑模型检测[J]. J4, 2015, 37(11): 2162-2168.
[12]	刘姣，雷丽晖. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法[J]. J4, 2015, 37(10): 1884-1889.
[13]	张兴兴,邓楠轶,马占有,李永明. 广义可能性互模拟及其逻辑刻画[J]. J4, 2015, 37(05): 951-957.
[14]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[15]	周璇,汪学明. 微支付协议Millicent的改进与模型检测[J]. J4, 2012, 34(12): 22-26.