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

摘要

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