Symbolic Model Checking in External Memory
Steffan Christ Sølvsten, Jaco van de Pol
我们扩展了外部内存 BDD 包 Adiar,支持单调变量替换。 这样做,它现在支持符号模型检查的核心关系产品操作。 我们还确定了完全合并变量替换和在关系产品存在量化步骤中的联合操作的其他途径。 对于较小的BDD,这些额外的想法改善了Adiar的运行,用于模型检查任务,高达47个未受影响,因为它由存在量化主导。 Adiar的关系产品比传统的深度优先BDD实现慢约一个数量级。 然而,它的I/O效率允许其运行时间几乎独立于内部内存量。 这使得它可以在内部内存少得多的BDD上计算,并可能解决传统实现之外的模型检查任务。 与唯一的其他外部内存 BDD 包 CAL 相比,Adiar 在更大的实例上计算时要快几个数量级。
We extend the external memory BDD package Adiar with support for monotone variable substitution. Doing so, it now supports the relational product operation at the heart of symbolic model checking. We also identify additional avenues for merging variable substitution fully and the conjunction operation partially inside the relational product's existential quantification step. For smaller BDDs, these additional ideas improve the running of Adiar for model checking tasks up to 47 unaffected as it i...