wiki

Counterexample-Guided Strategy Refinement

2 min read

Counterexample-Guided Strategy Refinement

Context

Luo2022 - Automated Synthesis of Generalized Invariant Strategies adapts the counterexample-guided synthesis idea to generalized strategy synthesis in finite-state turn-based safety games. The goal is not merely to verify a candidate formula, but to iteratively strengthen it using structured failures.

Formal Statement

The loop is:

  1. Propose a candidate generalized invariant strategy.
  2. Verify the associated first-order obligations in the situation calculus.
  3. If verification fails, extract a counterexample.
  4. Construct a finite game instance induced by that counterexample.
  5. Solve the finite instance with a model checker to obtain winning-strategy information.
  6. Refine the candidate generalized strategy using the solved instance and repeat.

The method is sound but incomplete: successful termination yields a correct invariant strategy for the represented game family, but failure to find one does not prove that none exists.

Derivation / Construction

  • The candidate strategy lives at the symbolic level as formulas over the shared game structure.
  • Verification provides logical counterexamples showing where the strategy fails to preserve the intended invariant relation.
  • A counterexample is turned into a concrete finite game instance with the same structural vocabulary.
  • Existing model-checking machinery is then used to compute a winning strategy on that induced instance.
  • The winning-strategy information tells the synthesizer which regions of the symbolic formula should be included, excluded, or tightened in the next candidate.

In pseudocode:

candidate <- initial rough strategy
while candidate fails verification:
    ce <- extract counterexample
    game <- build finite instance from ce
    witness <- solve game by model checking
    candidate <- refine(candidate, witness, ce)
return candidate

Implications

  • This turns failed proofs into structured supervision for synthesis rather than treating them as dead ends.
  • The approach is practical when symbolic formulas are reusable across many structurally similar instances but exact second-order synthesis is too hard.
  • Incompleteness matters: the loop can stall because the refinement language is too weak, not necessarily because the domain lacks a generalized winning strategy.

Graph View

Backlinks