Improving Convergence Rate Of IC3

TL;DR

This paper introduces IC4, an improved version of IC3, which guarantees convergence within the reachability diameter and enhances the average convergence rate, facilitating property decomposition techniques.

Contribution

The paper presents IC4, an algorithm that guarantees convergence within the reachability diameter and improves convergence rates over IC3, enabling more effective property decomposition.

Findings

IC4 guarantees convergence within the reachability diameter.

IC4 has a better average convergence rate than IC3.

Enabling property decomposition with IC4 improves model checking efficiency.

Abstract

IC3, a well-known model checker, proves a property of a transition system by building a sequence of formulas $F_0,\dots,F_k$. Formula $F_i$, $0 \leq i \leq k$ over-approximates the set of states reachable in at most $i$ transitions. The basic algorithm of IC3 cannot guarantee that the value of $k$ never exceeds the reachability diameter of the system. We describe an algorithm called IC4 that gives such a guarantee. (IC4 stands for 'IC3 + Improved Convergence'). One can argue that the average convergence rate of IC4 is better than for IC3 as well. Improving convergence can facilitate some other variations of the basic algorithm. As an example, we describe a version of IC4 employing property decomposition. The latter means replacing an original (strong) property with a conjunction of weaker properties to prove by IC4. We argue that addressing the convergence problem is important for making the property decomposition approach work.