Invariant Strategy Verification Conditions

Context

In Luo2022 - Automated Synthesis of Generalized Invariant Strategies, a generalized strategy is represented symbolically in the situation calculus. The key restriction is to invariant strategies, because they can be checked with first-order reasoning rather than full second-order search.

Formal Statement

A postdiction strategy is written as

$$\varphi ?;\pi a.a;\psi ?,$$

which reads: when $\varphi$ holds, choose an action so that $\psi$ holds afterward.

For this schema to define an invariant strategy for player $p$, the paper’s informal verification pattern is:

• Controlled turn condition: whenever it is $p$‘s turn and $\varphi$ holds, there exists an executable action $a$ such that performing $a$ makes $\psi$ true.
• Opponent turn condition: whenever it is the opponent’s turn and $\psi$ holds, every executable opponent action makes $\varphi$ true again in the successor situation.

This creates an alternation between $\varphi$ and $\psi$ that is preserved across the two-player dynamics.

Derivation / Construction

• Choose formulas $\varphi$ and $\psi$ over the shared state vocabulary of the game family.
• Encode legal moves with the action-theory executability machinery.
• Prove existence of a suitable controlled action from $\varphi$ to $\psi$.
• Prove universal restoration from $\psi$ back to $\varphi$ over opponent moves.
• Use these obligations as first-order proof goals; if they fail, hand the failure to Counterexample-Guided Strategy Refinement.

The pattern mirrors ordinary inductive invariants:

• entry into the invariant region
• preservation across transitions
• enough strength to imply the desired safety objective

Implications

• The restriction to invariant strategies is what makes the synthesis problem computationally tractable enough for theorem proving plus refinement.
• The formulas $\varphi$ and $\psi$ act as a compact symbolic policy summary that can transfer across many structurally similar game instances.
• A candidate may satisfy the preservation obligations and still be useless if it is too weak to imply the intended winning or safety condition.

Links

• Parent concept: Invariant Synthesis
• Companion annex: Counterexample-Guided Strategy Refinement
• Source anchor: Luo2022 - Automated Synthesis of Generalized Invariant Strategies