Invariant Synthesis

Definition

Invariant synthesis constructs formulas that are preserved across reachable behaviors and are strong enough to certify a target property. In transition-system terms, an invariant $I$ should satisfy $Init\Rightarrow I$, $I\wedge T\Rightarrow I^{\prime }$, and usually $I\Rightarrow Safe$.

Why It Matters

Invariants compress global safety arguments into reusable logical structure and often make difficult verification problems manageable. In synthesis settings they can also act as strategy summaries, replacing per-instance search with formulas that scale across families of problems.

Formalism / Key Objects

• Inductive invariant condition: propose a formula $I$ such that the initial states imply $I$, every legal transition preserves $I$, and $I$ is strong enough for the goal of interest.
• Strategy schema: in Luo2022 - Automated Synthesis of Generalized Invariant Strategies, a postdiction strategy has the form $\varphi ?;\pi a.a;\psi ?$.
• Verification conditions: when it is the controlled player’s turn and $\varphi$ holds, there must exist an executable action making $\psi$ true; when it is the opponent’s turn and $\psi$ holds, every executable action must re-establish $\varphi$.
• Refinement loop: counterexamples are turned into finite game instances whose winning strategies are then used to refine the candidate generalized strategy; see Invariant Strategy Verification Conditions and Counterexample-Guided Strategy Refinement.

Connections

• Central inside Formal Methods.
• Often benefits from Predicate Abstraction.
• Can clarify the expressive boundary of symbolic action theories such as Situation Calculus.
• Invariant Strategy Verification Conditions captures the first-order obligations for proving a candidate invariant strategy.
• Counterexample-Guided Strategy Refinement records the sound-but-incomplete synthesis loop used to improve candidate strategies.
• Probabilistic Controlled Invariant Sets are an adjacent stochastic/control version: the invariant object is a safe set with a probability threshold and an associated policy or action map.

Common Confusions

• An invariant can be correct but too weak to solve the task you care about.
• Synthesizing invariants is often the hard part, not checking them once proposed.
• Verifying an invariant is not the same as synthesizing one; the former checks candidate formulas, while the latter must discover or refine them.
• A generalized invariant strategy is stronger than a per-instance winning move because it is meant to transfer across a whole class of game instances.

Key Sources

• Luo2022 - Automated Synthesis of Generalized Invariant Strategies
• Hashimoto2026 - Data-Driven Synthesis of Probabilistic Controlled Invariant Sets for Linear MDPs