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

Optimization of the Boolean Function Representing Transition Relation

摘要: 符号模型检测中，将迁移关系表示为OBDD的一种较为高效的方法是先借助SMV语言将迁移关系表示为布尔函数，再利用相关算法综合得其OBDD。但在将迁移关系表示为布尔函数时常会遇到两个问题：第一，下一状态取值不确定；第二，具有一定变化规律的非输入变量较多。本文提出等效输入变量的概念，对迁移关系的布尔函数公式的取值条件加以限制，给出了这两个问题的具体解决办法，进而使得迁移关系的布尔函数表示更加准确、高效。

Abstract: 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.