• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 软件工程 • 上一篇    下一篇

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

袁申,魏杰林,李永明   

  1. (陕西师范大学计算机科学学院,陕西 西安 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   

  1. (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:

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