Symbolic Model Checking without BDDs
Symbolic Model Checking without BDDs
复制标题
DOI：
10.1007/3-540-49059-0_14
复制
发表时间：
1999-03
期刊：
影响因子：
--
通讯作者：
Armin Biere;A. Cimatti;E. Clarke;Yunshan Zhu
中科院分区：
文献类型：
--
作者：
Armin Biere;A. Cimatti;E. Clarke;Yunshan Zhu
符号模型检查[3]，[14]已被证明是验证反应系统的强大技术。BDD [2]传统上被用作系统的符号表示。在本文中，我们展示了布尔决策过程，如Stålmarck方法[16]或Davis & Putnam过程[7]，可以取代BDD。这种新技术避免了BDD的空间爆炸，生成反例的速度更快，有时还加快了验证速度。此外，它还产生了最小长度的反例。本文介绍了LTL的有界模型检验过程，它将模型检验归结为命题可满足性问题，并证明了有界LTL模型检验可以在不构造tableau的情况下进行。我们已经实现了一个模型检查BMC，有界模型检查的基础上，并提出了初步的结果。
Symbolic Model Checking [3], [14] has proven to be a powerful technique for the verification of reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system. In this paper we show how boolean decision procedures, like Stålmarck’s Method [16] or the Davis & Putnam Procedure [7], can replace BDDs. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. In addition, it produces counterexamples of minimal length. We introduce abounded model checkingprocedure for LTL which reduces model checking to propositional satisfiability.We show that bounded LTL model checking can be done without a tableau construction. We have implemented a model checker BMC, based on bounded model checking, and preliminary results are presented.