[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
|