Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling
Advanced Unbounded Model Checking Based on AIGs, BDD Sweeping, And Quantifier Scheduling
复制标题
基于 AIG、BDD 扫描和量词调度的高级无界模型检查
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Stefan Disch
中科院分区：
文献类型：
--
作者：
Florian Pigorsch;Christoph Scholl;Stefan Disch
在本文中，我们提出了一个完整的方法来验证在时间逻辑CTL中表达的属性。与前几年提出的大多数验证方法相比，我们支持基于特征函数的符号表示的无界模型检查。其中，我们的方法是基于先进的和逆变器图（AIG）实现、量词调度和BDD扫描。对于几个例子，我们的方法在数量级上优于基于BDD的符号模型检查。然而，我们的方法也能够在已知BDD表现良好的情况下产生有竞争力的结果
In this paper we present a complete method for verifying properties expressed in the temporal logic CTL. In contrast to the majority of verification methods presented in previous years, we support unbounded model checking based on symbolic representations of characteristic functions. Among others, our method is based on an advanced and-inverter graph (AIG) implementation, quantifier scheduling, and BDD sweeping. For several examples, our method outperforms BDD based symbolic model checking by orders of magnitude. However, our approach is also able to produce competitive results for cases where BDD are known to perform well