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

J4 ›› 2015, Vol. 37 ›› Issue (11): 2162-2168.

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

马占有1，2，李永明1

(1.陕西师范大学计算机科学学院，陕西西安 710062；2.北方民族大学计算机科学与工程学院，宁夏银川 750021)

收稿日期:2015-08-13 修回日期:2015-10-11 出版日期:2015-11-25 发布日期:2015-11-25
基金资助:
国家自然科学基金资助项目(11271237,61228305,61462001);北方民族大学资助项目(2014XB213)

Computation tree logic model checking for
generalized possibilistic decision processes

MA Zhanyou1，2，LI Yongming1

(1.College of Computer Science,Shaanxi Normal University,Xi’an 710062;
2.College of Computer Science and Engineering,Beifang University of Nationalities,Yinchuan 750021,China)

Received:2015-08-13 Revised:2015-10-11 Online:2015-11-25 Published:2015-11-25

摘要/Abstract

摘要：

模型检测作为一种形式化验证技术，已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统，引入广义可能性决策过程作为此类系统的模型；给出描述其性质的规范语言广义可能性计算树逻辑的概念；研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明，其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。

关键词: 并发系统, 广义可能性决策过程, 广义可能性计算树逻辑, 模型检测

Abstract:

Model checking is a widespread formal technique for verifying the correctness of concurrent systems. We introduce the generalized possibilistic decision process as the model of the systems, which have nondeterministic choices and generalized possibility distributions.To describe its attributes, we define the concept of generalized possibilistic computation tree logic (GPCTL) specification language and study the GPCTL model checking problems.The time complexity of the computation tree logic model checking algorithm shows to be polynomial time. The results obtained in this paper extend the application scope of model checking based on generalized possibility measurement.

Key words: concurrent systems；generalized possibilistic decision process；generalized possibilistic computation tree logic (GPCTL)；model checking

马占有1，2，李永明1. 广义可能性决策过程的计算树逻辑模型检测[J]. J4, 2015, 37(11): 2162-2168.

MA Zhanyou1，2，LI Yongming1. Computation tree logic model checking for
generalized possibilistic decision processes [J]. J4, 2015, 37(11): 2162-2168.

参考文献

［1］Clarke E,Grumberg O,Peled D. Model Checking［M］.Massachusetts:The MIT Press,1999.
［2］Lin H M, Zhang W H. Model checking: Theories, techniques and applications ［J］. Chinese Journal of Electronics,2002,30(12A): 19071912. (in Chinese)
［3］Baier C, Katoen J P. Principles of model checking［M］. Massachusetts:The MIT Press, 2007.
［4］Cranen S, Groote J F, Reniers M. A linear translation from CTL* to the firstorder modal μcalculus ［J］. Theoretical Computer Science, 2011,412(28): 31293139.
［5］Rozier K Y. Linear temporal logic symbolic model checking［J］. Computer Science Review, 2011,5(2):163203.
［6］Cleaveland R, Purushothaman S, Narasimha I M. Probabilistic temporal logics via the modal mucalculus［J］. Theoretical Computer Science, 2005,342(23): 316350.
［7］Bentahar J, Yahyaoui H, Kova M, et al. Symbolic model checking composite web services using operational and control behaviors［J］．Expert Systems with Applications, 2013,40(2)：508522．
［8］Fischer D, Gradel E, Kaiser L. Model checking games for the quantitative μcalculus［J］. Theory of Computing Systems, 2010,47(3): 696719．
［9］Chechik M, Devereux B, Easterbrook S, et al. Multivalued symbolic modelchecking［J］. ACM Transactions on Software Engineering and Methodology,2003,12(4):138．
［10］Li Y M, Li L J. Model checking of lineartime properties based on possibility measure［J］. IEEE Transactions in Fuzzy Systems, 2013,21(5)：842854.
［11］Li Y M, Li Y L, Ma Z Y. Computation tree logic model checking based on possibility measure ［J］. Fuzzy Sets and Systems, 2015,262(5): 4459.
［12］Li Y M, Ma Z Y. Quantitative computation tree logic model checking based on generalized possibility measures［J］. IEEE Transactions on Fuzzy Systems,2014(09),doi:10.1109/TFUZZ.2015.2396537.
［13］Zhang X X, Deng N Y, Ma Z Y, et al. Possibilistic bisimulation based on generalized possibility measures and its logical characterizations ［J］. Computer Engineering & Science, 2015,37(5)：951957. (in Chinese)
［14］Garmendia L, González R, del Campo V, et al. An algorithm to compute the transitive closure, a transitive approximation and a transitive opening of a fuzzy proximity［J］. Mathware and Soft Computing, 2009,16(2)：175191.
［15］Xing H Y, Zhang Q S, Huang K S. Analysis and control of fuzzy discrete event systems using bisimulation equivalence［J］. Theoretical Computer Science, 2012,456(19)：100111.
附中文参考文献：
［2］林惠民,张文辉.模型检测:理论方法与应用［J］.电子学报, 2002,36(12A)：19071012.
［13］张兴兴, 邓楠轶, 马占有, 等. 广义可能性互模拟及其逻辑刻画［J］. 计算机工程与科学, 2015,37(5)：951957.

[1]	李召恺, 马占有, 李健祥, 郭昊. 基于模糊决策过程的模糊计算树逻辑模型检测[J]. 计算机工程与科学, 2022, 44(02): 266-275.
[2]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[3]	袁申,魏杰林,李永明. 具有多值决策过程的广义可能性计算树逻辑模型检测[J]. 计算机工程与科学, 2019, 41(01): 88-97.
[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]	刘姣，雷丽晖. 一种基于扩展不完全Kripke结构的三值逻辑模型检测方法[J]. J4, 2015, 37(10): 1884-1889.
[12]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[13]	周璇,汪学明. 微支付协议Millicent的改进与模型检测[J]. J4, 2012, 34(12): 22-26.
[14]	陈国彬1，任〓强2,张广泉2,3. 一种基于抽象与精化技术的Web服务组合验证方法[J]. J4, 2011, 33(9): 76-80.
[15]	龙士工，王扣武. 多智体系统时序认知规范的SPIN模型检测[J]. J4, 2011, 33(12): 12-16.