Software Engineering and Applications 软件工程与应用, 2016, 5(6), 319-326 Published Online December 2016 in Hans.
Optimization of the Boolean Function Representing Transition Relation
Xiaozhen Zhang, Jianguo Jiang
School of Mathematics, Liaoning Normal University, Dalian Liaoning
Received: Dec. 1st , 2016; accepted: Dec. 18th , 2016; published: Dec. 21st , 2016
Copyright 2016 by authors and Hans Publishers Inc.
This work is licensed under the Creative Commons Attribution International License (CC BY).
Open Access
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 va-riables, 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 boo-lean function representation of transition relation is further accurate and efficient.
Keywords
Symbolic Model Checking, OBDD, Transition Relation, Boolean Function, Equivalent-Input Variables
迁移关系的布尔函数表示的优化
张小珍，江建国
辽宁师范大学数学学院，辽宁 大连
收稿日期：2016年12月1日；录用日期：2016年12月18日；发布日期：2016年12月21日
文章引用: 张小珍, 江建国. 迁移关系的布尔函数表示的优化[J]. 软件工程与应用, 2016, 5(6): 319-326.
张小珍，江建国
摘 要
符号模型检测中，将迁移关系表示为OBDD 的一种较为高效的方法是先借助SMV 语言将迁移关系表示为布尔函数，再利用相关算法综合得其OBDD 。但在将迁移关系表示为布尔函数时常会遇到两个问题：第一，下一状态取值不确定；第二，具有一定变化规律的非输入变量较多。本文提出等效输入变量的概念，对迁移关系的布尔函数公式的取值条件加以限制，给出了这两个问题的具体解决办法，进而使得迁移关系的布尔函数表示更加准确、高效。
关键词
符号模型检测，OBDD ，迁移关系，布尔函数，等效输入变量
1. 引言
随着计算机科学技术的迅速发展，关于计算机硬件和软件系统的正确性验证也越来越重要，而关于其功能的验证主要采用模拟法和形式化验证法。相对于模拟法来说，形式化验证法更能保证验证的完备性，所以其在工业上的应用更为广泛。此外，形式化验证法大体上可分为等价性检测、模型检测和定理证明三类。
模型检测[1] [2]是一种自动的、基于模型的形式化验证技术，它通过遍历状态空间来对系统某方面的性质作出验证。然而，随着系统规模的不断扩大，状态空间的大小呈指数级增长，于是就引起了状态空间爆炸问题。为了克服显式模型检测在解决此问题上的局限性，符号模型检测应运而生。
符号模型检测是由J. R. Burch，E. M. Clarke和K. L. McMillan等人于20世纪90年代初提出的[3] [4] [5]，它通过布尔函数来表示状态集、迁移关系，而布尔函数则以有序二叉判定图(Ordered Binary Decision Di-agrams ，简称OBDD) [6] [7] [8]来呈现。符号模型检测的提出使得状态数超过1020的实际系统得到了验证，在很大程度上缓解了状态空间爆炸问题，进而促进了验证技术的重大突破。而近几年关于OBDD 变量序的研究[9] [10]及符号模型检测在应用中的研究[11] [12] [13] [14]使得形式化验证技术得到了重大发展。
符号模型检测中，在将迁移关系表示为数据结构OBDD 时常会遇到两个问题：第一，状态变量在下一状态的取值不确定；第二，具有一定变化规律的非输入变量较多时，它们之间关系的处理。对于这两个问题，文献[15]中给出了一些相应的的解决办法，但其较为抽象，而且形式化过程、结果都存在有一些赘余表示。
本文通过提出等效输入变量的概念，给出了借助SMV (Symbolic Model Verifier)语言描述迁移系统并由此得出迁移关系的布尔函数时，对于这两个问题具体明确的解决办法，此外对文献[15]中所提关于f →的公式进行了改进，使得形式化过程更加高效，形式化结果更加简洁，进而直接或者间接地提高了符号模型检测中某些具体问题的验证效率。
2. 基本概念
模型检测中，对系统某方面的性质作出验证时，首先要对实际系统建模得出一个迁移系统。 定义1：迁移系统TS 是一个多元组(S , I , →, P , L )，其中S 表示系统的状态集合，I 表示系统的初始它是状态集S 上的二元关系：对于∀s ∈S ，都∃s ′∈S 满足s →s ′，状态集合且满足I ⊆S ，→表示迁移关系，
P 是用于描述状态的原子命题集，L 是从状态集S 到原子命题集P 的幂集上的函数，称为标记函数。
=TS 一个迁移系统
(S , I , →, P , L )可以通过一个有向图来表示，如图1所示。
张小珍，江建国
对于图1所示迁移系统TS 有：
S ={s 0, s 1, s 2} I ={s 0}
→={(s 0, s 1), (s 0, s 2), (s 1, s 2), (s 2, s 1)}
P ={x , y , z }
=L (s 0)
y }, L (s 1){=y }, L (s 2){z } {x , =
符号模型检测中，需首先将迁移系统中的状态集和迁移关系表示为布尔函数的形式，而且在此表示过程中会涉及到一些变量。
定义2：若一个变量x 的定义域是{0,1}，则称此变量x 为布尔变量。令x , y 为布尔变量，若集合{0,1}
n
n
n
n
n
上的函数f :{0,1}→{0,1}满足布尔运算、 、+、⊕，则称此函数f 为从{0,1}到{0,1}上的n 元布尔函数。
用来描述系统各状态的自变量，称为状态变量。系统模型的任意一个状态可以认为是对状态变量集中各元素的一个赋值。状态变量的取值可能会随着状态的迁移而变化。而由外界环境所决定的变量，称为输入变量。在有限状态的迁移系统中，不可以指定输入变量的初值，而且它的取值变化完全取决于模拟环境，而与状态迁移毫无关系。
布尔函数的表示方法有很多种，在诸多表示中，OBDD 是布尔函数较为紧凑且较为规范的表示形式。 定义3：二叉判定图(Binary Decision Diagrams，简称BDD) 是一个有限有向无环图，满足条件： 1) 具有唯一初始结点；
2) 所有非终止结点用布尔变量标记，且都恰好有两条边指向其它结点：一个用虚线表示，一个用实线表示，其中虚线表示布尔变量取值为0，实线表示取值为1；
3) 所有终止结点标记为0或1。
有序二叉判定图(Ordered Binary Decision Diagrams，简称OBDD) 是带有某些有序变量表的BDD 。 如图2是无变量序的BDD ，而图3是带有序[x , y ]的OBDD 。
3. 迁移关系的布尔函数表示
符号模型检测中，需要将迁移系统中的迁移关系表示为OBDD ，而当系统较大较为复杂时，则需借助SMV 语言描述迁移系统，并依据此得出表示迁移关系的布尔函数f →，进而通过相关算法综合求得其OBDD 。而用SMV 语言描述迁移系统以及由此得出迁移关系的布尔函数时，通常会遇到两个问题的处理：第一个问题是，状态变量在下一状态的取值不确定；第二个问题是：具有一定变化规律的非输入变量较多时，它们之间关系的处理。
为有效解决这两个问题，我们引入了一种叫做等效输入变量的状态变量：在任意下一状态取值都不确定的状态变量，称为等效输入变量。很明显，等效输入变量不是输入变量，但其取值不会随着状态的迁移呈现一定的变化规律。
本节工作前提是状态集已被表示为布尔值和布尔函数。符号说明：x i 表示状态变量，f i 表示状态变量x i 在下一状态的取值所满足的关系表达式，而x i ′则表示状态变量x i 在下一状态的取值。
3.1. 非确定的下一状态
迁移关系表示为布尔函数过程中，为解决下一状态为非确定赋值的问题，我们对所研究的状态变量
张小珍，江建国
Figure 1. The directed graph of the transition system =TS (S , I , →, P , L ) 图1. 迁移系统=TS
(S , I , →, P , L )的有向图
Figure 2. A BDD without an ordering of variables 图2. 无变量序的BDD
进行考究，看状态变量是否为等效输入变量，进而给出不同的解决办法，使得形式化结果更加简明。
若状态变量x k 为非等效输入变量，即只在某些条件下，其下一状态取值不确定：
1) 用SMV 语言描述迁移关系时，需将该条件下的next (x k )赋值为所有可能的取值组成的集合； 2) 由SMV 语言求得迁移关系的布尔函数时，只需将该条件的f i 取值为x i ′来表示，而无需再引入其它输入变量，因为输入变量的引入表示系统状态的增多。
若状态变量x k 为等效输入变量，即其在任意下一状态的赋值都不确定：
1) 用SMV 语言进行描述时，不需要对其下一状态取值进行描述； 2) 由SMV 语言求得迁移关系的布尔函数时，即依据f =∏x ′f 求取f →时，我们对x i 的条件进
→
i
i
1≤i ≤n
行修改，要求其不仅不可以是输入变量，而且不可以是等效输入变量。假设x j 是等效输入变量，则无论
→
任何时候都满足f j =x ′j ，而x ′j f j =x ′j x ′j =1，于是f =
∏x
1≤i ≤n
i
f =i
∏
1≤i ≤n , i ≠j
x i f i , 通过这样的限制，可
张小珍，江建国
以避免形式化过程中的冗余表示。
例1：已知迁移系统TS 1的有向图如图4所示，试用SMV 语言对该系统进行描述，并由此给出其迁移关系的布尔函数f →。
首先，分析非输入变量x 1, x 2的变化规律可知：变量x 1在任意一个下一状态的取值是不确定的，既有TRUE ，也有FALSE ，因此为等效输入变量，所以在SMV 语言描绘中不对next (x )进行说明。而变量x 2则
1
遵循一定的变化规率：当x 1为TRUE 时，x 2在下一状态的取值为FALSE ；而x 1为FALSE 时，x 2在下一状态的取值是不确定的，既有TRUE 也有FALSE 。
由此得出该迁移系统的SMV 语言描绘如下所示：
Figure 3. A OBDD with variable ordering [x , y ] 图3. 带有序[x , y ]的OBDD
Figure 4. The directed graph of transition system TS 1 图4. 迁移系统TS 1的有向图
张小珍，江建国
其次，由SMV 语言描绘求得迁移关系的布尔函数f →时，关于下一状态是不确定值的处理：首先分
析x 1是等效输入变量，所以不需要求f 1。而x 2是非等效输入变量的状态变量，当x 1=0时，f 2的取值是′即可；而且写f 2表达式时，没有必要列真值表，只需将f 2=1时的各种不确定的，此时需使f 2取值为x 2
情况用布尔表达式表示然后再相加即可。
′=1，故f 2′。 由SMV 语言中的next 表达式分析：f 2=1时的条件是x 1=0且x 2=1⋅x 2
最后，得出图4所示系统TS 1的迁移关系的布尔函数是：
f
→
′f 2=2⊕=x 2(1⋅x 2′)
3.2. 多个非等效输入
当迁移系统中有具有一定变化规律的非输入变量较多，即有多个非等效输入变量的状态变量x i 时，处理好各next (x i )之间的关系，方可得到原迁移系统的正确描述。因为用SMV 语言描述迁移系统时，需分析各x i 的变化规律，而当非等效输入变量的状态变量较多时，分析某个变量的变化规律可能会引入一些原迁移系统中不存在的迁移，此时在分析其他变量的变化规律时需避免这些赘余迁移，也就是说，依据每个next (x i )都会得到一个迁移图，而它们的公共部分才为已知迁移系统的有向图。
例2：已知迁移系统TS 2的有向图如图5所示，试用SMV 语言对该系统进行描述，并由此给出其迁移关系的布尔函数f →。
Figure 5. The directed graph of transition system TS 2 图5. 迁移系统TS 2的有向图
张小珍，江建国
首先，分析可知，状态变量x 1和x 2都不是等效输入变量，而变量x 1的变化规律是：只有当x 1和x 2均为FALSE 时，下一状态x 1的真值不确定，既有TRUE ，也有FALSE ；而其它情况下，下一状态x 1的取值一定为FALSE ；但殊不知，这个变化规律增加了迁移s 0→s 2, s 3→s 1, s 1→s 1, s 2→s 1, s 2→s 3，如图6中的左图虚线箭头所示，因此在分析x 2的变化规律时，必须避免这些迁移的出现。对于x 2，要求当x 1=1且x 2=0时，x 2在下一状态的取值为TRUE ，这样避免了迁移s 0→s 2；而其他情况下，x 2在下一状态的取值一定为FALSE ，这样的赋值避免了其他的赘余迁移。虽然又引入了额外的迁移，但也不影响最后结果，如图6中的右图说明了变量x 2的变化规律，其中虚线部分为所引入的无关迁移。图6中左图和右图的公共部分即为图5中的迁移。
该迁移系统的SMV 语言描绘如下所示：
由迁移系统的SMV 语言描述求f →时，利用同例1的方法，只需将各f i =1时的条件转化为对应的布
x 1⋅2，于是可得图5中所示迁移系统TS 2的迁移关尔表达式再相加即可。所以可求得f 1=1⋅2⋅x 1′，f =2
系的布尔函数是：
f →=
′f 2)=(1⊕1⋅2⋅x 1′)⋅(2⊕x 1⋅2) (x 1′f 1)⋅(x 2
4.
结语
本文给出了符号模型检测中将迁移关系表示为布尔函数时，关于下一状态取值不确定以及非等效输
Figure 6. The respectively corresponding transition graph of the varying rules of x 1 and x 2 图6. x 1和x 2的变化规律各自所对应的迁移图
张小珍，江建国
入变量较多时的处理方法，从而使得迁移关系的布尔函数表示更加高效、准确。但对于该表示过程中所遇到的其它问题，比如用当前值无法表示下一状态取值而需要引入其它输入变量等问题的处理，还有待于进一步研究。
参考文献 (References)
[1] Clarke, E.M. and Emerson, E.A. (1981) Design and Synthesis of Synchronization Skeletons Using Branching-time
Temporal Logic. Logic of Programs, Lecture Notes in Computer Science, 133, 52-71. [2] Queille J.P. and Sifakis. J. (1981) Specification and Verification of Concurrent Systems in CESAR. 5th International
Symposium on Programming, 137, 337-351. [3] Burch J.R., Clarke J.M., McMillan K.L., Dill D.L. and Hwang, J. (1992) System Model Checking: 1020 States and
Beyond. Information and Computation, 98, 142-170. [4] Clarke E., Grumberg O. and Long, D. (1993) Verification Tools for Finite-State Concurrent Systems. In: de Bakker,
J.W., de Roever, W.P. and Rozenberg, G. Eds., A Decade of Concurrency, Lecture Notes in Computer Science, Sprin-ger, Verlag, 124-175. [5] McMillan, K.L. (1993) Symbol Model Checking. Kluwer Academic Publishers, Norwell.
[6] Bryant, R.E. (1986) Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Compilers,
35, 677-691. [7] Bryant, R.E. (1991) On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions
with Application to Integer Multiplication. IEEE Transactions on Computers, 40, 205-213. [8] Bryant, R.E. (1992) Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Sur-veys , 24, 293-318. [9] Lai Y., Liu D.Y. and Wang, S.S. (2013) Reduced Ordered Binary Decision Diagram with Implied Literals: A New
Knowledge Compilation Approach. Knowledge and Information Systems, 35, 665-712. [10] Bollig, B. (2016) On the Minimization of (Complete) Ordered Binary Decision Diagrams. Theory of Computing Sys-tems , 59, 532-559. [11] Beyer, D. and Stahlbauer, A. (2013) BDD-Based Software Model Checking with CPACHECKER . Doctoral Workshop on
Mathematical & Engineering Methods in Computer Science, 7721, 1-11. [12] Beyer, D. and Stahlbauer, A. (2014) BDD-based Software Verification Applications to Event-Condition-Action Sys-tems. International Journal on Software Tools for Technology Transfer, 16, 507-518. [13] 孔庆爱. 基于符号模型检测若干问题的研究及应用[D]: [硕士学位论文]. 长春: 吉林大学, 2008: 1-70.
[14] 逄涛. 命题投影时序逻辑符号模型检测及其应用研究[D]: [博士学位论文]. 西安: 西安电子科技大学, 2014: 1-
89. [15] Huth, M. and Ryan, M. (2004) Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge Uni-versity, Cambridge, 382-390.
期刊投稿者将享受如下服务：
1. 投稿前咨询服务 (QQ、微信、邮箱皆可) 2. 为您匹配最合适的期刊
3. 24小时以内解答您的所有疑问 4. 友好的在线投稿界面 5. 专业的同行评审 6. 知网检索
7. 全网络覆盖式推广您的研究
投稿请点击：http://www.hanspub.org/Submission.aspx 期刊邮箱：[email protected]
Software Engineering and Applications 软件工程与应用, 2016, 5(6), 319-326 Published Online December 2016 in Hans.
Optimization of the Boolean Function Representing Transition Relation
Xiaozhen Zhang, Jianguo Jiang
School of Mathematics, Liaoning Normal University, Dalian Liaoning
Received: Dec. 1st , 2016; accepted: Dec. 18th , 2016; published: Dec. 21st , 2016
Copyright 2016 by authors and Hans Publishers Inc.
This work is licensed under the Creative Commons Attribution International License (CC BY).
Open Access
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 va-riables, 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 boo-lean function representation of transition relation is further accurate and efficient.
Keywords
Symbolic Model Checking, OBDD, Transition Relation, Boolean Function, Equivalent-Input Variables
迁移关系的布尔函数表示的优化
张小珍，江建国
辽宁师范大学数学学院，辽宁 大连
收稿日期：2016年12月1日；录用日期：2016年12月18日；发布日期：2016年12月21日
文章引用: 张小珍, 江建国. 迁移关系的布尔函数表示的优化[J]. 软件工程与应用, 2016, 5(6): 319-326.
张小珍，江建国
摘 要
符号模型检测中，将迁移关系表示为OBDD 的一种较为高效的方法是先借助SMV 语言将迁移关系表示为布尔函数，再利用相关算法综合得其OBDD 。但在将迁移关系表示为布尔函数时常会遇到两个问题：第一，下一状态取值不确定；第二，具有一定变化规律的非输入变量较多。本文提出等效输入变量的概念，对迁移关系的布尔函数公式的取值条件加以限制，给出了这两个问题的具体解决办法，进而使得迁移关系的布尔函数表示更加准确、高效。
关键词
符号模型检测，OBDD ，迁移关系，布尔函数，等效输入变量
1. 引言
随着计算机科学技术的迅速发展，关于计算机硬件和软件系统的正确性验证也越来越重要，而关于其功能的验证主要采用模拟法和形式化验证法。相对于模拟法来说，形式化验证法更能保证验证的完备性，所以其在工业上的应用更为广泛。此外，形式化验证法大体上可分为等价性检测、模型检测和定理证明三类。
模型检测[1] [2]是一种自动的、基于模型的形式化验证技术，它通过遍历状态空间来对系统某方面的性质作出验证。然而，随着系统规模的不断扩大，状态空间的大小呈指数级增长，于是就引起了状态空间爆炸问题。为了克服显式模型检测在解决此问题上的局限性，符号模型检测应运而生。
符号模型检测是由J. R. Burch，E. M. Clarke和K. L. McMillan等人于20世纪90年代初提出的[3] [4] [5]，它通过布尔函数来表示状态集、迁移关系，而布尔函数则以有序二叉判定图(Ordered Binary Decision Di-agrams ，简称OBDD) [6] [7] [8]来呈现。符号模型检测的提出使得状态数超过1020的实际系统得到了验证，在很大程度上缓解了状态空间爆炸问题，进而促进了验证技术的重大突破。而近几年关于OBDD 变量序的研究[9] [10]及符号模型检测在应用中的研究[11] [12] [13] [14]使得形式化验证技术得到了重大发展。
符号模型检测中，在将迁移关系表示为数据结构OBDD 时常会遇到两个问题：第一，状态变量在下一状态的取值不确定；第二，具有一定变化规律的非输入变量较多时，它们之间关系的处理。对于这两个问题，文献[15]中给出了一些相应的的解决办法，但其较为抽象，而且形式化过程、结果都存在有一些赘余表示。
本文通过提出等效输入变量的概念，给出了借助SMV (Symbolic Model Verifier)语言描述迁移系统并由此得出迁移关系的布尔函数时，对于这两个问题具体明确的解决办法，此外对文献[15]中所提关于f →的公式进行了改进，使得形式化过程更加高效，形式化结果更加简洁，进而直接或者间接地提高了符号模型检测中某些具体问题的验证效率。
2. 基本概念
模型检测中，对系统某方面的性质作出验证时，首先要对实际系统建模得出一个迁移系统。 定义1：迁移系统TS 是一个多元组(S , I , →, P , L )，其中S 表示系统的状态集合，I 表示系统的初始它是状态集S 上的二元关系：对于∀s ∈S ，都∃s ′∈S 满足s →s ′，状态集合且满足I ⊆S ，→表示迁移关系，
P 是用于描述状态的原子命题集，L 是从状态集S 到原子命题集P 的幂集上的函数，称为标记函数。
=TS 一个迁移系统
(S , I , →, P , L )可以通过一个有向图来表示，如图1所示。
张小珍，江建国
对于图1所示迁移系统TS 有：
S ={s 0, s 1, s 2} I ={s 0}
→={(s 0, s 1), (s 0, s 2), (s 1, s 2), (s 2, s 1)}
P ={x , y , z }
=L (s 0)
y }, L (s 1){=y }, L (s 2){z } {x , =
符号模型检测中，需首先将迁移系统中的状态集和迁移关系表示为布尔函数的形式，而且在此表示过程中会涉及到一些变量。
定义2：若一个变量x 的定义域是{0,1}，则称此变量x 为布尔变量。令x , y 为布尔变量，若集合{0,1}
n
n
n
n
n
上的函数f :{0,1}→{0,1}满足布尔运算、 、+、⊕，则称此函数f 为从{0,1}到{0,1}上的n 元布尔函数。
用来描述系统各状态的自变量，称为状态变量。系统模型的任意一个状态可以认为是对状态变量集中各元素的一个赋值。状态变量的取值可能会随着状态的迁移而变化。而由外界环境所决定的变量，称为输入变量。在有限状态的迁移系统中，不可以指定输入变量的初值，而且它的取值变化完全取决于模拟环境，而与状态迁移毫无关系。
布尔函数的表示方法有很多种，在诸多表示中，OBDD 是布尔函数较为紧凑且较为规范的表示形式。 定义3：二叉判定图(Binary Decision Diagrams，简称BDD) 是一个有限有向无环图，满足条件： 1) 具有唯一初始结点；
2) 所有非终止结点用布尔变量标记，且都恰好有两条边指向其它结点：一个用虚线表示，一个用实线表示，其中虚线表示布尔变量取值为0，实线表示取值为1；
3) 所有终止结点标记为0或1。
有序二叉判定图(Ordered Binary Decision Diagrams，简称OBDD) 是带有某些有序变量表的BDD 。 如图2是无变量序的BDD ，而图3是带有序[x , y ]的OBDD 。
3. 迁移关系的布尔函数表示
符号模型检测中，需要将迁移系统中的迁移关系表示为OBDD ，而当系统较大较为复杂时，则需借助SMV 语言描述迁移系统，并依据此得出表示迁移关系的布尔函数f →，进而通过相关算法综合求得其OBDD 。而用SMV 语言描述迁移系统以及由此得出迁移关系的布尔函数时，通常会遇到两个问题的处理：第一个问题是，状态变量在下一状态的取值不确定；第二个问题是：具有一定变化规律的非输入变量较多时，它们之间关系的处理。
为有效解决这两个问题，我们引入了一种叫做等效输入变量的状态变量：在任意下一状态取值都不确定的状态变量，称为等效输入变量。很明显，等效输入变量不是输入变量，但其取值不会随着状态的迁移呈现一定的变化规律。
本节工作前提是状态集已被表示为布尔值和布尔函数。符号说明：x i 表示状态变量，f i 表示状态变量x i 在下一状态的取值所满足的关系表达式，而x i ′则表示状态变量x i 在下一状态的取值。
3.1. 非确定的下一状态
迁移关系表示为布尔函数过程中，为解决下一状态为非确定赋值的问题，我们对所研究的状态变量
张小珍，江建国
Figure 1. The directed graph of the transition system =TS (S , I , →, P , L ) 图1. 迁移系统=TS
(S , I , →, P , L )的有向图
Figure 2. A BDD without an ordering of variables 图2. 无变量序的BDD
进行考究，看状态变量是否为等效输入变量，进而给出不同的解决办法，使得形式化结果更加简明。
若状态变量x k 为非等效输入变量，即只在某些条件下，其下一状态取值不确定：
1) 用SMV 语言描述迁移关系时，需将该条件下的next (x k )赋值为所有可能的取值组成的集合； 2) 由SMV 语言求得迁移关系的布尔函数时，只需将该条件的f i 取值为x i ′来表示，而无需再引入其它输入变量，因为输入变量的引入表示系统状态的增多。
若状态变量x k 为等效输入变量，即其在任意下一状态的赋值都不确定：
1) 用SMV 语言进行描述时，不需要对其下一状态取值进行描述； 2) 由SMV 语言求得迁移关系的布尔函数时，即依据f =∏x ′f 求取f →时，我们对x i 的条件进
→
i
i
1≤i ≤n
行修改，要求其不仅不可以是输入变量，而且不可以是等效输入变量。假设x j 是等效输入变量，则无论
→
任何时候都满足f j =x ′j ，而x ′j f j =x ′j x ′j =1，于是f =
∏x
1≤i ≤n
i
f =i
∏
1≤i ≤n , i ≠j
x i f i , 通过这样的限制，可
张小珍，江建国
以避免形式化过程中的冗余表示。
例1：已知迁移系统TS 1的有向图如图4所示，试用SMV 语言对该系统进行描述，并由此给出其迁移关系的布尔函数f →。
首先，分析非输入变量x 1, x 2的变化规律可知：变量x 1在任意一个下一状态的取值是不确定的，既有TRUE ，也有FALSE ，因此为等效输入变量，所以在SMV 语言描绘中不对next (x )进行说明。而变量x 2则
1
遵循一定的变化规率：当x 1为TRUE 时，x 2在下一状态的取值为FALSE ；而x 1为FALSE 时，x 2在下一状态的取值是不确定的，既有TRUE 也有FALSE 。
由此得出该迁移系统的SMV 语言描绘如下所示：
Figure 3. A OBDD with variable ordering [x , y ] 图3. 带有序[x , y ]的OBDD
Figure 4. The directed graph of transition system TS 1 图4. 迁移系统TS 1的有向图
张小珍，江建国
其次，由SMV 语言描绘求得迁移关系的布尔函数f →时，关于下一状态是不确定值的处理：首先分
析x 1是等效输入变量，所以不需要求f 1。而x 2是非等效输入变量的状态变量，当x 1=0时，f 2的取值是′即可；而且写f 2表达式时，没有必要列真值表，只需将f 2=1时的各种不确定的，此时需使f 2取值为x 2
情况用布尔表达式表示然后再相加即可。
′=1，故f 2′。 由SMV 语言中的next 表达式分析：f 2=1时的条件是x 1=0且x 2=1⋅x 2
最后，得出图4所示系统TS 1的迁移关系的布尔函数是：
f
→
′f 2=2⊕=x 2(1⋅x 2′)
3.2. 多个非等效输入
当迁移系统中有具有一定变化规律的非输入变量较多，即有多个非等效输入变量的状态变量x i 时，处理好各next (x i )之间的关系，方可得到原迁移系统的正确描述。因为用SMV 语言描述迁移系统时，需分析各x i 的变化规律，而当非等效输入变量的状态变量较多时，分析某个变量的变化规律可能会引入一些原迁移系统中不存在的迁移，此时在分析其他变量的变化规律时需避免这些赘余迁移，也就是说，依据每个next (x i )都会得到一个迁移图，而它们的公共部分才为已知迁移系统的有向图。
例2：已知迁移系统TS 2的有向图如图5所示，试用SMV 语言对该系统进行描述，并由此给出其迁移关系的布尔函数f →。
Figure 5. The directed graph of transition system TS 2 图5. 迁移系统TS 2的有向图
张小珍，江建国
首先，分析可知，状态变量x 1和x 2都不是等效输入变量，而变量x 1的变化规律是：只有当x 1和x 2均为FALSE 时，下一状态x 1的真值不确定，既有TRUE ，也有FALSE ；而其它情况下，下一状态x 1的取值一定为FALSE ；但殊不知，这个变化规律增加了迁移s 0→s 2, s 3→s 1, s 1→s 1, s 2→s 1, s 2→s 3，如图6中的左图虚线箭头所示，因此在分析x 2的变化规律时，必须避免这些迁移的出现。对于x 2，要求当x 1=1且x 2=0时，x 2在下一状态的取值为TRUE ，这样避免了迁移s 0→s 2；而其他情况下，x 2在下一状态的取值一定为FALSE ，这样的赋值避免了其他的赘余迁移。虽然又引入了额外的迁移，但也不影响最后结果，如图6中的右图说明了变量x 2的变化规律，其中虚线部分为所引入的无关迁移。图6中左图和右图的公共部分即为图5中的迁移。
该迁移系统的SMV 语言描绘如下所示：
由迁移系统的SMV 语言描述求f →时，利用同例1的方法，只需将各f i =1时的条件转化为对应的布
x 1⋅2，于是可得图5中所示迁移系统TS 2的迁移关尔表达式再相加即可。所以可求得f 1=1⋅2⋅x 1′，f =2
系的布尔函数是：
f →=
′f 2)=(1⊕1⋅2⋅x 1′)⋅(2⊕x 1⋅2) (x 1′f 1)⋅(x 2
4.
结语
本文给出了符号模型检测中将迁移关系表示为布尔函数时，关于下一状态取值不确定以及非等效输
Figure 6. The respectively corresponding transition graph of the varying rules of x 1 and x 2 图6. x 1和x 2的变化规律各自所对应的迁移图
张小珍，江建国
入变量较多时的处理方法，从而使得迁移关系的布尔函数表示更加高效、准确。但对于该表示过程中所遇到的其它问题，比如用当前值无法表示下一状态取值而需要引入其它输入变量等问题的处理，还有待于进一步研究。
参考文献 (References)
[1] Clarke, E.M. and Emerson, E.A. (1981) Design and Synthesis of Synchronization Skeletons Using Branching-time
Temporal Logic. Logic of Programs, Lecture Notes in Computer Science, 133, 52-71. [2] Queille J.P. and Sifakis. J. (1981) Specification and Verification of Concurrent Systems in CESAR. 5th International
Symposium on Programming, 137, 337-351. [3] Burch J.R., Clarke J.M., McMillan K.L., Dill D.L. and Hwang, J. (1992) System Model Checking: 1020 States and
Beyond. Information and Computation, 98, 142-170. [4] Clarke E., Grumberg O. and Long, D. (1993) Verification Tools for Finite-State Concurrent Systems. In: de Bakker,
J.W., de Roever, W.P. and Rozenberg, G. Eds., A Decade of Concurrency, Lecture Notes in Computer Science, Sprin-ger, Verlag, 124-175. [5] McMillan, K.L. (1993) Symbol Model Checking. Kluwer Academic Publishers, Norwell.
[6] Bryant, R.E. (1986) Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Compilers,
35, 677-691. [7] Bryant, R.E. (1991) On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions
with Application to Integer Multiplication. IEEE Transactions on Computers, 40, 205-213. [8] Bryant, R.E. (1992) Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Sur-veys , 24, 293-318. [9] Lai Y., Liu D.Y. and Wang, S.S. (2013) Reduced Ordered Binary Decision Diagram with Implied Literals: A New
Knowledge Compilation Approach. Knowledge and Information Systems, 35, 665-712. [10] Bollig, B. (2016) On the Minimization of (Complete) Ordered Binary Decision Diagrams. Theory of Computing Sys-tems , 59, 532-559. [11] Beyer, D. and Stahlbauer, A. (2013) BDD-Based Software Model Checking with CPACHECKER . Doctoral Workshop on
Mathematical & Engineering Methods in Computer Science, 7721, 1-11. [12] Beyer, D. and Stahlbauer, A. (2014) BDD-based Software Verification Applications to Event-Condition-Action Sys-tems. International Journal on Software Tools for Technology Transfer, 16, 507-518. [13] 孔庆爱. 基于符号模型检测若干问题的研究及应用[D]: [硕士学位论文]. 长春: 吉林大学, 2008: 1-70.
[14] 逄涛. 命题投影时序逻辑符号模型检测及其应用研究[D]: [博士学位论文]. 西安: 西安电子科技大学, 2014: 1-
89. [15] Huth, M. and Ryan, M. (2004) Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge Uni-versity, Cambridge, 382-390.
期刊投稿者将享受如下服务：
1. 投稿前咨询服务 (QQ、微信、邮箱皆可) 2. 为您匹配最合适的期刊
3. 24小时以内解答您的所有疑问 4. 友好的在线投稿界面 5. 专业的同行评审 6. 知网检索
7. 全网络覆盖式推广您的研究
投稿请点击：http://www.hanspub.org/Submission.aspx 期刊邮箱：[email protected]