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  
  • 下载量: 225  浏览量: 799  

作者:  

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

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

摘要:

符号模型检测中,将迁移关系表示为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.

文章引用:
张小珍, 江建国. 迁移关系的布尔函数表示的优化[J]. 软件工程与应用, 2016, 5(6): 319-326. http://dx.doi.org/10.12677/SEA.2016.56037

参考文献

[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.
https://doi.org/10.1016/0890-5401(92)90017-A
[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.
https://doi.org/10.1007/978-1-4615-3190-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] 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] 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] 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] 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] 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] 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] 孔庆爱. 基于符号模型检测若干问题的研究及应用[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.
https://doi.org/10.1017/cbo9780511810275