Applying variable minimal unsatisfiability in model checking

被引：1

作者：

Chen, Zhen-Yu ^{[1
]}

Tao, Zhi-Hong ^{[2
]}

Kleine, Büning Hans ^{[3
]}

Wang, Li-Fu ^{[2
]}

机构：

[1] School of Computer Science and Engineering, Southeast University

[2] School of Software and Microelectronics, Peking University

[3] Department of Computer Science, University of Paderborn

来源：

Ruan Jian Xue Bao/Journal of Software | 2008年 / 19卷 / 01期

关键词：

Abstraction refinement; Minimal unsatisfiability; Model checking;

D O I：

10.3724/SP.J.1001.2008.00039

中图分类号：

学科分类号：

摘要：

This paper presents a framework combining variable abstraction with bounded model checking, in order to prove the counterexamples' absence or establish the counterexamples' existence. A mathematical definition of variable minimal unsatisfiability (VMU) is introduced to drive this abstraction refinement process. The set of variables of VMU formula is a minimal one guaranteeing its unsatisfiability. Furthermore, the authors prove that VMU-driven refinement is valid and minimal by mathematical reasoning. Although the determining problem of VMU is as hard as the well-known problem called minimal unsatisfiability (MU), i.e. Dp-complete, the case study has shown that VMU could be more effective than MU in variable abstraction refinement process.

引用

页码：39 / 47

页数：8

共 17 条

[1]

Clarke E.M., Grumberg O., Peled D.A., Model Checking, (1999)

[2]

Lin H.M., Zhang W.H., Model checking: Theories, techniques and applications, Acta Electronica Sinica, 30, 12 A, pp. 1907-1912, (2002)

[3]

Su K.L., Luo X.Y., Lu G.F., Symbolic model checking for CTL*, Chinese Journal of Computers, 28, 11, pp. 1798-1806, (2005)

[4]

Biere A., Cimatti A., Clarke E.M., Strichman O., Zhu Y., Bounded Model Checking. Advances in Computers, (2003)

[5]

Clarke E.M., Grumberg O., Long D.E., Model checking and abstraction, ACM Trans. on Programming Languages and Systems, 16, 5, pp. 1512-1542, (1994)

[6]

Kurshan R.P., Computer-Aided Verification of Coordinating Processes, (1994)

[7]

Chen Z.Y., Ding D.C., Variable minimal unsatisfiability, Proc. of the Theory and Applications of Models of Computation, pp. 262-273, (2006)

[8]

Zhao X.S., Complexity results on minimal unsatisfiable formulas - A survey, Proc. of the 9th Asian Logic Conf. Novosbirsk, pp. 301-319, (2005)

[9]

Papadimitriou C.H., Wolfe D., The complexity of facets resolved, Journal of Computer and System Science, 37, 1, pp. 2-13, (1988)

[10]

Chautian P., Clarke E.M., Kukula J., Sapra S., Veith H., Wang D., Automated abstraction refinement for model checking large state spaces using sat based conflict analysis, Proc. of the Conf. on Formal Methods in Computer Aided Design, pp. 33-51, (2002)

← 1 2 →