k步相对归纳泛化

我们引入了一种基于SAT的符号模型检验新形式。基于SAT的符号模型检验中的一个常见思想是从可能导致性质违反的状态生成新子句。我们先前的工作建议应用归纳法从这类状态进行泛化。尽管在某些基准测试上有效，但归纳泛化的主要问题在于，在分析过程中的给定时刻，并非所有此类状态都能被归纳泛化，这导致在某些基准测试上对可泛化状态的搜索时间过长。本文引入了相对于$k$步过近似对状态进行归纳泛化的思想：给定状态相对于最新的$k$步过近似进行归纳泛化，而该状态的非相对于该过近似本身是归纳的。这一思想催生了一种算法，该算法在迄今为止检查的最高层级$k$上对给定状态进行归纳泛化，可能通过生成多个互为$k$步相对归纳子句来实现。我们给出了实验证据，证明该算法在实践中是有效的。