﻿ 迁移关系的布尔函数表示的优化 Optimization of the Boolean Function Representing Transition Relation

Software Engineering and Applications
Vol.05 No.06(2016), Article ID:19314,8 pages
10.12677/SEA.2016.56037

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

ABSTRACT

In Symbolic Model checking, as a comparatively efficient method of representing transition relation 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 representation 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.

Keywords:Symbolic Model Checking, OBDD, Transition Relation, Boolean Function, Equivalent-Input Variables

1. 引言

2. 基本概念

1) 具有唯一初始结点；

2) 所有非终止结点用布尔变量标记，且都恰好有两条边指向其它结点：一个用虚线表示，一个用实线表示，其中虚线表示布尔变量取值为0，实线表示取值为1；

3) 所有终止结点标记为0或1。

3. 迁移关系的布尔函数表示

3.1. 非确定的下一状态

Figure 1. The directed graph of the transition system

Figure 2. A BDD without an ordering of variables

1) 用SMV语言描述迁移关系时，需将该条件下的赋值为所有可能的取值组成的集合；

2) 由SMV语言求得迁移关系的布尔函数时，只需将该条件的取值为来表示，而无需再引入其它输入变量，因为输入变量的引入表示系统状态的增多。

1) 用SMV语言进行描述时，不需要对其下一状态取值进行描述；

2) 由SMV语言求得迁移关系的布尔函数时，即依据求取时，我们对的条件进行修改，要求其不仅不可以是输入变量，而且不可以是等效输入变量。假设是等效输入变量，则无论任何时候都满足，而，于是通过这样的限制，可

Figure 3. A OBDD with variable ordering [x,y]

Figure 4. The directed graph of transition system TS1

3.2. 多个非等效输入

Figure 5. The directed graph of transition system TS2

4. 结语

Figure 6. The respectively corresponding transition graph of the varying rules of x1 and x2

Optimization of the Boolean Function Representing Transition Relation[J]. 软件工程与应用, 2016, 05(06): 319-326. http://dx.doi.org/10.12677/SEA.2016.56037

1. 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. 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. 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. https://doi.org/10.1016/0890-5401(92)90017-A

4. 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, Springer, Verlag, 124-175.

5. 5. McMillan, K.L. (1993) Symbol Model Checking. Kluwer Academic Publishers, Norwell. https://doi.org/10.1007/978-1-4615-3190-6

6. 6. Bryant, R.E. (1986) Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Compilers, 35, 677-691. https://doi.org/10.1109/TC.1986.1676819

7. 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. https://doi.org/10.1109/12.73590

8. 8. Bryant, R.E. (1992) Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24, 293-318. https://doi.org/10.1145/136035.136043

9. 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. https://doi.org/10.1007/s10115-012-0525-6

10. 10. Bollig, B. (2016) On the Minimization of (Complete) Ordered Binary Decision Diagrams. Theory of Computing Systems, 59, 532-559. https://doi.org/10.1007/s00224-015-9657-x

11. 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. https://doi.org/10.1007/978-3-642-36046-6_1

12. 12. Beyer, D. and Stahlbauer, A. (2014) BDD-based Software Verification Applications to Event-Condition-Action Systems. International Journal on Software Tools for Technology Transfer, 16, 507-518. https://doi.org/10.1007/s10009-014-0334-1

13. 13. 孔庆爱. 基于符号模型检测若干问题的研究及应用[D]: [硕士学位论文]. 长春: 吉林大学, 2008: 1-70.

14. 14. 逄涛. 命题投影时序逻辑符号模型检测及其应用研究[D]: [博士学位论文]. 西安: 西安电子科技大学, 2014: 1- 89.

15. 15. Huth, M. and Ryan, M. (2004) Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge University, Cambridge, 382-390. https://doi.org/10.1017/cbo9780511810275