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

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

Model checking of generalized possibilistic computation tree logic with multi-valued decision process

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.