articles/interpolants-vibes

In terms of interpolant as a forward image, it follows from an interpolant that partitions a length N BMC instance into the first timestep with some initial constraint (A) and the rest of the timesteps (B), where it is checked if the property can fail in any of the timesteps of B. I have a diagram for this but utteranc.es doesn't seem to support images :<

If this is UNSAT, an interpolant is an expression over the state variables after one timestep (as these are the ones shared by A and B). The constraints in A specify that these variables can only be SAT in the exact image of the initial condition, and the interpolant is by definition implied by A, so overapproximates the image of the initial constraint under the transition relation. It also by definition implies ¬B, so overapproximates the set of states that don't reach a bad state in the next N-1 steps.

Classic exact image based reachability (normally performed with BDDs, but whatever you use you need an explicit way of calculating/expressing forward images) looks something like follows (assuming you have already checked initial states aren't bad)

reachable_states = initial_states
while true:
    new_states = image_T(reachable_states)
    if new_states intersect bad_states:
        return UNSAFE
    if new_states are subset of reachable_states:
        return SAFE
    reachable_states = reachable_states union new_states

It can also alternatively look like the following, which instead repeatedly calculates the set of states reachable at each timestep, rather than just the total set of reachable states thus far

reachable_states = initial_states
current_states = initial_states
while true:
    new_states = image_T(current_states)
    if new_states intersect bad_states:
        return UNSAFE
    if new_states are subset of reachable_states:
        return SAFE
    reachable_states = reachable_states union new_states
    current_states = new_states

Remembering that the interpolant generated from a BMC instance as above overapproximates the image of the initial conditions, we can implement image_T as this interpolation algorithm, with the initial condition for the BMC instance being the states we want to compute the (overapproximate) image of (current_states).

As this image operator is overapproximate, this algorithm overapproximates the set of reachable states, so can conclude that a bad state is reachable when in reality it isn't. Thus, when this algorithm concludes UNSAFE, the solution must be checked for feasibility (with a standard BMC instance). If the counterexample is spurious, the model can be refined by increasing the length of the BMC instance used for interpolation. This means that the new interpolants imply the property holds for more cycles in a row, and thus more tightly overapproximate ¬B. For finite systems this must eventually converge and be able to prove the system SAFE/UNSAFE.

bollu / bollu.github.io

articles/interpolants-vibes #50

A Universe of Sorts