改进 IC3 的收敛速度
计算机科学中的逻辑
2018-10-19 v3
摘要
IC3 是一种著名的模型检测器，它通过构建公式序列 来证明迁移系统的一个性质。公式 （）过度逼近了最多经 次迁移可达的状态集合。IC3 的基本算法不能保证 的值不超过系统的可达直径。我们描述了一种称为 IC4 的算法，它给出了这样的保证。（IC4 代表“IC3 + 改进收敛”）。也可以认为 IC4 的平均收敛速度优于 IC3。改进收敛有助于基本算法的其他一些变体。作为一个例子，我们描述了一种采用性质分解的 IC4 版本。后者是指将原始的（强）性质替换为若干较弱性质的合取，以供 IC4 证明。我们认为，解决收敛问题对于使性质分解方法奏效十分重要。
引用
@article{arxiv.1809.00503,
title = {Improving Convergence Rate Of IC3},
author = {Eugene Goldberg},
journal= {arXiv preprint arXiv:1809.00503},
year = {2018}
}