Abstraction-Refinement Cycling¶

Why It Matters¶

Full detail is often intractable - too much to reason about. Pure abstraction is often useless - too imprecise to conclude anything. The power is in strategic cycling: start simple, add detail only where needed. This prevents both oversimplification and drowning in irrelevant details.

The Key Move¶

Begin with the simplest model that might answer your question. Analyze it. Did it give a definitive answer? Done. Did it give a spurious result (false positive/negative from over-abstraction)? Identify which omitted detail matters and refine the model to include it. Repeat until you get a real answer or determine the question is intractable.

Classic Application¶

Counterexample-guided abstraction refinement (CEGAR) in model checking. Start with an abstract state space. If model checking finds a counterexample (apparent bug), check if it's real or spurious (artifact of abstraction). If spurious, refine the abstraction to eliminate that false alarm. Continue until you find real bugs or verify correctness.

Surprising Application¶

Debugging relationship conflicts. Start abstract: "We disagree about money." Is this the real issue? Often yes - resolved. Sometimes no - it's spurious, really about control or values. Refine: "We disagree about how much autonomy each person has over shared resources." Check this. Real? Resolve. Spurious? Refine further. Don't start at maximum detail.

Failure Modes¶

Premature refinement - adding detail before confirming the abstraction is insufficient. Refining the wrong dimension - adding detail that doesn't address the spuriousness. Infinite refinement - the problem truly requires tracking unbounded detail. Failing to recognize when refinement has reached the limit of tractability.

Go Deeper¶

Clarke et al., "Counterexample-Guided Abstraction Refinement" (2000); Cousot & Cousot, "Abstract Interpretation: A Unified Lattice Model" (1977)