Automated Synthesis of Generalized Invariant Strategies via Counterexample-Guided Strategy Refinement

Automated Synthesis of Generalized Invariant Strategies

Summary

This partial ingest is based on the abstract and preliminaries from the extracted text. The paper formalizes generalized strategy synthesis in the situation calculus and proposes a sound but incomplete counterexample-guided method for synthesizing invariant strategies.

Key Claims

• Generalized strategy synthesis for finite-state turn-based safety games can be represented in the situation calculus.
• Restricting attention to invariant strategies makes verification reducible to first-order theorem proving.
• Counterexamples can be recycled into finite game instances whose model-checked solutions refine the current candidate generalized strategy.
• The implemented system reportedly solves most evaluated domains within reasonable time, though the full experimental breakdown still needs deeper ingest.

Methods / Formalism

• Strategy schema: postdiction strategies are written as $\varphi ?;\pi a.a;\psi ?$.
• Verification idea: if $\varphi$ holds on the controlled player’s turn, some executable action should enforce $\psi$; if $\psi$ holds on the opponent’s turn, every executable opponent action should restore $\varphi$.
• Refinement loop: propose a rough generalized strategy, verify it, extract a counterexample if verification fails, solve the induced finite game with model checking, and use the resulting strategy information to refine the candidate.
• Scope: the method is sound but incomplete and targets finite-state turn-based two-player games with safety objectives; see Invariant Strategy Verification Conditions and Counterexample-Guided Strategy Refinement.

Evidence / Experiments

• The paper reports experiments on combinatorial games, grid games, and a protocol-style leader-election variant.
• The full tables and failure cases still need a deeper ingest, so this note should not yet be treated as a complete experimental summary.

Connections

• Primary source for Invariant Synthesis.
• Likely adjacent to Predicate Abstraction and broader counterexample-guided refinement patterns.
• Invariant Strategy Verification Conditions captures the reusable proof obligations for the invariant-strategy schema.
• Counterexample-Guided Strategy Refinement captures the reusable synthesis loop extracted from this paper.

Open Questions

• What notion of strategy invariance is used?
• Does the method transfer to learning-based or partially observed settings?

Citation

Luo, K., and Liu, Y. (2022). Automated Synthesis of Generalized Invariant Strategies via Counterexample-Guided Strategy Refinement. AAAI-22.