可能性测度下的CTL符号化模型检测

Symbolic CTL model checking based on possibility measure

随着系统复杂性的增加,系统中的不确定信息亟待处理,状态爆炸问题也越来越严峻,现有的模型检测技术已不能完全适用于复杂系统的验证。对可能性测度下CTL符号化模型检测进行了研究。首先用多终端二值决策图和布尔公式分别描述系统模型和待验证性质,然后再对系统模型进行归一化和简化,最后利用不动点计算完成系统验证。该研究是对可能性测度下的模型检测技术和符号化模型检测技术的整合,不但能处理系统的不确定信息,而且保持了符号化模型检测对计算时空要求低的优点,对于复杂系统模型检测具有重要意义。

With the increasing complexity of systems, it is urgent to deal with the uncertain informa tion in the systems. Besides, the state explosion problem is getting more and more serious. Existing model checking techniques are no longer suitable for the verification of such complex systems. We study symbolic CTL model checking based on possibility measure. Firstly, multi terminal binary decision trees （MTBDDs） and Boolean formula are respectively used to describe system models and properties to be verified. Secondly, the system models are normalized and simplified. Finally, system verification is corn pleted by fixed point calculation. Our work is an integration of symbolic model checking and CTL model checking based on possibility measure, which can not only handle uncertain information in systems, hut also maintain symbolic model checking＇s advantage of low demand for computation time and storage space. It is thus significant for the verification of complex systems.