SEA  >> Vol. 5 No. 6 (December 2016)

    Optimization of the Boolean Function Representing Transition Relation

  • 全文下载: PDF(642KB) HTML   XML   PP.319-326   DOI: 10.12677/SEA.2016.56037  
  • 下载量: 72  浏览量: 106  


张小珍,江建国:辽宁师范大学数学学院,辽宁 大连

符号模型检测OBDD迁移关系布尔函数等效输入变量Symbolic Model Checking OBDD Transition Relation Boolean Function Equivalent-Input Variables



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.

张小珍, 江建国. 迁移关系的布尔函数表示的优化[J]. 软件工程与应用, 2016, 5(6): 319-326.


[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, Springer, 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 Surveys, 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 Systems, 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 Systems. 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 University, Cambridge, 382-390.