迁移关系的布尔函数表示的优化  

Optimization of the Boolean Function Representing Transition Relation

作　　者：张小珍 江建国[1] 

机构地区：[1]辽宁师范大学数学学院,辽宁大连

出　　处：《软件工程与应用》2016年第6期319-326,共8页Software Engineering and Applications

摘　　要：符号模型检测中,将迁移关系表示为OBDD的一种较为高效的方法是先借助SMV语言将迁移关系表示为布尔函数,再利用相关算法综合得其OBDD。但在将迁移关系表示为布尔函数时常会遇到两个问题:第一,下一状态取值不确定;第二,具有一定变化规律的非输入变量较多。本文提出等效输入变量的概念,对迁移关系的布尔函数公式的取值条件加以限制,给出了这两个问题的具体解决办法,进而使得迁移关系的布尔函数表示更加准确、高效。In Symbolic Model checking, as a comparatively efficient method of representing transition rela-tion with OBDD, we need firstly represent it as a boolean function with the aid of SMV language, and then synthesize the OBDD using relevant algorithms. However, during the course of repre-sentation from transition relation to the boolean function, we often encounter two problems: first, the assignment of next state is non-deterministic;second, the number of non-input variables with certain variation regularity is more. In this paper, through the concept of equivalent-input variables, we impose restriction on the assignment of the boolean function formula used to represent transition relation, and give definite solutions to these two problems, enabling the boolean function representation of transition relation is further accurate and efficient.

关 键 词：符号模型检测 OBDD 迁移关系 布尔函数 等效输入变量 

分 类 号：TP30[自动化与计算机技术—计算机系统结构]